{-# 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
    { unEIO :: IO a
    } deriving newtype (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 = coerce

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

@since 0.0.0.0
-}
return :: forall a . a -> EIO '[] a
return = coerce @(a -> IO 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
(>>=) = coerce @(IO a -> (a -> IO b) -> IO 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
(>>) = coerce @(IO a -> IO b -> IO 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 = coerce @(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 = coerce @(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