-- | A pure MonadFail.
module Agda.Utils.Fail where

-- Control.Monad.Fail import is redundant since GHC 8.8.1
import Control.Monad.Fail

newtype Fail a = Fail { forall a. Fail a -> Either String a
runFail :: Either String a }
  deriving ((forall a b. (a -> b) -> Fail a -> Fail b)
-> (forall a b. a -> Fail b -> Fail a) -> Functor Fail
forall a b. a -> Fail b -> Fail a
forall a b. (a -> b) -> Fail a -> Fail 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 -> Fail b -> Fail a
$c<$ :: forall a b. a -> Fail b -> Fail a
fmap :: forall a b. (a -> b) -> Fail a -> Fail b
$cfmap :: forall a b. (a -> b) -> Fail a -> Fail b
Functor, Functor Fail
Functor Fail
-> (forall a. a -> Fail a)
-> (forall a b. Fail (a -> b) -> Fail a -> Fail b)
-> (forall a b c. (a -> b -> c) -> Fail a -> Fail b -> Fail c)
-> (forall a b. Fail a -> Fail b -> Fail b)
-> (forall a b. Fail a -> Fail b -> Fail a)
-> Applicative Fail
forall a. a -> Fail a
forall a b. Fail a -> Fail b -> Fail a
forall a b. Fail a -> Fail b -> Fail b
forall a b. Fail (a -> b) -> Fail a -> Fail b
forall a b c. (a -> b -> c) -> Fail a -> Fail b -> Fail 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
<* :: forall a b. Fail a -> Fail b -> Fail a
$c<* :: forall a b. Fail a -> Fail b -> Fail a
*> :: forall a b. Fail a -> Fail b -> Fail b
$c*> :: forall a b. Fail a -> Fail b -> Fail b
liftA2 :: forall a b c. (a -> b -> c) -> Fail a -> Fail b -> Fail c
$cliftA2 :: forall a b c. (a -> b -> c) -> Fail a -> Fail b -> Fail c
<*> :: forall a b. Fail (a -> b) -> Fail a -> Fail b
$c<*> :: forall a b. Fail (a -> b) -> Fail a -> Fail b
pure :: forall a. a -> Fail a
$cpure :: forall a. a -> Fail a
Applicative, Applicative Fail
Applicative Fail
-> (forall a b. Fail a -> (a -> Fail b) -> Fail b)
-> (forall a b. Fail a -> Fail b -> Fail b)
-> (forall a. a -> Fail a)
-> Monad Fail
forall a. a -> Fail a
forall a b. Fail a -> Fail b -> Fail b
forall a b. Fail a -> (a -> Fail b) -> Fail 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
return :: forall a. a -> Fail a
$creturn :: forall a. a -> Fail a
>> :: forall a b. Fail a -> Fail b -> Fail b
$c>> :: forall a b. Fail a -> Fail b -> Fail b
>>= :: forall a b. Fail a -> (a -> Fail b) -> Fail b
$c>>= :: forall a b. Fail a -> (a -> Fail b) -> Fail b
Monad)

instance MonadFail Fail where
  fail :: forall a. String -> Fail a
fail = Either String a -> Fail a
forall a. Either String a -> Fail a
Fail (Either String a -> Fail a)
-> (String -> Either String a) -> String -> Fail a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Either String a
forall a b. a -> Either a b
Left

runFail_ :: Fail a -> a
runFail_ :: forall a. Fail a -> a
runFail_ = (String -> a) -> (a -> a) -> Either String a -> a
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either String -> a
forall a. HasCallStack => String -> a
error a -> a
forall a. a -> a
id (Either String a -> a)
-> (Fail a -> Either String a) -> Fail a -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Fail a -> Either String a
forall a. Fail a -> Either String a
runFail