{-# OPTIONS_GHC -Wno-pattern-namespace-specifier #-}

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

-- | Basic API of t'CheckedExceptT'

module Control.Monad.CheckedExcept
  ( -- * Types

    CheckedExceptT(..)
  , CheckedExcept
  , OneOf
  , oneOf
  , ElemIx(..)
  , Subset(..)
  , CaseException(..)
  , pattern CaseEnd
  , ShowException(..)
  , ExceptionException(..)
  -- * Typeclass

  , CheckedException(..)
  -- * Utility functions

  , runCheckedExcept
  , throwCheckedException
  , applyAll
  , weakenExceptions
  , weakenExceptionsWith
  , weakenOneOf
  , weakenOneOfWith
  , withOneOf
  , withOneOf'
  , caseException
  , (<:)
  , catchSomeException
  , containsRefl
  , lookupSubset
  -- * 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 GHC.TypeLits
import GHC.TypeError (Unsatisfiable, unsatisfiable)
import Data.Typeable (Typeable, eqT)
import Data.Type.Equality
import Control.Monad.IO.Class (MonadIO)
import Control.Monad.Trans (MonadTrans (..))
import Data.Constraint (Dict (..), withDict)
import Control.Monad.Catch (MonadCatch (..))

-- | Isomorphic to t'ExceptT' over our open-union exceptions type @t'OneOf' es@.

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. HasCallStack => String -> CheckedExceptT exceptions m a)
-> MonadFail (CheckedExceptT exceptions m)
forall (exceptions :: [*]) (m :: * -> *).
MonadFail m =>
Monad (CheckedExceptT exceptions m)
forall (exceptions :: [*]) (m :: * -> *) a.
(MonadFail m, HasCallStack) =>
String -> CheckedExceptT exceptions m a
forall a. HasCallStack => String -> CheckedExceptT exceptions m a
forall (m :: * -> *).
Monad m =>
(forall a. HasCallStack => String -> m a) -> MonadFail m
$cfail :: forall (exceptions :: [*]) (m :: * -> *) a.
(MonadFail m, HasCallStack) =>
String -> CheckedExceptT exceptions m a
fail :: forall a. HasCallStack => 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

-- | Reflexive subset witness for abstract exception lists.

containsRefl :: Subset es es
containsRefl :: forall (es :: [*]). Subset es es
containsRefl = Subset es es
forall (es :: [*]). Subset es es
SubRefl

-- | See 'weakenOneOfWith'.

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 exceptions1 m a
ce = Subset exceptions1 exceptions2
-> CheckedExceptT exceptions1 m a -> CheckedExceptT exceptions2 m a
forall (m :: * -> *) (exceptions1 :: [*]) (exceptions2 :: [*]) a.
Functor m =>
Subset exceptions1 exceptions2
-> CheckedExceptT exceptions1 m a -> CheckedExceptT exceptions2 m a
weakenExceptionsWith Subset exceptions1 exceptions2
forall (es1 :: [*]) (es2 :: [*]).
Contains es1 es2 =>
Subset es1 es2
subset CheckedExceptT exceptions1 m a
ce

-- | Weaken using an explicit subset witness.

weakenExceptionsWith ::
     Functor m
  => Subset exceptions1 exceptions2
  -> CheckedExceptT exceptions1 m a
  -> CheckedExceptT exceptions2 m a
weakenExceptionsWith :: forall (m :: * -> *) (exceptions1 :: [*]) (exceptions2 :: [*]) a.
Functor m =>
Subset exceptions1 exceptions2
-> CheckedExceptT exceptions1 m a -> CheckedExceptT exceptions2 m a
weakenExceptionsWith Subset exceptions1 exceptions2
s (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
$ Subset exceptions1 exceptions2
-> OneOf exceptions1 -> OneOf exceptions2
forall (exceptions1 :: [*]) (exceptions2 :: [*]).
Subset exceptions1 exceptions2
-> OneOf exceptions1 -> OneOf exceptions2
weakenOneOfWith Subset exceptions1 exceptions2
s OneOf exceptions1
e
    Right a
a -> a -> Either (OneOf exceptions2) a
forall a b. b -> Either a b
Right a
a

-- | See 'weakenOneOfWith'.

weakenOneOf :: forall exceptions1 exceptions2.
     Contains exceptions1 exceptions2
  => OneOf exceptions1
  -> OneOf exceptions2
weakenOneOf :: forall (exceptions1 :: [*]) (exceptions2 :: [*]).
Contains exceptions1 exceptions2 =>
OneOf exceptions1 -> OneOf exceptions2
weakenOneOf OneOf exceptions1
e = Subset exceptions1 exceptions2
-> OneOf exceptions1 -> OneOf exceptions2
forall (exceptions1 :: [*]) (exceptions2 :: [*]).
Subset exceptions1 exceptions2
-> OneOf exceptions1 -> OneOf exceptions2
weakenOneOfWith Subset exceptions1 exceptions2
forall (es1 :: [*]) (es2 :: [*]).
Contains es1 es2 =>
Subset es1 es2
subset OneOf exceptions1
e

-- | Reconstruct a @t'OneOf' exceptions1@ as part of a larger @t'OneOf' exceptions2@.

weakenOneOfWith :: Subset exceptions1 exceptions2 -> OneOf exceptions1 -> OneOf exceptions2
weakenOneOfWith :: forall (exceptions1 :: [*]) (exceptions2 :: [*]).
Subset exceptions1 exceptions2
-> OneOf exceptions1 -> OneOf exceptions2
weakenOneOfWith Subset exceptions1 exceptions2
s (MkOneOf ElemIx e exceptions1
ix e
e) = ElemIx e exceptions2 -> e -> OneOf exceptions2
forall e (es :: [*]).
(CheckedException e, Typeable e) =>
ElemIx e es -> e -> OneOf es
MkOneOf (Subset exceptions1 exceptions2
-> ElemIx e exceptions1 -> ElemIx e exceptions2
forall (es1 :: [*]) (es2 :: [*]) e.
Subset es1 es2 -> ElemIx e es1 -> ElemIx e es2
lookupSubset Subset exceptions1 exceptions2
s ElemIx e exceptions1
ix) e
e

-- | 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
  encodeException :: e -> String
  -- | Reify an exception from a 'OneOf' when its runtime type matches @e@.

  -- Custom instances should preserve this contract: @'Just'@ only when the

  -- payload type equals @e@ (same rule as the default 'eqT' witness path).

  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 :: forall es. OneOf es -> Maybe e
  fromOneOf OneOf es
o = 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
o e -> Maybe e
forall e'. Typeable e' => e' -> Maybe e
forall e.
(Elem e es, CheckedException e, Typeable e) =>
e -> Maybe e
match
    where
      match :: forall e'. Typeable e' => e' -> Maybe e
      match :: forall e'. Typeable e' => e' -> Maybe e
match e'
x = case forall {k} (a :: k) (b :: k).
(Typeable a, Typeable b) =>
Maybe (a :~: b)
forall a b. (Typeable a, Typeable b) => Maybe (a :~: b)
eqT @e @e' of
        Just e :~: e'
Refl -> e -> Maybe e
forall a. a -> Maybe a
Just e
e'
x
        Maybe (e :~: e')
Nothing -> Maybe e
forall a. Maybe a
Nothing

-- | DerivingVia newtype wrapper to derive 'CheckedException' from a 'Show' instance.

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
  fromOneOf :: forall (es :: [*]). OneOf es -> Maybe (ShowException a)
fromOneOf OneOf es
o = OneOf es
-> (forall e.
    (Elem e es, CheckedException e, Typeable e) =>
    e -> Maybe (ShowException a))
-> Maybe (ShowException a)
forall (es :: [*]) a.
OneOf es
-> (forall e.
    (Elem e es, CheckedException e, Typeable e) =>
    e -> a)
-> a
withOneOf' OneOf es
o ((forall e.
  (Elem e es, CheckedException e, Typeable e) =>
  e -> Maybe (ShowException a))
 -> Maybe (ShowException a))
-> (forall e.
    (Elem e es, CheckedException e, Typeable e) =>
    e -> Maybe (ShowException a))
-> Maybe (ShowException a)
forall a b. (a -> b) -> a -> b
$ \(e
x :: e') -> case forall {k} (a :: k) (b :: k).
(Typeable a, Typeable b) =>
Maybe (a :~: b)
forall a b. (Typeable a, Typeable b) => Maybe (a :~: b)
eqT @a @e' of
    Just a :~: e
Refl -> ShowException a -> Maybe (ShowException a)
forall a. a -> Maybe a
Just (a -> ShowException a
forall a. a -> ShowException a
ShowException a
e
x)
    Maybe (a :~: e)
Nothing -> Maybe (ShowException a)
forall a. Maybe a
Nothing

-- | DerivingVia newtype wrapper to derive 'CheckedException' from 'Exception'.

newtype ExceptionException a = ExceptionException a

instance (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
  fromOneOf :: forall (es :: [*]). OneOf es -> Maybe (ExceptionException a)
fromOneOf OneOf es
o = OneOf es
-> (forall e.
    (Elem e es, CheckedException e, Typeable e) =>
    e -> Maybe (ExceptionException a))
-> Maybe (ExceptionException a)
forall (es :: [*]) a.
OneOf es
-> (forall e.
    (Elem e es, CheckedException e, Typeable e) =>
    e -> a)
-> a
withOneOf' OneOf es
o ((forall e.
  (Elem e es, CheckedException e, Typeable e) =>
  e -> Maybe (ExceptionException a))
 -> Maybe (ExceptionException a))
-> (forall e.
    (Elem e es, CheckedException e, Typeable e) =>
    e -> Maybe (ExceptionException a))
-> Maybe (ExceptionException a)
forall a b. (a -> b) -> a -> b
$ \(e
x :: e') -> case forall {k} (a :: k) (b :: k).
(Typeable a, Typeable b) =>
Maybe (a :~: b)
forall a b. (Typeable a, Typeable b) => Maybe (a :~: b)
eqT @a @e' of
    Just a :~: e
Refl -> ExceptionException a -> Maybe (ExceptionException a)
forall a. a -> Maybe a
Just (a -> ExceptionException a
forall a. a -> ExceptionException a
ExceptionException a
e
x)
    Maybe (a :~: e)
Nothing -> Maybe (ExceptionException a)
forall a. Maybe a
Nothing

deriving via (ExceptionException SomeException) instance CheckedException SomeException

-- | Witness that @e@ occurs at a specific position in @es@.

data ElemIx (e :: Type) (es :: [Type]) where
  Here :: ElemIx e (e ': es)
  There :: !(ElemIx e es) -> ElemIx e (f ': es)

-- | Witness that every element of @es1@ is contained in @es2@.

data Subset (es1 :: [Type]) (es2 :: [Type]) where
  SubRefl :: Subset es es
  SubNil :: Subset '[] es2
  SubCons :: !(ElemIx e es2) -> !(Subset es1 es2) -> Subset (e ': es1) es2

-- | Translate a membership index along a subset witness.

lookupSubset :: Subset es1 es2 -> ElemIx e es1 -> ElemIx e es2
lookupSubset :: forall (es1 :: [*]) (es2 :: [*]) e.
Subset es1 es2 -> ElemIx e es1 -> ElemIx e es2
lookupSubset Subset es1 es2
SubRefl ElemIx e es1
ix = ElemIx e es1
ElemIx e es2
ix
lookupSubset (SubCons ElemIx e es2
ix Subset es1 es2
_) ElemIx e es1
Here = ElemIx e es2
ElemIx e es2
ix
lookupSubset (SubCons ElemIx e es2
_ Subset es1 es2
s) (There ElemIx e es
ix) = Subset es1 es2 -> ElemIx e es1 -> ElemIx e es2
forall (es1 :: [*]) (es2 :: [*]) e.
Subset es1 es2 -> ElemIx e es1 -> ElemIx e es2
lookupSubset Subset es1 es2
s ElemIx e es1
ElemIx e es
ix
lookupSubset Subset es1 es2
SubNil ElemIx e es1
ix = case ElemIx e es1
ix of {}

-- | Recover an 'Elem' dictionary from a membership index.

elemDictFromIx :: forall e es. ElemIx e es -> Dict (Elem e es)
elemDictFromIx :: forall e (es :: [*]). ElemIx e es -> Dict (Elem e es)
elemDictFromIx ElemIx e es
Here = Dict (Elem e es)
forall (a :: Constraint). a => Dict a
Dict
elemDictFromIx (There ElemIx e es
ix) = Dict (Elem e es)
-> (Elem e es => Dict (Elem e es)) -> Dict (Elem e es)
forall (c :: Constraint) e r. HasDict c e => e -> (c => r) -> r
withDict (ElemIx e es -> Dict (Elem e es)
forall e (es :: [*]). ElemIx e es -> Dict (Elem e es)
elemDictFromIx ElemIx e es
ix) Dict (Elem e es)
Elem e es => Dict (Elem e es)
forall (a :: Constraint). a => Dict a
Dict

-- | Membership in a type-level list, backed by a value-level index.

--

-- Duplicate types in @es@ are not supported: the incoherent tail instance

-- picks the first index, so prefer @'Nub' es@ (or a duplicate-free list) at

-- the kind level.

class Elem (e :: Type) (es :: [Type]) where
  elemIx :: ElemIx e es

instance {-# OVERLAPPING #-} Elem e (e ': es) where
  elemIx :: ElemIx e (e : es)
elemIx = ElemIx e (e : es)
forall e (es :: [*]). ElemIx e (e : es)
Here

instance {-# INCOHERENT #-} Elem e es => Elem e (x ': es) where
  elemIx :: ElemIx e (x : es)
elemIx = ElemIx e es -> ElemIx e (x : es)
forall e (e :: [*]) es1. ElemIx e e -> ElemIx e (es1 : e)
There (forall e (es :: [*]). Elem e es => ElemIx e es
elemIx @e @es)

instance Unsatisfiable (NotElemTypeError e '[]) => Elem e '[] where
  elemIx :: ElemIx e '[]
elemIx = ElemIx e '[]
forall (msg :: ErrorMessage) a. Unsatisfiable msg => a
unsatisfiable

-- | @es1@ is a subset of @es2@.

--

-- There is no reflexive instance for abstract @es@: use 'containsRefl' or

-- 'weakenExceptionsWith' when @es1@ and @es2@ are the same type variable.

class Contains (es1 :: [Type]) (es2 :: [Type]) where
  subset :: Subset es1 es2

instance Contains '[] es2 where
  subset :: Subset '[] es2
subset = Subset '[] es2
forall (es2 :: [*]). Subset '[] es2
SubNil

instance (Elem e es2, Contains es1 es2) => Contains (e ': es1) es2 where
  subset :: Subset (e : es1) es2
subset = ElemIx e es2 -> Subset es1 es2 -> Subset (e : es1) es2
forall e (es2 :: [*]) (es1 :: [*]).
ElemIx e es2 -> Subset es1 es2 -> Subset (e : es1) es2
SubCons (forall e (es :: [*]). Elem e es => ElemIx e es
elemIx @e @es2) (forall (es1 :: [*]) (es2 :: [*]).
Contains es1 es2 =>
Subset es1 es2
subset @es1 @es2)

-- | A sort of pseudo-open union backed by membership witnesses.

data OneOf (es :: [Type]) where
  MkOneOf :: forall e es. (CheckedException e, Typeable e) => !(ElemIx e es) -> !e -> OneOf es

{-# COMPLETE MkOneOf #-}

-- | Construct a checked exception value.

oneOf :: forall e es. (Elem e es, CheckedException e) => e -> OneOf es
oneOf :: forall e (es :: [*]).
(Elem e es, CheckedException e) =>
e -> OneOf es
oneOf e
e = ElemIx e es -> e -> OneOf es
forall e (es :: [*]).
(CheckedException e, Typeable e) =>
ElemIx e es -> e -> OneOf es
MkOneOf (forall e (es :: [*]). Elem e es => ElemIx e es
elemIx @e @es) e
e

-- | 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 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")

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

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 = 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 (e -> OneOf es
forall e (es :: [*]).
(Elem e es, CheckedException e) =>
e -> OneOf es
oneOf e
e)

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 (MkOneOf ElemIx e es
_ e
e) = e -> b
forall e. CheckedException e => e -> b
f e
e

-- | Run @f@ when the payload type equals @e@; otherwise return 'mempty'.

--

-- Uses an @eqT@ witness (like the default 'fromOneOf'), not a custom

-- 'fromOneOf' instance — a custom 'fromOneOf' returning 'Nothing' does not

-- affect this function.

withOneOf :: forall e es a. (Monoid a, CheckedException e) => OneOf es -> (e -> a) -> a
withOneOf :: forall e (es :: [*]) a.
(Monoid a, CheckedException e) =>
OneOf es -> (e -> a) -> a
withOneOf OneOf es
o e -> a
f = OneOf es
-> (forall e.
    (Elem e es, CheckedException e, Typeable e) =>
    e -> a)
-> a
forall (es :: [*]) a.
OneOf es
-> (forall e.
    (Elem e es, CheckedException e, Typeable e) =>
    e -> a)
-> a
withOneOf' OneOf es
o ((forall e. (Elem e es, CheckedException e, Typeable e) => e -> a)
 -> a)
-> (forall e.
    (Elem e es, CheckedException e, Typeable e) =>
    e -> a)
-> a
forall a b. (a -> b) -> a -> b
$ \(e
x :: e') -> case forall {k} (a :: k) (b :: k).
(Typeable a, Typeable b) =>
Maybe (a :~: b)
forall a b. (Typeable a, Typeable b) => Maybe (a :~: b)
eqT @e @e' of
  Just e :~: e
Refl -> e -> a
f e
e
x
  Maybe (e :~: e)
Nothing -> a
forall a. Monoid a => a
mempty

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' (MkOneOf ElemIx e es
ix e
e) forall e. (Elem e es, CheckedException e, Typeable e) => e -> a
f = Dict (Elem e es) -> (Elem e es => a) -> a
forall (c :: Constraint) e r. HasDict c e => e -> (c => r) -> r
withDict (ElemIx e es -> Dict (Elem e es)
forall e (es :: [*]). ElemIx e es -> Dict (Elem e es)
elemDictFromIx ElemIx e es
ix) (e -> a
forall e. (Elem e es, CheckedException e, Typeable e) => e -> a
f e
e)

type family Nub xs where
  Nub '[] = '[]
  Nub (x ': xs) = x ': Nub (Remove x xs)

infixr 5 ++
type family (++) (xs :: [k]) (ys :: [k]) :: [k] where
  '[] ++ ys = ys
  (x ': xs) ++ ys = x ': xs ++ ys

type family Remove x xs where
  Remove x '[] = '[]
  Remove x (x ': ys) = Remove x ys
  Remove x (y ': ys) = y ': Remove x ys

type family Elem' x xs where
  Elem' x '[] = 'False
  Elem' x (x ': xs) = 'True
  Elem' x (y ': xs) = Elem' x xs

type NotElemTypeError x xs =
  TypeError ('ShowType x ':<>: 'Text " is not a member of " ':<>: 'ShowType xs)

type family NonEmpty xs :: Constraint where
  NonEmpty '[] = TypeError ('Text "type level list must be non-empty")
  NonEmpty _ = () :: Constraint

caseException :: OneOf es -> CaseException x (Nub es) -> x
caseException :: forall (es :: [*]) x. OneOf es -> CaseException x (Nub es) -> x
caseException (MkOneOf ElemIx e es
_ e
e') = e -> CaseException x (Nub es) -> x
forall e x (es :: [*]).
CheckedException e =>
e -> CaseException x es -> x
go e
e'
  where
  -- Dispatch uses the case-arm type (@eCase@, from @f@'s domain), not runtime

  -- inspection beyond @eqT@. Safe while 'CaseCons' keeps this typing; revisit

  -- if 'CaseCons' is ever generalized.

  branch :: forall eVal eCase x'. (Typeable eVal, Typeable eCase) => eVal -> (eCase -> x') -> Maybe x'
  branch :: forall eVal eCase x'.
(Typeable eVal, Typeable eCase) =>
eVal -> (eCase -> x') -> Maybe x'
branch eVal
x eCase -> x'
f = case forall {k} (a :: k) (b :: k).
(Typeable a, Typeable b) =>
Maybe (a :~: b)
forall a b. (Typeable a, Typeable b) => Maybe (a :~: b)
eqT @eCase @eVal of
    Just eCase :~: eVal
Refl -> x' -> Maybe x'
forall a. a -> Maybe a
Just (eCase -> x'
f eVal
eCase
x)
    Maybe (eCase :~: eVal)
Nothing -> Maybe x'
forall a. Maybe a
Nothing
  go :: CheckedException e => e -> CaseException x es -> x
  go :: forall e x (es :: [*]).
CheckedException e =>
e -> CaseException x es -> x
go e
e (CaseCons e -> x
f CaseException x es
rec) = case e -> (e -> x) -> Maybe x
forall eVal eCase x'.
(Typeable eVal, Typeable eCase) =>
eVal -> (eCase -> x') -> Maybe x'
branch e
e e -> x
f of
    Just x
x -> x
x
    Maybe x
Nothing -> e -> CaseException x es -> x
forall e x (es :: [*]).
CheckedException 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

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)