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

    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
    $cfmap :: forall a b. (a -> b) -> Fail a -> Fail b
    fmap :: forall a b. (a -> b) -> Fail a -> Fail b
    $c<$ :: forall a b. a -> Fail b -> Fail a
    <$ :: forall a b. a -> Fail b -> Fail a
    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
    $cpure :: forall a. a -> Fail a
    pure :: forall a. a -> Fail a
    $c<*> :: forall a b. Fail (a -> b) -> Fail a -> Fail b
    <*> :: forall a b. Fail (a -> b) -> Fail a -> Fail b
    $cliftA2 :: forall a b c. (a -> b -> c) -> Fail a -> Fail b -> Fail c
    liftA2 :: forall a b c. (a -> b -> c) -> Fail a -> Fail b -> Fail c
    $c*> :: forall a b. Fail a -> Fail b -> Fail b
    *> :: forall a b. Fail a -> Fail b -> Fail b
    $c<* :: forall a b. Fail a -> Fail b -> Fail a
    <* :: forall a b. Fail a -> Fail b -> 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
    $c>>= :: forall a b. Fail a -> (a -> Fail b) -> Fail b
    >>= :: forall a b. Fail a -> (a -> Fail b) -> Fail b
    $c>> :: forall a b. Fail a -> Fail b -> Fail b
    >> :: forall a b. Fail a -> Fail b -> Fail b
    $creturn :: forall a. a -> Fail a
    return :: forall a. a -> Fail a
    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