e.hs

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}

import Data.Proxy
import Unsafe.Coerce

class KnownBool (b :: Bool) where
  boolVal :: proxy b -> Bool

instance KnownBool True where
  boolVal _ = True
instance KnownBool False where
  boolVal _ = False

data E (r :: [*]) m a = E (m a)

type family MakeEithers es a where
  MakeEithers (e ': es) a = Either e (MakeEithers es a)
  MakeEithers '[] a = a

type family Null xs where
  Null '[] = True
  Null _ = False

runE :: Monad m => E (e ': r) m a -> E r m (Either e a)
runE (E x) = E (Right <$> x)

runAll :: forall r m a. (Monad m, KnownBool (Null r)) => E r m a -> E '[] m (MakeEithers r a)
runAll e | isNull = unsafeCoerce e
         | otherwise = runAll (runE e)
  where isNull = boolVal (Proxy :: Proxy (Null r))

-- Fails due to:
-- chain.hs:35:37: error:
--     • Couldn't match type ‘r’ with ‘e0 : r0’
--       ‘r’ is a rigid type variable bound by
--         the type signature for:
--           runAll :: forall (r :: [*]) (m :: * -> *) a.
--                     (Monad m, KnownBool (Null r)) =>
--                     E r m a -> E '[] m (MakeEithers r a)
--         at chain.hs:33:1-93
--       Expected type: E (e0 : r0) m a
--         Actual type: E r m a
--     • In the first argument of ‘runE’, namely ‘e’
--       In the first argument of ‘runAll’, namely ‘(runE e)’
--       In the expression: runAll (runE e)
--     • Relevant bindings include
--         e :: E r m a (bound at chain.hs:34:8)
--         runAll :: E r m a -> E '[] m (MakeEithers r a)
--           (bound at chain.hs:34:1)
--    |
-- 35 |          | otherwise = runAll (runE e)
--    |

run :: Monad m => E '[] m a -> m a
run (E x) = x

foo :: E '[String, Int] IO ()
foo = E (print "Hello world!")

main = do x <- run $ runAll foo
          return ()