    {-# OPTIONS_GHC -Wunused-imports #-}

    -- | Generic traversal and reduce for concrete syntax,
    --   in the style of "Agda.Syntax.Internal.Generic".
    --
    --   However, here we use the terminology of 'Data.Traversable'.

    module Agda.Syntax.Concrete.Generic where

    import Data.Bifunctor
    import Data.Functor

    import Agda.Syntax.Common
    import Agda.Syntax.Concrete

    import Agda.Utils.Either
    import Agda.Utils.List1 (List1)
    import Agda.Utils.List2 (List2)

    import Agda.Utils.Impossible

    -- Generic traversals for concrete expressions.
    -- ========================================================================

    -- | Generic traversals for concrete expressions.
    --
    --   Note: does not go into patterns!
    class ExprLike a where
      mapExpr :: (Expr -> Expr) -> a -> a
      -- ^ This corresponds to 'map'.

      foldExpr :: Monoid m => (Expr -> m) -> a -> m
      -- ^ This corresponds to 'foldMap'.

      traverseExpr :: Monad m => (Expr -> m Expr) -> a -> m a
      -- ^ This corresponds to 'mapM'.

      default mapExpr :: (Functor t, ExprLike b, t b ~ a) => (Expr -> Expr) -> a -> a
      mapExpr = (b -> b) -> a -> a
    (b -> b) -> t b -> t b
    forall a b. (a -> b) -> t a -> t b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap ((b -> b) -> a -> a)
    -> ((Expr -> Expr) -> b -> b) -> (Expr -> Expr) -> a -> a
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Expr -> Expr) -> b -> b
    forall a. ExprLike a => (Expr -> Expr) -> a -> a
    mapExpr

      default foldExpr
        :: (Monoid m, Foldable t, ExprLike b, t b ~ a)
        => (Expr -> m) -> a -> m
      foldExpr = (b -> m) -> a -> m
    (b -> m) -> t b -> m
    forall m a. Monoid m => (a -> m) -> t a -> m
    forall (t :: * -> *) m a.
    (Foldable t, Monoid m) =>
    (a -> m) -> t a -> m
    foldMap ((b -> m) -> a -> m)
    -> ((Expr -> m) -> b -> m) -> (Expr -> m) -> a -> m
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Expr -> m) -> b -> m
    forall m. Monoid m => (Expr -> m) -> b -> m
    forall a m. (ExprLike a, Monoid m) => (Expr -> m) -> a -> m
    foldExpr

      default traverseExpr
        :: (Monad m, Traversable t, ExprLike b, t b ~ a)
        => (Expr -> m Expr) -> a -> m a
      traverseExpr = (b -> m b) -> a -> m a
    (b -> m b) -> t b -> m (t b)
    forall (t :: * -> *) (f :: * -> *) a b.
    (Traversable t, Applicative f) =>
    (a -> f b) -> t a -> f (t b)
    forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> t a -> f (t b)
    traverse ((b -> m b) -> a -> m a)
    -> ((Expr -> m Expr) -> b -> m b) -> (Expr -> m Expr) -> a -> m a
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Expr -> m Expr) -> b -> m b
    forall a (m :: * -> *).
    (ExprLike a, Monad m) =>
    (Expr -> m Expr) -> a -> m a
    forall (m :: * -> *). Monad m => (Expr -> m Expr) -> b -> m b
    traverseExpr

    -- Instances for things that do not contain expressions.
    ---------------------------------------------------------------------------

    instance ExprLike () where
      mapExpr :: (Expr -> Expr) -> () -> ()
    mapExpr Expr -> Expr
    _      = () -> ()
    forall a. a -> a
    id
      foldExpr :: forall m. Monoid m => (Expr -> m) -> () -> m
    foldExpr Expr -> m
    _ ()
    _   = m
    forall a. Monoid a => a
    mempty
      traverseExpr :: forall (m :: * -> *). Monad m => (Expr -> m Expr) -> () -> m ()
    traverseExpr Expr -> m Expr
    _ = () -> m ()
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return

    instance ExprLike Name where
      mapExpr :: (Expr -> Expr) -> Name -> Name
    mapExpr Expr -> Expr
    _      = Name -> Name
    forall a. a -> a
    id
      foldExpr :: forall m. Monoid m => (Expr -> m) -> Name -> m
    foldExpr Expr -> m
    _ Name
    _   = m
    forall a. Monoid a => a
    mempty
      traverseExpr :: forall (m :: * -> *). Monad m => (Expr -> m Expr) -> Name -> m Name
    traverseExpr Expr -> m Expr
    _ = Name -> m Name
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return

    instance ExprLike QName where
      mapExpr :: (Expr -> Expr) -> QName -> QName
    mapExpr Expr -> Expr
    _      = QName -> QName
    forall a. a -> a
    id
      foldExpr :: forall m. Monoid m => (Expr -> m) -> QName -> m
    foldExpr Expr -> m
    _ QName
    _   = m
    forall a. Monoid a => a
    mempty
      traverseExpr :: forall (m :: * -> *).
    Monad m =>
    (Expr -> m Expr) -> QName -> m QName
    traverseExpr Expr -> m Expr
    _ = QName -> m QName
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return

    instance ExprLike Bool where
      mapExpr :: (Expr -> Expr) -> Bool -> Bool
    mapExpr Expr -> Expr
    _      = Bool -> Bool
    forall a. a -> a
    id
      foldExpr :: forall m. Monoid m => (Expr -> m) -> Bool -> m
    foldExpr Expr -> m
    _ Bool
    _   = m
    forall a. Monoid a => a
    mempty
      traverseExpr :: forall (m :: * -> *). Monad m => (Expr -> m Expr) -> Bool -> m Bool
    traverseExpr Expr -> m Expr
    _ = Bool -> m Bool
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return

    -- Instances for collections and decorations.
    ---------------------------------------------------------------------------

    instance ExprLike a => ExprLike [a]
    instance ExprLike a => ExprLike (List1 a)
    instance ExprLike a => ExprLike (List2 a)
    instance ExprLike a => ExprLike (Maybe a)

    instance ExprLike a => ExprLike (Arg a)
    instance ExprLike a => ExprLike (Named name a)
    instance ExprLike a => ExprLike (Ranged a)
    instance ExprLike a => ExprLike (WithHiding a)

    instance ExprLike a => ExprLike (MaybePlaceholder a)
    instance ExprLike a => ExprLike (RHS' a)
    instance ExprLike a => ExprLike (TacticAttribute' a)
    instance ExprLike a => ExprLike (TypedBinding' a)
    instance ExprLike a => ExprLike (WhereClause' a)

    instance (ExprLike a, ExprLike b) => ExprLike (Either a b) where
      mapExpr :: (Expr -> Expr) -> Either a b -> Either a b
    mapExpr Expr -> Expr
    f      = (a -> a) -> (b -> b) -> Either a b -> Either a b
    forall a b c d. (a -> b) -> (c -> d) -> Either a c -> Either b d
    forall (p :: * -> * -> *) a b c d.
    Bifunctor p =>
    (a -> b) -> (c -> d) -> p a c -> p b d
    bimap ((Expr -> Expr) -> a -> a
    forall a. ExprLike a => (Expr -> Expr) -> a -> a
    mapExpr Expr -> Expr
    f) ((Expr -> Expr) -> b -> b
    forall a. ExprLike a => (Expr -> Expr) -> a -> a
    mapExpr Expr -> Expr
    f)
      traverseExpr :: forall (m :: * -> *).
    Monad m =>
    (Expr -> m Expr) -> Either a b -> m (Either a b)
    traverseExpr Expr -> m Expr
    f = (a -> m a) -> (b -> m b) -> Either a b -> m (Either a b)
    forall (f :: * -> *) a c b d.
    Functor f =>
    (a -> f c) -> (b -> f d) -> Either a b -> f (Either c d)
    traverseEither ((Expr -> m Expr) -> a -> m a
    forall a (m :: * -> *).
    (ExprLike a, Monad m) =>
    (Expr -> m Expr) -> a -> m a
    forall (m :: * -> *). Monad m => (Expr -> m Expr) -> a -> m a
    traverseExpr Expr -> m Expr
    f) ((Expr -> m Expr) -> b -> m b
    forall a (m :: * -> *).
    (ExprLike a, Monad m) =>
    (Expr -> m Expr) -> a -> m a
    forall (m :: * -> *). Monad m => (Expr -> m Expr) -> b -> m b
    traverseExpr Expr -> m Expr
    f)
      foldExpr :: forall m. Monoid m => (Expr -> m) -> Either a b -> m
    foldExpr Expr -> m
    f     = (a -> m) -> (b -> m) -> Either a b -> m
    forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
    either ((Expr -> m) -> a -> m
    forall m. Monoid m => (Expr -> m) -> a -> m
    forall a m. (ExprLike a, Monoid m) => (Expr -> m) -> a -> m
    foldExpr Expr -> m
    f) ((Expr -> m) -> b -> m
    forall m. Monoid m => (Expr -> m) -> b -> m
    forall a m. (ExprLike a, Monoid m) => (Expr -> m) -> a -> m
    foldExpr Expr -> m
    f)

    instance (ExprLike a, ExprLike b) => ExprLike (a, b) where
      mapExpr :: (Expr -> Expr) -> (a, b) -> (a, b)
    mapExpr      Expr -> Expr
    f (a
    x, b
    y) = ((Expr -> Expr) -> a -> a
    forall a. ExprLike a => (Expr -> Expr) -> a -> a
    mapExpr Expr -> Expr
    f a
    x, (Expr -> Expr) -> b -> b
    forall a. ExprLike a => (Expr -> Expr) -> a -> a
    mapExpr Expr -> Expr
    f b
    y)
      traverseExpr :: forall (m :: * -> *).
    Monad m =>
    (Expr -> m Expr) -> (a, b) -> m (a, b)
    traverseExpr Expr -> m Expr
    f (a
    x, b
    y) = (,) (a -> b -> (a, b)) -> m a -> m (b -> (a, b))
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (Expr -> m Expr) -> a -> m a
    forall a (m :: * -> *).
    (ExprLike a, Monad m) =>
    (Expr -> m Expr) -> a -> m a
    forall (m :: * -> *). Monad m => (Expr -> m Expr) -> a -> m a
    traverseExpr Expr -> m Expr
    f a
    x m (b -> (a, b)) -> m b -> m (a, b)
    forall a b. m (a -> b) -> m a -> m b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> (Expr -> m Expr) -> b -> m b
    forall a (m :: * -> *).
    (ExprLike a, Monad m) =>
    (Expr -> m Expr) -> a -> m a
    forall (m :: * -> *). Monad m => (Expr -> m Expr) -> b -> m b
    traverseExpr Expr -> m Expr
    f b
    y
      foldExpr :: forall m. Monoid m => (Expr -> m) -> (a, b) -> m
    foldExpr     Expr -> m
    f (a
    x, b
    y) = (Expr -> m) -> a -> m
    forall m. Monoid m => (Expr -> m) -> a -> m
    forall a m. (ExprLike a, Monoid m) => (Expr -> m) -> a -> m
    foldExpr Expr -> m
    f a
    x m -> m -> m
    forall a. Monoid a => a -> a -> a
    `mappend` (Expr -> m) -> b -> m
    forall m. Monoid m => (Expr -> m) -> b -> m
    forall a m. (ExprLike a, Monoid m) => (Expr -> m) -> a -> m
    foldExpr Expr -> m
    f b
    y

    instance (ExprLike a, ExprLike b, ExprLike c) => ExprLike (a, b, c) where
      mapExpr :: (Expr -> Expr) -> (a, b, c) -> (a, b, c)
    mapExpr      Expr -> Expr
    f (a
    x, b
    y, c
    z) = ((Expr -> Expr) -> a -> a
    forall a. ExprLike a => (Expr -> Expr) -> a -> a
    mapExpr Expr -> Expr
    f a
    x, (Expr -> Expr) -> b -> b
    forall a. ExprLike a => (Expr -> Expr) -> a -> a
    mapExpr Expr -> Expr
    f b
    y, (Expr -> Expr) -> c -> c
    forall a. ExprLike a => (Expr -> Expr) -> a -> a
    mapExpr Expr -> Expr
    f c
    z)
      traverseExpr :: forall (m :: * -> *).
    Monad m =>
    (Expr -> m Expr) -> (a, b, c) -> m (a, b, c)
    traverseExpr Expr -> m Expr
    f (a
    x, b
    y, c
    z) = (,,) (a -> b -> c -> (a, b, c)) -> m a -> m (b -> c -> (a, b, c))
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (Expr -> m Expr) -> a -> m a
    forall a (m :: * -> *).
    (ExprLike a, Monad m) =>
    (Expr -> m Expr) -> a -> m a
    forall (m :: * -> *). Monad m => (Expr -> m Expr) -> a -> m a
    traverseExpr Expr -> m Expr
    f a
    x m (b -> c -> (a, b, c)) -> m b -> m (c -> (a, b, c))
    forall a b. m (a -> b) -> m a -> m b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> (Expr -> m Expr) -> b -> m b
    forall a (m :: * -> *).
    (ExprLike a, Monad m) =>
    (Expr -> m Expr) -> a -> m a
    forall (m :: * -> *). Monad m => (Expr -> m Expr) -> b -> m b
    traverseExpr Expr -> m Expr
    f b
    y m (c -> (a, b, c)) -> m c -> m (a, b, c)
    forall a b. m (a -> b) -> m a -> m b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> (Expr -> m Expr) -> c -> m c
    forall a (m :: * -> *).
    (ExprLike a, Monad m) =>
    (Expr -> m Expr) -> a -> m a
    forall (m :: * -> *). Monad m => (Expr -> m Expr) -> c -> m c
    traverseExpr Expr -> m Expr
    f c
    z
      foldExpr :: forall m. Monoid m => (Expr -> m) -> (a, b, c) -> m
    foldExpr     Expr -> m
    f (a
    x, b
    y, c
    z) = (Expr -> m) -> a -> m
    forall m. Monoid m => (Expr -> m) -> a -> m
    forall a m. (ExprLike a, Monoid m) => (Expr -> m) -> a -> m
    foldExpr Expr -> m
    f a
    x m -> m -> m
    forall a. Monoid a => a -> a -> a
    `mappend` (Expr -> m) -> b -> m
    forall m. Monoid m => (Expr -> m) -> b -> m
    forall a m. (ExprLike a, Monoid m) => (Expr -> m) -> a -> m
    foldExpr Expr -> m
    f b
    y m -> m -> m
    forall a. Monoid a => a -> a -> a
    `mappend` (Expr -> m) -> c -> m
    forall m. Monoid m => (Expr -> m) -> c -> m
    forall a m. (ExprLike a, Monoid m) => (Expr -> m) -> a -> m
    foldExpr Expr -> m
    f c
    z

    instance (ExprLike a, ExprLike b, ExprLike c, ExprLike d) => ExprLike (a, b, c, d) where
      mapExpr :: (Expr -> Expr) -> (a, b, c, d) -> (a, b, c, d)
    mapExpr      Expr -> Expr
    f (a
    x, b
    y, c
    z, d
    w) = ((Expr -> Expr) -> a -> a
    forall a. ExprLike a => (Expr -> Expr) -> a -> a
    mapExpr Expr -> Expr
    f a
    x, (Expr -> Expr) -> b -> b
    forall a. ExprLike a => (Expr -> Expr) -> a -> a
    mapExpr Expr -> Expr
    f b
    y, (Expr -> Expr) -> c -> c
    forall a. ExprLike a => (Expr -> Expr) -> a -> a
    mapExpr Expr -> Expr
    f c
    z, (Expr -> Expr) -> d -> d
    forall a. ExprLike a => (Expr -> Expr) -> a -> a
    mapExpr Expr -> Expr
    f d
    w)
      traverseExpr :: forall (m :: * -> *).
    Monad m =>
    (Expr -> m Expr) -> (a, b, c, d) -> m (a, b, c, d)
    traverseExpr Expr -> m Expr
    f (a
    x, b
    y, c
    z, d
    w) = (,,,) (a -> b -> c -> d -> (a, b, c, d))
    -> m a -> m (b -> c -> d -> (a, b, c, d))
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (Expr -> m Expr) -> a -> m a
    forall a (m :: * -> *).
    (ExprLike a, Monad m) =>
    (Expr -> m Expr) -> a -> m a
    forall (m :: * -> *). Monad m => (Expr -> m Expr) -> a -> m a
    traverseExpr Expr -> m Expr
    f a
    x m (b -> c -> d -> (a, b, c, d))
    -> m b -> m (c -> d -> (a, b, c, d))
    forall a b. m (a -> b) -> m a -> m b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> (Expr -> m Expr) -> b -> m b
    forall a (m :: * -> *).
    (ExprLike a, Monad m) =>
    (Expr -> m Expr) -> a -> m a
    forall (m :: * -> *). Monad m => (Expr -> m Expr) -> b -> m b
    traverseExpr Expr -> m Expr
    f b
    y m (c -> d -> (a, b, c, d)) -> m c -> m (d -> (a, b, c, d))
    forall a b. m (a -> b) -> m a -> m b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> (Expr -> m Expr) -> c -> m c
    forall a (m :: * -> *).
    (ExprLike a, Monad m) =>
    (Expr -> m Expr) -> a -> m a
    forall (m :: * -> *). Monad m => (Expr -> m Expr) -> c -> m c
    traverseExpr Expr -> m Expr
    f c
    z m (d -> (a, b, c, d)) -> m d -> m (a, b, c, d)
    forall a b. m (a -> b) -> m a -> m b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> (Expr -> m Expr) -> d -> m d
    forall a (m :: * -> *).
    (ExprLike a, Monad m) =>
    (Expr -> m Expr) -> a -> m a
    forall (m :: * -> *). Monad m => (Expr -> m Expr) -> d -> m d
    traverseExpr Expr -> m Expr
    f d
    w
      foldExpr :: forall m. Monoid m => (Expr -> m) -> (a, b, c, d) -> m
    foldExpr     Expr -> m
    f (a
    x, b
    y, c
    z, d
    w) = (Expr -> m) -> a -> m
    forall m. Monoid m => (Expr -> m) -> a -> m
    forall a m. (ExprLike a, Monoid m) => (Expr -> m) -> a -> m
    foldExpr Expr -> m
    f a
    x m -> m -> m
    forall a. Monoid a => a -> a -> a
    `mappend` (Expr -> m) -> b -> m
    forall m. Monoid m => (Expr -> m) -> b -> m
    forall a m. (ExprLike a, Monoid m) => (Expr -> m) -> a -> m
    foldExpr Expr -> m
    f b
    y m -> m -> m
    forall a. Monoid a => a -> a -> a
    `mappend` (Expr -> m) -> c -> m
    forall m. Monoid m => (Expr -> m) -> c -> m
    forall a m. (ExprLike a, Monoid m) => (Expr -> m) -> a -> m
    foldExpr Expr -> m
    f c
    z m -> m -> m
    forall a. Monoid a => a -> a -> a
    `mappend` (Expr -> m) -> d -> m
    forall m. Monoid m => (Expr -> m) -> d -> m
    forall a m. (ExprLike a, Monoid m) => (Expr -> m) -> a -> m
    foldExpr Expr -> m
    f d
    w

    -- Interesting instances
    ---------------------------------------------------------------------------

    instance ExprLike Expr where
      mapExpr :: (Expr -> Expr) -> Expr -> Expr
    mapExpr Expr -> Expr
    f Expr
    e0 = case Expr
    e0 of
         Ident{}                 -> Expr -> Expr
    f (Expr -> Expr) -> Expr -> Expr
    forall a b. (a -> b) -> a -> b
    $ Expr
    e0
         Lit{}                   -> Expr -> Expr
    f (Expr -> Expr) -> Expr -> Expr
    forall a b. (a -> b) -> a -> b
    $ Expr
    e0
         QuestionMark{}          -> Expr -> Expr
    f (Expr -> Expr) -> Expr -> Expr
    forall a b. (a -> b) -> a -> b
    $ Expr
    e0
         Underscore{}            -> Expr -> Expr
    f (Expr -> Expr) -> Expr -> Expr
    forall a b. (a -> b) -> a -> b
    $ Expr
    e0
         RawApp Range
    r List2 Expr
    es             -> Expr -> Expr
    f (Expr -> Expr) -> Expr -> Expr
    forall a b. (a -> b) -> a -> b
    $ Range -> List2 Expr -> Expr
    RawApp Range
    r               (List2 Expr -> Expr) -> List2 Expr -> Expr
    forall a b. (a -> b) -> a -> b
    $ List2 Expr -> List2 Expr
    forall e. ExprLike e => e -> e
    mapE List2 Expr
    es
         App Range
    r Expr
    e NamedArg Expr
    es              -> Expr -> Expr
    f (Expr -> Expr) -> Expr -> Expr
    forall a b. (a -> b) -> a -> b
    $ Range -> Expr -> NamedArg Expr -> Expr
    App Range
    r       (Expr -> Expr
    forall e. ExprLike e => e -> e
    mapE Expr
    e)   (NamedArg Expr -> Expr) -> NamedArg Expr -> Expr
    forall a b. (a -> b) -> a -> b
    $ NamedArg Expr -> NamedArg Expr
    forall e. ExprLike e => e -> e
    mapE NamedArg Expr
    es
         OpApp Range
    r QName
    q Set1 Name
    ns OpAppArgs
    es         -> Expr -> Expr
    f (Expr -> Expr) -> Expr -> Expr
    forall a b. (a -> b) -> a -> b
    $ Range -> QName -> Set1 Name -> OpAppArgs -> Expr
    OpApp Range
    r QName
    q Set1 Name
    ns           (OpAppArgs -> Expr) -> OpAppArgs -> Expr
    forall a b. (a -> b) -> a -> b
    $ OpAppArgs -> OpAppArgs
    forall e. ExprLike e => e -> e
    mapE OpAppArgs
    es
         WithApp Range
    r Expr
    e List1 Expr
    es          -> Expr -> Expr
    f (Expr -> Expr) -> Expr -> Expr
    forall a b. (a -> b) -> a -> b
    $ Range -> Expr -> List1 Expr -> Expr
    WithApp Range
    r   (Expr -> Expr
    forall e. ExprLike e => e -> e
    mapE Expr
    e)   (List1 Expr -> Expr) -> List1 Expr -> Expr
    forall a b. (a -> b) -> a -> b
    $ List1 Expr -> List1 Expr
    forall e. ExprLike e => e -> e
    mapE List1 Expr
    es
         HiddenArg Range
    r Named_ Expr
    e           -> Expr -> Expr
    f (Expr -> Expr) -> Expr -> Expr
    forall a b. (a -> b) -> a -> b
    $ Range -> Named_ Expr -> Expr
    HiddenArg Range
    r            (Named_ Expr -> Expr) -> Named_ Expr -> Expr
    forall a b. (a -> b) -> a -> b
    $ Named_ Expr -> Named_ Expr
    forall e. ExprLike e => e -> e
    mapE Named_ Expr
    e
         InstanceArg Range
    r Named_ Expr
    e         -> Expr -> Expr
    f (Expr -> Expr) -> Expr -> Expr
    forall a b. (a -> b) -> a -> b
    $ Range -> Named_ Expr -> Expr
    InstanceArg Range
    r          (Named_ Expr -> Expr) -> Named_ Expr -> Expr
    forall a b. (a -> b) -> a -> b
    $ Named_ Expr -> Named_ Expr
    forall e. ExprLike e => e -> e
    mapE Named_ Expr
    e
         Lam Range
    r List1 LamBinding
    bs Expr
    e              -> Expr -> Expr
    f (Expr -> Expr) -> Expr -> Expr
    forall a b. (a -> b) -> a -> b
    $ Range -> List1 LamBinding -> Expr -> Expr
    Lam Range
    r       (List1 LamBinding -> List1 LamBinding
    forall e. ExprLike e => e -> e
    mapE List1 LamBinding
    bs)  (Expr -> Expr) -> Expr -> Expr
    forall a b. (a -> b) -> a -> b
    $ Expr -> Expr
    forall e. ExprLike e => e -> e
    mapE Expr
    e
         AbsurdLam{}             -> Expr -> Expr
    f (Expr -> Expr) -> Expr -> Expr
    forall a b. (a -> b) -> a -> b
    $ Expr
    e0
         ExtendedLam Range
    r Erased
    e List1 LamClause
    cs      -> Expr -> Expr
    f (Expr -> Expr) -> Expr -> Expr
    forall a b. (a -> b) -> a -> b
    $ Range -> Erased -> List1 LamClause -> Expr
    ExtendedLam Range
    r Erased
    e        (List1 LamClause -> Expr) -> List1 LamClause -> Expr
    forall a b. (a -> b) -> a -> b
    $ List1 LamClause -> List1 LamClause
    forall e. ExprLike e => e -> e
    mapE List1 LamClause
    cs
         Fun Range
    r Arg Expr
    a Expr
    b               -> Expr -> Expr
    f (Expr -> Expr) -> Expr -> Expr
    forall a b. (a -> b) -> a -> b
    $ Range -> Arg Expr -> Expr -> Expr
    Fun Range
    r     (Expr -> Expr
    forall e. ExprLike e => e -> e
    mapE (Expr -> Expr) -> Arg Expr -> Arg Expr
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Arg Expr
    a) (Expr -> Expr) -> Expr -> Expr
    forall a b. (a -> b) -> a -> b
    $ Expr -> Expr
    forall e. ExprLike e => e -> e
    mapE Expr
    b
         Pi Telescope1
    tel Expr
    e                -> Expr -> Expr
    f (Expr -> Expr) -> Expr -> Expr
    forall a b. (a -> b) -> a -> b
    $ Telescope1 -> Expr -> Expr
    Pi          (Telescope1 -> Telescope1
    forall e. ExprLike e => e -> e
    mapE Telescope1
    tel) (Expr -> Expr) -> Expr -> Expr
    forall a b. (a -> b) -> a -> b
    $ Expr -> Expr
    forall e. ExprLike e => e -> e
    mapE Expr
    e
         Rec KwRange
    kwr Range
    r RecordAssignments
    es            -> Expr -> Expr
    f (Expr -> Expr) -> Expr -> Expr
    forall a b. (a -> b) -> a -> b
    $ KwRange -> Range -> RecordAssignments -> Expr
    Rec KwRange
    kwr Range
    r              (RecordAssignments -> Expr) -> RecordAssignments -> Expr
    forall a b. (a -> b) -> a -> b
    $ RecordAssignments -> RecordAssignments
    forall e. ExprLike e => e -> e
    mapE RecordAssignments
    es
         RecUpdate KwRange
    kwr Range
    r Expr
    e [FieldAssignment]
    es    -> Expr -> Expr
    f (Expr -> Expr) -> Expr -> Expr
    forall a b. (a -> b) -> a -> b
    $ KwRange -> Range -> Expr -> [FieldAssignment] -> Expr
    RecUpdate KwRange
    kwr Range
    r (Expr -> Expr
    forall e. ExprLike e => e -> e
    mapE Expr
    e) ([FieldAssignment] -> Expr) -> [FieldAssignment] -> Expr
    forall a b. (a -> b) -> a -> b
    $ [FieldAssignment] -> [FieldAssignment]
    forall e. ExprLike e => e -> e
    mapE [FieldAssignment]
    es
         Let Range
    r List1 Declaration
    ds Maybe Expr
    e              -> Expr -> Expr
    f (Expr -> Expr) -> Expr -> Expr
    forall a b. (a -> b) -> a -> b
    $ Range -> List1 Declaration -> Maybe Expr -> Expr
    Let Range
    r       (List1 Declaration -> List1 Declaration
    forall e. ExprLike e => e -> e
    mapE List1 Declaration
    ds)  (Maybe Expr -> Expr) -> Maybe Expr -> Expr
    forall a b. (a -> b) -> a -> b
    $ Maybe Expr -> Maybe Expr
    forall e. ExprLike e => e -> e
    mapE Maybe Expr
    e
         Paren Range
    r Expr
    e               -> Expr -> Expr
    f (Expr -> Expr) -> Expr -> Expr
    forall a b. (a -> b) -> a -> b
    $ Range -> Expr -> Expr
    Paren Range
    r                (Expr -> Expr) -> Expr -> Expr
    forall a b. (a -> b) -> a -> b
    $ Expr -> Expr
    forall e. ExprLike e => e -> e
    mapE Expr
    e
         IdiomBrackets Range
    r [Expr]
    es      -> Expr -> Expr
    f (Expr -> Expr) -> Expr -> Expr
    forall a b. (a -> b) -> a -> b
    $ Range -> [Expr] -> Expr
    IdiomBrackets Range
    r        ([Expr] -> Expr) -> [Expr] -> Expr
    forall a b. (a -> b) -> a -> b
    $ [Expr] -> [Expr]
    forall e. ExprLike e => e -> e
    mapE [Expr]
    es
         DoBlock Range
    r List1 DoStmt
    ss            -> Expr -> Expr
    f (Expr -> Expr) -> Expr -> Expr
    forall a b. (a -> b) -> a -> b
    $ Range -> List1 DoStmt -> Expr
    DoBlock Range
    r              (List1 DoStmt -> Expr) -> List1 DoStmt -> Expr
    forall a b. (a -> b) -> a -> b
    $ List1 DoStmt -> List1 DoStmt
    forall e. ExprLike e => e -> e
    mapE List1 DoStmt
    ss
         Absurd{}                -> Expr -> Expr
    f (Expr -> Expr) -> Expr -> Expr
    forall a b. (a -> b) -> a -> b
    $ Expr
    e0
         As Range
    r Name
    x Expr
    e                -> Expr -> Expr
    f (Expr -> Expr) -> Expr -> Expr
    forall a b. (a -> b) -> a -> b
    $ Range -> Name -> Expr -> Expr
    As Range
    r Name
    x                 (Expr -> Expr) -> Expr -> Expr
    forall a b. (a -> b) -> a -> b
    $ Expr -> Expr
    forall e. ExprLike e => e -> e
    mapE Expr
    e
         Dot KwRange
    r Expr
    e                 -> Expr -> Expr
    f (Expr -> Expr) -> Expr -> Expr
    forall a b. (a -> b) -> a -> b
    $ KwRange -> Expr -> Expr
    Dot KwRange
    r                  (Expr -> Expr) -> Expr -> Expr
    forall a b. (a -> b) -> a -> b
    $ Expr -> Expr
    forall e. ExprLike e => e -> e
    mapE Expr
    e
         DoubleDot KwRange
    r Expr
    e           -> Expr -> Expr
    f (Expr -> Expr) -> Expr -> Expr
    forall a b. (a -> b) -> a -> b
    $ KwRange -> Expr -> Expr
    DoubleDot KwRange
    r            (Expr -> Expr) -> Expr -> Expr
    forall a b. (a -> b) -> a -> b
    $ Expr -> Expr
    forall e. ExprLike e => e -> e
    mapE Expr
    e
         Tactic Range
    r Expr
    e              -> Expr -> Expr
    f (Expr -> Expr) -> Expr -> Expr
    forall a b. (a -> b) -> a -> b
    $ Range -> Expr -> Expr
    Tactic Range
    r     (Expr -> Expr
    forall e. ExprLike e => e -> e
    mapE Expr
    e)
         Quote{}                 -> Expr -> Expr
    f (Expr -> Expr) -> Expr -> Expr
    forall a b. (a -> b) -> a -> b
    $ Expr
    e0
         QuoteTerm{}             -> Expr -> Expr
    f (Expr -> Expr) -> Expr -> Expr
    forall a b. (a -> b) -> a -> b
    $ Expr
    e0
         Unquote{}               -> Expr -> Expr
    f (Expr -> Expr) -> Expr -> Expr
    forall a b. (a -> b) -> a -> b
    $ Expr
    e0
         DontCare Expr
    e              -> Expr -> Expr
    f (Expr -> Expr) -> Expr -> Expr
    forall a b. (a -> b) -> a -> b
    $ Expr -> Expr
    DontCare               (Expr -> Expr) -> Expr -> Expr
    forall a b. (a -> b) -> a -> b
    $ Expr -> Expr
    forall e. ExprLike e => e -> e
    mapE Expr
    e
         Equal{}                 -> Expr -> Expr
    f (Expr -> Expr) -> Expr -> Expr
    forall a b. (a -> b) -> a -> b
    $ Expr
    e0
         Ellipsis{}              -> Expr -> Expr
    f (Expr -> Expr) -> Expr -> Expr
    forall a b. (a -> b) -> a -> b
    $ Expr
    e0
         Generalized Expr
    e           -> Expr -> Expr
    f (Expr -> Expr) -> Expr -> Expr
    forall a b. (a -> b) -> a -> b
    $ Expr -> Expr
    Generalized            (Expr -> Expr) -> Expr -> Expr
    forall a b. (a -> b) -> a -> b
    $ Expr -> Expr
    forall e. ExprLike e => e -> e
    mapE Expr
    e
         KnownIdent{}            -> Expr -> Expr
    f (Expr -> Expr) -> Expr -> Expr
    forall a b. (a -> b) -> a -> b
    $ Expr
    e0
         KnownOpApp NameKind
    nk Range
    r QName
    q Set1 Name
    ns OpAppArgs
    es -> Expr -> Expr
    f (Expr -> Expr) -> Expr -> Expr
    forall a b. (a -> b) -> a -> b
    $ NameKind -> Range -> QName -> Set1 Name -> OpAppArgs -> Expr
    KnownOpApp NameKind
    nk Range
    r QName
    q Set1 Name
    ns   (OpAppArgs -> Expr) -> OpAppArgs -> Expr
    forall a b. (a -> b) -> a -> b
    $ OpAppArgs -> OpAppArgs
    forall e. ExprLike e => e -> e
    mapE OpAppArgs
    es
       where
         mapE :: ExprLike e => e -> e
         mapE :: forall e. ExprLike e => e -> e
    mapE = (Expr -> Expr) -> e -> e
    forall a. ExprLike a => (Expr -> Expr) -> a -> a
    mapExpr Expr -> Expr
    f

      foldExpr :: forall m. Monoid m => (Expr -> m) -> Expr -> m
    foldExpr     = (Expr -> m) -> Expr -> m
    forall a. HasCallStack => a
    __IMPOSSIBLE__
      traverseExpr :: forall (m :: * -> *). Monad m => (Expr -> m Expr) -> Expr -> m Expr
    traverseExpr = (Expr -> m Expr) -> Expr -> m Expr
    forall a. HasCallStack => a
    __IMPOSSIBLE__

    instance ExprLike FieldAssignment where
      mapExpr :: (Expr -> Expr) -> FieldAssignment -> FieldAssignment
    mapExpr      Expr -> Expr
    f (FieldAssignment Name
    x Expr
    e) = Name -> Expr -> FieldAssignment
    forall a. Name -> a -> FieldAssignment' a
    FieldAssignment Name
    x ((Expr -> Expr) -> Expr -> Expr
    forall a. ExprLike a => (Expr -> Expr) -> a -> a
    mapExpr Expr -> Expr
    f Expr
    e)
      traverseExpr :: forall (m :: * -> *).
    Monad m =>
    (Expr -> m Expr) -> FieldAssignment -> m FieldAssignment
    traverseExpr Expr -> m Expr
    f (FieldAssignment Name
    x Expr
    e) = (\Expr
    e' -> Name -> Expr -> FieldAssignment
    forall a. Name -> a -> FieldAssignment' a
    FieldAssignment Name
    x Expr
    e') (Expr -> FieldAssignment) -> m Expr -> m FieldAssignment
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (Expr -> m Expr) -> Expr -> m Expr
    forall a (m :: * -> *).
    (ExprLike a, Monad m) =>
    (Expr -> m Expr) -> a -> m a
    forall (m :: * -> *). Monad m => (Expr -> m Expr) -> Expr -> m Expr
    traverseExpr Expr -> m Expr
    f Expr
    e
      foldExpr :: forall m. Monoid m => (Expr -> m) -> FieldAssignment -> m
    foldExpr     Expr -> m
    f (FieldAssignment Name
    _ Expr
    e) = (Expr -> m) -> Expr -> m
    forall m. Monoid m => (Expr -> m) -> Expr -> m
    forall a m. (ExprLike a, Monoid m) => (Expr -> m) -> a -> m
    foldExpr Expr -> m
    f Expr
    e

    instance ExprLike ModuleAssignment where
      mapExpr :: (Expr -> Expr) -> ModuleAssignment -> ModuleAssignment
    mapExpr      Expr -> Expr
    f (ModuleAssignment QName
    m [Expr]
    es ImportDirective
    i) = QName -> [Expr] -> ImportDirective -> ModuleAssignment
    ModuleAssignment QName
    m ((Expr -> Expr) -> [Expr] -> [Expr]
    forall a. ExprLike a => (Expr -> Expr) -> a -> a
    mapExpr Expr -> Expr
    f [Expr]
    es) ImportDirective
    i
      traverseExpr :: forall (m :: * -> *).
    Monad m =>
    (Expr -> m Expr) -> ModuleAssignment -> m ModuleAssignment
    traverseExpr Expr -> m Expr
    f (ModuleAssignment QName
    m [Expr]
    es ImportDirective
    i) = (\[Expr]
    es' -> QName -> [Expr] -> ImportDirective -> ModuleAssignment
    ModuleAssignment QName
    m [Expr]
    es' ImportDirective
    i) ([Expr] -> ModuleAssignment) -> m [Expr] -> m ModuleAssignment
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (Expr -> m Expr) -> [Expr] -> m [Expr]
    forall a (m :: * -> *).
    (ExprLike a, Monad m) =>
    (Expr -> m Expr) -> a -> m a
    forall (m :: * -> *).
    Monad m =>
    (Expr -> m Expr) -> [Expr] -> m [Expr]
    traverseExpr Expr -> m Expr
    f [Expr]
    es
      foldExpr :: forall m. Monoid m => (Expr -> m) -> ModuleAssignment -> m
    foldExpr     Expr -> m
    f (ModuleAssignment QName
    m [Expr]
    es ImportDirective
    i) = (Expr -> m) -> [Expr] -> m
    forall m. Monoid m => (Expr -> m) -> [Expr] -> m
    forall a m. (ExprLike a, Monoid m) => (Expr -> m) -> a -> m
    foldExpr Expr -> m
    f [Expr]
    es

    instance ExprLike a => ExprLike (OpApp a) where
      mapExpr :: (Expr -> Expr) -> OpApp a -> OpApp a
    mapExpr Expr -> Expr
    f = \case
         SyntaxBindingLambda Range
    r List1 LamBinding
    bs a
    e -> Range -> List1 LamBinding -> a -> OpApp a
    forall e. Range -> List1 LamBinding -> e -> OpApp e
    SyntaxBindingLambda Range
    r (List1 LamBinding -> List1 LamBinding
    forall e. ExprLike e => e -> e
    mapE List1 LamBinding
    bs) (a -> OpApp a) -> a -> OpApp a
    forall a b. (a -> b) -> a -> b
    $ a -> a
    forall e. ExprLike e => e -> e
    mapE a
    e
         Ordinary                 a
    e -> a -> OpApp a
    forall e. e -> OpApp e
    Ordinary                        (a -> OpApp a) -> a -> OpApp a
    forall a b. (a -> b) -> a -> b
    $ a -> a
    forall e. ExprLike e => e -> e
    mapE a
    e
       where
         mapE :: ExprLike e => e -> e
         mapE :: forall e. ExprLike e => e -> e
    mapE = (Expr -> Expr) -> e -> e
    forall a. ExprLike a => (Expr -> Expr) -> a -> a
    mapExpr Expr -> Expr
    f
      foldExpr :: forall m. Monoid m => (Expr -> m) -> OpApp a -> m
    foldExpr     = (Expr -> m) -> OpApp a -> m
    forall a. HasCallStack => a
    __IMPOSSIBLE__
      traverseExpr :: forall (m :: * -> *).
    Monad m =>
    (Expr -> m Expr) -> OpApp a -> m (OpApp a)
    traverseExpr = (Expr -> m Expr) -> OpApp a -> m (OpApp a)
    forall a. HasCallStack => a
    __IMPOSSIBLE__

    instance ExprLike LamBinding where
      mapExpr :: (Expr -> Expr) -> LamBinding -> LamBinding
    mapExpr Expr -> Expr
    f = \case
         e :: LamBinding
    e@DomainFree{}-> LamBinding
    e
         DomainFull TypedBinding' Expr
    bs -> TypedBinding' Expr -> LamBinding
    forall a. a -> LamBinding' a
    DomainFull (TypedBinding' Expr -> LamBinding)
    -> TypedBinding' Expr -> LamBinding
    forall a b. (a -> b) -> a -> b
    $ TypedBinding' Expr -> TypedBinding' Expr
    mapE TypedBinding' Expr
    bs
       where mapE :: TypedBinding' Expr -> TypedBinding' Expr
    mapE TypedBinding' Expr
    e = (Expr -> Expr) -> TypedBinding' Expr -> TypedBinding' Expr
    forall a. ExprLike a => (Expr -> Expr) -> a -> a
    mapExpr Expr -> Expr
    f TypedBinding' Expr
    e
      foldExpr :: forall m. Monoid m => (Expr -> m) -> LamBinding -> m
    foldExpr     = (Expr -> m) -> LamBinding -> m
    forall a. HasCallStack => a
    __IMPOSSIBLE__
      traverseExpr :: forall (m :: * -> *).
    Monad m =>
    (Expr -> m Expr) -> LamBinding -> m LamBinding
    traverseExpr = (Expr -> m Expr) -> LamBinding -> m LamBinding
    forall a. HasCallStack => a
    __IMPOSSIBLE__

    instance ExprLike LHS where
      mapExpr :: (Expr -> Expr) -> LHS -> LHS
    mapExpr Expr -> Expr
    f = \case
         LHS Pattern
    ps [RewriteEqn]
    res [WithExpr]
    wes -> Pattern -> [RewriteEqn] -> [WithExpr] -> LHS
    LHS Pattern
    ps ([RewriteEqn] -> [RewriteEqn]
    forall e. ExprLike e => e -> e
    mapE [RewriteEqn]
    res) ([WithExpr] -> [WithExpr]
    forall e. ExprLike e => e -> e
    mapE [WithExpr]
    wes)
       where
         mapE :: ExprLike a => a -> a
         mapE :: forall e. ExprLike e => e -> e
    mapE = (Expr -> Expr) -> a -> a
    forall a. ExprLike a => (Expr -> Expr) -> a -> a
    mapExpr Expr -> Expr
    f
      foldExpr :: forall m. Monoid m => (Expr -> m) -> LHS -> m
    foldExpr     = (Expr -> m) -> LHS -> m
    forall a. HasCallStack => a
    __IMPOSSIBLE__
      traverseExpr :: forall (m :: * -> *). Monad m => (Expr -> m Expr) -> LHS -> m LHS
    traverseExpr = (Expr -> m Expr) -> LHS -> m LHS
    forall a. HasCallStack => a
    __IMPOSSIBLE__

    instance (ExprLike qn, ExprLike e) => ExprLike (RewriteEqn' qn nm p e) where
      mapExpr :: (Expr -> Expr) -> RewriteEqn' qn nm p e -> RewriteEqn' qn nm p e
    mapExpr Expr -> Expr
    f = \case
        Rewrite List1 (qn, e)
    es    -> List1 (qn, e) -> RewriteEqn' qn nm p e
    forall qn nm p e. List1 (qn, e) -> RewriteEqn' qn nm p e
    Rewrite ((Expr -> Expr) -> List1 (qn, e) -> List1 (qn, e)
    forall a. ExprLike a => (Expr -> Expr) -> a -> a
    mapExpr Expr -> Expr
    f List1 (qn, e)
    es)
        Invert qn
    qn List1 (Named nm (p, e))
    pes -> qn -> List1 (Named nm (p, e)) -> RewriteEqn' qn nm p e
    forall qn nm p e.
    qn -> List1 (Named nm (p, e)) -> RewriteEqn' qn nm p e
    Invert qn
    qn (List1 (Named nm (p, e)) -> RewriteEqn' qn nm p e)
    -> List1 (Named nm (p, e)) -> RewriteEqn' qn nm p e
    forall a b. (a -> b) -> a -> b
    $ ((Named nm (p, e) -> Named nm (p, e))
    -> List1 (Named nm (p, e)) -> List1 (Named nm (p, e))
    forall a b. (a -> b) -> NonEmpty a -> NonEmpty b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap ((Named nm (p, e) -> Named nm (p, e))
     -> List1 (Named nm (p, e)) -> List1 (Named nm (p, e)))
    -> ((Expr -> Expr) -> Named nm (p, e) -> Named nm (p, e))
    -> (Expr -> Expr)
    -> List1 (Named nm (p, e))
    -> List1 (Named nm (p, e))
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ((p, e) -> (p, e)) -> Named nm (p, e) -> Named nm (p, e)
    forall a b. (a -> b) -> Named nm a -> Named nm b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (((p, e) -> (p, e)) -> Named nm (p, e) -> Named nm (p, e))
    -> ((Expr -> Expr) -> (p, e) -> (p, e))
    -> (Expr -> Expr)
    -> Named nm (p, e)
    -> Named nm (p, e)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (e -> e) -> (p, e) -> (p, e)
    forall a b. (a -> b) -> (p, a) -> (p, b)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap ((e -> e) -> (p, e) -> (p, e))
    -> ((Expr -> Expr) -> e -> e) -> (Expr -> Expr) -> (p, e) -> (p, e)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Expr -> Expr) -> e -> e
    forall a. ExprLike a => (Expr -> Expr) -> a -> a
    mapExpr) Expr -> Expr
    f List1 (Named nm (p, e))
    pes
        LeftLet List1 (p, e)
    pes   -> List1 (p, e) -> RewriteEqn' qn nm p e
    forall qn nm p e. List1 (p, e) -> RewriteEqn' qn nm p e
    LeftLet (List1 (p, e) -> RewriteEqn' qn nm p e)
    -> List1 (p, e) -> RewriteEqn' qn nm p e
    forall a b. (a -> b) -> a -> b
    $ (((p, e) -> (p, e)) -> List1 (p, e) -> List1 (p, e)
    forall a b. (a -> b) -> NonEmpty a -> NonEmpty b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (((p, e) -> (p, e)) -> List1 (p, e) -> List1 (p, e))
    -> ((Expr -> Expr) -> (p, e) -> (p, e))
    -> (Expr -> Expr)
    -> List1 (p, e)
    -> List1 (p, e)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (e -> e) -> (p, e) -> (p, e)
    forall a b. (a -> b) -> (p, a) -> (p, b)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap ((e -> e) -> (p, e) -> (p, e))
    -> ((Expr -> Expr) -> e -> e) -> (Expr -> Expr) -> (p, e) -> (p, e)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Expr -> Expr) -> e -> e
    forall a. ExprLike a => (Expr -> Expr) -> a -> a
    mapExpr) Expr -> Expr
    f List1 (p, e)
    pes
      foldExpr :: forall m. Monoid m => (Expr -> m) -> RewriteEqn' qn nm p e -> m
    foldExpr     = (Expr -> m) -> RewriteEqn' qn nm p e -> m
    forall a. HasCallStack => a
    __IMPOSSIBLE__
      traverseExpr :: forall (m :: * -> *).
    Monad m =>
    (Expr -> m Expr)
    -> RewriteEqn' qn nm p e -> m (RewriteEqn' qn nm p e)
    traverseExpr = (Expr -> m Expr)
    -> RewriteEqn' qn nm p e -> m (RewriteEqn' qn nm p e)
    forall a. HasCallStack => a
    __IMPOSSIBLE__

    instance ExprLike LamClause where
      mapExpr :: (Expr -> Expr) -> LamClause -> LamClause
    mapExpr Expr -> Expr
    f (LamClause [Pattern]
    ps RHS
    rhs Catchall
    ca) = [Pattern] -> RHS -> Catchall -> LamClause
    LamClause [Pattern]
    ps ((Expr -> Expr) -> RHS -> RHS
    forall a. ExprLike a => (Expr -> Expr) -> a -> a
    mapExpr Expr -> Expr
    f RHS
    rhs) Catchall
    ca
      foldExpr :: forall m. Monoid m => (Expr -> m) -> LamClause -> m
    foldExpr     = (Expr -> m) -> LamClause -> m
    forall a. HasCallStack => a
    __IMPOSSIBLE__
      traverseExpr :: forall (m :: * -> *).
    Monad m =>
    (Expr -> m Expr) -> LamClause -> m LamClause
    traverseExpr = (Expr -> m Expr) -> LamClause -> m LamClause
    forall a. HasCallStack => a
    __IMPOSSIBLE__

    instance ExprLike DoStmt where
      mapExpr :: (Expr -> Expr) -> DoStmt -> DoStmt
    mapExpr Expr -> Expr
    f (DoBind Range
    r Pattern
    p Expr
    e [LamClause]
    cs) = Range -> Pattern -> Expr -> [LamClause] -> DoStmt
    DoBind Range
    r Pattern
    p ((Expr -> Expr) -> Expr -> Expr
    forall a. ExprLike a => (Expr -> Expr) -> a -> a
    mapExpr Expr -> Expr
    f Expr
    e) ((Expr -> Expr) -> [LamClause] -> [LamClause]
    forall a. ExprLike a => (Expr -> Expr) -> a -> a
    mapExpr Expr -> Expr
    f [LamClause]
    cs)
      mapExpr Expr -> Expr
    f (DoThen Expr
    e)        = Expr -> DoStmt
    DoThen ((Expr -> Expr) -> Expr -> Expr
    forall a. ExprLike a => (Expr -> Expr) -> a -> a
    mapExpr Expr -> Expr
    f Expr
    e)
      mapExpr Expr -> Expr
    f (DoLet Range
    r List1 Declaration
    ds)      = Range -> List1 Declaration -> DoStmt
    DoLet Range
    r ((Expr -> Expr) -> List1 Declaration -> List1 Declaration
    forall a. ExprLike a => (Expr -> Expr) -> a -> a
    mapExpr Expr -> Expr
    f List1 Declaration
    ds)

      foldExpr :: forall m. Monoid m => (Expr -> m) -> DoStmt -> m
    foldExpr     = (Expr -> m) -> DoStmt -> m
    forall a. HasCallStack => a
    __IMPOSSIBLE__
      traverseExpr :: forall (m :: * -> *).
    Monad m =>
    (Expr -> m Expr) -> DoStmt -> m DoStmt
    traverseExpr = (Expr -> m Expr) -> DoStmt -> m DoStmt
    forall a. HasCallStack => a
    __IMPOSSIBLE__

    instance ExprLike ModuleApplication where
      mapExpr :: (Expr -> Expr) -> ModuleApplication -> ModuleApplication
    mapExpr Expr -> Expr
    f = \case
         SectionApp Range
    r Telescope
    bs QName
    x [Expr]
    es -> Range -> Telescope -> QName -> [Expr] -> ModuleApplication
    SectionApp Range
    r (Telescope -> Telescope
    forall e. ExprLike e => e -> e
    mapE Telescope
    bs) QName
    x ([Expr] -> ModuleApplication) -> [Expr] -> ModuleApplication
    forall a b. (a -> b) -> a -> b
    $ [Expr] -> [Expr]
    forall e. ExprLike e => e -> e
    mapE [Expr]
    es
         e :: ModuleApplication
    e@RecordModuleInstance{} -> ModuleApplication
    e
       where
         mapE :: ExprLike e => e -> e
         mapE :: forall e. ExprLike e => e -> e
    mapE = (Expr -> Expr) -> e -> e
    forall a. ExprLike a => (Expr -> Expr) -> a -> a
    mapExpr Expr -> Expr
    f
      foldExpr :: forall m. Monoid m => (Expr -> m) -> ModuleApplication -> m
    foldExpr     = (Expr -> m) -> ModuleApplication -> m
    forall a. HasCallStack => a
    __IMPOSSIBLE__
      traverseExpr :: forall (m :: * -> *).
    Monad m =>
    (Expr -> m Expr) -> ModuleApplication -> m ModuleApplication
    traverseExpr = (Expr -> m Expr) -> ModuleApplication -> m ModuleApplication
    forall a. HasCallStack => a
    __IMPOSSIBLE__

    instance ExprLike Declaration where
      mapExpr :: (Expr -> Expr) -> Declaration -> Declaration
    mapExpr Expr -> Expr
    f = \case
         TypeSig ArgInfo
    ai TacticAttribute
    t Name
    x Expr
    e          -> ArgInfo -> TacticAttribute -> Name -> Expr -> Declaration
    TypeSig ArgInfo
    ai (TacticAttribute -> TacticAttribute
    forall e. ExprLike e => e -> e
    mapE TacticAttribute
    t) Name
    x (Expr -> Expr
    forall e. ExprLike e => e -> e
    mapE Expr
    e)
         FieldSig IsInstance
    i TacticAttribute
    t Name
    n Arg Expr
    e          -> IsInstance -> TacticAttribute -> Name -> Arg Expr -> Declaration
    FieldSig IsInstance
    i (TacticAttribute -> TacticAttribute
    forall e. ExprLike e => e -> e
    mapE TacticAttribute
    t) Name
    n (Arg Expr -> Arg Expr
    forall e. ExprLike e => e -> e
    mapE Arg Expr
    e)
         Field KwRange
    r [Declaration]
    fs                -> KwRange -> [Declaration] -> Declaration
    Field KwRange
    r                              ([Declaration] -> Declaration) -> [Declaration] -> Declaration
    forall a b. (a -> b) -> a -> b
    $ (Declaration -> Declaration) -> [Declaration] -> [Declaration]
    forall a b. (a -> b) -> [a] -> [b]
    map ((Expr -> Expr) -> Declaration -> Declaration
    forall a. ExprLike a => (Expr -> Expr) -> a -> a
    mapExpr Expr -> Expr
    f) [Declaration]
    fs
         FunClause LHS
    lhs RHS
    rhs WhereClause
    wh Catchall
    ca   -> LHS -> RHS -> WhereClause -> Catchall -> Declaration
    FunClause (LHS -> LHS
    forall e. ExprLike e => e -> e
    mapE LHS
    lhs) (RHS -> RHS
    forall e. ExprLike e => e -> e
    mapE RHS
    rhs) (WhereClause -> WhereClause
    forall e. ExprLike e => e -> e
    mapE WhereClause
    wh) Catchall
    ca
         DataSig Range
    r Erased
    er Name
    x [LamBinding]
    bs Expr
    e       -> Range -> Erased -> Name -> [LamBinding] -> Expr -> Declaration
    DataSig Range
    r Erased
    er Name
    x ([LamBinding] -> [LamBinding]
    forall e. ExprLike e => e -> e
    mapE [LamBinding]
    bs)             (Expr -> Declaration) -> Expr -> Declaration
    forall a b. (a -> b) -> a -> b
    $ Expr -> Expr
    forall e. ExprLike e => e -> e
    mapE Expr
    e
         DataDef Range
    r Name
    n [LamBinding]
    bs [Declaration]
    cs         -> Range -> Name -> [LamBinding] -> [Declaration] -> Declaration
    DataDef Range
    r Name
    n ([LamBinding] -> [LamBinding]
    forall e. ExprLike e => e -> e
    mapE [LamBinding]
    bs)                ([Declaration] -> Declaration) -> [Declaration] -> Declaration
    forall a b. (a -> b) -> a -> b
    $ [Declaration] -> [Declaration]
    forall e. ExprLike e => e -> e
    mapE [Declaration]
    cs
         Data Range
    r Erased
    er Name
    n [LamBinding]
    bs Expr
    e [Declaration]
    cs       -> Range
    -> Erased
    -> Name
    -> [LamBinding]
    -> Expr
    -> [Declaration]
    -> Declaration
    Data Range
    r Erased
    er Name
    n ([LamBinding] -> [LamBinding]
    forall e. ExprLike e => e -> e
    mapE [LamBinding]
    bs) (Expr -> Expr
    forall e. ExprLike e => e -> e
    mapE Expr
    e)       ([Declaration] -> Declaration) -> [Declaration] -> Declaration
    forall a b. (a -> b) -> a -> b
    $ [Declaration] -> [Declaration]
    forall e. ExprLike e => e -> e
    mapE [Declaration]
    cs
         RecordSig Range
    r Erased
    er Name
    ind [LamBinding]
    bs Expr
    e   -> Range -> Erased -> Name -> [LamBinding] -> Expr -> Declaration
    RecordSig Range
    r Erased
    er Name
    ind ([LamBinding] -> [LamBinding]
    forall e. ExprLike e => e -> e
    mapE [LamBinding]
    bs)         (Expr -> Declaration) -> Expr -> Declaration
    forall a b. (a -> b) -> a -> b
    $ Expr -> Expr
    forall e. ExprLike e => e -> e
    mapE Expr
    e
         RecordDef Range
    r Name
    n [RecordDirective]
    dir [LamBinding]
    tel [Declaration]
    ds  -> Range
    -> Name
    -> [RecordDirective]
    -> [LamBinding]
    -> [Declaration]
    -> Declaration
    RecordDef Range
    r Name
    n [RecordDirective]
    dir ([LamBinding] -> [LamBinding]
    forall e. ExprLike e => e -> e
    mapE [LamBinding]
    tel)         ([Declaration] -> Declaration) -> [Declaration] -> Declaration
    forall a b. (a -> b) -> a -> b
    $ [Declaration] -> [Declaration]
    forall e. ExprLike e => e -> e
    mapE [Declaration]
    ds
         Record Range
    r Erased
    er Name
    n [RecordDirective]
    dir [LamBinding]
    tel Expr
    e [Declaration]
    ds
                                   -> Range
    -> Erased
    -> Name
    -> [RecordDirective]
    -> [LamBinding]
    -> Expr
    -> [Declaration]
    -> Declaration
    Record Range
    r Erased
    er Name
    n [RecordDirective]
    dir ([LamBinding] -> [LamBinding]
    forall e. ExprLike e => e -> e
    mapE [LamBinding]
    tel) (Expr -> Expr
    forall e. ExprLike e => e -> e
    mapE Expr
    e)
                                                                           ([Declaration] -> Declaration) -> [Declaration] -> Declaration
    forall a b. (a -> b) -> a -> b
    $ [Declaration] -> [Declaration]
    forall e. ExprLike e => e -> e
    mapE [Declaration]
    ds
         e :: Declaration
    e@Infix{}                 -> Declaration
    e
         e :: Declaration
    e@Syntax{}                -> Declaration
    e
         e :: Declaration
    e@PatternSyn{}            -> Declaration
    e
         Mutual    KwRange
    r [Declaration]
    ds            -> KwRange -> [Declaration] -> Declaration
    Mutual    KwRange
    r                          ([Declaration] -> Declaration) -> [Declaration] -> Declaration
    forall a b. (a -> b) -> a -> b
    $ [Declaration] -> [Declaration]
    forall e. ExprLike e => e -> e
    mapE [Declaration]
    ds
         InterleavedMutual KwRange
    r [Declaration]
    ds    -> KwRange -> [Declaration] -> Declaration
    InterleavedMutual KwRange
    r                  ([Declaration] -> Declaration) -> [Declaration] -> Declaration
    forall a b. (a -> b) -> a -> b
    $ [Declaration] -> [Declaration]
    forall e. ExprLike e => e -> e
    mapE [Declaration]
    ds
         LoneConstructor KwRange
    r [Declaration]
    ds      -> KwRange -> [Declaration] -> Declaration
    LoneConstructor KwRange
    r                    ([Declaration] -> Declaration) -> [Declaration] -> Declaration
    forall a b. (a -> b) -> a -> b
    $ [Declaration] -> [Declaration]
    forall e. ExprLike e => e -> e
    mapE [Declaration]
    ds
         Abstract  KwRange
    r [Declaration]
    ds            -> KwRange -> [Declaration] -> Declaration
    Abstract  KwRange
    r                          ([Declaration] -> Declaration) -> [Declaration] -> Declaration
    forall a b. (a -> b) -> a -> b
    $ [Declaration] -> [Declaration]
    forall e. ExprLike e => e -> e
    mapE [Declaration]
    ds
         Private   KwRange
    r Origin
    o [Declaration]
    ds          -> KwRange -> Origin -> [Declaration] -> Declaration
    Private   KwRange
    r Origin
    o                        ([Declaration] -> Declaration) -> [Declaration] -> Declaration
    forall a b. (a -> b) -> a -> b
    $ [Declaration] -> [Declaration]
    forall e. ExprLike e => e -> e
    mapE [Declaration]
    ds
         InstanceB KwRange
    r [Declaration]
    ds            -> KwRange -> [Declaration] -> Declaration
    InstanceB KwRange
    r                          ([Declaration] -> Declaration) -> [Declaration] -> Declaration
    forall a b. (a -> b) -> a -> b
    $ [Declaration] -> [Declaration]
    forall e. ExprLike e => e -> e
    mapE [Declaration]
    ds
         Macro     KwRange
    r [Declaration]
    ds            -> KwRange -> [Declaration] -> Declaration
    Macro     KwRange
    r                          ([Declaration] -> Declaration) -> [Declaration] -> Declaration
    forall a b. (a -> b) -> a -> b
    $ [Declaration] -> [Declaration]
    forall e. ExprLike e => e -> e
    mapE [Declaration]
    ds
         Postulate KwRange
    r [Declaration]
    ds            -> KwRange -> [Declaration] -> Declaration
    Postulate KwRange
    r                          ([Declaration] -> Declaration) -> [Declaration] -> Declaration
    forall a b. (a -> b) -> a -> b
    $ [Declaration] -> [Declaration]
    forall e. ExprLike e => e -> e
    mapE [Declaration]
    ds
         Primitive KwRange
    r [Declaration]
    ds            -> KwRange -> [Declaration] -> Declaration
    Primitive KwRange
    r                          ([Declaration] -> Declaration) -> [Declaration] -> Declaration
    forall a b. (a -> b) -> a -> b
    $ [Declaration] -> [Declaration]
    forall e. ExprLike e => e -> e
    mapE [Declaration]
    ds
         Generalize KwRange
    r [Declaration]
    ds           -> KwRange -> [Declaration] -> Declaration
    Generalize KwRange
    r                         ([Declaration] -> Declaration) -> [Declaration] -> Declaration
    forall a b. (a -> b) -> a -> b
    $ [Declaration] -> [Declaration]
    forall e. ExprLike e => e -> e
    mapE [Declaration]
    ds
         Opaque  KwRange
    r [Declaration]
    ds              -> KwRange -> [Declaration] -> Declaration
    Opaque KwRange
    r                             ([Declaration] -> Declaration) -> [Declaration] -> Declaration
    forall a b. (a -> b) -> a -> b
    $ [Declaration] -> [Declaration]
    forall e. ExprLike e => e -> e
    mapE [Declaration]
    ds
         e :: Declaration
    e@Open{}                  -> Declaration
    e
         e :: Declaration
    e@Import{}                -> Declaration
    e
         ModuleMacro Range
    r Erased
    e Name
    n ModuleApplication
    es OpenShortHand
    op ImportDirective
    dir
                                   -> Range
    -> Erased
    -> Name
    -> ModuleApplication
    -> OpenShortHand
    -> ImportDirective
    -> Declaration
    ModuleMacro Range
    r Erased
    e Name
    n (ModuleApplication -> ModuleApplication
    forall e. ExprLike e => e -> e
    mapE ModuleApplication
    es) OpenShortHand
    op ImportDirective
    dir
         Module Range
    r Erased
    e QName
    n Telescope
    tel [Declaration]
    ds       -> Range
    -> Erased -> QName -> Telescope -> [Declaration] -> Declaration
    Module Range
    r Erased
    e QName
    n (Telescope -> Telescope
    forall e. ExprLike e => e -> e
    mapE Telescope
    tel)              ([Declaration] -> Declaration) -> [Declaration] -> Declaration
    forall a b. (a -> b) -> a -> b
    $ [Declaration] -> [Declaration]
    forall e. ExprLike e => e -> e
    mapE [Declaration]
    ds
         UnquoteDecl Range
    r [Name]
    x Expr
    e         -> Range -> [Name] -> Expr -> Declaration
    UnquoteDecl Range
    r [Name]
    x (Expr -> Expr
    forall e. ExprLike e => e -> e
    mapE Expr
    e)
         UnquoteDef Range
    r [Name]
    x Expr
    e          -> Range -> [Name] -> Expr -> Declaration
    UnquoteDef Range
    r [Name]
    x (Expr -> Expr
    forall e. ExprLike e => e -> e
    mapE Expr
    e)
         UnquoteData Range
    r Name
    x [Name]
    xs Expr
    e      -> Range -> Name -> [Name] -> Expr -> Declaration
    UnquoteData Range
    r Name
    x [Name]
    xs (Expr -> Expr
    forall e. ExprLike e => e -> e
    mapE Expr
    e)
         e :: Declaration
    e@Pragma{}                -> Declaration
    e
         e :: Declaration
    e@Unfolding{}             -> Declaration
    e
       where
         mapE :: ExprLike e => e -> e
         mapE :: forall e. ExprLike e => e -> e
    mapE = (Expr -> Expr) -> e -> e
    forall a. ExprLike a => (Expr -> Expr) -> a -> a
    mapExpr Expr -> Expr
    f

      foldExpr :: forall m. Monoid m => (Expr -> m) -> Declaration -> m
    foldExpr     = (Expr -> m) -> Declaration -> m
    forall a. HasCallStack => a
    __IMPOSSIBLE__
      traverseExpr :: forall (m :: * -> *).
    Monad m =>
    (Expr -> m Expr) -> Declaration -> m Declaration
    traverseExpr = (Expr -> m Expr) -> Declaration -> m Declaration
    forall a. HasCallStack => a
    __IMPOSSIBLE__

    {- Template

    instance ExprLike a where
      mapExpr f = \case
        where mapE e = mapExpr f e
      foldExpr     = __IMPOSSIBLE__
      traverseExpr = __IMPOSSIBLE__

    -}

    -- Generic traversals for concrete declarations.
    -- ========================================================================

    class FoldDecl a where

      -- | Collect declarations and subdeclarations, transitively.
      -- Prefix-order tree traversal.
      foldDecl :: Monoid m => (Declaration -> m) -> a -> m

      default foldDecl :: (Monoid m, Foldable t, FoldDecl b, t b ~ a)
        => (Declaration -> m) -> a -> m
      foldDecl = (b -> m) -> a -> m
    (b -> m) -> t b -> m
    forall m a. Monoid m => (a -> m) -> t a -> m
    forall (t :: * -> *) m a.
    (Foldable t, Monoid m) =>
    (a -> m) -> t a -> m
    foldMap ((b -> m) -> a -> m)
    -> ((Declaration -> m) -> b -> m) -> (Declaration -> m) -> a -> m
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Declaration -> m) -> b -> m
    forall m. Monoid m => (Declaration -> m) -> b -> m
    forall a m. (FoldDecl a, Monoid m) => (Declaration -> m) -> a -> m
    foldDecl

    instance FoldDecl a => FoldDecl [a]
    instance FoldDecl a => FoldDecl (List1 a)
    instance FoldDecl a => FoldDecl (List2 a)
    instance FoldDecl a => FoldDecl (WhereClause' a)

    instance FoldDecl Declaration where
      foldDecl :: forall m. Monoid m => (Declaration -> m) -> Declaration -> m
    foldDecl Declaration -> m
    f Declaration
    d = Declaration -> m
    f Declaration
    d m -> m -> m
    forall a. Semigroup a => a -> a -> a
    <> case Declaration
    d of
        Private  KwRange
    _ Origin
    _        [Declaration]
    ds  -> (Declaration -> m) -> [Declaration] -> m
    forall m. Monoid m => (Declaration -> m) -> [Declaration] -> m
    forall a m. (FoldDecl a, Monoid m) => (Declaration -> m) -> a -> m
    foldDecl Declaration -> m
    f [Declaration]
    ds
        Abstract KwRange
    _          [Declaration]
    ds  -> (Declaration -> m) -> [Declaration] -> m
    forall m. Monoid m => (Declaration -> m) -> [Declaration] -> m
    forall a m. (FoldDecl a, Monoid m) => (Declaration -> m) -> a -> m
    foldDecl Declaration -> m
    f [Declaration]
    ds
        InstanceB KwRange
    _         [Declaration]
    ds  -> (Declaration -> m) -> [Declaration] -> m
    forall m. Monoid m => (Declaration -> m) -> [Declaration] -> m
    forall a m. (FoldDecl a, Monoid m) => (Declaration -> m) -> a -> m
    foldDecl Declaration -> m
    f [Declaration]
    ds
        InterleavedMutual KwRange
    _ [Declaration]
    ds  -> (Declaration -> m) -> [Declaration] -> m
    forall m. Monoid m => (Declaration -> m) -> [Declaration] -> m
    forall a m. (FoldDecl a, Monoid m) => (Declaration -> m) -> a -> m
    foldDecl Declaration -> m
    f [Declaration]
    ds
        LoneConstructor KwRange
    _   [Declaration]
    ds  -> (Declaration -> m) -> [Declaration] -> m
    forall m. Monoid m => (Declaration -> m) -> [Declaration] -> m
    forall a m. (FoldDecl a, Monoid m) => (Declaration -> m) -> a -> m
    foldDecl Declaration -> m
    f [Declaration]
    ds
        Mutual KwRange
    _            [Declaration]
    ds  -> (Declaration -> m) -> [Declaration] -> m
    forall m. Monoid m => (Declaration -> m) -> [Declaration] -> m
    forall a m. (FoldDecl a, Monoid m) => (Declaration -> m) -> a -> m
    foldDecl Declaration -> m
    f [Declaration]
    ds
        Module Range
    _ Erased
    _ QName
    _ Telescope
    _      [Declaration]
    ds  -> (Declaration -> m) -> [Declaration] -> m
    forall m. Monoid m => (Declaration -> m) -> [Declaration] -> m
    forall a m. (FoldDecl a, Monoid m) => (Declaration -> m) -> a -> m
    foldDecl Declaration -> m
    f [Declaration]
    ds
        Macro KwRange
    _             [Declaration]
    ds  -> (Declaration -> m) -> [Declaration] -> m
    forall m. Monoid m => (Declaration -> m) -> [Declaration] -> m
    forall a m. (FoldDecl a, Monoid m) => (Declaration -> m) -> a -> m
    foldDecl Declaration -> m
    f [Declaration]
    ds
        Record Range
    _ Erased
    _ Name
    _ [RecordDirective]
    _ [LamBinding]
    _ Expr
    _  [Declaration]
    ds  -> (Declaration -> m) -> [Declaration] -> m
    forall m. Monoid m => (Declaration -> m) -> [Declaration] -> m
    forall a m. (FoldDecl a, Monoid m) => (Declaration -> m) -> a -> m
    foldDecl Declaration -> m
    f [Declaration]
    ds
        RecordDef Range
    _ Name
    _ [RecordDirective]
    _ [LamBinding]
    _   [Declaration]
    ds  -> (Declaration -> m) -> [Declaration] -> m
    forall m. Monoid m => (Declaration -> m) -> [Declaration] -> m
    forall a m. (FoldDecl a, Monoid m) => (Declaration -> m) -> a -> m
    foldDecl Declaration -> m
    f [Declaration]
    ds
        TypeSig ArgInfo
    _ TacticAttribute
    _ Name
    _ Expr
    _         -> m
    forall a. Monoid a => a
    mempty
        FieldSig IsInstance
    _ TacticAttribute
    _ Name
    _ Arg Expr
    _        -> m
    forall a. Monoid a => a
    mempty
        Generalize KwRange
    _ [Declaration]
    _          -> m
    forall a. Monoid a => a
    mempty
        Field KwRange
    _ [Declaration]
    _               -> m
    forall a. Monoid a => a
    mempty
        FunClause LHS
    _ RHS
    _ WhereClause
    wh Catchall
    _      -> (Declaration -> m) -> WhereClause -> m
    forall m. Monoid m => (Declaration -> m) -> WhereClause -> m
    forall a m. (FoldDecl a, Monoid m) => (Declaration -> m) -> a -> m
    foldDecl Declaration -> m
    f WhereClause
    wh
        DataSig Range
    _ Erased
    _ Name
    _ [LamBinding]
    _ Expr
    _       -> m
    forall a. Monoid a => a
    mempty
        Data Range
    _ Erased
    _ Name
    _ [LamBinding]
    _ Expr
    _ [Declaration]
    _        -> m
    forall a. Monoid a => a
    mempty
        DataDef Range
    _ Name
    _ [LamBinding]
    _ [Declaration]
    _         -> m
    forall a. Monoid a => a
    mempty
        RecordSig Range
    _ Erased
    _ Name
    _ [LamBinding]
    _ Expr
    _     -> m
    forall a. Monoid a => a
    mempty
        Infix Fixity
    _ List1 Name
    _               -> m
    forall a. Monoid a => a
    mempty
        Syntax Name
    _ Notation
    _              -> m
    forall a. Monoid a => a
    mempty
        PatternSyn Range
    _ Name
    _ [WithHiding Name]
    _ Pattern
    _      -> m
    forall a. Monoid a => a
    mempty
        Postulate KwRange
    _ [Declaration]
    _           -> m
    forall a. Monoid a => a
    mempty
        Primitive KwRange
    _ [Declaration]
    _           -> m
    forall a. Monoid a => a
    mempty
        Open Range
    _ QName
    _ ImportDirective
    _              -> m
    forall a. Monoid a => a
    mempty
        Import Range
    _ QName
    _ Maybe AsName
    _ OpenShortHand
    _ ImportDirective
    _        -> m
    forall a. Monoid a => a
    mempty
        ModuleMacro Range
    _ Erased
    _ Name
    _ ModuleApplication
    _ OpenShortHand
    _ ImportDirective
    _ -> m
    forall a. Monoid a => a
    mempty
        UnquoteDecl Range
    _ [Name]
    _ Expr
    _       -> m
    forall a. Monoid a => a
    mempty
        UnquoteDef Range
    _ [Name]
    _ Expr
    _        -> m
    forall a. Monoid a => a
    mempty
        UnquoteData Range
    _ Name
    _ [Name]
    _ Expr
    _     -> m
    forall a. Monoid a => a
    mempty
        Pragma Pragma
    _                -> m
    forall a. Monoid a => a
    mempty
        Opaque KwRange
    _ [Declaration]
    ds             -> (Declaration -> m) -> [Declaration] -> m
    forall m. Monoid m => (Declaration -> m) -> [Declaration] -> m
    forall a m. (FoldDecl a, Monoid m) => (Declaration -> m) -> a -> m
    foldDecl Declaration -> m
    f [Declaration]
    ds
        Unfolding KwRange
    _ [QName]
    _           -> m
    forall a. Monoid a => a
    mempty

    class TraverseDecl a where

      -- | Update declarations and their subdeclarations.
      -- Prefix-order traversal: traverses subdeclarations of updated declaration.
      --
      preTraverseDecl :: Monad m => (Declaration -> m Declaration) -> a -> m a

      default preTraverseDecl :: (Monad m, Traversable t, TraverseDecl b, t b ~ a)
        => (Declaration -> m Declaration) -> a -> m a
      preTraverseDecl = (b -> m b) -> a -> m a
    (b -> m b) -> t b -> m (t b)
    forall (t :: * -> *) (f :: * -> *) a b.
    (Traversable t, Applicative f) =>
    (a -> f b) -> t a -> f (t b)
    forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> t a -> f (t b)
    traverse ((b -> m b) -> a -> m a)
    -> ((Declaration -> m Declaration) -> b -> m b)
    -> (Declaration -> m Declaration)
    -> a
    -> m a
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Declaration -> m Declaration) -> b -> m b
    forall a (m :: * -> *).
    (TraverseDecl a, Monad m) =>
    (Declaration -> m Declaration) -> a -> m a
    forall (m :: * -> *).
    Monad m =>
    (Declaration -> m Declaration) -> b -> m b
    preTraverseDecl

    instance TraverseDecl a => TraverseDecl [a]
    instance TraverseDecl a => TraverseDecl (List1 a)
    instance TraverseDecl a => TraverseDecl (List2 a)
    instance TraverseDecl a => TraverseDecl (WhereClause' a)

    instance TraverseDecl Declaration where
      preTraverseDecl :: forall (m :: * -> *).
    Monad m =>
    (Declaration -> m Declaration) -> Declaration -> m Declaration
    preTraverseDecl Declaration -> m Declaration
    f Declaration
    d0 = do
        d <- Declaration -> m Declaration
    f Declaration
    d0
        case d of
          Private  KwRange
    r Origin
    o        [Declaration]
    ds     -> KwRange -> Origin -> [Declaration] -> Declaration
    Private KwRange
    r Origin
    o             ([Declaration] -> Declaration) -> m [Declaration] -> m Declaration
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (Declaration -> m Declaration) -> [Declaration] -> m [Declaration]
    forall a (m :: * -> *).
    (TraverseDecl a, Monad m) =>
    (Declaration -> m Declaration) -> a -> m a
    forall (m :: * -> *).
    Monad m =>
    (Declaration -> m Declaration) -> [Declaration] -> m [Declaration]
    preTraverseDecl Declaration -> m Declaration
    f [Declaration]
    ds
          Abstract KwRange
    r          [Declaration]
    ds     -> KwRange -> [Declaration] -> Declaration
    Abstract KwRange
    r              ([Declaration] -> Declaration) -> m [Declaration] -> m Declaration
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (Declaration -> m Declaration) -> [Declaration] -> m [Declaration]
    forall a (m :: * -> *).
    (TraverseDecl a, Monad m) =>
    (Declaration -> m Declaration) -> a -> m a
    forall (m :: * -> *).
    Monad m =>
    (Declaration -> m Declaration) -> [Declaration] -> m [Declaration]
    preTraverseDecl Declaration -> m Declaration
    f [Declaration]
    ds
          InstanceB KwRange
    r         [Declaration]
    ds     -> KwRange -> [Declaration] -> Declaration
    InstanceB KwRange
    r             ([Declaration] -> Declaration) -> m [Declaration] -> m Declaration
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (Declaration -> m Declaration) -> [Declaration] -> m [Declaration]
    forall a (m :: * -> *).
    (TraverseDecl a, Monad m) =>
    (Declaration -> m Declaration) -> a -> m a
    forall (m :: * -> *).
    Monad m =>
    (Declaration -> m Declaration) -> [Declaration] -> m [Declaration]
    preTraverseDecl Declaration -> m Declaration
    f [Declaration]
    ds
          InterleavedMutual KwRange
    r [Declaration]
    ds     -> KwRange -> [Declaration] -> Declaration
    InterleavedMutual KwRange
    r     ([Declaration] -> Declaration) -> m [Declaration] -> m Declaration
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (Declaration -> m Declaration) -> [Declaration] -> m [Declaration]
    forall a (m :: * -> *).
    (TraverseDecl a, Monad m) =>
    (Declaration -> m Declaration) -> a -> m a
    forall (m :: * -> *).
    Monad m =>
    (Declaration -> m Declaration) -> [Declaration] -> m [Declaration]
    preTraverseDecl Declaration -> m Declaration
    f [Declaration]
    ds
          LoneConstructor KwRange
    r   [Declaration]
    ds     -> KwRange -> [Declaration] -> Declaration
    LoneConstructor KwRange
    r       ([Declaration] -> Declaration) -> m [Declaration] -> m Declaration
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (Declaration -> m Declaration) -> [Declaration] -> m [Declaration]
    forall a (m :: * -> *).
    (TraverseDecl a, Monad m) =>
    (Declaration -> m Declaration) -> a -> m a
    forall (m :: * -> *).
    Monad m =>
    (Declaration -> m Declaration) -> [Declaration] -> m [Declaration]
    preTraverseDecl Declaration -> m Declaration
    f [Declaration]
    ds
          Mutual KwRange
    r            [Declaration]
    ds     -> KwRange -> [Declaration] -> Declaration
    Mutual KwRange
    r                ([Declaration] -> Declaration) -> m [Declaration] -> m Declaration
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (Declaration -> m Declaration) -> [Declaration] -> m [Declaration]
    forall a (m :: * -> *).
    (TraverseDecl a, Monad m) =>
    (Declaration -> m Declaration) -> a -> m a
    forall (m :: * -> *).
    Monad m =>
    (Declaration -> m Declaration) -> [Declaration] -> m [Declaration]
    preTraverseDecl Declaration -> m Declaration
    f [Declaration]
    ds
          Module Range
    r Erased
    er QName
    n Telescope
    tel   [Declaration]
    ds     -> Range
    -> Erased -> QName -> Telescope -> [Declaration] -> Declaration
    Module Range
    r Erased
    er QName
    n Telescope
    tel       ([Declaration] -> Declaration) -> m [Declaration] -> m Declaration
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (Declaration -> m Declaration) -> [Declaration] -> m [Declaration]
    forall a (m :: * -> *).
    (TraverseDecl a, Monad m) =>
    (Declaration -> m Declaration) -> a -> m a
    forall (m :: * -> *).
    Monad m =>
    (Declaration -> m Declaration) -> [Declaration] -> m [Declaration]
    preTraverseDecl Declaration -> m Declaration
    f [Declaration]
    ds
          Macro KwRange
    r             [Declaration]
    ds     -> KwRange -> [Declaration] -> Declaration
    Macro KwRange
    r                 ([Declaration] -> Declaration) -> m [Declaration] -> m Declaration
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (Declaration -> m Declaration) -> [Declaration] -> m [Declaration]
    forall a (m :: * -> *).
    (TraverseDecl a, Monad m) =>
    (Declaration -> m Declaration) -> a -> m a
    forall (m :: * -> *).
    Monad m =>
    (Declaration -> m Declaration) -> [Declaration] -> m [Declaration]
    preTraverseDecl Declaration -> m Declaration
    f [Declaration]
    ds
          Opaque KwRange
    r [Declaration]
    ds                -> KwRange -> [Declaration] -> Declaration
    Opaque KwRange
    r                ([Declaration] -> Declaration) -> m [Declaration] -> m Declaration
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (Declaration -> m Declaration) -> [Declaration] -> m [Declaration]
    forall a (m :: * -> *).
    (TraverseDecl a, Monad m) =>
    (Declaration -> m Declaration) -> a -> m a
    forall (m :: * -> *).
    Monad m =>
    (Declaration -> m Declaration) -> [Declaration] -> m [Declaration]
    preTraverseDecl Declaration -> m Declaration
    f [Declaration]
    ds
          Record Range
    r Erased
    er Name
    n [RecordDirective]
    dir [LamBinding]
    tel Expr
    t [Declaration]
    ds -> Range
    -> Erased
    -> Name
    -> [RecordDirective]
    -> [LamBinding]
    -> Expr
    -> [Declaration]
    -> Declaration
    Record Range
    r Erased
    er Name
    n [RecordDirective]
    dir [LamBinding]
    tel Expr
    t ([Declaration] -> Declaration) -> m [Declaration] -> m Declaration
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (Declaration -> m Declaration) -> [Declaration] -> m [Declaration]
    forall a (m :: * -> *).
    (TraverseDecl a, Monad m) =>
    (Declaration -> m Declaration) -> a -> m a
    forall (m :: * -> *).
    Monad m =>
    (Declaration -> m Declaration) -> [Declaration] -> m [Declaration]
    preTraverseDecl Declaration -> m Declaration
    f [Declaration]
    ds
          RecordDef Range
    r Name
    n [RecordDirective]
    dir [LamBinding]
    tel   [Declaration]
    ds -> Range
    -> Name
    -> [RecordDirective]
    -> [LamBinding]
    -> [Declaration]
    -> Declaration
    RecordDef Range
    r Name
    n [RecordDirective]
    dir [LamBinding]
    tel   ([Declaration] -> Declaration) -> m [Declaration] -> m Declaration
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (Declaration -> m Declaration) -> [Declaration] -> m [Declaration]
    forall a (m :: * -> *).
    (TraverseDecl a, Monad m) =>
    (Declaration -> m Declaration) -> a -> m a
    forall (m :: * -> *).
    Monad m =>
    (Declaration -> m Declaration) -> [Declaration] -> m [Declaration]
    preTraverseDecl Declaration -> m Declaration
    f [Declaration]
    ds
          TypeSig ArgInfo
    _ TacticAttribute
    _ Name
    _ Expr
    _            -> Declaration -> m Declaration
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Declaration
    d
          FieldSig IsInstance
    _ TacticAttribute
    _ Name
    _ Arg Expr
    _           -> Declaration -> m Declaration
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Declaration
    d
          Generalize KwRange
    _ [Declaration]
    _             -> Declaration -> m Declaration
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Declaration
    d
          Field KwRange
    _ [Declaration]
    _                  -> Declaration -> m Declaration
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Declaration
    d
          FunClause LHS
    lhs RHS
    rhs WhereClause
    wh Catchall
    ca    -> (Declaration -> m Declaration) -> WhereClause -> m WhereClause
    forall a (m :: * -> *).
    (TraverseDecl a, Monad m) =>
    (Declaration -> m Declaration) -> a -> m a
    forall (m :: * -> *).
    Monad m =>
    (Declaration -> m Declaration) -> WhereClause -> m WhereClause
    preTraverseDecl Declaration -> m Declaration
    f WhereClause
    wh m WhereClause -> (WhereClause -> Declaration) -> m Declaration
    forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
    <&> \ WhereClause
    wh' -> LHS -> RHS -> WhereClause -> Catchall -> Declaration
    FunClause LHS
    lhs RHS
    rhs WhereClause
    wh' Catchall
    ca
          DataSig Range
    _ Erased
    _ Name
    _ [LamBinding]
    _ Expr
    _          -> Declaration -> m Declaration
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Declaration
    d
          Data Range
    _ Erased
    _ Name
    _ [LamBinding]
    _ Expr
    _ [Declaration]
    _           -> Declaration -> m Declaration
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Declaration
    d
          DataDef Range
    _ Name
    _ [LamBinding]
    _ [Declaration]
    _            -> Declaration -> m Declaration
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Declaration
    d
          RecordSig Range
    _ Erased
    _ Name
    _ [LamBinding]
    _ Expr
    _        -> Declaration -> m Declaration
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Declaration
    d
          Infix Fixity
    _ List1 Name
    _                  -> Declaration -> m Declaration
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Declaration
    d
          Syntax Name
    _ Notation
    _                 -> Declaration -> m Declaration
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Declaration
    d
          PatternSyn Range
    _ Name
    _ [WithHiding Name]
    _ Pattern
    _         -> Declaration -> m Declaration
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Declaration
    d
          Postulate KwRange
    _ [Declaration]
    _              -> Declaration -> m Declaration
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Declaration
    d
          Primitive KwRange
    _ [Declaration]
    _              -> Declaration -> m Declaration
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Declaration
    d
          Open Range
    _ QName
    _ ImportDirective
    _                 -> Declaration -> m Declaration
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Declaration
    d
          Import Range
    _ QName
    _ Maybe AsName
    _ OpenShortHand
    _ ImportDirective
    _           -> Declaration -> m Declaration
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Declaration
    d
          ModuleMacro Range
    _ Erased
    _ Name
    _ ModuleApplication
    _ OpenShortHand
    _ ImportDirective
    _    -> Declaration -> m Declaration
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Declaration
    d
          UnquoteDecl Range
    _ [Name]
    _ Expr
    _          -> Declaration -> m Declaration
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Declaration
    d
          UnquoteDef Range
    _ [Name]
    _ Expr
    _           -> Declaration -> m Declaration
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Declaration
    d
          UnquoteData Range
    _ Name
    _ [Name]
    _ Expr
    _        -> Declaration -> m Declaration
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Declaration
    d
          Pragma Pragma
    _                   -> Declaration -> m Declaration
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Declaration
    d
          Unfolding KwRange
    _ [QName]
    _              -> Declaration -> m Declaration
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Declaration
    d