{- Data/Singletons/TH/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.
-}

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

import Control.Monad.Reader
import Control.Monad.Writer
import qualified Data.Foldable as F
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.TH.Options
import Data.Singletons.TH.Syntax

-- environment during promotion
data PrEnv =
  PrEnv { PrEnv -> Options
pr_options     :: Options
        , PrEnv -> OSet LocalVar
pr_scoped_vars :: OSet LocalVar
          -- ^ The set of scoped type variables currently in scope.
          -- See @Note [Scoped type variables]@.
        , PrEnv -> OMap Name LocalVar
pr_lambda_vars :: OMap Name LocalVar
          -- ^ Map from term-level 'Name's of variables bound in lambdas and
          -- function clauses to their type-level counterparts.
          -- See @Note [Tracking local variables]@.
        , PrEnv -> OMap Name DType
pr_local_vars  :: OMap Name DType
          -- ^ Map from term-level 'Name's of local variables to their
          -- type-level counterparts. Note that scoped type variables are stored
          -- separately in 'pr_scoped_tvs'.
          -- See @Note [Tracking local variables]@.
        , PrEnv -> [Dec]
pr_local_decls :: [Dec]
        }

emptyPrEnv :: PrEnv
emptyPrEnv :: PrEnv
emptyPrEnv = PrEnv { pr_options :: Options
pr_options     = Options
defaultOptions
                   , pr_scoped_vars :: OSet LocalVar
pr_scoped_vars = OSet LocalVar
forall a. OSet a
OSet.empty
                   , pr_lambda_vars :: OMap Name LocalVar
pr_lambda_vars = OMap Name LocalVar
forall k v. OMap k v
OMap.empty
                   , pr_local_vars :: OMap Name DType
pr_local_vars  = OMap Name DType
forall k v. OMap k v
OMap.empty
                   , pr_local_decls :: [Dec]
pr_local_decls = [] }

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

instance OptionsMonad PrM where
  getOptions :: PrM Options
getOptions = (PrEnv -> Options) -> PrM Options
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks PrEnv -> Options
pr_options

-- return *type-level* names
allLocals :: MonadReader PrEnv m => m [LocalVar]
allLocals :: forall (m :: * -> *). MonadReader PrEnv m => m [LocalVar]
allLocals = do
  scoped <- (PrEnv -> [LocalVar]) -> m [LocalVar]
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks (OSet LocalVar -> [LocalVar]
forall a. OSet a -> [a]
forall (t :: * -> *) a. Foldable t => t a -> [a]
F.toList (OSet LocalVar -> [LocalVar])
-> (PrEnv -> OSet LocalVar) -> PrEnv -> [LocalVar]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PrEnv -> OSet LocalVar
pr_scoped_vars)
  lambdas <- asks (OMap.assocs . pr_lambda_vars)
  return $ scoped ++ map snd lambdas

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

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

-- ^ Bring a set of type variables into scope for the duration the supplied
-- computation. See @Note [Tracking local variables]@ and
-- @Note [Scoped type variables]@.
scopedBind :: OSet LocalVar -> PrM a -> PrM a
scopedBind :: forall a. OSet LocalVar -> PrM a -> PrM a
scopedBind OSet LocalVar
binds =
  (PrEnv -> PrEnv) -> PrM a -> PrM a
forall a. (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_scoped_vars :: PrEnv -> OSet LocalVar
pr_scoped_vars = OSet LocalVar
scoped }) ->
    PrEnv
env { pr_scoped_vars = binds `OSet.union` scoped })

-- ^ Bring a list of 'VarPromotions' into scope for the duration the supplied
-- computation. See @Note [Tracking local variables]@.
lambdaBind :: VarPromotions -> PrM a -> PrM a
lambdaBind :: forall a. [(Name, LocalVar)] -> PrM a -> PrM a
lambdaBind [(Name, LocalVar)]
binds = (PrEnv -> PrEnv) -> PrM a -> PrM a
forall a. (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_vars :: PrEnv -> OMap Name LocalVar
pr_lambda_vars = OMap Name LocalVar
lambdas
                             , pr_local_vars :: PrEnv -> OMap Name DType
pr_local_vars  = OMap Name DType
locals }) =
          -- Per Note [Tracking local variables], these will be added to both
          -- `pr_lambda_vars` and `pr_local_vars`.
          let new_lambdas :: OMap Name LocalVar
new_lambdas = [(Name, LocalVar)] -> OMap Name LocalVar
forall k v. Ord k => [(k, v)] -> OMap k v
OMap.fromList [(Name, LocalVar)]
binds
              new_locals :: OMap Name DType
new_locals  = (LocalVar -> DType) -> OMap Name LocalVar -> OMap Name DType
forall a b. (a -> b) -> OMap Name a -> OMap Name b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap LocalVar -> DType
localVarToType OMap Name LocalVar
new_lambdas in
          PrEnv
env { pr_lambda_vars = new_lambdas `OMap.union` lambdas
              , pr_local_vars  = new_locals  `OMap.union` locals }

-- ^ A pair consisting of a term-level 'Name' of a variable, bound in a @let@
-- binding or @where@ clause, and its type-level counterpart. The type will
-- always be a defunctionalization symbol so that it can be partially applied if
-- necessary. See @Note [Tracking local variables]@.
type LetBind = (Name, DType)

-- ^ Bring a list of 'LetBind's into scope for the duration the supplied
-- computation. See @Note [Tracking local variables]@.
letBind :: [LetBind] -> PrM a -> PrM a
letBind :: forall a. [LetBind] -> PrM a -> PrM a
letBind [LetBind]
binds = (PrEnv -> PrEnv) -> PrM a -> PrM a
forall a. (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_local_vars :: PrEnv -> OMap Name DType
pr_local_vars = OMap Name DType
locals }) =
          PrEnv
env { pr_local_vars = OMap.fromList binds `OMap.union` locals }

-- | Map a term-level 'Name' to its type-level counterpart. This function is
-- aware of any local variables that are currently in scope.
-- See @Note [Tracking local variables]@.
lookupVarE :: Name -> PrM DType
lookupVarE :: Name -> PrM DType
lookupVarE Name
n = do
  opts <- PrM Options
forall (m :: * -> *). OptionsMonad m => m Options
getOptions
  locals <- asks pr_local_vars
  case OMap.lookup n locals of
    Just DType
ty -> DType -> PrM DType
forall a. a -> PrM a
forall (m :: * -> *) a. Monad m => a -> m a
return DType
ty
    Maybe DType
Nothing -> DType -> PrM DType
forall a. a -> PrM a
forall (m :: * -> *) a. Monad m => a -> m a
return (DType -> PrM DType) -> DType -> PrM DType
forall a b. (a -> b) -> a -> b
$ Name -> DType
DConT (Name -> DType) -> Name -> DType
forall a b. (a -> b) -> a -> b
$ Options -> Name -> Name
defunctionalizedName0 Options
opts Name
n

promoteM :: OptionsMonad q => [Dec] -> PrM a -> q (a, [DDec])
promoteM :: forall (q :: * -> *) a.
OptionsMonad q =>
[Dec] -> PrM a -> q (a, [DDec])
promoteM [Dec]
locals (PrM ReaderT PrEnv (WriterT [DDec] Q) a
rdr) = do
  opts         <- q Options
forall (m :: * -> *). OptionsMonad m => m Options
getOptions
  other_locals <- localDeclarations
  let 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_options     = opts
                                      , pr_local_decls = other_locals ++ locals })
      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
  runQ q

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

-- promoteM specialized to [DDec]
promoteMDecs :: OptionsMonad q => [Dec] -> PrM [DDec] -> q [DDec]
promoteMDecs :: forall (q :: * -> *).
OptionsMonad q =>
[Dec] -> PrM [DDec] -> q [DDec]
promoteMDecs [Dec]
locals PrM [DDec]
thing = do
  (decs1, decs2) <- [Dec] -> PrM [DDec] -> q ([DDec], [DDec])
forall (q :: * -> *) a.
OptionsMonad q =>
[Dec] -> PrM a -> q (a, [DDec])
promoteM [Dec]
locals PrM [DDec]
thing
  return $ decs1 ++ decs2

{-
Note [Tracking local variables]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Handling local variables in singletons-th requires some care. There are three
sorts of local variables that singletons-th tracks:

1. Scoped type variables, e.g.,

     d :: forall a. Maybe a
     d = Nothing :: Maybe a

     e (x :: a) = Nothing :: Maybe a

   In both `d` and `e`, the variable `a` in `:: Maybe a` is scoped.

2. Lambda-bound variables, e.g.,

     f = \x -> x
     g x = x

   In both `f` and `g`, the variable `x` is considered lambda-bound.

3. Let-bound variables, e.g.,

     h =
       let x = 42 in
       x + x

     i = x + x
       where
         x = 42

   In both `h` and `i`, the variable `x` is considered let-bound.

Why does singletons-th need to track local variables? It's because they must
be promoted differently depending on whether they are local or not. Consider:

  j = ... x ...

When promoting the `j` function to a type family `J`, there are four possible
ways of promoting `x`:

* If `x` is a scoped type variable, then `x` must be promoted to the same
  name. This is because promoting a type variable to a kind variable is a
  no-op. For instance, we would promote this:

    j (z :: x) = (z :: x)

  Here, `(%%)`, `x`, and `y` are lambda-bound variables. But we cannot promote
  `j` to this type family:

    type family J arg where
      J (z :: x) = (z :: x)

* If `x` is a lambda-bound variable, then `x` must be promoted to a type
  variable. In general, we cannot promote `x` to the same name. Consider this
  example:

    j (%%) x y = x %% y

  Here, `(%%)`, `x`, and `y` are lambda-bound variables. But we cannot promote
  `j` to this type family:

    type family J (%%) x y where
      J (%%) x y = x %% y

  This is because type variable names cannot be symbolic like `(%%)` is. As a
  result, we create a fresh name `ty` and promote each occurrence of `(%%)` to
  `ty`:

    type family J ty x y where
      J ty x y = x `ty` y

  See `mkTyName` in Data.Singletons.TH.Names. In fact, `mkTyName` will also
  freshen alphanumeric names, so it would be more accurate to say that `j` will
  be promoted to this:

    type family J ty x_123 y_456 where
      J ty x_123 y_456 = x_123 `ty` y_456

  Where `x_123` and `y_456` are fresh names that are distinct from `x` and `y`.
  Freshening alphanumeric names like `x` and `y` is probably not strictly
  necessary, but `mkTyName` does it anyway (1) for consistency with symbolic
  names and (2) to make the type-level names easier to tell apart from the
  original term-level names.

* If `x` is a let-bound variable, then `x` must be promoted to something like
  `LetX`, where `LetX` is the lambda-lifted version of `x`. For instance, we
  would promote this:

    j = x
      where
        x = True

  To this:

    type family J where
      J = LetX
    type family LetX where
      LetX = True

* If `x` is not a local variable at all, then `x` must be promoted to something
  like `X`, which is assumed to be a top-level function. For instance, we would
  promote this:

    x = 42
    j = x

  To this:

    type family X where
      X = 42
    type family J where
      J = X

Being able to distinguish between all these sorts of variables requires
recording whether they are scoped, lambda-bound, or let-bound at their binding
sites during promotion and singling. This is primarily done in two places:

* During promotion, the `pr_local_vars` field of `PrEnv` tracks lambda- and
  let-bound variables.

* During singling, the `sg_local_vars` field of `SgEnv` tracks lambda- and
  let-bound variables.

Each of these fields are Maps from the original, term-level Names to the
promoted or singled versions of the Names. The `lookupVarE` functions (which
can be found in both Data.Singletons.TH.Promote.Monad and
Data.Singletons.TH.Single.Monad) are responsible for determining what a
term-level Name should be mapped to.

In addition to `pr_local_vars` and `sg_local_vars`, which include both lambda-
and let-bound variables, `PrEnv` also includes two additional fields for
tracking other sorts of local variables:

* The `pr_scoped_vars` field tracks which scoped type variables are currently
  in scope. As discussed above, promoting an occurrence of a scoped type
  variable is a no-op, and as such, we never need to use `lookupVarE` to figure
  out what a scoped type variable promotes to. As such, there is no need to put
  the scoped type variables in `pr_local_vars`.

  On the other hand, we /do/ need to track the scoped type variables for
  lambda-lifting purposes (see Note [Scoped type variables]), and this is the
  only reason why we bother maintaining the `pr_scoped_vars` field in the first
  place. See the `scopedBind` function, which is responsible for adding new
  scoped type variables to `pr_scoped_vars`.

* The `pr_lambda_vars` field only tracks lambda-bound variables, unlike
  `pr_local_vars`, which also includes let-bound variables. We must do this
  because lambda-bound variables are treated differently during lambda lifting.
  Lambda-lifted functions must close over any lambda-bound variables in scope,
  but /not/ any let-bound variables in scope, since the latter are
  lambda-lifted separately.

  A consequence of this is that when we lambda-bind a variable during promotion
  (see `lambdaBind`), we add the variable to both `pr_lambda_vars` and
  `pr_local_vars`.  When we let-bind a variable during promotion (see
  `letBind`), we only add the variable to `pr_local_vars`. This means that
  `pr_lambda_vars` will always be a subset of `pr_local_vars`.

Because singling does not do anything akin to lambda lifting, `SgEnv` does not
have anything like `sg_scoped_vars` or `sg_lambda_vars`.

Note [Scoped type variables]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Scoped type variables are a particular form of local variable (see Note
[Tracking local variables]). They are arguably the trickiest form of local
variable to handle, and as noted in the singletons README, there are still some
forms of scoped type variables that singletons-th cannot handle during
promotion.

First, let's discuss how singletons-th promotes scoped type variables in
general:

* When promoting a function with a top-level type signature, we annotate each
  argument on the left-hand sides of type family equations with its kind. This
  is usually redundant, but it can sometimes be useful for bringing type
  variables into scope. For example, this:

    f :: forall a. a -> Maybe a
    f x = (Just x :: Maybe a)

  Will be promoted to something like this:

    type F :: forall a. a -> Maybe a
    type family F x where
      F (x :: a) = (Just x :: Maybe a)

  Note that we gave the `x` on the left-hand side of `F`'s equation an explicit
  `:: a` kind signature to ensure that the `a` on the right-hand side of the
  type family equation is in scope.

  The `promoteClause` function in Data.Singletons.TH.Promote is responsible for
  implementing this.

* Sometimes, there are no arguments available to bring type variables into
  scope. In these situations, we can sometimes use `@` in type family equations
  as an alternative. For example, this:

    g :: forall a. Maybe a
    g = (Nothing :: Maybe a)

  Will be promoted to this:

    type G :: forall a. Maybe a
    type family G where
      G @a = (Nothing :: Maybe a)

  Note the `@a` on `G`'s left-hand side. This relies on `G` having a standalone
  kind signature to work.

  The `promoteLetDecName` function in Data.Singletons.TH.Promote is responsible
  for implementing this.

* When lambda-lifting, singletons-th tracks the current set of scoped type
  variables and includes them as explicit arguments when promoting local
  definitions. For example, this:

    h :: forall a. a -> a
    h x = i
      where
        i = (x :: a)

  Will be promoted to this:

    type H :: forall a. a -> a
    type family H x where
      H @a (x :: a) = LetI a x

    type I a x where
      I a x = (x :: a)

  The `I` type family includes both `a` (a scoped type variable) and `x` (a
  lambda-bound variable) as explicit arguments to ensure that they are in scope
  on the right-hand side, which mentions both of them.

  singletons-th uses the `pr_scoped_vars` field of `PrM` to track scoped type
  variables. Whenever new scoped type variables are bound during promotion, the
  `scopedBind` function is used to add the variables to `pr_scoped_vars`.

These three tricks suffice to handle a substantial number of ways that scoped
type variables can be used. The approach is not perfect, however. Here are two
scenarios where singletons-th fails to promote scoped type variables:

* Funky pattern signatures like this one will not work:

    j :: forall a. a -> a
    j (x :: b) = b

  This is because singletons-th will attempt to promote `j` like so:

    type J :: forall a. a -> a
    type J x where
      J @a ((x :: b) :: a) = b

  But unlike in terms, GHC has no way to know that `a` and `b` are meant to
  refer to the same type variable. In order to make this work, we would need to
  substitute all occurrences of `a` with `b` in the type family equation (or
  vice versa), which seems challenging in the general case.

* Scoped type variables that are only mentioned in the return types of local
  definitions may not always work, such as in this example:

    k x = y
      where
        y :: forall b. Maybe b
        y = Nothing :: Maybe b

  singletons-th would promote `k` and `y` to the following type families:

    type K x where
      K x = LetY x

    type LetY x :: Maybe b where
      LetY x = Nothing :: Maybe b

  Note that because `LetY` closes over the `x` argument, it cannot easily be
  given a standalone kind signature, and this prevents us from writing
  `LetY @b x = ...`. Moreover, `LetY` does not have an argument that we can
  attach an explicit `:: b` signature to. (Attaching it to `x` would be
  incorrect, as that would give `LetY` a less general kind.)

  One possible way forward here would be to give type families the ability to
  write result signatures on their left-hand sides, similar to what GHC
  proposal #228
  (https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0228-function-result-sigs.rst)
  offers:

    type LetY x :: Maybe b where
      LetY x :: Maybe b = Nothing :: Maybe b

Note [Scoped type variables and class methods]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Implementing support for scoped type variables (see Note [Scoped type variables]
as a primer) in the type signatures of class methods is surprisingly tricky.
First, let's consider a small but illustrative example:

  class C a where
    m :: forall b. a -> b -> (a, b)
    m x y = (x, y) :: (a, b)

In the default implementation of `m`, there are /two/ levels of scoped type
variables:

* The `a` type variable from the `class C a` header.
* The `b` type variable from the method signature `forall b. a -> b -> (a, b)`

This means that in order to promote `m` to an associated type family, we need
to ensure that both `a` and `b` are brought into scope. Roughly speaking, we
promote `C` and `m` like so:

  class PC a where
    type M (x :: a) (y :: b) :: (a, b)
    type M x y = MDefault x y

  type MDefault :: forall a b. a -> b -> (a, b)
  type family MDefault x y where
    MDefault @a @b x y = '(x, y) :: (a, b)

The most subtle part is defining MDefault, as we need to give it a standalone
kind signature in order to bind `@a` and `@b` in the definition of `MDefault`.
Note that it's not enough to promote the method signature, as that doesn't
quantify `a`. Instead, we simply collect the free variables of the argument and
result types (`a -> b -> a`) and quantify those, giving us `forall a b. a -> b
-> a`. Note that the exact order of type variables doesn't matter, as the user
doesn't invoke MDefault directly. We mainly use the `forall` to ensure /some/
predictable ordering for the type variables so that we can match the order in
the invisible arguments in the type family equation.

A similar process applies to class instances. For example:

  instance C [a] where
    m :: forall b. [a] -> b -> ([a], b)
    m x y = (reverse x, y) :: ([a], b)

In this example, there are also two levels of scoped type variables: the `a`
from the instance head, and the `b` in the instance signature. We would promote
this instance similarly:

  instance PC [a] where
    type M x y = MImpl x y

  type MImpl :: forall a b. [a] -> b -> ([a], b)
  type family MImpl x y where
    MImpl @a @b x y = '(Reverse x, y) :: ([a], b)

-----
-- Wrinkle: Partial scoping
-----

Although the examples above use two levels of scoped type variables, it is not
necessarily the case that you /have/ to use both levels. Consider, for example:

  instance C (Maybe a) where
    m :: Maybe a -> b -> (Maybe a, b)
    m x y = (fmap (\xx -> (xx :: a)) x, y)

Note that the `a` scopes over the body of `m`'s implementation, but /not/ `b`,
as `m`'s instance signature does not have an outermost `forall`. A more extreme
version of this example is:

  instance C (Maybe a) where
    m x y = (fmap (\xx -> (xx :: a)) x, y)

Here, `m` does not have an instance signature at all, so there is no `b` in
sight.

In both examples, we are presented with a challenge: how do we ensure that `a`
(and only `a`) scopes? Note that singletons-th's approach to promoting class
methods means that we will promote this instance to code that looks like:

  instance PC (Maybe a) where
    type M x y = MImpl x y

  type MImpl :: forall a b. Maybe a -> b -> (Maybe a, b)
  type family MImpl x y where
    ...

We need to give `MImpl` a standalone kind signature we ensure that we can bring
`a` into scope over the right-hand side of `MImpl`'s type family equation. What
does this mean for `b`? One idea is that we could bring `b` into scope over the
right-hand side of the equation as well. This would give rise to this
definition:

  type MImpl :: forall a b. Maybe a -> b -> (Maybe a, b)
  type family MImpl x y where
    M @a @b x y = (Fmap (LambdaSym1 a b x y) x, y)

  data LambdaSym1 a b x y xx
  type instance Apply (LambdaSym1 a b x y) xx = Lambda a b x y xx

  type family Lambda a b x y xx where
    Lambda a b x y xx = xx :: a

Note that Lambda (the lambda-lifted version of the `\xx -> (xx :: a)`
expression) includes both `a` and `b` as local variables. Somewhat
surprisingly, this ends up being a problem when /singling/ the instance. To see
why, consider the singled code for the extreme version of the instance:

  instance SC (Maybe a) where
    sM (sX :: Sing x) (sY :: Sing y) =
      ( sFmap (singFun1 @(LambdaSym1 a b x y)
              (\(sXX :: Sing xx) -> (sXX :: Sing (xx :: a)))
      , sY
      )

GHC will reject this code, as `b` is not in scope in the subexpression
`singFun1 @(LambdaSym1 a b x y)`. And indeed, the original code doesn't bring
`b` into scope, so it makes sense that `b` wouldn't be in scope in the singled
code. We could try to infer an instance signature for `sM` that quantifies `b`
in an outermost `forall`, but doing so is fraught with peril (see #590).

Luckily, there is a relatively simple way to make this work. The reason that
LambdaSym1 includes `b` as an argument is because we typically call
`scopedBind` (see Note [Scoped type variables]) on all of the type variables
bound in the outermost `forall` to bring them into scope in the right-hand
side. For class methods, however, we need not call `scopedBind` on /every/ type
variable in the outermost `forall`. Instead, we can only call `scopedBind` on
the type variables that actually interact with ScopedTypeVariables, and we can
leave all other type variables alone. Concretely, this means that we would
generate the following code for `MImpl`:

  type MImpl :: forall a b. Maybe a -> b -> (Maybe a, b)
  type family MImpl x y where
    M @a @b x y =
      -- NB: Call `scopedBind [a]` here, not `scopedBind [a, b]`
      (Fmap (LambdaSym1 a x y) x, y)

  data LambdaSym1 a x y xx
  type instance Apply (LambdaSym1 a x y) xx = Lambda a x y xx

  type family Lambda a x y xx where
    Lambda a x y xx = xx :: a

Note that we still bind `@b` in an invisible argument, but we no longer pass it
along to LambdaSym1. This means that when we generate `singFun1 @(LambdaSym1 a
x y)` in the singled instance, we no longer reference `b` at all, avoiding the
issue above. (Note that we don't need to bind `@b` in an invisible argument
anymore, but it would require more work to special-case class methods in
`promoteClause` to avoid this, and it doesn't hurt anything to leave `@b` in
place).

The `OSet LocalVar` field of `ClassMethodRHS` dictates which type variables to
bring into scope via `scopedBind`. There are multiple places in the code which
determine which type variables get put into the `OSet`:

* For class declarations, the scoped type variables from the class header
  (e.g., the `a` in `class C a`) are determined in `promoteClassDec`.
* For instance declarations, the scoped type variables from the instance head
  (e.g., the `a` in `instance C (Maybe a)`) are determined in
  `promoteInstanceDec`.
* The scoped type variables from class method signatures and instance signatures
  are determined in `promoteMethod.promote_meth_ty`.

Each of these functions have references to this Note near the particular lines
of relevant code.
-}