{- 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 [DecidedStrictness]
Name -> PrM [Role]
Name -> PrM (Maybe Fixity)
Name -> PrM Info
Name -> [Type] -> PrM [Dec]
(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
Extension -> PrM Bool
ForeignSrcLang -> String -> PrM ()
Module -> PrM ModuleInfo
AnnLookup -> PrM [a]
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
-}