{-# LANGUAGE DataKinds            #-}
{-# LANGUAGE TypeFamilies         #-}
{-# LANGUAGE TypeOperators        #-}
{-# LANGUAGE UndecidableInstances #-}

{- |
Copyright: (c) 2021 Kowainik
SPDX-License-Identifier: MPL-2.0
Maintainer: Kowainik <xrom.xkov@gmail.com>

IO with Exceptions tracked on the type-level
-}

module EIO
    ( -- * Main type
      EIO (..)
    , runEIO
      -- * Basic API
    , throw
    , catch
      -- * QualifieDo interface
    , return
    , (>>=)
    , (>>)
    ) where

import Prelude hiding (return, (>>), (>>=))

import Control.Exception (Exception)
import Data.Coerce (coerce)
import Data.Kind (Type)

import qualified GHC.IO as IO
import qualified Prelude


{- | Main type for 'IO' that tracks exceptions on the
type-level. Simply wraps 'IO' and adds exceptions meta-information.

@since 0.0.0.0
-}
newtype EIO (exceptions :: [Type]) a = EIO
    { forall (exceptions :: [*]) a. EIO exceptions a -> IO a
unEIO :: IO a
    } deriving newtype ((forall a b. (a -> b) -> EIO exceptions a -> EIO exceptions b)
-> (forall a b. a -> EIO exceptions b -> EIO exceptions a)
-> Functor (EIO exceptions)
forall (exceptions :: [*]) a b.
a -> EIO exceptions b -> EIO exceptions a
forall (exceptions :: [*]) a b.
(a -> b) -> EIO exceptions a -> EIO exceptions b
forall a b. a -> EIO exceptions b -> EIO exceptions a
forall a b. (a -> b) -> EIO exceptions a -> EIO exceptions b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: forall a b. a -> EIO exceptions b -> EIO exceptions a
$c<$ :: forall (exceptions :: [*]) a b.
a -> EIO exceptions b -> EIO exceptions a
fmap :: forall a b. (a -> b) -> EIO exceptions a -> EIO exceptions b
$cfmap :: forall (exceptions :: [*]) a b.
(a -> b) -> EIO exceptions a -> EIO exceptions b
Functor)

{- | Run the the 'EIO' main with exception tracking.


Usually used in the @main@ function like so:

@
__import__ EIO (EIO)
__import qualified__ EIO

main :: IO ()
main = EIO.'runEIO' safeMain

safeMain :: EIO '[] ()
safeMain = EIO.do
    ... your code ...
@

@since 0.0.0.0
-}
runEIO :: EIO '[] () -> IO ()
runEIO :: EIO '[] () -> IO ()
runEIO = EIO '[] () -> IO ()
coerce

{- | Wrap a value into 'EIO' without throwing any exceptions.

@since 0.0.0.0
-}
return :: forall a . a -> EIO '[] a
return :: forall a. a -> EIO '[] a
return = forall a b. Coercible a b => a -> b
coerce @(a -> IO a) a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
Prelude.return

{- | Bind the value inside the first action to the second one and
combine thrown exceptions.

@since 0.0.0.0
-}
(>>=) :: forall e1 e2 a b . EIO e1 a -> (a -> EIO e2 b) -> EIO (e1 <> e2) b
>>= :: forall (e1 :: [*]) (e2 :: [*]) a b.
EIO e1 a -> (a -> EIO e2 b) -> EIO (e1 <> e2) b
(>>=) = forall a b. Coercible a b => a -> b
coerce @(IO a -> (a -> IO b) -> IO b) IO a -> (a -> IO b) -> IO b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
(Prelude.>>=)

{- | Run two actions sequentially and combine thrown exceptions.

@since 0.0.0.0
-}
(>>) :: forall e1 e2 a b . EIO e1 a -> EIO e2 b -> EIO (e1 <> e2) b
>> :: forall (e1 :: [*]) (e2 :: [*]) a b.
EIO e1 a -> EIO e2 b -> EIO (e1 <> e2) b
(>>) = forall a b. Coercible a b => a -> b
coerce @(IO a -> IO b -> IO b) IO a -> IO b -> IO b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
(Prelude.>>)

type family (<>) (xs :: [Type]) (ys :: [Type]) :: [Type] where
    '[] <> ys = ys
    xs <> '[] = xs
    (x ': xs) <> ys = x ': (xs <> ys)

{- | Throw exception.

@since 0.0.0.0
-}
throw :: forall e a . Exception e => e -> EIO '[ e ] a
throw :: forall e a. Exception e => e -> EIO '[e] a
throw = forall a b. Coercible a b => a -> b
coerce @(e -> IO a) e -> IO a
forall e a. Exception e => e -> IO a
IO.throwIO

{- | Catch exception and remove it from the list of handled exceptions.

@since 0.0.0.0
-}
catch
    :: forall e a e1 e2
    .  Exception e
    => EIO e1 a
    -> (e -> EIO e2 a)
    -> EIO (Delete e (e1 <> e2)) a
catch :: forall e a (e1 :: [*]) (e2 :: [*]).
Exception e =>
EIO e1 a -> (e -> EIO e2 a) -> EIO (Delete e (e1 <> e2)) a
catch = forall a b. Coercible a b => a -> b
coerce @(IO a -> (e -> IO a) -> IO a) IO a -> (e -> IO a) -> IO a
forall e a. Exception e => IO a -> (e -> IO a) -> IO a
IO.catch

type family Delete (x :: Type) (xs :: [Type]) :: [Type] where
    Delete _ '[] = '[]
    Delete x (x ': xs) = Delete x xs
    Delete x (y ': xs) = y ': Delete x xs