runSeveral with constraint error

runSeveralConstraints.hs

module Polysemy.Several where

import Data.Kind
import Polysemy
import Polysemy.Reader
import Prelude

infixr 5 :::

data HList a where
  HNil :: HList '[]
  (:::) :: a -> HList (b :: [Type]) -> HList (a ': b)

type family TypeMap (f :: a -> b) (xs :: [a]) where
  TypeMap _ '[] = '[]
  TypeMap f (x ': xs) = f x ': TypeMap f xs

type family TypeConcat (a :: [t]) (b :: [t]) where
  TypeConcat '[] b = b
  TypeConcat (a ': as) b = a ': TypeConcat as b

runSeveral ::
  (forall r' k x. k -> Sem (e k ': r') x -> Sem r' x) ->
  HList t ->
  Sem (TypeConcat (TypeMap e t) r) a ->
  Sem r a
runSeveral f (a ::: as) = runSeveral f as . f a
runSeveral _ HNil = id

runReaderWithLog :: (Members '[Embed IO] r) => i -> Sem (Reader i : r) a -> Sem r a
runReaderWithLog i sem = do
  result <- runReader i sem
  embed $ putStrLn "hello"
  return result

runSeveralReaders :: (Members '[Embed IO] r) => Sem (Reader Integer : Reader Integer : r) a -> Sem r a
runSeveralReaders = runSeveral runReaderWithLog (1 ::: 2 ::: HNil)

-- Could not deduce (Member (Embed IO) r')
--     arising from a use of ‘runReaderWithLog’
--   from the context: Members '[Embed IO] r
--     bound by the type signature for:
--                runSeveralReaders :: forall (r :: EffectRow) a.
--                                     Members '[Embed IO] r =>
--                                     Sem (Reader Integer : Reader Integer : r) a -> Sem r a
--     at .../Polysemy/Several.hs:36:1-102
-- • In the first argument of ‘runSeveral’, namely ‘runReaderWithLog’
--   In the expression: runSeveral runReaderWithLog (1 ::: 2 ::: HNil)
--   In an equation for ‘runSeveralReaders’:
--       runSeveralReaders = runSeveral runReaderWithLog (1 ::: 2 ::: HNil) (lsp)