{-# LANGUAGE
    KindSignatures
  , TypeFamilies
  , DataKinds
  , TypeOperators
  , UndecidableInstances
  , GADTs
  , TypeApplications
  , ScopedTypeVariables
  , RankNTypes
  , StandaloneDeriving
  , DefaultSignatures
  , DerivingVia
  , PolyKinds
  , LambdaCase
  , MultiParamTypeClasses
  , AllowAmbiguousTypes
  , ConstraintKinds
#-}
{-# LANGUAGE PatternSynonyms #-}

-- | Basic API of t'CheckedExceptT'
module Control.Monad.CheckedExcept
  ( -- * Types
    CheckedExceptT(..)
  , CheckedExcept
  , OneOf(..)
  , CaseException(..)
  , pattern CaseEnd
  , ShowException(..)
  , ExceptionException(..)
  -- * Typeclass
  , CheckedException(..)
  -- * Utility functions
  , runCheckedExcept
  , throwCheckedException
  , applyAll
  , weakenExceptions
  , weakenOneOf
  , withOneOf
  , withOneOf'
  , caseException
  , (<:)
  , catchSomeException
  -- * Type families / constraints
  , Contains
  , Elem
  , Elem'
  , NonEmpty
  , NotElemTypeError
  , Nub
  , Remove
  , type (++)
  ) where

import Data.Functor ((<&>))
import Control.Exception (Exception(..), SomeException)
import Control.Monad.Except
import Data.Functor.Identity
import Data.Kind
import Data.Type.Bool
import GHC.TypeLits
import Data.Constraint
import Data.Typeable (Typeable, cast, eqT)
import Data.Type.Equality
import Control.Monad.IO.Class (MonadIO)
import Control.Monad.Trans (MonadTrans (..))
import Data.Constraint.Unsafe (unsafeCoerceConstraint)
import Control.Monad.Catch (MonadCatch (..))

-- | Isomorphic to t'ExceptT' over our open-union exceptions type @t'OneOf' es@.
-- Because many effects systems have an t'ExceptT' analogue, this would be pretty simple to port to any effects system.
-- See "Control.Monad.CheckedExcept.QualifiedDo" for example usages.
newtype CheckedExceptT (exceptions :: [Type]) m a
  = CheckedExceptT { forall (exceptions :: [*]) (m :: * -> *) a.
CheckedExceptT exceptions m a -> m (Either (OneOf exceptions) a)
runCheckedExceptT :: m (Either (OneOf exceptions) a) }
  deriving (Applicative (CheckedExceptT exceptions m)
Applicative (CheckedExceptT exceptions m) =>
(forall a b.
 CheckedExceptT exceptions m a
 -> (a -> CheckedExceptT exceptions m b)
 -> CheckedExceptT exceptions m b)
-> (forall a b.
    CheckedExceptT exceptions m a
    -> CheckedExceptT exceptions m b -> CheckedExceptT exceptions m b)
-> (forall a. a -> CheckedExceptT exceptions m a)
-> Monad (CheckedExceptT exceptions m)
forall (exceptions :: [*]) (m :: * -> *).
Monad m =>
Applicative (CheckedExceptT exceptions m)
forall (exceptions :: [*]) (m :: * -> *) a.
Monad m =>
a -> CheckedExceptT exceptions m a
forall (exceptions :: [*]) (m :: * -> *) a b.
Monad m =>
CheckedExceptT exceptions m a
-> CheckedExceptT exceptions m b -> CheckedExceptT exceptions m b
forall (exceptions :: [*]) (m :: * -> *) a b.
Monad m =>
CheckedExceptT exceptions m a
-> (a -> CheckedExceptT exceptions m b)
-> CheckedExceptT exceptions m b
forall a. a -> CheckedExceptT exceptions m a
forall a b.
CheckedExceptT exceptions m a
-> CheckedExceptT exceptions m b -> CheckedExceptT exceptions m b
forall a b.
CheckedExceptT exceptions m a
-> (a -> CheckedExceptT exceptions m b)
-> CheckedExceptT exceptions m b
forall (m :: * -> *).
Applicative m =>
(forall a b. m a -> (a -> m b) -> m b)
-> (forall a b. m a -> m b -> m b)
-> (forall a. a -> m a)
-> Monad m
$c>>= :: forall (exceptions :: [*]) (m :: * -> *) a b.
Monad m =>
CheckedExceptT exceptions m a
-> (a -> CheckedExceptT exceptions m b)
-> CheckedExceptT exceptions m b
>>= :: forall a b.
CheckedExceptT exceptions m a
-> (a -> CheckedExceptT exceptions m b)
-> CheckedExceptT exceptions m b
$c>> :: forall (exceptions :: [*]) (m :: * -> *) a b.
Monad m =>
CheckedExceptT exceptions m a
-> CheckedExceptT exceptions m b -> CheckedExceptT exceptions m b
>> :: forall a b.
CheckedExceptT exceptions m a
-> CheckedExceptT exceptions m b -> CheckedExceptT exceptions m b
$creturn :: forall (exceptions :: [*]) (m :: * -> *) a.
Monad m =>
a -> CheckedExceptT exceptions m a
return :: forall a. a -> CheckedExceptT exceptions m a
Monad, Functor (CheckedExceptT exceptions m)
Functor (CheckedExceptT exceptions m) =>
(forall a. a -> CheckedExceptT exceptions m a)
-> (forall a b.
    CheckedExceptT exceptions m (a -> b)
    -> CheckedExceptT exceptions m a -> CheckedExceptT exceptions m b)
-> (forall a b c.
    (a -> b -> c)
    -> CheckedExceptT exceptions m a
    -> CheckedExceptT exceptions m b
    -> CheckedExceptT exceptions m c)
-> (forall a b.
    CheckedExceptT exceptions m a
    -> CheckedExceptT exceptions m b -> CheckedExceptT exceptions m b)
-> (forall a b.
    CheckedExceptT exceptions m a
    -> CheckedExceptT exceptions m b -> CheckedExceptT exceptions m a)
-> Applicative (CheckedExceptT exceptions m)
forall (exceptions :: [*]) (m :: * -> *).
Monad m =>
Functor (CheckedExceptT exceptions m)
forall (exceptions :: [*]) (m :: * -> *) a.
Monad m =>
a -> CheckedExceptT exceptions m a
forall (exceptions :: [*]) (m :: * -> *) a b.
Monad m =>
CheckedExceptT exceptions m a
-> CheckedExceptT exceptions m b -> CheckedExceptT exceptions m a
forall (exceptions :: [*]) (m :: * -> *) a b.
Monad m =>
CheckedExceptT exceptions m a
-> CheckedExceptT exceptions m b -> CheckedExceptT exceptions m b
forall (exceptions :: [*]) (m :: * -> *) a b.
Monad m =>
CheckedExceptT exceptions m (a -> b)
-> CheckedExceptT exceptions m a -> CheckedExceptT exceptions m b
forall (exceptions :: [*]) (m :: * -> *) a b c.
Monad m =>
(a -> b -> c)
-> CheckedExceptT exceptions m a
-> CheckedExceptT exceptions m b
-> CheckedExceptT exceptions m c
forall a. a -> CheckedExceptT exceptions m a
forall a b.
CheckedExceptT exceptions m a
-> CheckedExceptT exceptions m b -> CheckedExceptT exceptions m a
forall a b.
CheckedExceptT exceptions m a
-> CheckedExceptT exceptions m b -> CheckedExceptT exceptions m b
forall a b.
CheckedExceptT exceptions m (a -> b)
-> CheckedExceptT exceptions m a -> CheckedExceptT exceptions m b
forall a b c.
(a -> b -> c)
-> CheckedExceptT exceptions m a
-> CheckedExceptT exceptions m b
-> CheckedExceptT exceptions m c
forall (f :: * -> *).
Functor f =>
(forall a. a -> f a)
-> (forall a b. f (a -> b) -> f a -> f b)
-> (forall a b c. (a -> b -> c) -> f a -> f b -> f c)
-> (forall a b. f a -> f b -> f b)
-> (forall a b. f a -> f b -> f a)
-> Applicative f
$cpure :: forall (exceptions :: [*]) (m :: * -> *) a.
Monad m =>
a -> CheckedExceptT exceptions m a
pure :: forall a. a -> CheckedExceptT exceptions m a
$c<*> :: forall (exceptions :: [*]) (m :: * -> *) a b.
Monad m =>
CheckedExceptT exceptions m (a -> b)
-> CheckedExceptT exceptions m a -> CheckedExceptT exceptions m b
<*> :: forall a b.
CheckedExceptT exceptions m (a -> b)
-> CheckedExceptT exceptions m a -> CheckedExceptT exceptions m b
$cliftA2 :: forall (exceptions :: [*]) (m :: * -> *) a b c.
Monad m =>
(a -> b -> c)
-> CheckedExceptT exceptions m a
-> CheckedExceptT exceptions m b
-> CheckedExceptT exceptions m c
liftA2 :: forall a b c.
(a -> b -> c)
-> CheckedExceptT exceptions m a
-> CheckedExceptT exceptions m b
-> CheckedExceptT exceptions m c
$c*> :: forall (exceptions :: [*]) (m :: * -> *) a b.
Monad m =>
CheckedExceptT exceptions m a
-> CheckedExceptT exceptions m b -> CheckedExceptT exceptions m b
*> :: forall a b.
CheckedExceptT exceptions m a
-> CheckedExceptT exceptions m b -> CheckedExceptT exceptions m b
$c<* :: forall (exceptions :: [*]) (m :: * -> *) a b.
Monad m =>
CheckedExceptT exceptions m a
-> CheckedExceptT exceptions m b -> CheckedExceptT exceptions m a
<* :: forall a b.
CheckedExceptT exceptions m a
-> CheckedExceptT exceptions m b -> CheckedExceptT exceptions m a
Applicative, (forall a b.
 (a -> b)
 -> CheckedExceptT exceptions m a -> CheckedExceptT exceptions m b)
-> (forall a b.
    a
    -> CheckedExceptT exceptions m b -> CheckedExceptT exceptions m a)
-> Functor (CheckedExceptT exceptions m)
forall (exceptions :: [*]) (m :: * -> *) a b.
Functor m =>
a -> CheckedExceptT exceptions m b -> CheckedExceptT exceptions m a
forall (exceptions :: [*]) (m :: * -> *) a b.
Functor m =>
(a -> b)
-> CheckedExceptT exceptions m a -> CheckedExceptT exceptions m b
forall a b.
a -> CheckedExceptT exceptions m b -> CheckedExceptT exceptions m a
forall a b.
(a -> b)
-> CheckedExceptT exceptions m a -> CheckedExceptT exceptions m b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
$cfmap :: forall (exceptions :: [*]) (m :: * -> *) a b.
Functor m =>
(a -> b)
-> CheckedExceptT exceptions m a -> CheckedExceptT exceptions m b
fmap :: forall a b.
(a -> b)
-> CheckedExceptT exceptions m a -> CheckedExceptT exceptions m b
$c<$ :: forall (exceptions :: [*]) (m :: * -> *) a b.
Functor m =>
a -> CheckedExceptT exceptions m b -> CheckedExceptT exceptions m a
<$ :: forall a b.
a -> CheckedExceptT exceptions m b -> CheckedExceptT exceptions m a
Functor, Monad (CheckedExceptT exceptions m)
Monad (CheckedExceptT exceptions m) =>
(forall a. String -> CheckedExceptT exceptions m a)
-> MonadFail (CheckedExceptT exceptions m)
forall (exceptions :: [*]) (m :: * -> *).
MonadFail m =>
Monad (CheckedExceptT exceptions m)
forall (exceptions :: [*]) (m :: * -> *) a.
MonadFail m =>
String -> CheckedExceptT exceptions m a
forall a. String -> CheckedExceptT exceptions m a
forall (m :: * -> *).
Monad m =>
(forall a. String -> m a) -> MonadFail m
$cfail :: forall (exceptions :: [*]) (m :: * -> *) a.
MonadFail m =>
String -> CheckedExceptT exceptions m a
fail :: forall a. String -> CheckedExceptT exceptions m a
MonadFail, Monad (CheckedExceptT exceptions m)
Monad (CheckedExceptT exceptions m) =>
(forall a. IO a -> CheckedExceptT exceptions m a)
-> MonadIO (CheckedExceptT exceptions m)
forall (exceptions :: [*]) (m :: * -> *).
MonadIO m =>
Monad (CheckedExceptT exceptions m)
forall (exceptions :: [*]) (m :: * -> *) a.
MonadIO m =>
IO a -> CheckedExceptT exceptions m a
forall a. IO a -> CheckedExceptT exceptions m a
forall (m :: * -> *).
Monad m =>
(forall a. IO a -> m a) -> MonadIO m
$cliftIO :: forall (exceptions :: [*]) (m :: * -> *) a.
MonadIO m =>
IO a -> CheckedExceptT exceptions m a
liftIO :: forall a. IO a -> CheckedExceptT exceptions m a
MonadIO, MonadError (OneOf exceptions)) via (ExceptT (OneOf exceptions) m)
  deriving ((forall (m :: * -> *).
 Monad m =>
 Monad (CheckedExceptT exceptions m)) =>
(forall (m :: * -> *) a.
 Monad m =>
 m a -> CheckedExceptT exceptions m a)
-> MonadTrans (CheckedExceptT exceptions)
forall (exceptions :: [*]) (m :: * -> *).
Monad m =>
Monad (CheckedExceptT exceptions m)
forall (exceptions :: [*]) (m :: * -> *) a.
Monad m =>
m a -> CheckedExceptT exceptions m a
forall (m :: * -> *).
Monad m =>
Monad (CheckedExceptT exceptions m)
forall (m :: * -> *) a.
Monad m =>
m a -> CheckedExceptT exceptions m a
forall (t :: (* -> *) -> * -> *).
(forall (m :: * -> *). Monad m => Monad (t m)) =>
(forall (m :: * -> *) a. Monad m => m a -> t m a) -> MonadTrans t
$clift :: forall (exceptions :: [*]) (m :: * -> *) a.
Monad m =>
m a -> CheckedExceptT exceptions m a
lift :: forall (m :: * -> *) a.
Monad m =>
m a -> CheckedExceptT exceptions m a
MonadTrans) via (ExceptT (OneOf exceptions))

-- | Pure checked exceptions.
type CheckedExcept es a = CheckedExceptT es Identity a

-- | See 'weakenOneOf'.
weakenExceptions :: forall exceptions1 exceptions2 m a.
     Functor m
  => Contains exceptions1 exceptions2
  => CheckedExceptT exceptions1 m a
  -> CheckedExceptT exceptions2 m a
weakenExceptions :: forall (exceptions1 :: [*]) (exceptions2 :: [*]) (m :: * -> *) a.
(Functor m, Contains exceptions1 exceptions2) =>
CheckedExceptT exceptions1 m a -> CheckedExceptT exceptions2 m a
weakenExceptions (CheckedExceptT m (Either (OneOf exceptions1) a)
ma) = m (Either (OneOf exceptions2) a) -> CheckedExceptT exceptions2 m a
forall (exceptions :: [*]) (m :: * -> *) a.
m (Either (OneOf exceptions) a) -> CheckedExceptT exceptions m a
CheckedExceptT (m (Either (OneOf exceptions2) a)
 -> CheckedExceptT exceptions2 m a)
-> m (Either (OneOf exceptions2) a)
-> CheckedExceptT exceptions2 m a
forall a b. (a -> b) -> a -> b
$ do
  m (Either (OneOf exceptions1) a)
ma m (Either (OneOf exceptions1) a)
-> (Either (OneOf exceptions1) a -> Either (OneOf exceptions2) a)
-> m (Either (OneOf exceptions2) a)
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \case
    Left OneOf exceptions1
e -> OneOf exceptions2 -> Either (OneOf exceptions2) a
forall a b. a -> Either a b
Left (OneOf exceptions2 -> Either (OneOf exceptions2) a)
-> OneOf exceptions2 -> Either (OneOf exceptions2) a
forall a b. (a -> b) -> a -> b
$ forall (exceptions1 :: [*]) (exceptions2 :: [*]).
Contains exceptions1 exceptions2 =>
OneOf exceptions1 -> OneOf exceptions2
weakenOneOf @exceptions1 @exceptions2 OneOf exceptions1
e
    Right a
a -> a -> Either (OneOf exceptions2) a
forall a b. b -> Either a b
Right a
a

-- | Given a proof that @exceptions1@ is a subset of @exceptions2@,
-- reconstruct the value of the @t'OneOf' exceptions1@ open union to be part of the larger
-- @t'OneOf' exceptions2@ open union. This allows us to compose t'Control.Monad.CheckedExcept.CheckedExceptT' stacks
-- with differing exception sets.
weakenOneOf :: forall exceptions1 exceptions2.
     Contains exceptions1 exceptions2
  => OneOf exceptions1
  -> OneOf exceptions2
weakenOneOf :: forall (exceptions1 :: [*]) (exceptions2 :: [*]).
Contains exceptions1 exceptions2 =>
OneOf exceptions1 -> OneOf exceptions2
weakenOneOf (OneOf e
e') = e -> OneOf exceptions2
forall e.
(Elem e exceptions1, CheckedException e, Typeable e) =>
e -> OneOf exceptions2
weakenE e
e'
  where
  weakenE :: forall e.
      ( Elem e exceptions1
      , CheckedException e
      , Typeable e
      )
    => e
    -> OneOf exceptions2
  weakenE :: forall e.
(Elem e exceptions1, CheckedException e, Typeable e) =>
e -> OneOf exceptions2
weakenE e
e = do
    -- I don't know how to safely prove this, but the `Contains` constraint guarantees this is true/safe.
    let dict1 :: Dict (Elem e exceptions2)
        dict1 :: Dict (Elem e exceptions2)
dict1 = forall (exceptions1 :: [*]) (exceptions2 :: [*]) e.
(Contains exceptions1 exceptions2, Elem e exceptions1) =>
Dict (Elem e exceptions2)
forall {t} (exceptions1 :: [t]) (exceptions2 :: [t]) (e :: t).
(Contains exceptions1 exceptions2, Elem e exceptions1) =>
Dict (Elem e exceptions2)
proveElem @exceptions1 @exceptions2 @e
    e -> OneOf exceptions2
forall e (es :: [*]).
(Elem e es, CheckedException e, Typeable e) =>
e -> OneOf es
OneOf e
e (If (Elem' e exceptions2) (() :: Constraint) (TypeError ...) =>
 OneOf exceptions2)
-> Dict
     (If (Elem' e exceptions2) (() :: Constraint) (TypeError ...))
-> OneOf exceptions2
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ Dict (If (Elem' e exceptions2) (() :: Constraint) (TypeError ...))
Dict (Elem e exceptions2)
dict1

-- | Prove that if @e@ is an element of @exceptions1@ and @exceptions1@ is a subset of @exceptions2@,
-- then @e@ is an element of @exceptions2@.
proveElem :: forall exceptions1 exceptions2 e.
  ( Contains exceptions1 exceptions2
  , Elem e exceptions1
  ) => Dict (Elem e exceptions2)
proveElem :: forall {t} (exceptions1 :: [t]) (exceptions2 :: [t]) (e :: t).
(Contains exceptions1 exceptions2, Elem e exceptions1) =>
Dict (Elem e exceptions2)
proveElem = ((If (Elem' e exceptions1) (() :: Constraint) (TypeError ...),
  Contains exceptions1 exceptions2)
 :- If (Elem' e exceptions2) (() :: Constraint) (TypeError ...))
-> (If (Elem' e exceptions2) (() :: Constraint) (TypeError ...) =>
    Dict (If (Elem' e exceptions2) (() :: Constraint) (TypeError ...)))
-> Dict
     (If (Elem' e exceptions2) (() :: Constraint) (TypeError ...))
forall (c :: Constraint) e r. HasDict c e => e -> (c => r) -> r
withDict ((If (Elem' e exceptions1) (() :: Constraint) (TypeError ...),
 Contains exceptions1 exceptions2)
:- If (Elem' e exceptions2) (() :: Constraint) (TypeError ...)
(Elem e exceptions1, Contains exceptions1 exceptions2)
:- Elem e exceptions2
forall (a :: Constraint) (b :: Constraint). a :- b
unsafeCoerceConstraint :: (Elem e exceptions1, Contains exceptions1 exceptions2) :- (Elem e exceptions2)) Dict (If (Elem' e exceptions2) (() :: Constraint) (TypeError ...))
If (Elem' e exceptions2) (() :: Constraint) (TypeError ...) =>
Dict (If (Elem' e exceptions2) (() :: Constraint) (TypeError ...))
forall (a :: Constraint). a => Dict a
Dict

-- | Get the error from t'CheckedExcept'.
runCheckedExcept :: CheckedExcept es a -> Either (OneOf es) a
runCheckedExcept :: forall (es :: [*]) a. CheckedExcept es a -> Either (OneOf es) a
runCheckedExcept CheckedExcept es a
ce = Identity (Either (OneOf es) a) -> Either (OneOf es) a
forall a. Identity a -> a
runIdentity (CheckedExcept es a -> Identity (Either (OneOf es) a)
forall (exceptions :: [*]) (m :: * -> *) a.
CheckedExceptT exceptions m a -> m (Either (OneOf exceptions) a)
runCheckedExceptT CheckedExcept es a
ce)

-- | The class for checked exceptions.
class Typeable e => CheckedException e where
  -- | Encode an exception to 'String'. Defaults to 'displayException' when available.
  encodeException :: e -> String
  -- | Reify the exception. Defaults to @'withOneOf\'' e cast@.
  fromOneOf :: forall es. OneOf es -> Maybe e

  default encodeException :: Exception e => e -> String
  encodeException = e -> String
forall e. Exception e => e -> String
displayException

  default fromOneOf :: Typeable e => OneOf es -> Maybe e
  fromOneOf OneOf es
e = OneOf es
-> (forall e.
    (Elem e es, CheckedException e, Typeable e) =>
    e -> Maybe e)
-> Maybe e
forall (es :: [*]) a.
OneOf es
-> (forall e.
    (Elem e es, CheckedException e, Typeable e) =>
    e -> a)
-> a
withOneOf' OneOf es
e e -> Maybe e
forall e.
(Elem e es, CheckedException e, Typeable e) =>
e -> Maybe e
forall a b. (Typeable a, Typeable b) => a -> Maybe b
cast

-- | DerivingVia newtype wrapper to derive 'Control.Monad.CheckedExcept.CheckedException' from a 'Show' instance declaration.
-- Useful for prototyping, but I wouldn't recommend this for serious work.
newtype ShowException a = ShowException a

instance (Show a, Typeable a) => CheckedException (ShowException a) where
  encodeException :: ShowException a -> String
encodeException (ShowException a
x) = a -> String
forall a. Show a => a -> String
show a
x

-- | DerivingVia newtype wrapper to derive 'Control.Monad.CheckedExcept.CheckedException' from 'Exception'.
newtype ExceptionException a = ExceptionException a

instance (Show a, Typeable a, Exception a) => CheckedException (ExceptionException a) where
  encodeException :: ExceptionException a -> String
encodeException (ExceptionException a
e) = a -> String
forall e. Exception e => e -> String
displayException a
e

deriving via (ExceptionException SomeException) instance CheckedException SomeException

-- | A sort of pseudo-open union that is easy to construct but difficult to
-- deconstruct. In lieu of singletons we opt for 'Typeable' to prove the type
-- of the existentially quantified exception @e@ in the set @es@.
data OneOf (es :: [Type]) where
  OneOf :: forall e es. (Elem e es, CheckedException e, Typeable e) => !e -> OneOf es

-- | Data type used for constructing a coverage checked case-like `catch`.
data CaseException x es where
  CaseEndWith :: x -> CaseException x '[]
  CaseCons :: Typeable e => (e -> x) -> CaseException x es -> CaseException x (e ': es)
  CaseAny :: (forall e. CheckedException e => (e -> x)) -> CaseException x es

-- | Pattern synonym for @CaseEndWith (error "impossible")@.
-- This should never be evaluated since 'caseException' does not accept empty lists.
pattern CaseEnd :: forall x. CaseException x '[]
pattern $mCaseEnd :: forall {r} {x}.
CaseException x '[] -> ((# #) -> r) -> ((# #) -> r) -> r
$bCaseEnd :: forall x. CaseException x '[]
CaseEnd <- _ where
  CaseEnd = x -> CaseException x '[]
forall x. x -> CaseException x '[]
CaseEndWith (String -> x
forall a. HasCallStack => String -> a
error String
"impossible")

-- | Infix 'CaseCons' with proper fixity.
infixr 7 <:
(<:) :: Typeable e => (e -> x) -> CaseException x es -> CaseException x (e : es)
<: :: forall e x (es :: [*]).
Typeable e =>
(e -> x) -> CaseException x es -> CaseException x (e : es)
(<:) = (e -> x) -> CaseException x es -> CaseException x (e : es)
forall e x (es :: [*]).
Typeable e =>
(e -> x) -> CaseException x es -> CaseException x (e : es)
CaseCons

-- | Throw a checked exception @e@ that is a member of the exception set @es@.
throwCheckedException :: forall e es m a. (Elem e es, CheckedException e, Applicative m) => e -> CheckedExceptT es m a
throwCheckedException :: forall e (es :: [*]) (m :: * -> *) a.
(Elem e es, CheckedException e, Applicative m) =>
e -> CheckedExceptT es m a
throwCheckedException e
e = do
  let oneOf :: OneOf es
      oneOf :: OneOf es
oneOf = e -> OneOf es
forall e (es :: [*]).
(Elem e es, CheckedException e, Typeable e) =>
e -> OneOf es
OneOf e
e
  m (Either (OneOf es) a) -> CheckedExceptT es m a
forall (exceptions :: [*]) (m :: * -> *) a.
m (Either (OneOf exceptions) a) -> CheckedExceptT exceptions m a
CheckedExceptT (m (Either (OneOf es) a) -> CheckedExceptT es m a)
-> m (Either (OneOf es) a) -> CheckedExceptT es m a
forall a b. (a -> b) -> a -> b
$ Either (OneOf es) a -> m (Either (OneOf es) a)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Either (OneOf es) a -> m (Either (OneOf es) a))
-> Either (OneOf es) a -> m (Either (OneOf es) a)
forall a b. (a -> b) -> a -> b
$ OneOf es -> Either (OneOf es) a
forall a b. a -> Either a b
Left OneOf es
oneOf

-- | Apply a function @f@ over a checked exception, using methods from the 'Control.Monad.CheckedExcept.CheckedException' typeclass.
applyAll :: (forall e. CheckedException e => e -> b) -> OneOf es -> b
applyAll :: forall b (es :: [*]).
(forall e. CheckedException e => e -> b) -> OneOf es -> b
applyAll forall e. CheckedException e => e -> b
f (OneOf e
e) = e -> b
forall e. CheckedException e => e -> b
f e
e

-- | Catch an exception or @mempty@ (think @pure ()@ or @Nothing@).
withOneOf :: (Elem e es, Monoid a, CheckedException e) => OneOf es -> (e -> a) -> a
withOneOf :: forall e (es :: [*]) a.
(Elem e es, Monoid a, CheckedException e) =>
OneOf es -> (e -> a) -> a
withOneOf OneOf es
e e -> a
f = case OneOf es -> Maybe e
forall (es :: [*]). OneOf es -> Maybe e
forall e (es :: [*]). CheckedException e => OneOf es -> Maybe e
fromOneOf OneOf es
e of
  Just e
x -> e -> a
f e
x
  Maybe e
Nothing -> a
forall a. Monoid a => a
mempty

-- | Catch an exception, totally.
withOneOf' :: OneOf es -> (forall e. (Elem e es, CheckedException e, Typeable e) => e -> a) -> a
withOneOf' :: forall (es :: [*]) a.
OneOf es
-> (forall e.
    (Elem e es, CheckedException e, Typeable e) =>
    e -> a)
-> a
withOneOf' (OneOf e
e) forall e. (Elem e es, CheckedException e, Typeable e) => e -> a
f = e -> a
forall e. (Elem e es, CheckedException e, Typeable e) => e -> a
f e
e

-- | Remove duplicates from a type-level list.
type family Nub xs where
  Nub '[] = '[]
  Nub (x ': xs) = x ': Nub (Remove x xs)

-- | Type-level list concatenation.
infixr 5 ++
type family (++) (xs :: [k]) (ys :: [k]) :: [k] where
    '[]       ++ ys = ys
    (x ': xs) ++ ys = x ': xs ++ ys

-- | Remove element from a type-level list.
type family Remove x xs where
  Remove x '[]       = '[]
  Remove x (x ': ys) =      Remove x ys
  Remove x (y ': ys) = y ': Remove x ys

-- | Is @x@ present in the list @xs@?
type family Elem' x xs where
  Elem' x '[] = 'False
  Elem' x (x ': xs) = 'True
  Elem' x (y ': xs) = Elem' x xs

-- TODO: Sometimes causes weird type errors when it doesn't propagate correctly.
-- | @ type Elem x xs = Elem' x xs ~ 'True @
type family Elem x xs :: Constraint where
  Elem x xs =
    If (Elem' x xs)
      (() :: Constraint)
      (NotElemTypeError x xs)

-- | Type error for when @'Elem' e es'@ fails to hold.
type NotElemTypeError x xs = TypeError ('ShowType x ':<>: 'Text " is not a member of " ':<>: 'ShowType xs)

-- | Constraint that the list @as@ is a subset of list @bs@.
type family Contains (as :: [k]) (bs :: [k]) :: Constraint where
  Contains '[] _ = ()
  Contains as as = ()
  Contains (a ': as) bs = (Elem' a bs ~ 'True, Contains as bs)

-- | Type-level proof that a list is non-empty, used for constraining 'caseException' so that you don't
-- pointlessly throw @'error'@.
type family NonEmpty xs :: Constraint where
  NonEmpty '[] = TypeError ('Text "type level list must be non-empty")
  NonEmpty _ = () :: Constraint

-- TODO: Exceptions can show up more than once in the list, which we handle with
-- 'Nub', but the error message we give to the user for trying to catch an exception
-- twice is really bad.
--
-- | Case on a checked exception with coverage checking. Note: while @es@ may not be a set,
-- the 'CaseException' you supply must be.
caseException :: NonEmpty es => OneOf es -> CaseException x (Nub es) -> x
caseException :: forall (es :: [*]) x.
NonEmpty es =>
OneOf es -> CaseException x (Nub es) -> x
caseException (OneOf e
e') = e -> CaseException x (Nub es) -> x
forall e x (es :: [*]).
(CheckedException e, Typeable e) =>
e -> CaseException x es -> x
go e
e'
  where
  test :: (Typeable e1, Typeable e2) => e2 -> (e1 -> x) -> Maybe (e1 :~: e2)
  test :: forall e1 e2 x.
(Typeable e1, Typeable e2) =>
e2 -> (e1 -> x) -> Maybe (e1 :~: e2)
test e2
_ e1 -> x
_ = Maybe (e1 :~: e2)
forall {k} (a :: k) (b :: k).
(Typeable a, Typeable b) =>
Maybe (a :~: b)
eqT
  go :: (CheckedException e, Typeable e) => e -> CaseException x es -> x
  go :: forall e x (es :: [*]).
(CheckedException e, Typeable e) =>
e -> CaseException x es -> x
go e
e (CaseCons e -> x
f CaseException x es
rec) = case e -> (e -> x) -> Maybe (e :~: e)
forall e1 e2 x.
(Typeable e1, Typeable e2) =>
e2 -> (e1 -> x) -> Maybe (e1 :~: e2)
test e
e e -> x
f of
    Just e :~: e
Refl -> e -> x
f e
e
e
    Maybe (e :~: e)
Nothing -> e -> CaseException x es -> x
forall e x (es :: [*]).
(CheckedException e, Typeable e) =>
e -> CaseException x es -> x
go e
e CaseException x es
rec
  go e
e (CaseAny forall e. CheckedException e => e -> x
f) = e -> x
forall e. CheckedException e => e -> x
f e
e
  go e
_ (CaseEndWith x
x) = x
x

-- | Add 'SomeException' to the exceptions set. Preferably, call this before catching the checked
-- exceptions so there are no surprising exceptions.
catchSomeException :: (Monad m, MonadCatch m, Elem SomeException es) => CheckedExceptT es m a -> CheckedExceptT es m a
catchSomeException :: forall (m :: * -> *) (es :: [*]) a.
(Monad m, MonadCatch m, Elem SomeException es) =>
CheckedExceptT es m a -> CheckedExceptT es m a
catchSomeException CheckedExceptT es m a
ce = do
  me <- m (Either SomeException (Either (OneOf es) a))
-> CheckedExceptT es m (Either SomeException (Either (OneOf es) a))
forall (m :: * -> *) a. Monad m => m a -> CheckedExceptT es m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m (Either SomeException (Either (OneOf es) a))
 -> CheckedExceptT
      es m (Either SomeException (Either (OneOf es) a)))
-> m (Either SomeException (Either (OneOf es) a))
-> CheckedExceptT es m (Either SomeException (Either (OneOf es) a))
forall a b. (a -> b) -> a -> b
$ m (Either SomeException (Either (OneOf es) a))
-> (SomeException
    -> m (Either SomeException (Either (OneOf es) a)))
-> m (Either SomeException (Either (OneOf es) a))
forall e a. (HasCallStack, Exception e) => m a -> (e -> m a) -> m a
forall (m :: * -> *) e a.
(MonadCatch m, HasCallStack, Exception e) =>
m a -> (e -> m a) -> m a
catch (Either (OneOf es) a -> Either SomeException (Either (OneOf es) a)
forall a b. b -> Either a b
Right (Either (OneOf es) a -> Either SomeException (Either (OneOf es) a))
-> m (Either (OneOf es) a)
-> m (Either SomeException (Either (OneOf es) a))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> CheckedExceptT es m a -> m (Either (OneOf es) a)
forall (exceptions :: [*]) (m :: * -> *) a.
CheckedExceptT exceptions m a -> m (Either (OneOf exceptions) a)
runCheckedExceptT CheckedExceptT es m a
ce) (Either SomeException (Either (OneOf es) a)
-> m (Either SomeException (Either (OneOf es) a))
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Either SomeException (Either (OneOf es) a)
 -> m (Either SomeException (Either (OneOf es) a)))
-> (SomeException -> Either SomeException (Either (OneOf es) a))
-> SomeException
-> m (Either SomeException (Either (OneOf es) a))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SomeException -> Either SomeException (Either (OneOf es) a)
forall a b. a -> Either a b
Left)
  case me of
    Right Either (OneOf es) a
a -> m (Either (OneOf es) a) -> CheckedExceptT es m a
forall (exceptions :: [*]) (m :: * -> *) a.
m (Either (OneOf exceptions) a) -> CheckedExceptT exceptions m a
CheckedExceptT (m (Either (OneOf es) a) -> CheckedExceptT es m a)
-> m (Either (OneOf es) a) -> CheckedExceptT es m a
forall a b. (a -> b) -> a -> b
$ Either (OneOf es) a -> m (Either (OneOf es) a)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Either (OneOf es) a
a
    Left SomeException
e -> SomeException -> CheckedExceptT es m a
forall e (es :: [*]) (m :: * -> *) a.
(Elem e es, CheckedException e, Applicative m) =>
e -> CheckedExceptT es m a
throwCheckedException (SomeException
e :: SomeException)