lightweight checked exceptions with freer

checked.hs

{-# LANGUAGE CPP                       #-}
{-# LANGUAGE DataKinds                 #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE FlexibleContexts          #-}
{-# LANGUAGE GADTs                     #-}
{-# LANGUAGE IncoherentInstances       #-}
{-# LANGUAGE RankNTypes                #-}
{-# LANGUAGE RoleAnnotations           #-}
{-# LANGUAGE ScopedTypeVariables       #-}
{-# LANGUAGE TypeOperators             #-}

module Checked where

import           Control.Exception            hiding (throw)
import           Control.Monad.Freer
import           Control.Monad.Freer.Internal
import           Control.Monad.Freer.State
import           Data.Proxy

data Throws e a where
  Throw :: Exception e => e -> Throws e a

throw :: (Member (Throws e) r, Exception e) => e -> Eff r a
throw = send . Throw

handleException :: (e -> a) -> Eff (Throws e ': r) a -> Eff r a
handleException _ (Val a) = return a
handleException h (E u q) =
    case decomp u of
      Right (Throw e) -> return (h e)
      Left  u1        -> E u1 (tsingleton (handleException h . qApp q))

f :: (Member (Throws IOException) r, Member (Throws AssertionFailed) r) => Int -> Eff r Int
f _ = do
    throw (AssertionFailed "asfd")
    throw (userError "foo")

throwIO' :: Member IO r => Proxy e -> Eff (Throws e ': r) a -> Eff r a
-- throwIO' :: Proxy e -> Eff (Throws e ': IO ': r) a -> Eff (IO ': r) a
throwIO' _ (Val a) = return a
throwIO' p (E u q) =
    case decomp u of
      Right (Throw e) -> send (throwIO e)
      Left  u1        -> E u1 (tsingleton (throwIO' p . qApp q))

run_f :: Int -> Either IOException (Either AssertionFailed Int)
run_f i = run $ handleException Left $ handleException (Right . Left) $ fmap (Right . Right) (f i)

return_f :: (Member (State Int) r, Member (Throws IOException) r1, Member (Throws AssertionFailed) r1) => Eff r (Eff r1 Int)
return_f = do
    i <- get
    return (f i)

get_f :: (Member (Throws IOException) r1, Member (Throws AssertionFailed) r1) => Eff r1 Int
get_f =
    let
      f' :: (Member (Throws IOException) r1, Member (Throws AssertionFailed) r1) => Eff '[State Int] (Eff r1 Int)
      f' = return_f

      f'' :: (Member (Throws IOException) r1, Member (Throws AssertionFailed) r1) => Eff r1 Int
      f'' = fst (run (runState f' 123))
    in
      f''

f1 :: (Member (Throws IOException) r, Member (Throws AssertionFailed) r) => Eff r Int
f1 = f 10

-- f1_ :: Eff '[Throws IOException, IO] Int
f1_ :: (Member (Throws IOException) r, Member IO r) => Eff r Int
-- f1_ :: Eff (Throws IOException ': IO ': r) Int
-- f1_ :: Eff (IO ': Throws IOException ': r) Int
-- f1_ :: (Member (Throws IOException) (r ': rs), Member IO (r ': rs)) => Eff (r ': rs) Int
f1_ = throwIO' (Proxy :: Proxy AssertionFailed) f1

f1__ :: Member IO r => Eff r Int
f1__ = throwIO' (Proxy :: Proxy IOException) f1_