    module Agda.Syntax.Abstract.Views where

    import Prelude hiding (null)

    import Control.Applicative ( Const(Const), getConst )
    import Control.Arrow (first)
    import Control.Monad.Identity

    import Data.Foldable (foldMap)
    import Data.Semigroup ((<>))
    import Data.Void

    import Agda.Syntax.Common
    import Agda.Syntax.Abstract as A
    import Agda.Syntax.Concrete (FieldAssignment', exprFieldA)
    import Agda.Syntax.Info
    import Agda.Syntax.Scope.Base (KindOfName(..), conKindOfName, WithKind(..))

    import Agda.Utils.Either
    import Agda.Utils.List1 (List1)
    import Agda.Utils.Null
    import Agda.Utils.Singleton

    import Agda.Utils.Impossible

    data AppView' arg = Application Expr [NamedArg arg]
      deriving ((forall a b. (a -> b) -> AppView' a -> AppView' b)
    -> (forall a b. a -> AppView' b -> AppView' a) -> Functor AppView'
    forall a b. a -> AppView' b -> AppView' a
    forall a b. (a -> b) -> AppView' a -> AppView' 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 -> AppView' b -> AppView' a
    $c<$ :: forall a b. a -> AppView' b -> AppView' a
    fmap :: forall a b. (a -> b) -> AppView' a -> AppView' b
    $cfmap :: forall a b. (a -> b) -> AppView' a -> AppView' b
    Functor)

    type AppView = AppView' Expr

    -- | Gather applications to expose head and spine.
    --
    --   Note: everything is an application, possibly of itself to 0 arguments
    appView :: Expr -> AppView
    appView :: Expr -> AppView
    appView = ((AppInfo, Expr) -> Expr) -> AppView' (AppInfo, Expr) -> AppView
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (AppInfo, Expr) -> Expr
    forall a b. (a, b) -> b
    snd (AppView' (AppInfo, Expr) -> AppView)
    -> (Expr -> AppView' (AppInfo, Expr)) -> Expr -> AppView
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Expr -> AppView' (AppInfo, Expr)
    appView'

    appView' :: Expr -> AppView' (AppInfo, Expr)
    appView' :: Expr -> AppView' (AppInfo, Expr)
    appView' Expr
    e =
      case Expr
    e of
        App AppInfo
    i Expr
    e1 NamedArg Expr
    e2
          | Dot ExprInfo
    _ Expr
    e2' <- Expr -> Expr
    unScope (Expr -> Expr) -> Expr -> Expr
    forall a b. (a -> b) -> a -> b
    $ NamedArg Expr -> Expr
    forall a. NamedArg a -> a
    namedArg NamedArg Expr
    e2
          , Just Expr
    f <- Expr -> Maybe Expr
    maybeProjTurnPostfix Expr
    e2'
          , NamedArg Expr -> Hiding
    forall a. LensHiding a => a -> Hiding
    getHiding NamedArg Expr
    e2 Hiding -> Hiding -> Bool
    forall a. Eq a => a -> a -> Bool
    == Hiding
    NotHidden -- Jesper, 2018-12-13: postfix projections shouldn't be hidden
                       -> Expr -> [NamedArg (AppInfo, Expr)] -> AppView' (AppInfo, Expr)
    forall arg. Expr -> [NamedArg arg] -> AppView' arg
    Application Expr
    f [(AppInfo, Expr) -> NamedArg (AppInfo, Expr)
    forall a. a -> NamedArg a
    defaultNamedArg (AppInfo
    i, Expr
    e1)]
        App AppInfo
    i Expr
    e1 NamedArg Expr
    arg
          | Application Expr
    hd [NamedArg (AppInfo, Expr)]
    es <- Expr -> AppView' (AppInfo, Expr)
    appView' Expr
    e1
                       -> Expr -> [NamedArg (AppInfo, Expr)] -> AppView' (AppInfo, Expr)
    forall arg. Expr -> [NamedArg arg] -> AppView' arg
    Application Expr
    hd ([NamedArg (AppInfo, Expr)] -> AppView' (AppInfo, Expr))
    -> [NamedArg (AppInfo, Expr)] -> AppView' (AppInfo, Expr)
    forall a b. (a -> b) -> a -> b
    $ [NamedArg (AppInfo, Expr)]
    es [NamedArg (AppInfo, Expr)]
    -> [NamedArg (AppInfo, Expr)] -> [NamedArg (AppInfo, Expr)]
    forall a. [a] -> [a] -> [a]
    ++ [((Named NamedName Expr -> Named NamedName (AppInfo, Expr))
    -> NamedArg Expr -> NamedArg (AppInfo, Expr)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap ((Named NamedName Expr -> Named NamedName (AppInfo, Expr))
     -> NamedArg Expr -> NamedArg (AppInfo, Expr))
    -> ((Expr -> (AppInfo, Expr))
        -> Named NamedName Expr -> Named NamedName (AppInfo, Expr))
    -> (Expr -> (AppInfo, Expr))
    -> NamedArg Expr
    -> NamedArg (AppInfo, Expr)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Expr -> (AppInfo, Expr))
    -> Named NamedName Expr -> Named NamedName (AppInfo, Expr)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap) (AppInfo
    i,) NamedArg Expr
    arg]
        ScopedExpr ScopeInfo
    _ Expr
    e -> Expr -> AppView' (AppInfo, Expr)
    appView' Expr
    e
        Expr
    _              -> Expr -> [NamedArg (AppInfo, Expr)] -> AppView' (AppInfo, Expr)
    forall arg. Expr -> [NamedArg arg] -> AppView' arg
    Application Expr
    e []

    maybeProjTurnPostfix :: Expr -> Maybe Expr
    maybeProjTurnPostfix :: Expr -> Maybe Expr
    maybeProjTurnPostfix Expr
    e =
      case Expr
    e of
        ScopedExpr ScopeInfo
    i Expr
    e' -> ScopeInfo -> Expr -> Expr
    ScopedExpr ScopeInfo
    i (Expr -> Expr) -> Maybe Expr -> Maybe Expr
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Expr -> Maybe Expr
    maybeProjTurnPostfix Expr
    e'
        Proj ProjOrigin
    _ AmbiguousQName
    x        -> Expr -> Maybe Expr
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Expr -> Maybe Expr) -> Expr -> Maybe Expr
    forall a b. (a -> b) -> a -> b
    $ ProjOrigin -> AmbiguousQName -> Expr
    Proj ProjOrigin
    ProjPostfix AmbiguousQName
    x
        Expr
    _               -> Maybe Expr
    forall a. Maybe a
    Nothing

    unAppView :: AppView -> Expr
    unAppView :: AppView -> Expr
    unAppView (Application Expr
    h [NamedArg Expr]
    es) =
      (Expr -> NamedArg Expr -> Expr) -> Expr -> [NamedArg Expr] -> Expr
    forall (t :: * -> *) b a.
    Foldable t =>
    (b -> a -> b) -> b -> t a -> b
    foldl (AppInfo -> Expr -> NamedArg Expr -> Expr
    App AppInfo
    defaultAppInfo_) Expr
    h [NamedArg Expr]
    es

    -- | Collects plain lambdas.
    data LamView = LamView [LamBinding] Expr

    lamView :: Expr -> LamView
    lamView :: Expr -> LamView
    lamView (Lam ExprInfo
    i LamBinding
    b Expr
    e) = LamBinding -> LamView -> LamView
    cons LamBinding
    b (LamView -> LamView) -> LamView -> LamView
    forall a b. (a -> b) -> a -> b
    $ Expr -> LamView
    lamView Expr
    e
      where cons :: LamBinding -> LamView -> LamView
    cons LamBinding
    b (LamView [LamBinding]
    bs Expr
    e) = [LamBinding] -> Expr -> LamView
    LamView (LamBinding
    b LamBinding -> [LamBinding] -> [LamBinding]
    forall a. a -> [a] -> [a]
    : [LamBinding]
    bs) Expr
    e
    lamView (ScopedExpr ScopeInfo
    _ Expr
    e) = Expr -> LamView
    lamView Expr
    e
    lamView Expr
    e = [LamBinding] -> Expr -> LamView
    LamView [] Expr
    e

    -- | Gather top-level 'AsP'atterns and 'AnnP'atterns to expose underlying pattern.
    asView :: A.Pattern -> ([Name], [A.Expr], A.Pattern)
    asView :: Pattern -> ([Name], [Expr], Pattern)
    asView (A.AsP PatInfo
    _ BindName
    x Pattern
    p)  = (\([Name]
    asb, [Expr]
    ann, Pattern
    p) -> (BindName -> Name
    unBind BindName
    x Name -> [Name] -> [Name]
    forall a. a -> [a] -> [a]
    : [Name]
    asb, [Expr]
    ann, Pattern
    p)) (([Name], [Expr], Pattern) -> ([Name], [Expr], Pattern))
    -> ([Name], [Expr], Pattern) -> ([Name], [Expr], Pattern)
    forall a b. (a -> b) -> a -> b
    $ Pattern -> ([Name], [Expr], Pattern)
    asView Pattern
    p
    asView (A.AnnP PatInfo
    _ Expr
    a Pattern
    p) = (\([Name]
    asb, [Expr]
    ann, Pattern
    p) -> ([Name]
    asb, Expr
    a Expr -> [Expr] -> [Expr]
    forall a. a -> [a] -> [a]
    : [Expr]
    ann, Pattern
    p))        (([Name], [Expr], Pattern) -> ([Name], [Expr], Pattern))
    -> ([Name], [Expr], Pattern) -> ([Name], [Expr], Pattern)
    forall a b. (a -> b) -> a -> b
    $ Pattern -> ([Name], [Expr], Pattern)
    asView Pattern
    p
    asView Pattern
    p              = ([], [], Pattern
    p)

    -- | Remove top 'ScopedExpr' wrappers.
    unScope :: Expr -> Expr
    unScope :: Expr -> Expr
    unScope (ScopedExpr ScopeInfo
    scope Expr
    e) = Expr -> Expr
    unScope Expr
    e
    unScope (QuestionMark MetaInfo
    i InteractionId
    ii)  = MetaInfo -> InteractionId -> Expr
    QuestionMark (MetaInfo
    i {metaScope :: ScopeInfo
    metaScope = ScopeInfo
    forall a. Null a => a
    empty}) InteractionId
    ii
    unScope (Underscore MetaInfo
    i)       = MetaInfo -> Expr
    Underscore (MetaInfo
    i {metaScope :: ScopeInfo
    metaScope = ScopeInfo
    forall a. Null a => a
    empty})
    unScope Expr
    e                    = Expr
    e

    -- | Remove 'ScopedExpr' wrappers everywhere.
    --
    --   NB: Unless the implementation of 'ExprLike' for clauses
    --   has been finished, this does not work for clauses yet.
    deepUnscope :: ExprLike a => a -> a
    deepUnscope :: forall a. ExprLike a => a -> a
    deepUnscope = (Expr -> Expr) -> a -> a
    forall a. ExprLike a => (Expr -> Expr) -> a -> a
    mapExpr Expr -> Expr
    unScope

    deepUnscopeDecls :: [A.Declaration] -> [A.Declaration]
    deepUnscopeDecls :: [Declaration] -> [Declaration]
    deepUnscopeDecls = (Declaration -> [Declaration]) -> [Declaration] -> [Declaration]
    forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
    concatMap Declaration -> [Declaration]
    deepUnscopeDecl

    deepUnscopeDecl :: A.Declaration -> [A.Declaration]
    deepUnscopeDecl :: Declaration -> [Declaration]
    deepUnscopeDecl (A.ScopedDecl ScopeInfo
    _ [Declaration]
    ds)              = [Declaration] -> [Declaration]
    deepUnscopeDecls [Declaration]
    ds
    deepUnscopeDecl (A.Mutual MutualInfo
    i [Declaration]
    ds)                  = [MutualInfo -> [Declaration] -> Declaration
    A.Mutual MutualInfo
    i ([Declaration] -> [Declaration]
    deepUnscopeDecls [Declaration]
    ds)]
    deepUnscopeDecl (A.Section Range
    i ModuleName
    m GeneralizeTelescope
    tel [Declaration]
    ds)           = [Range
    -> ModuleName
    -> GeneralizeTelescope
    -> [Declaration]
    -> Declaration
    A.Section Range
    i ModuleName
    m (GeneralizeTelescope -> GeneralizeTelescope
    forall a. ExprLike a => a -> a
    deepUnscope GeneralizeTelescope
    tel) ([Declaration] -> [Declaration]
    deepUnscopeDecls [Declaration]
    ds)]
    deepUnscopeDecl (A.RecDef DefInfo
    i QName
    x UniverseCheck
    uc RecordDirectives
    dir DataDefParams
    bs Expr
    e [Declaration]
    ds) =
      [ DefInfo
    -> QName
    -> UniverseCheck
    -> RecordDirectives
    -> DataDefParams
    -> Expr
    -> [Declaration]
    -> Declaration
    A.RecDef DefInfo
    i QName
    x UniverseCheck
    uc RecordDirectives
    dir (DataDefParams -> DataDefParams
    forall a. ExprLike a => a -> a
    deepUnscope DataDefParams
    bs) (Expr -> Expr
    forall a. ExprLike a => a -> a
    deepUnscope Expr
    e) ([Declaration] -> [Declaration]
    deepUnscopeDecls [Declaration]
    ds) ]
    deepUnscopeDecl Declaration
    d                                = [Declaration -> Declaration
    forall a. ExprLike a => a -> a
    deepUnscope Declaration
    d]

    -- * Traversal
    ---------------------------------------------------------------------------

    -- Type aliases to abbreviate the quantified foralls which we use to avoid
    -- giving in to NoMonoLocalBinds.
    type RecurseExprFn m a = Applicative m => (Expr -> m Expr -> m Expr) -> a -> m a
    type RecurseExprRecFn m = forall a. ExprLike a => a -> m a

    type FoldExprFn m a = Monoid m => (Expr -> m) -> a -> m
    type FoldExprRecFn m = forall a. ExprLike a => a -> m

    type TraverseExprFn m a = (Applicative m, Monad m) => (Expr -> m Expr) -> a -> m a
    type TraverseExprRecFn m = forall a. ExprLike a => a -> m a

    -- | Apply an expression rewriting to every subexpression, inside-out.
    --   See "Agda.Syntax.Internal.Generic".
    class ExprLike a where
      -- | The first expression is pre-traversal, the second one post-traversal.
      recurseExpr :: RecurseExprFn m a
      default recurseExpr :: (Traversable f, ExprLike a', a ~ f a', Applicative m)
                          => (Expr -> m Expr -> m Expr) -> a -> m a
      recurseExpr = (a' -> m a') -> f a' -> m (f a')
    forall (t :: * -> *) (f :: * -> *) a b.
    (Traversable t, Applicative f) =>
    (a -> f b) -> t a -> f (t b)
    traverse ((a' -> m a') -> f a' -> m (f a'))
    -> ((Expr -> m Expr -> m Expr) -> a' -> m a')
    -> (Expr -> m Expr -> m Expr)
    -> f a'
    -> m (f a')
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Expr -> m Expr -> m Expr) -> a' -> m a'
    forall a (m :: * -> *). ExprLike a => RecurseExprFn m a
    recurseExpr

      foldExpr :: FoldExprFn m a
      foldExpr Expr -> m
    f = Const m a -> m
    forall {k} a (b :: k). Const a b -> a
    getConst (Const m a -> m) -> (a -> Const m a) -> a -> m
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Expr -> Const m Expr -> Const m Expr) -> a -> Const m a
    forall a (m :: * -> *). ExprLike a => RecurseExprFn m a
    recurseExpr (\ Expr
    pre Const m Expr
    post -> m -> Const m Expr
    forall {k} a (b :: k). a -> Const a b
    Const (Expr -> m
    f Expr
    pre) Const m Expr -> Const m Expr -> Const m Expr
    forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
    <* Const m Expr
    post)

      traverseExpr :: TraverseExprFn m a
      traverseExpr Expr -> m Expr
    f = (Expr -> m Expr -> m Expr) -> a -> m a
    forall a (m :: * -> *). ExprLike a => RecurseExprFn m a
    recurseExpr (\ Expr
    pre m Expr
    post -> Expr -> m Expr
    f (Expr -> m Expr) -> m Expr -> m Expr
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< m Expr
    post)

      mapExpr :: (Expr -> Expr) -> (a -> a)
      mapExpr Expr -> Expr
    f = Identity a -> a
    forall a. Identity a -> a
    runIdentity (Identity a -> a) -> (a -> Identity a) -> a -> a
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Expr -> Identity Expr) -> a -> Identity a
    forall a (m :: * -> *). ExprLike a => TraverseExprFn m a
    traverseExpr (Expr -> Identity Expr
    forall a. a -> Identity a
    Identity (Expr -> Identity Expr) -> (Expr -> Expr) -> Expr -> Identity Expr
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Expr -> Expr
    f)

    instance ExprLike Expr where
      recurseExpr :: forall m. RecurseExprFn m Expr
      recurseExpr :: forall (m :: * -> *). RecurseExprFn m Expr
    recurseExpr Expr -> m Expr -> m Expr
    f Expr
    e0 = Expr -> m Expr -> m Expr
    f Expr
    e0 (m Expr -> m Expr) -> m Expr -> m Expr
    forall a b. (a -> b) -> a -> b
    $ do
        let
          recurse :: RecurseExprRecFn m
          recurse :: RecurseExprRecFn m
    recurse a
    e = (Expr -> m Expr -> m Expr) -> a -> m a
    forall a (m :: * -> *). ExprLike a => RecurseExprFn m a
    recurseExpr Expr -> m Expr -> m Expr
    f a
    e
        case Expr
    e0 of
          Var{}                      -> Expr -> m Expr
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Expr
    e0
          Def'{}                     -> Expr -> m Expr
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Expr
    e0
          Proj{}                     -> Expr -> m Expr
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Expr
    e0
          Con{}                      -> Expr -> m Expr
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Expr
    e0
          Lit{}                      -> Expr -> m Expr
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Expr
    e0
          QuestionMark{}             -> Expr -> m Expr
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Expr
    e0
          Underscore{}               -> Expr -> m Expr
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Expr
    e0
          Dot ExprInfo
    ei Expr
    e                   -> ExprInfo -> Expr -> Expr
    Dot ExprInfo
    ei (Expr -> Expr) -> m Expr -> m Expr
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Expr -> m Expr
    RecurseExprRecFn m
    recurse Expr
    e
          App AppInfo
    ei Expr
    e NamedArg Expr
    arg               -> AppInfo -> Expr -> NamedArg Expr -> Expr
    App AppInfo
    ei (Expr -> NamedArg Expr -> Expr)
    -> m Expr -> m (NamedArg Expr -> Expr)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Expr -> m Expr
    RecurseExprRecFn m
    recurse Expr
    e m (NamedArg Expr -> Expr) -> m (NamedArg Expr) -> m Expr
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> NamedArg Expr -> m (NamedArg Expr)
    RecurseExprRecFn m
    recurse NamedArg Expr
    arg
          WithApp ExprInfo
    ei Expr
    e [Expr]
    es            -> ExprInfo -> Expr -> [Expr] -> Expr
    WithApp ExprInfo
    ei (Expr -> [Expr] -> Expr) -> m Expr -> m ([Expr] -> Expr)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Expr -> m Expr
    RecurseExprRecFn m
    recurse Expr
    e m ([Expr] -> Expr) -> m [Expr] -> m Expr
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> [Expr] -> m [Expr]
    RecurseExprRecFn m
    recurse [Expr]
    es
          Lam ExprInfo
    ei LamBinding
    b Expr
    e                 -> ExprInfo -> LamBinding -> Expr -> Expr
    Lam ExprInfo
    ei (LamBinding -> Expr -> Expr) -> m LamBinding -> m (Expr -> Expr)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> LamBinding -> m LamBinding
    RecurseExprRecFn m
    recurse LamBinding
    b m (Expr -> Expr) -> m Expr -> m Expr
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> Expr -> m Expr
    RecurseExprRecFn m
    recurse Expr
    e
          AbsurdLam{}                -> Expr -> m Expr
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Expr
    e0
          ExtendedLam ExprInfo
    ei DefInfo
    di Erased
    er QName
    x List1 Clause
    cls -> ExprInfo -> DefInfo -> Erased -> QName -> List1 Clause -> Expr
    ExtendedLam ExprInfo
    ei DefInfo
    di Erased
    er QName
    x (List1 Clause -> Expr) -> m (List1 Clause) -> m Expr
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> List1 Clause -> m (List1 Clause)
    RecurseExprRecFn m
    recurse List1 Clause
    cls
          Pi ExprInfo
    ei Telescope1
    tel Expr
    e                -> ExprInfo -> Telescope1 -> Expr -> Expr
    Pi ExprInfo
    ei (Telescope1 -> Expr -> Expr) -> m Telescope1 -> m (Expr -> Expr)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Telescope1 -> m Telescope1
    RecurseExprRecFn m
    recurse Telescope1
    tel m (Expr -> Expr) -> m Expr -> m Expr
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> Expr -> m Expr
    RecurseExprRecFn m
    recurse Expr
    e
          Generalized  Set QName
    s Expr
    e           -> Set QName -> Expr -> Expr
    Generalized Set QName
    s (Expr -> Expr) -> m Expr -> m Expr
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Expr -> m Expr
    RecurseExprRecFn m
    recurse Expr
    e
          Fun ExprInfo
    ei Arg Expr
    arg Expr
    e               -> ExprInfo -> Arg Expr -> Expr -> Expr
    Fun ExprInfo
    ei (Arg Expr -> Expr -> Expr) -> m (Arg Expr) -> m (Expr -> Expr)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Arg Expr -> m (Arg Expr)
    RecurseExprRecFn m
    recurse Arg Expr
    arg m (Expr -> Expr) -> m Expr -> m Expr
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> Expr -> m Expr
    RecurseExprRecFn m
    recurse Expr
    e
          Let ExprInfo
    ei List1 LetBinding
    bs Expr
    e                -> ExprInfo -> List1 LetBinding -> Expr -> Expr
    Let ExprInfo
    ei (List1 LetBinding -> Expr -> Expr)
    -> m (List1 LetBinding) -> m (Expr -> Expr)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> List1 LetBinding -> m (List1 LetBinding)
    RecurseExprRecFn m
    recurse List1 LetBinding
    bs m (Expr -> Expr) -> m Expr -> m Expr
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> Expr -> m Expr
    RecurseExprRecFn m
    recurse Expr
    e
          ETel Telescope
    tel                   -> Telescope -> Expr
    ETel (Telescope -> Expr) -> m Telescope -> m Expr
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Telescope -> m Telescope
    RecurseExprRecFn m
    recurse Telescope
    tel
          Rec ExprInfo
    ei RecordAssigns
    bs                  -> ExprInfo -> RecordAssigns -> Expr
    Rec ExprInfo
    ei (RecordAssigns -> Expr) -> m RecordAssigns -> m Expr
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> RecordAssigns -> m RecordAssigns
    RecurseExprRecFn m
    recurse RecordAssigns
    bs
          RecUpdate ExprInfo
    ei Expr
    e Assigns
    bs          -> ExprInfo -> Expr -> Assigns -> Expr
    RecUpdate ExprInfo
    ei (Expr -> Assigns -> Expr) -> m Expr -> m (Assigns -> Expr)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Expr -> m Expr
    RecurseExprRecFn m
    recurse Expr
    e m (Assigns -> Expr) -> m Assigns -> m Expr
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> Assigns -> m Assigns
    RecurseExprRecFn m
    recurse Assigns
    bs
          ScopedExpr ScopeInfo
    sc Expr
    e            -> ScopeInfo -> Expr -> Expr
    ScopedExpr ScopeInfo
    sc (Expr -> Expr) -> m Expr -> m Expr
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Expr -> m Expr
    RecurseExprRecFn m
    recurse Expr
    e
          Quote{}                    -> Expr -> m Expr
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Expr
    e0
          QuoteTerm{}                -> Expr -> m Expr
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Expr
    e0
          Unquote{}                  -> Expr -> m Expr
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Expr
    e0
          DontCare Expr
    e                 -> Expr -> Expr
    DontCare (Expr -> Expr) -> m Expr -> m Expr
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Expr -> m Expr
    RecurseExprRecFn m
    recurse Expr
    e
          PatternSyn{}               -> Expr -> m Expr
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Expr
    e0
          Macro{}                    -> Expr -> m Expr
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Expr
    e0

      foldExpr :: forall m. FoldExprFn m Expr
      foldExpr :: forall m. FoldExprFn m Expr
    foldExpr Expr -> m
    f Expr
    e =
        case Expr
    e of
          Var{}                  -> m
    m
          Def'{}                 -> m
    m
          Proj{}                 -> m
    m
          Con{}                  -> m
    m
          PatternSyn{}           -> m
    m
          Macro{}                -> m
    m
          Lit{}                  -> m
    m
          QuestionMark{}         -> m
    m
          Underscore{}           -> m
    m
          Dot ExprInfo
    _ Expr
    e                -> m
    m m -> m -> m
    forall a. Monoid a => a -> a -> a
    `mappend` Expr -> m
    FoldExprRecFn m
    fold Expr
    e
          App AppInfo
    _ Expr
    e NamedArg Expr
    e'             -> m
    m m -> m -> m
    forall a. Monoid a => a -> a -> a
    `mappend` Expr -> m
    FoldExprRecFn m
    fold Expr
    e m -> m -> m
    forall a. Monoid a => a -> a -> a
    `mappend` NamedArg Expr -> m
    FoldExprRecFn m
    fold NamedArg Expr
    e'
          WithApp ExprInfo
    _ Expr
    e [Expr]
    es         -> m
    m m -> m -> m
    forall a. Monoid a => a -> a -> a
    `mappend` Expr -> m
    FoldExprRecFn m
    fold Expr
    e m -> m -> m
    forall a. Monoid a => a -> a -> a
    `mappend` [Expr] -> m
    FoldExprRecFn m
    fold [Expr]
    es
          Lam ExprInfo
    _ LamBinding
    b Expr
    e              -> m
    m m -> m -> m
    forall a. Monoid a => a -> a -> a
    `mappend` LamBinding -> m
    FoldExprRecFn m
    fold LamBinding
    b m -> m -> m
    forall a. Monoid a => a -> a -> a
    `mappend` Expr -> m
    FoldExprRecFn m
    fold Expr
    e
          AbsurdLam{}            -> m
    m
          ExtendedLam ExprInfo
    _ DefInfo
    _ Erased
    _ QName
    _ List1 Clause
    cs -> m
    m m -> m -> m
    forall a. Monoid a => a -> a -> a
    `mappend` List1 Clause -> m
    FoldExprRecFn m
    fold List1 Clause
    cs
          Pi ExprInfo
    _ Telescope1
    tel Expr
    e             -> m
    m m -> m -> m
    forall a. Monoid a => a -> a -> a
    `mappend` Telescope1 -> m
    FoldExprRecFn m
    fold Telescope1
    tel m -> m -> m
    forall a. Monoid a => a -> a -> a
    `mappend` Expr -> m
    FoldExprRecFn m
    fold Expr
    e
          Generalized Set QName
    _ Expr
    e        -> m
    m m -> m -> m
    forall a. Monoid a => a -> a -> a
    `mappend` Expr -> m
    FoldExprRecFn m
    fold Expr
    e
          Fun ExprInfo
    _ Arg Expr
    e Expr
    e'             -> m
    m m -> m -> m
    forall a. Monoid a => a -> a -> a
    `mappend` Arg Expr -> m
    FoldExprRecFn m
    fold Arg Expr
    e m -> m -> m
    forall a. Monoid a => a -> a -> a
    `mappend` Expr -> m
    FoldExprRecFn m
    fold Expr
    e'
          Let ExprInfo
    _ List1 LetBinding
    bs Expr
    e             -> m
    m m -> m -> m
    forall a. Monoid a => a -> a -> a
    `mappend` List1 LetBinding -> m
    FoldExprRecFn m
    fold List1 LetBinding
    bs m -> m -> m
    forall a. Monoid a => a -> a -> a
    `mappend` Expr -> m
    FoldExprRecFn m
    fold Expr
    e
          ETel Telescope
    tel               -> m
    m m -> m -> m
    forall a. Monoid a => a -> a -> a
    `mappend` Telescope -> m
    FoldExprRecFn m
    fold Telescope
    tel
          Rec ExprInfo
    _ RecordAssigns
    as               -> m
    m m -> m -> m
    forall a. Monoid a => a -> a -> a
    `mappend` RecordAssigns -> m
    FoldExprRecFn m
    fold RecordAssigns
    as
          RecUpdate ExprInfo
    _ Expr
    e Assigns
    as       -> m
    m m -> m -> m
    forall a. Monoid a => a -> a -> a
    `mappend` Expr -> m
    FoldExprRecFn m
    fold Expr
    e m -> m -> m
    forall a. Monoid a => a -> a -> a
    `mappend` Assigns -> m
    FoldExprRecFn m
    fold Assigns
    as
          ScopedExpr ScopeInfo
    _ Expr
    e         -> m
    m m -> m -> m
    forall a. Monoid a => a -> a -> a
    `mappend` Expr -> m
    FoldExprRecFn m
    fold Expr
    e
          Quote{}                -> m
    m
          QuoteTerm{}            -> m
    m
          Unquote{}              -> m
    m
          DontCare Expr
    e             -> m
    m m -> m -> m
    forall a. Monoid a => a -> a -> a
    `mappend` Expr -> m
    FoldExprRecFn m
    fold Expr
    e
       where
         m :: m
    m = Expr -> m
    f Expr
    e
         fold :: FoldExprRecFn m
         fold :: FoldExprRecFn m
    fold = (Expr -> m) -> a -> m
    forall a m. ExprLike a => FoldExprFn m a
    foldExpr Expr -> m
    f

      traverseExpr :: forall m. TraverseExprFn m Expr
      traverseExpr :: forall (m :: * -> *). TraverseExprFn m Expr
    traverseExpr Expr -> m Expr
    f Expr
    e = do
        let
          trav :: TraverseExprRecFn m
          trav :: TraverseExprRecFn m
    trav a
    e = (Expr -> m Expr) -> a -> m a
    forall a (m :: * -> *). ExprLike a => TraverseExprFn m a
    traverseExpr Expr -> m Expr
    f a
    e
        case Expr
    e of
          Var{}                      -> Expr -> m Expr
    f Expr
    e
          Def'{}                     -> Expr -> m Expr
    f Expr
    e
          Proj{}                     -> Expr -> m Expr
    f Expr
    e
          Con{}                      -> Expr -> m Expr
    f Expr
    e
          Lit{}                      -> Expr -> m Expr
    f Expr
    e
          QuestionMark{}             -> Expr -> m Expr
    f Expr
    e
          Underscore{}               -> Expr -> m Expr
    f Expr
    e
          Dot ExprInfo
    ei Expr
    e                   -> Expr -> m Expr
    f (Expr -> m Expr) -> m Expr -> m Expr
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< ExprInfo -> Expr -> Expr
    Dot ExprInfo
    ei (Expr -> Expr) -> m Expr -> m Expr
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Expr -> m Expr
    TraverseExprRecFn m
    trav Expr
    e
          App AppInfo
    ei Expr
    e NamedArg Expr
    arg               -> Expr -> m Expr
    f (Expr -> m Expr) -> m Expr -> m Expr
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< AppInfo -> Expr -> NamedArg Expr -> Expr
    App AppInfo
    ei (Expr -> NamedArg Expr -> Expr)
    -> m Expr -> m (NamedArg Expr -> Expr)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Expr -> m Expr
    TraverseExprRecFn m
    trav Expr
    e m (NamedArg Expr -> Expr) -> m (NamedArg Expr) -> m Expr
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> NamedArg Expr -> m (NamedArg Expr)
    TraverseExprRecFn m
    trav NamedArg Expr
    arg
          WithApp ExprInfo
    ei Expr
    e [Expr]
    es            -> Expr -> m Expr
    f (Expr -> m Expr) -> m Expr -> m Expr
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< ExprInfo -> Expr -> [Expr] -> Expr
    WithApp ExprInfo
    ei (Expr -> [Expr] -> Expr) -> m Expr -> m ([Expr] -> Expr)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Expr -> m Expr
    TraverseExprRecFn m
    trav Expr
    e m ([Expr] -> Expr) -> m [Expr] -> m Expr
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> [Expr] -> m [Expr]
    TraverseExprRecFn m
    trav [Expr]
    es
          Lam ExprInfo
    ei LamBinding
    b Expr
    e                 -> Expr -> m Expr
    f (Expr -> m Expr) -> m Expr -> m Expr
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< ExprInfo -> LamBinding -> Expr -> Expr
    Lam ExprInfo
    ei (LamBinding -> Expr -> Expr) -> m LamBinding -> m (Expr -> Expr)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> LamBinding -> m LamBinding
    TraverseExprRecFn m
    trav LamBinding
    b m (Expr -> Expr) -> m Expr -> m Expr
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> Expr -> m Expr
    TraverseExprRecFn m
    trav Expr
    e
          AbsurdLam{}                -> Expr -> m Expr
    f Expr
    e
          ExtendedLam ExprInfo
    ei DefInfo
    di Erased
    re QName
    x List1 Clause
    cls -> Expr -> m Expr
    f (Expr -> m Expr) -> m Expr -> m Expr
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< ExprInfo -> DefInfo -> Erased -> QName -> List1 Clause -> Expr
    ExtendedLam ExprInfo
    ei DefInfo
    di Erased
    re QName
    x (List1 Clause -> Expr) -> m (List1 Clause) -> m Expr
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> List1 Clause -> m (List1 Clause)
    TraverseExprRecFn m
    trav List1 Clause
    cls
          Pi ExprInfo
    ei Telescope1
    tel Expr
    e                -> Expr -> m Expr
    f (Expr -> m Expr) -> m Expr -> m Expr
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< ExprInfo -> Telescope1 -> Expr -> Expr
    Pi ExprInfo
    ei (Telescope1 -> Expr -> Expr) -> m Telescope1 -> m (Expr -> Expr)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Telescope1 -> m Telescope1
    TraverseExprRecFn m
    trav Telescope1
    tel m (Expr -> Expr) -> m Expr -> m Expr
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> Expr -> m Expr
    TraverseExprRecFn m
    trav Expr
    e
          Generalized Set QName
    s Expr
    e            -> Expr -> m Expr
    f (Expr -> m Expr) -> m Expr -> m Expr
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< Set QName -> Expr -> Expr
    Generalized Set QName
    s (Expr -> Expr) -> m Expr -> m Expr
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Expr -> m Expr
    TraverseExprRecFn m
    trav Expr
    e
          Fun ExprInfo
    ei Arg Expr
    arg Expr
    e               -> Expr -> m Expr
    f (Expr -> m Expr) -> m Expr -> m Expr
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< ExprInfo -> Arg Expr -> Expr -> Expr
    Fun ExprInfo
    ei (Arg Expr -> Expr -> Expr) -> m (Arg Expr) -> m (Expr -> Expr)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Arg Expr -> m (Arg Expr)
    TraverseExprRecFn m
    trav Arg Expr
    arg m (Expr -> Expr) -> m Expr -> m Expr
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> Expr -> m Expr
    TraverseExprRecFn m
    trav Expr
    e
          Let ExprInfo
    ei List1 LetBinding
    bs Expr
    e                -> Expr -> m Expr
    f (Expr -> m Expr) -> m Expr -> m Expr
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< ExprInfo -> List1 LetBinding -> Expr -> Expr
    Let ExprInfo
    ei (List1 LetBinding -> Expr -> Expr)
    -> m (List1 LetBinding) -> m (Expr -> Expr)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> List1 LetBinding -> m (List1 LetBinding)
    TraverseExprRecFn m
    trav List1 LetBinding
    bs m (Expr -> Expr) -> m Expr -> m Expr
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> Expr -> m Expr
    TraverseExprRecFn m
    trav Expr
    e
          ETel Telescope
    tel                   -> Expr -> m Expr
    f (Expr -> m Expr) -> m Expr -> m Expr
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< Telescope -> Expr
    ETel (Telescope -> Expr) -> m Telescope -> m Expr
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Telescope -> m Telescope
    TraverseExprRecFn m
    trav Telescope
    tel
          Rec ExprInfo
    ei RecordAssigns
    bs                  -> Expr -> m Expr
    f (Expr -> m Expr) -> m Expr -> m Expr
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< ExprInfo -> RecordAssigns -> Expr
    Rec ExprInfo
    ei (RecordAssigns -> Expr) -> m RecordAssigns -> m Expr
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> RecordAssigns -> m RecordAssigns
    TraverseExprRecFn m
    trav RecordAssigns
    bs
          RecUpdate ExprInfo
    ei Expr
    e Assigns
    bs          -> Expr -> m Expr
    f (Expr -> m Expr) -> m Expr -> m Expr
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< ExprInfo -> Expr -> Assigns -> Expr
    RecUpdate ExprInfo
    ei (Expr -> Assigns -> Expr) -> m Expr -> m (Assigns -> Expr)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Expr -> m Expr
    TraverseExprRecFn m
    trav Expr
    e m (Assigns -> Expr) -> m Assigns -> m Expr
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> Assigns -> m Assigns
    TraverseExprRecFn m
    trav Assigns
    bs
          ScopedExpr ScopeInfo
    sc Expr
    e            -> Expr -> m Expr
    f (Expr -> m Expr) -> m Expr -> m Expr
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< ScopeInfo -> Expr -> Expr
    ScopedExpr ScopeInfo
    sc (Expr -> Expr) -> m Expr -> m Expr
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Expr -> m Expr
    TraverseExprRecFn m
    trav Expr
    e
          Quote{}                    -> Expr -> m Expr
    f Expr
    e
          QuoteTerm{}                -> Expr -> m Expr
    f Expr
    e
          Unquote{}                  -> Expr -> m Expr
    f Expr
    e
          DontCare Expr
    e                 -> Expr -> m Expr
    f (Expr -> m Expr) -> m Expr -> m Expr
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< Expr -> Expr
    DontCare (Expr -> Expr) -> m Expr -> m Expr
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Expr -> m Expr
    TraverseExprRecFn m
    trav Expr
    e
          PatternSyn{}               -> Expr -> m Expr
    f Expr
    e
          Macro{}                    -> Expr -> m Expr
    f Expr
    e

    instance ExprLike a => ExprLike (Arg a)
    instance ExprLike a => ExprLike (Maybe a)
    instance ExprLike a => ExprLike (Named x a)
    instance ExprLike a => ExprLike [a]
    instance ExprLike a => ExprLike (List1 a)

    instance (ExprLike a, ExprLike b) => ExprLike (a, b) where
      recurseExpr :: forall (m :: * -> *). RecurseExprFn m (a, b)
    recurseExpr Expr -> m 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 -> m Expr) -> a -> m a
    forall a (m :: * -> *). ExprLike a => RecurseExprFn m a
    recurseExpr Expr -> m Expr -> m Expr
    f a
    x m (b -> (a, b)) -> m b -> m (a, b)
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> (Expr -> m Expr -> m Expr) -> b -> m b
    forall a (m :: * -> *). ExprLike a => RecurseExprFn m a
    recurseExpr Expr -> m Expr -> m Expr
    f b
    y

    instance ExprLike Void where
      recurseExpr :: forall (m :: * -> *). RecurseExprFn m Void
    recurseExpr Expr -> m Expr -> m Expr
    f = Void -> m Void
    forall a. Void -> a
    absurd

    instance ExprLike a => ExprLike (FieldAssignment' a) where
      recurseExpr :: forall (m :: * -> *). RecurseExprFn m (FieldAssignment' a)
    recurseExpr = (a -> m a) -> FieldAssignment' a -> m (FieldAssignment' a)
    forall a. Lens' a (FieldAssignment' a)
    exprFieldA ((a -> m a) -> FieldAssignment' a -> m (FieldAssignment' a))
    -> ((Expr -> m Expr -> m Expr) -> a -> m a)
    -> (Expr -> m Expr -> m Expr)
    -> FieldAssignment' a
    -> m (FieldAssignment' a)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Expr -> m Expr -> m Expr) -> a -> m a
    forall a (m :: * -> *). ExprLike a => RecurseExprFn m a
    recurseExpr

    instance (ExprLike a, ExprLike b) => ExprLike (Either a b) where
      recurseExpr :: forall (m :: * -> *). RecurseExprFn m (Either a b)
    recurseExpr Expr -> m 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 -> m Expr) -> a -> m a
    forall a (m :: * -> *). ExprLike a => RecurseExprFn m a
    recurseExpr Expr -> m Expr -> m Expr
    f)
                                     ((Expr -> m Expr -> m Expr) -> b -> m b
    forall a (m :: * -> *). ExprLike a => RecurseExprFn m a
    recurseExpr Expr -> m Expr -> m Expr
    f)

    instance ExprLike BindName where
      recurseExpr :: forall (m :: * -> *). RecurseExprFn m BindName
    recurseExpr Expr -> m Expr -> m Expr
    f = BindName -> m BindName
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure

    instance ExprLike ModuleName where
      recurseExpr :: forall (m :: * -> *). RecurseExprFn m ModuleName
    recurseExpr Expr -> m Expr -> m Expr
    f = ModuleName -> m ModuleName
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure

    instance ExprLike QName where
      recurseExpr :: forall (m :: * -> *). RecurseExprFn m QName
    recurseExpr Expr -> m Expr -> m Expr
    _ = QName -> m QName
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure

    instance ExprLike LamBinding where
      recurseExpr :: forall (m :: * -> *). RecurseExprFn m LamBinding
    recurseExpr Expr -> m Expr -> m Expr
    f LamBinding
    e =
        case LamBinding
    e of
          DomainFree Maybe Expr
    t NamedArg Binder
    x -> Maybe Expr -> NamedArg Binder -> LamBinding
    DomainFree (Maybe Expr -> NamedArg Binder -> LamBinding)
    -> m (Maybe Expr) -> m (NamedArg Binder -> LamBinding)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (Expr -> m Expr -> m Expr) -> Maybe Expr -> m (Maybe Expr)
    forall a (m :: * -> *). ExprLike a => RecurseExprFn m a
    recurseExpr Expr -> m Expr -> m Expr
    f Maybe Expr
    t m (NamedArg Binder -> LamBinding)
    -> m (NamedArg Binder) -> m LamBinding
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> NamedArg Binder -> m (NamedArg Binder)
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure NamedArg Binder
    x
          DomainFull TypedBinding
    bs  -> TypedBinding -> LamBinding
    DomainFull (TypedBinding -> LamBinding) -> m TypedBinding -> m LamBinding
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (Expr -> m Expr -> m Expr) -> TypedBinding -> m TypedBinding
    forall a (m :: * -> *). ExprLike a => RecurseExprFn m a
    recurseExpr Expr -> m Expr -> m Expr
    f TypedBinding
    bs
      foldExpr :: forall m. FoldExprFn m LamBinding
    foldExpr Expr -> m
    f LamBinding
    e =
        case LamBinding
    e of
          DomainFree Maybe Expr
    t NamedArg Binder
    _ -> (Expr -> m) -> Maybe Expr -> m
    forall a m. ExprLike a => FoldExprFn m a
    foldExpr Expr -> m
    f Maybe Expr
    t
          DomainFull TypedBinding
    bs -> (Expr -> m) -> TypedBinding -> m
    forall a m. ExprLike a => FoldExprFn m a
    foldExpr Expr -> m
    f TypedBinding
    bs
      traverseExpr :: forall (m :: * -> *). TraverseExprFn m LamBinding
    traverseExpr Expr -> m Expr
    f LamBinding
    e =
        case LamBinding
    e of
          DomainFree Maybe Expr
    t NamedArg Binder
    x -> Maybe Expr -> NamedArg Binder -> LamBinding
    DomainFree (Maybe Expr -> NamedArg Binder -> LamBinding)
    -> m (Maybe Expr) -> m (NamedArg Binder -> LamBinding)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (Expr -> m Expr) -> Maybe Expr -> m (Maybe Expr)
    forall a (m :: * -> *). ExprLike a => TraverseExprFn m a
    traverseExpr Expr -> m Expr
    f Maybe Expr
    t m (NamedArg Binder -> LamBinding)
    -> m (NamedArg Binder) -> m LamBinding
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> NamedArg Binder -> m (NamedArg Binder)
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure NamedArg Binder
    x
          DomainFull TypedBinding
    bs  -> TypedBinding -> LamBinding
    DomainFull (TypedBinding -> LamBinding) -> m TypedBinding -> m LamBinding
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (Expr -> m Expr) -> TypedBinding -> m TypedBinding
    forall a (m :: * -> *). ExprLike a => TraverseExprFn m a
    traverseExpr Expr -> m Expr
    f TypedBinding
    bs

    instance ExprLike GeneralizeTelescope where
      recurseExpr :: forall (m :: * -> *). RecurseExprFn m GeneralizeTelescope
    recurseExpr  Expr -> m Expr -> m Expr
    f (GeneralizeTel Map QName Name
    s Telescope
    tel) = Map QName Name -> Telescope -> GeneralizeTelescope
    GeneralizeTel Map QName Name
    s (Telescope -> GeneralizeTelescope)
    -> m Telescope -> m GeneralizeTelescope
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (Expr -> m Expr -> m Expr) -> Telescope -> m Telescope
    forall a (m :: * -> *). ExprLike a => RecurseExprFn m a
    recurseExpr Expr -> m Expr -> m Expr
    f Telescope
    tel
      foldExpr :: forall m. FoldExprFn m GeneralizeTelescope
    foldExpr     Expr -> m
    f (GeneralizeTel Map QName Name
    s Telescope
    tel) = (Expr -> m) -> Telescope -> m
    forall a m. ExprLike a => FoldExprFn m a
    foldExpr Expr -> m
    f Telescope
    tel
      traverseExpr :: forall (m :: * -> *). TraverseExprFn m GeneralizeTelescope
    traverseExpr Expr -> m Expr
    f (GeneralizeTel Map QName Name
    s Telescope
    tel) = Map QName Name -> Telescope -> GeneralizeTelescope
    GeneralizeTel Map QName Name
    s (Telescope -> GeneralizeTelescope)
    -> m Telescope -> m GeneralizeTelescope
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (Expr -> m Expr) -> Telescope -> m Telescope
    forall a (m :: * -> *). ExprLike a => TraverseExprFn m a
    traverseExpr Expr -> m Expr
    f Telescope
    tel

    instance ExprLike DataDefParams where
      recurseExpr :: forall (m :: * -> *). RecurseExprFn m DataDefParams
    recurseExpr  Expr -> m Expr -> m Expr
    f (DataDefParams Set Name
    s [LamBinding]
    tel) = Set Name -> [LamBinding] -> DataDefParams
    DataDefParams Set Name
    s ([LamBinding] -> DataDefParams)
    -> m [LamBinding] -> m DataDefParams
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (Expr -> m Expr -> m Expr) -> [LamBinding] -> m [LamBinding]
    forall a (m :: * -> *). ExprLike a => RecurseExprFn m a
    recurseExpr Expr -> m Expr -> m Expr
    f [LamBinding]
    tel
      foldExpr :: forall m. FoldExprFn m DataDefParams
    foldExpr     Expr -> m
    f (DataDefParams Set Name
    s [LamBinding]
    tel) = (Expr -> m) -> [LamBinding] -> m
    forall a m. ExprLike a => FoldExprFn m a
    foldExpr Expr -> m
    f [LamBinding]
    tel
      traverseExpr :: forall (m :: * -> *). TraverseExprFn m DataDefParams
    traverseExpr Expr -> m Expr
    f (DataDefParams Set Name
    s [LamBinding]
    tel) = Set Name -> [LamBinding] -> DataDefParams
    DataDefParams Set Name
    s ([LamBinding] -> DataDefParams)
    -> m [LamBinding] -> m DataDefParams
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (Expr -> m Expr) -> [LamBinding] -> m [LamBinding]
    forall a (m :: * -> *). ExprLike a => TraverseExprFn m a
    traverseExpr Expr -> m Expr
    f [LamBinding]
    tel

    instance ExprLike TypedBinding where
      recurseExpr :: forall (m :: * -> *). RecurseExprFn m TypedBinding
    recurseExpr Expr -> m Expr -> m Expr
    f TypedBinding
    e =
        case TypedBinding
    e of
          TBind Range
    r Maybe Expr
    t List1 (NamedArg Binder)
    xs Expr
    e -> Range
    -> Maybe Expr -> List1 (NamedArg Binder) -> Expr -> TypedBinding
    TBind Range
    r (Maybe Expr -> List1 (NamedArg Binder) -> Expr -> TypedBinding)
    -> m (Maybe Expr)
    -> m (List1 (NamedArg Binder) -> Expr -> TypedBinding)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (Expr -> m Expr -> m Expr) -> Maybe Expr -> m (Maybe Expr)
    forall a (m :: * -> *). ExprLike a => RecurseExprFn m a
    recurseExpr Expr -> m Expr -> m Expr
    f Maybe Expr
    t m (List1 (NamedArg Binder) -> Expr -> TypedBinding)
    -> m (List1 (NamedArg Binder)) -> m (Expr -> TypedBinding)
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> List1 (NamedArg Binder) -> m (List1 (NamedArg Binder))
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure List1 (NamedArg Binder)
    xs m (Expr -> TypedBinding) -> m Expr -> m TypedBinding
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> (Expr -> m Expr -> m Expr) -> Expr -> m Expr
    forall a (m :: * -> *). ExprLike a => RecurseExprFn m a
    recurseExpr Expr -> m Expr -> m Expr
    f Expr
    e
          TLet Range
    r List1 LetBinding
    ds      -> Range -> List1 LetBinding -> TypedBinding
    TLet Range
    r (List1 LetBinding -> TypedBinding)
    -> m (List1 LetBinding) -> m TypedBinding
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (Expr -> m Expr -> m Expr)
    -> List1 LetBinding -> m (List1 LetBinding)
    forall a (m :: * -> *). ExprLike a => RecurseExprFn m a
    recurseExpr Expr -> m Expr -> m Expr
    f List1 LetBinding
    ds
      foldExpr :: forall m. FoldExprFn m TypedBinding
    foldExpr Expr -> m
    f TypedBinding
    e =
        case TypedBinding
    e of
          TBind Range
    _ Maybe Expr
    t List1 (NamedArg Binder)
    _ Expr
    e -> (Expr -> m) -> Maybe Expr -> m
    forall a m. ExprLike a => FoldExprFn m a
    foldExpr Expr -> m
    f Maybe Expr
    t m -> m -> m
    forall a. Monoid a => a -> a -> a
    `mappend` (Expr -> m) -> Expr -> m
    forall a m. ExprLike a => FoldExprFn m a
    foldExpr Expr -> m
    f Expr
    e
          TLet Range
    _ List1 LetBinding
    ds     -> (Expr -> m) -> List1 LetBinding -> m
    forall a m. ExprLike a => FoldExprFn m a
    foldExpr Expr -> m
    f List1 LetBinding
    ds
      traverseExpr :: forall (m :: * -> *). TraverseExprFn m TypedBinding
    traverseExpr Expr -> m Expr
    f TypedBinding
    e =
        case TypedBinding
    e of
          TBind Range
    r Maybe Expr
    t List1 (NamedArg Binder)
    xs Expr
    e -> Range
    -> Maybe Expr -> List1 (NamedArg Binder) -> Expr -> TypedBinding
    TBind Range
    r (Maybe Expr -> List1 (NamedArg Binder) -> Expr -> TypedBinding)
    -> m (Maybe Expr)
    -> m (List1 (NamedArg Binder) -> Expr -> TypedBinding)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (Expr -> m Expr) -> Maybe Expr -> m (Maybe Expr)
    forall a (m :: * -> *). ExprLike a => TraverseExprFn m a
    traverseExpr Expr -> m Expr
    f Maybe Expr
    t m (List1 (NamedArg Binder) -> Expr -> TypedBinding)
    -> m (List1 (NamedArg Binder)) -> m (Expr -> TypedBinding)
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> List1 (NamedArg Binder) -> m (List1 (NamedArg Binder))
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure List1 (NamedArg Binder)
    xs m (Expr -> TypedBinding) -> m Expr -> m TypedBinding
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> (Expr -> m Expr) -> Expr -> m Expr
    forall a (m :: * -> *). ExprLike a => TraverseExprFn m a
    traverseExpr Expr -> m Expr
    f Expr
    e
          TLet Range
    r List1 LetBinding
    ds      -> Range -> List1 LetBinding -> TypedBinding
    TLet Range
    r (List1 LetBinding -> TypedBinding)
    -> m (List1 LetBinding) -> m TypedBinding
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (Expr -> m Expr) -> List1 LetBinding -> m (List1 LetBinding)
    forall a (m :: * -> *). ExprLike a => TraverseExprFn m a
    traverseExpr Expr -> m Expr
    f List1 LetBinding
    ds

    instance ExprLike LetBinding where
      recurseExpr :: forall m. RecurseExprFn m LetBinding
      recurseExpr :: forall (m :: * -> *). RecurseExprFn m LetBinding
    recurseExpr Expr -> m Expr -> m Expr
    f LetBinding
    e = do
        let
          recurse :: RecurseExprRecFn m
          recurse :: RecurseExprRecFn m
    recurse a
    e = (Expr -> m Expr -> m Expr) -> a -> m a
    forall a (m :: * -> *). ExprLike a => RecurseExprFn m a
    recurseExpr Expr -> m Expr -> m Expr
    f a
    e
        case LetBinding
    e of
          LetBind LetInfo
    li ArgInfo
    ai BindName
    x Expr
    e Expr
    e'  -> LetInfo -> ArgInfo -> BindName -> Expr -> Expr -> LetBinding
    LetBind LetInfo
    li ArgInfo
    ai BindName
    x (Expr -> Expr -> LetBinding) -> m Expr -> m (Expr -> LetBinding)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Expr -> m Expr
    RecurseExprRecFn m
    recurse Expr
    e m (Expr -> LetBinding) -> m Expr -> m LetBinding
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> Expr -> m Expr
    RecurseExprRecFn m
    recurse Expr
    e'
          LetPatBind LetInfo
    li Pattern
    p Expr
    e     -> LetInfo -> Pattern -> Expr -> LetBinding
    LetPatBind LetInfo
    li (Pattern -> Expr -> LetBinding)
    -> m Pattern -> m (Expr -> LetBinding)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Pattern -> m Pattern
    RecurseExprRecFn m
    recurse Pattern
    p m (Expr -> LetBinding) -> m Expr -> m LetBinding
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> Expr -> m Expr
    RecurseExprRecFn m
    recurse Expr
    e
          LetApply{}            -> LetBinding -> m LetBinding
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure LetBinding
    e
          LetOpen{}             -> LetBinding -> m LetBinding
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure LetBinding
    e
          LetDeclaredVariable BindName
    _ -> LetBinding -> m LetBinding
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure LetBinding
    e

      foldExpr :: forall m. FoldExprFn m LetBinding
      foldExpr :: forall m. FoldExprFn m LetBinding
    foldExpr Expr -> m
    f LetBinding
    e =
        case LetBinding
    e of
          LetBind LetInfo
    _ ArgInfo
    _ BindName
    _ Expr
    e Expr
    e'    -> Expr -> m
    FoldExprRecFn m
    fold Expr
    e m -> m -> m
    forall a. Monoid a => a -> a -> a
    `mappend` Expr -> m
    FoldExprRecFn m
    fold Expr
    e'
          LetPatBind LetInfo
    _ Pattern
    p Expr
    e      -> Pattern -> m
    FoldExprRecFn m
    fold Pattern
    p m -> m -> m
    forall a. Monoid a => a -> a -> a
    `mappend` Expr -> m
    FoldExprRecFn m
    fold Expr
    e
          LetApply{}            -> m
    forall a. Monoid a => a
    mempty
          LetOpen{}             -> m
    forall a. Monoid a => a
    mempty
          LetDeclaredVariable BindName
    _ -> m
    forall a. Monoid a => a
    mempty
        where
          fold :: FoldExprRecFn m
          fold :: FoldExprRecFn m
    fold a
    e = (Expr -> m) -> a -> m
    forall a m. ExprLike a => FoldExprFn m a
    foldExpr Expr -> m
    f a
    e

      traverseExpr :: forall m. TraverseExprFn m LetBinding
      traverseExpr :: forall (m :: * -> *). TraverseExprFn m LetBinding
    traverseExpr Expr -> m Expr
    f LetBinding
    e = do
        let
          trav :: TraverseExprRecFn m
          trav :: TraverseExprRecFn m
    trav a
    e = (Expr -> m Expr) -> a -> m a
    forall a (m :: * -> *). ExprLike a => TraverseExprFn m a
    traverseExpr Expr -> m Expr
    f a
    e
        case LetBinding
    e of
          LetBind LetInfo
    li ArgInfo
    ai BindName
    x Expr
    e Expr
    e'  -> LetInfo -> ArgInfo -> BindName -> Expr -> Expr -> LetBinding
    LetBind LetInfo
    li ArgInfo
    ai BindName
    x (Expr -> Expr -> LetBinding) -> m Expr -> m (Expr -> LetBinding)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Expr -> m Expr
    TraverseExprRecFn m
    trav Expr
    e m (Expr -> LetBinding) -> m Expr -> m LetBinding
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> Expr -> m Expr
    TraverseExprRecFn m
    trav Expr
    e'
          LetPatBind LetInfo
    li Pattern
    p Expr
    e     -> LetInfo -> Pattern -> Expr -> LetBinding
    LetPatBind LetInfo
    li (Pattern -> Expr -> LetBinding)
    -> m Pattern -> m (Expr -> LetBinding)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Pattern -> m Pattern
    TraverseExprRecFn m
    trav Pattern
    p m (Expr -> LetBinding) -> m Expr -> m LetBinding
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> Expr -> m Expr
    TraverseExprRecFn m
    trav Expr
    e
          LetApply{}            -> LetBinding -> m LetBinding
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure LetBinding
    e
          LetOpen{}             -> LetBinding -> m LetBinding
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure LetBinding
    e
          LetDeclaredVariable BindName
    _ -> LetBinding -> m LetBinding
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure LetBinding
    e

    instance ExprLike a => ExprLike (Pattern' a) where

    instance ExprLike a => ExprLike (Clause' a) where
      recurseExpr :: forall m. RecurseExprFn m (Clause' a)
      recurseExpr :: forall (m :: * -> *). RecurseExprFn m (Clause' a)
    recurseExpr Expr -> m Expr -> m Expr
    f (Clause a
    lhs [ProblemEq]
    spats RHS
    rhs WhereDeclarations
    ds Bool
    ca) = a -> [ProblemEq] -> RHS -> WhereDeclarations -> Bool -> Clause' a
    forall lhs.
    lhs
    -> [ProblemEq] -> RHS -> WhereDeclarations -> Bool -> Clause' lhs
    Clause (a -> [ProblemEq] -> RHS -> WhereDeclarations -> Bool -> Clause' a)
    -> m a
    -> m ([ProblemEq] -> RHS -> WhereDeclarations -> Bool -> Clause' a)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> a -> m a
    RecurseExprRecFn m
    rec a
    lhs m ([ProblemEq] -> RHS -> WhereDeclarations -> Bool -> Clause' a)
    -> m [ProblemEq]
    -> m (RHS -> WhereDeclarations -> Bool -> Clause' a)
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> [ProblemEq] -> m [ProblemEq]
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure [ProblemEq]
    spats m (RHS -> WhereDeclarations -> Bool -> Clause' a)
    -> m RHS -> m (WhereDeclarations -> Bool -> Clause' a)
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> RHS -> m RHS
    RecurseExprRecFn m
    rec RHS
    rhs m (WhereDeclarations -> Bool -> Clause' a)
    -> m WhereDeclarations -> m (Bool -> Clause' a)
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> WhereDeclarations -> m WhereDeclarations
    RecurseExprRecFn m
    rec WhereDeclarations
    ds m (Bool -> Clause' a) -> m Bool -> m (Clause' a)
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> Bool -> m Bool
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Bool
    ca
        where
          rec :: RecurseExprRecFn m
          rec :: RecurseExprRecFn m
    rec = (Expr -> m Expr -> m Expr) -> a -> m a
    forall a (m :: * -> *). ExprLike a => RecurseExprFn m a
    recurseExpr Expr -> m Expr -> m Expr
    f

    instance ExprLike RHS where
      recurseExpr :: forall m. RecurseExprFn m RHS
      recurseExpr :: forall (m :: * -> *). RecurseExprFn m RHS
    recurseExpr Expr -> m Expr -> m Expr
    f RHS
    rhs =
        case RHS
    rhs of
          RHS Expr
    e Maybe Expr
    c                 -> Expr -> Maybe Expr -> RHS
    RHS (Expr -> Maybe Expr -> RHS) -> m Expr -> m (Maybe Expr -> RHS)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Expr -> m Expr
    RecurseExprRecFn m
    rec Expr
    e m (Maybe Expr -> RHS) -> m (Maybe Expr) -> m RHS
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> Maybe Expr -> m (Maybe Expr)
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Maybe Expr
    c
          AbsurdRHS{}             -> RHS -> m RHS
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure RHS
    rhs
          WithRHS QName
    x [WithExpr]
    es [Clause]
    cs         -> QName -> [WithExpr] -> [Clause] -> RHS
    WithRHS QName
    x ([WithExpr] -> [Clause] -> RHS)
    -> m [WithExpr] -> m ([Clause] -> RHS)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> [WithExpr] -> m [WithExpr]
    RecurseExprRecFn m
    rec [WithExpr]
    es m ([Clause] -> RHS) -> m [Clause] -> m RHS
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> [Clause] -> m [Clause]
    RecurseExprRecFn m
    rec [Clause]
    cs
          RewriteRHS [RewriteEqn]
    xes [ProblemEq]
    spats RHS
    rhs WhereDeclarations
    ds -> [RewriteEqn] -> [ProblemEq] -> RHS -> WhereDeclarations -> RHS
    RewriteRHS ([RewriteEqn] -> [ProblemEq] -> RHS -> WhereDeclarations -> RHS)
    -> m [RewriteEqn]
    -> m ([ProblemEq] -> RHS -> WhereDeclarations -> RHS)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> [RewriteEqn] -> m [RewriteEqn]
    RecurseExprRecFn m
    rec [RewriteEqn]
    xes m ([ProblemEq] -> RHS -> WhereDeclarations -> RHS)
    -> m [ProblemEq] -> m (RHS -> WhereDeclarations -> RHS)
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> [ProblemEq] -> m [ProblemEq]
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure [ProblemEq]
    spats m (RHS -> WhereDeclarations -> RHS)
    -> m RHS -> m (WhereDeclarations -> RHS)
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> RHS -> m RHS
    RecurseExprRecFn m
    rec RHS
    rhs m (WhereDeclarations -> RHS) -> m WhereDeclarations -> m RHS
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> WhereDeclarations -> m WhereDeclarations
    RecurseExprRecFn m
    rec WhereDeclarations
    ds
        where
          rec :: RecurseExprRecFn m
          rec :: RecurseExprRecFn m
    rec a
    e = (Expr -> m Expr -> m Expr) -> a -> m a
    forall a (m :: * -> *). ExprLike a => RecurseExprFn m a
    recurseExpr Expr -> m Expr -> m Expr
    f a
    e

    instance (ExprLike qn, ExprLike nm, ExprLike p, ExprLike e) => ExprLike (RewriteEqn' qn nm p e) where
      recurseExpr :: forall (m :: * -> *). RecurseExprFn m (RewriteEqn' qn nm p e)
    recurseExpr Expr -> m Expr -> m 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 (List1 (qn, e) -> RewriteEqn' qn nm p e)
    -> m (List1 (qn, e)) -> m (RewriteEqn' qn nm p e)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (Expr -> m Expr -> m Expr) -> List1 (qn, e) -> m (List1 (qn, e))
    forall a (m :: * -> *). ExprLike a => RecurseExprFn m a
    recurseExpr Expr -> m Expr -> m 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 -> List1 (Named nm (p, e)) -> RewriteEqn' qn nm p e)
    -> m qn -> m (List1 (Named nm (p, e)) -> RewriteEqn' qn nm p e)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (Expr -> m Expr -> m Expr) -> qn -> m qn
    forall a (m :: * -> *). ExprLike a => RecurseExprFn m a
    recurseExpr Expr -> m Expr -> m Expr
    f qn
    qn m (List1 (Named nm (p, e)) -> RewriteEqn' qn nm p e)
    -> m (List1 (Named nm (p, e))) -> m (RewriteEqn' qn nm p e)
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> (Expr -> m Expr -> m Expr)
    -> List1 (Named nm (p, e)) -> m (List1 (Named nm (p, e)))
    forall a (m :: * -> *). ExprLike a => RecurseExprFn m a
    recurseExpr Expr -> m Expr -> m Expr
    f List1 (Named nm (p, e))
    pes

    instance ExprLike WhereDeclarations where
      recurseExpr :: forall (m :: * -> *). RecurseExprFn m WhereDeclarations
    recurseExpr Expr -> m Expr -> m Expr
    f (WhereDecls Maybe ModuleName
    a Maybe Declaration
    b) = Maybe ModuleName -> Maybe Declaration -> WhereDeclarations
    WhereDecls Maybe ModuleName
    a (Maybe Declaration -> WhereDeclarations)
    -> m (Maybe Declaration) -> m WhereDeclarations
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (Expr -> m Expr -> m Expr)
    -> Maybe Declaration -> m (Maybe Declaration)
    forall a (m :: * -> *). ExprLike a => RecurseExprFn m a
    recurseExpr Expr -> m Expr -> m Expr
    f Maybe Declaration
    b

    instance ExprLike ModuleApplication where
      recurseExpr :: forall m. RecurseExprFn m ModuleApplication
      recurseExpr :: forall (m :: * -> *). RecurseExprFn m ModuleApplication
    recurseExpr Expr -> m Expr -> m Expr
    f ModuleApplication
    a =
        case ModuleApplication
    a of
          SectionApp Telescope
    tel ModuleName
    m [NamedArg Expr]
    es -> Telescope -> ModuleName -> [NamedArg Expr] -> ModuleApplication
    SectionApp (Telescope -> ModuleName -> [NamedArg Expr] -> ModuleApplication)
    -> m Telescope
    -> m (ModuleName -> [NamedArg Expr] -> ModuleApplication)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Telescope -> m Telescope
    RecurseExprRecFn m
    rec Telescope
    tel m (ModuleName -> [NamedArg Expr] -> ModuleApplication)
    -> m ModuleName -> m ([NamedArg Expr] -> ModuleApplication)
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> ModuleName -> m ModuleName
    RecurseExprRecFn m
    rec ModuleName
    m m ([NamedArg Expr] -> ModuleApplication)
    -> m [NamedArg Expr] -> m ModuleApplication
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> [NamedArg Expr] -> m [NamedArg Expr]
    RecurseExprRecFn m
    rec [NamedArg Expr]
    es
          RecordModuleInstance{} -> ModuleApplication -> m ModuleApplication
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure ModuleApplication
    a
        where
          rec :: RecurseExprRecFn m
          rec :: RecurseExprRecFn m
    rec a
    e = (Expr -> m Expr -> m Expr) -> a -> m a
    forall a (m :: * -> *). ExprLike a => RecurseExprFn m a
    recurseExpr Expr -> m Expr -> m Expr
    f a
    e

    instance ExprLike Pragma where
      recurseExpr :: forall m. RecurseExprFn m Pragma
      recurseExpr :: forall (m :: * -> *). RecurseExprFn m Pragma
    recurseExpr Expr -> m Expr -> m Expr
    f Pragma
    p =
        case Pragma
    p of
          BuiltinPragma RString
    s ResolvedName
    x           -> Pragma -> m Pragma
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Pragma
    p
          OptionsPragma{}             -> Pragma -> m Pragma
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Pragma
    p
          BuiltinNoDefPragma{}        -> Pragma -> m Pragma
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Pragma
    p
          RewritePragma{}             -> Pragma -> m Pragma
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Pragma
    p
          CompilePragma{}             -> Pragma -> m Pragma
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Pragma
    p
          StaticPragma{}              -> Pragma -> m Pragma
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Pragma
    p
          InjectivePragma{}           -> Pragma -> m Pragma
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Pragma
    p
          InlinePragma{}              -> Pragma -> m Pragma
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Pragma
    p
          EtaPragma{}                 -> Pragma -> m Pragma
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Pragma
    p
          DisplayPragma QName
    f [NamedArg Pattern]
    xs Expr
    e        -> QName -> [NamedArg Pattern] -> Expr -> Pragma
    DisplayPragma QName
    f ([NamedArg Pattern] -> Expr -> Pragma)
    -> m [NamedArg Pattern] -> m (Expr -> Pragma)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> [NamedArg Pattern] -> m [NamedArg Pattern]
    RecurseExprRecFn m
    rec [NamedArg Pattern]
    xs m (Expr -> Pragma) -> m Expr -> m Pragma
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> Expr -> m Expr
    RecurseExprRecFn m
    rec Expr
    e
        where
          rec :: RecurseExprRecFn m
          rec :: RecurseExprRecFn m
    rec a
    e = (Expr -> m Expr -> m Expr) -> a -> m a
    forall a (m :: * -> *). ExprLike a => RecurseExprFn m a
    recurseExpr Expr -> m Expr -> m Expr
    f a
    e

    instance ExprLike LHS where
      recurseExpr :: forall (m :: * -> *). RecurseExprFn m LHS
    recurseExpr Expr -> m Expr -> m Expr
    f (LHS LHSInfo
    i LHSCore
    p) = LHSInfo -> LHSCore -> LHS
    LHS LHSInfo
    i (LHSCore -> LHS) -> m LHSCore -> m LHS
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (Expr -> m Expr -> m Expr) -> LHSCore -> m LHSCore
    forall a (m :: * -> *). ExprLike a => RecurseExprFn m a
    recurseExpr Expr -> m Expr -> m Expr
    f LHSCore
    p

    instance ExprLike a => ExprLike (LHSCore' a)   where
    instance ExprLike a => ExprLike (WithHiding a) where

    instance ExprLike SpineLHS where
      recurseExpr :: forall (m :: * -> *). RecurseExprFn m SpineLHS
    recurseExpr Expr -> m Expr -> m Expr
    f (SpineLHS LHSInfo
    i QName
    x [NamedArg Pattern]
    ps) = LHSInfo -> QName -> [NamedArg Pattern] -> SpineLHS
    SpineLHS LHSInfo
    i QName
    x ([NamedArg Pattern] -> SpineLHS)
    -> m [NamedArg Pattern] -> m SpineLHS
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (Expr -> m Expr -> m Expr)
    -> [NamedArg Pattern] -> m [NamedArg Pattern]
    forall a (m :: * -> *). ExprLike a => RecurseExprFn m a
    recurseExpr Expr -> m Expr -> m Expr
    f [NamedArg Pattern]
    ps

    instance ExprLike Declaration where
      recurseExpr :: forall m. RecurseExprFn m Declaration
      recurseExpr :: forall (m :: * -> *). RecurseExprFn m Declaration
    recurseExpr Expr -> m Expr -> m Expr
    f Declaration
    d =
        case Declaration
    d of
          Axiom KindOfName
    a DefInfo
    d ArgInfo
    i Maybe [Occurrence]
    mp QName
    x Expr
    e        -> KindOfName
    -> DefInfo
    -> ArgInfo
    -> Maybe [Occurrence]
    -> QName
    -> Expr
    -> Declaration
    Axiom KindOfName
    a DefInfo
    d ArgInfo
    i Maybe [Occurrence]
    mp QName
    x (Expr -> Declaration) -> m Expr -> m Declaration
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Expr -> m Expr
    RecurseExprRecFn m
    rec Expr
    e
          Generalize Set QName
    s DefInfo
    i ArgInfo
    j QName
    x Expr
    e      -> Set QName -> DefInfo -> ArgInfo -> QName -> Expr -> Declaration
    Generalize Set QName
    s DefInfo
    i ArgInfo
    j QName
    x (Expr -> Declaration) -> m Expr -> m Declaration
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Expr -> m Expr
    RecurseExprRecFn m
    rec Expr
    e
          Field DefInfo
    i QName
    x Arg Expr
    e               -> DefInfo -> QName -> Arg Expr -> Declaration
    Field DefInfo
    i QName
    x (Arg Expr -> Declaration) -> m (Arg Expr) -> m Declaration
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Arg Expr -> m (Arg Expr)
    RecurseExprRecFn m
    rec Arg Expr
    e
          Primitive DefInfo
    i QName
    x Arg Expr
    e           -> DefInfo -> QName -> Arg Expr -> Declaration
    Primitive DefInfo
    i QName
    x (Arg Expr -> Declaration) -> m (Arg Expr) -> m Declaration
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Arg Expr -> m (Arg Expr)
    RecurseExprRecFn m
    rec Arg Expr
    e
          Mutual MutualInfo
    i [Declaration]
    ds               -> MutualInfo -> [Declaration] -> Declaration
    Mutual MutualInfo
    i ([Declaration] -> Declaration) -> m [Declaration] -> m Declaration
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> [Declaration] -> m [Declaration]
    RecurseExprRecFn m
    rec [Declaration]
    ds
          Section Range
    i ModuleName
    m GeneralizeTelescope
    tel [Declaration]
    ds        -> Range
    -> ModuleName
    -> GeneralizeTelescope
    -> [Declaration]
    -> Declaration
    Section Range
    i ModuleName
    m (GeneralizeTelescope -> [Declaration] -> Declaration)
    -> m GeneralizeTelescope -> m ([Declaration] -> Declaration)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> GeneralizeTelescope -> m GeneralizeTelescope
    RecurseExprRecFn m
    rec GeneralizeTelescope
    tel m ([Declaration] -> Declaration)
    -> m [Declaration] -> m Declaration
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> [Declaration] -> m [Declaration]
    RecurseExprRecFn m
    rec [Declaration]
    ds
          Apply ModuleInfo
    i ModuleName
    m ModuleApplication
    a ScopeCopyInfo
    ci ImportDirective
    d          -> (\ ModuleApplication
    a -> ModuleInfo
    -> ModuleName
    -> ModuleApplication
    -> ScopeCopyInfo
    -> ImportDirective
    -> Declaration
    Apply ModuleInfo
    i ModuleName
    m ModuleApplication
    a ScopeCopyInfo
    ci ImportDirective
    d) (ModuleApplication -> Declaration)
    -> m ModuleApplication -> m Declaration
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> ModuleApplication -> m ModuleApplication
    RecurseExprRecFn m
    rec ModuleApplication
    a
          Import{}                  -> Declaration -> m Declaration
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Declaration
    d
          Pragma Range
    i Pragma
    p                -> Range -> Pragma -> Declaration
    Pragma Range
    i (Pragma -> Declaration) -> m Pragma -> m Declaration
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Pragma -> m Pragma
    RecurseExprRecFn m
    rec Pragma
    p
          Open{}                    -> Declaration -> m Declaration
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Declaration
    d
          FunDef DefInfo
    i QName
    f Delayed
    d [Clause]
    cs           -> DefInfo -> QName -> Delayed -> [Clause] -> Declaration
    FunDef DefInfo
    i QName
    f Delayed
    d ([Clause] -> Declaration) -> m [Clause] -> m Declaration
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> [Clause] -> m [Clause]
    RecurseExprRecFn m
    rec [Clause]
    cs
          DataSig DefInfo
    i QName
    d GeneralizeTelescope
    tel Expr
    e         -> DefInfo -> QName -> GeneralizeTelescope -> Expr -> Declaration
    DataSig DefInfo
    i QName
    d (GeneralizeTelescope -> Expr -> Declaration)
    -> m GeneralizeTelescope -> m (Expr -> Declaration)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> GeneralizeTelescope -> m GeneralizeTelescope
    RecurseExprRecFn m
    rec GeneralizeTelescope
    tel m (Expr -> Declaration) -> m Expr -> m Declaration
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> Expr -> m Expr
    RecurseExprRecFn m
    rec Expr
    e
          DataDef DefInfo
    i QName
    d UniverseCheck
    uc DataDefParams
    bs [Declaration]
    cs      -> DefInfo
    -> QName
    -> UniverseCheck
    -> DataDefParams
    -> [Declaration]
    -> Declaration
    DataDef DefInfo
    i QName
    d UniverseCheck
    uc (DataDefParams -> [Declaration] -> Declaration)
    -> m DataDefParams -> m ([Declaration] -> Declaration)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> DataDefParams -> m DataDefParams
    RecurseExprRecFn m
    rec DataDefParams
    bs m ([Declaration] -> Declaration)
    -> m [Declaration] -> m Declaration
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> [Declaration] -> m [Declaration]
    RecurseExprRecFn m
    rec [Declaration]
    cs
          RecSig DefInfo
    i QName
    r GeneralizeTelescope
    tel Expr
    e          -> DefInfo -> QName -> GeneralizeTelescope -> Expr -> Declaration
    RecSig DefInfo
    i QName
    r (GeneralizeTelescope -> Expr -> Declaration)
    -> m GeneralizeTelescope -> m (Expr -> Declaration)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> GeneralizeTelescope -> m GeneralizeTelescope
    RecurseExprRecFn m
    rec GeneralizeTelescope
    tel m (Expr -> Declaration) -> m Expr -> m Declaration
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> Expr -> m Expr
    RecurseExprRecFn m
    rec Expr
    e
          RecDef DefInfo
    i QName
    r UniverseCheck
    uc RecordDirectives
    dir DataDefParams
    bs Expr
    e [Declaration]
    ds -> DefInfo
    -> QName
    -> UniverseCheck
    -> RecordDirectives
    -> DataDefParams
    -> Expr
    -> [Declaration]
    -> Declaration
    RecDef DefInfo
    i QName
    r UniverseCheck
    uc RecordDirectives
    dir (DataDefParams -> Expr -> [Declaration] -> Declaration)
    -> m DataDefParams -> m (Expr -> [Declaration] -> Declaration)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> DataDefParams -> m DataDefParams
    RecurseExprRecFn m
    rec DataDefParams
    bs m (Expr -> [Declaration] -> Declaration)
    -> m Expr -> m ([Declaration] -> Declaration)
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> Expr -> m Expr
    RecurseExprRecFn m
    rec Expr
    e m ([Declaration] -> Declaration)
    -> m [Declaration] -> m Declaration
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> [Declaration] -> m [Declaration]
    RecurseExprRecFn m
    rec [Declaration]
    ds
          PatternSynDef QName
    f [Arg BindName]
    xs Pattern' Void
    p      -> QName -> [Arg BindName] -> Pattern' Void -> Declaration
    PatternSynDef QName
    f [Arg BindName]
    xs (Pattern' Void -> Declaration)
    -> m (Pattern' Void) -> m Declaration
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Pattern' Void -> m (Pattern' Void)
    RecurseExprRecFn m
    rec Pattern' Void
    p
          UnquoteDecl MutualInfo
    i [DefInfo]
    is [QName]
    xs Expr
    e     -> MutualInfo -> [DefInfo] -> [QName] -> Expr -> Declaration
    UnquoteDecl MutualInfo
    i [DefInfo]
    is [QName]
    xs (Expr -> Declaration) -> m Expr -> m Declaration
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Expr -> m Expr
    RecurseExprRecFn m
    rec Expr
    e
          UnquoteDef [DefInfo]
    i [QName]
    xs Expr
    e         -> [DefInfo] -> [QName] -> Expr -> Declaration
    UnquoteDef [DefInfo]
    i [QName]
    xs (Expr -> Declaration) -> m Expr -> m Declaration
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Expr -> m Expr
    RecurseExprRecFn m
    rec Expr
    e
          ScopedDecl ScopeInfo
    s [Declaration]
    ds           -> ScopeInfo -> [Declaration] -> Declaration
    ScopedDecl ScopeInfo
    s ([Declaration] -> Declaration) -> m [Declaration] -> m Declaration
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> [Declaration] -> m [Declaration]
    RecurseExprRecFn m
    rec [Declaration]
    ds
        where
          rec :: RecurseExprRecFn m
          rec :: RecurseExprRecFn m
    rec a
    e = (Expr -> m Expr -> m Expr) -> a -> m a
    forall a (m :: * -> *). ExprLike a => RecurseExprFn m a
    recurseExpr Expr -> m Expr -> m Expr
    f a
    e

    -- * Getting all declared names
    ---------------------------------------------------------------------------

    type KName = WithKind QName

    -- | Extracts "all" names which are declared in a 'Declaration'.
    --
    -- Includes: local modules and @where@ clauses.
    -- Excludes: @open public@, @let@, @with@ function names, extended lambdas.

    class DeclaredNames a where
      declaredNames :: Collection KName m => a -> m

      default declaredNames
         :: (Foldable t, DeclaredNames b, t b ~ a)
         => Collection KName m => a -> m
      declaredNames = (b -> m) -> t b -> m
    forall (t :: * -> *) m a.
    (Foldable t, Monoid m) =>
    (a -> m) -> t a -> m
    foldMap b -> m
    forall a m. (DeclaredNames a, Collection KName m) => a -> m
    declaredNames

    instance DeclaredNames a => DeclaredNames [a]
    instance DeclaredNames a => DeclaredNames (List1 a)
    instance DeclaredNames a => DeclaredNames (Maybe a)
    instance DeclaredNames a => DeclaredNames (Arg a)
    instance DeclaredNames a => DeclaredNames (Named name a)
    instance DeclaredNames a => DeclaredNames (FieldAssignment' a)

    instance (DeclaredNames a, DeclaredNames b) => DeclaredNames (Either a b) where
      declaredNames :: forall m. Collection KName m => Either a b -> m
    declaredNames = (a -> m) -> (b -> m) -> Either a b -> m
    forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
    either a -> m
    forall a m. (DeclaredNames a, Collection KName m) => a -> m
    declaredNames b -> m
    forall a m. (DeclaredNames a, Collection KName m) => a -> m
    declaredNames

    instance (DeclaredNames a, DeclaredNames b) => DeclaredNames (a,b) where
      declaredNames :: forall m. Collection KName m => (a, b) -> m
    declaredNames (a
    a,b
    b) = a -> m
    forall a m. (DeclaredNames a, Collection KName m) => a -> m
    declaredNames a
    a m -> m -> m
    forall a. Semigroup a => a -> a -> a
    <> b -> m
    forall a m. (DeclaredNames a, Collection KName m) => a -> m
    declaredNames b
    b

    instance DeclaredNames KName where
      declaredNames :: forall m. Collection KName m => KName -> m
    declaredNames = KName -> m
    forall el coll. Singleton el coll => el -> coll
    singleton

    instance DeclaredNames RecordDirectives where
      declaredNames :: forall m. Collection KName m => RecordDirectives -> m
    declaredNames (RecordDirectives Maybe (Ranged Induction)
    i Maybe HasEta0
    _ Maybe Range
    _ Maybe QName
    c) = m
    kc where
        kc :: m
    kc = m -> (QName -> m) -> Maybe QName -> m
    forall b a. b -> (a -> b) -> Maybe a -> b
    maybe m
    forall a. Monoid a => a
    mempty (KName -> m
    forall el coll. Singleton el coll => el -> coll
    singleton (KName -> m) -> (QName -> KName) -> QName -> m
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . KindOfName -> QName -> KName
    forall a. KindOfName -> a -> WithKind a
    WithKind KindOfName
    k) Maybe QName
    c
        k :: KindOfName
    k  = KindOfName
    -> (Ranged Induction -> KindOfName)
    -> Maybe (Ranged Induction)
    -> KindOfName
    forall b a. b -> (a -> b) -> Maybe a -> b
    maybe KindOfName
    ConName (Induction -> KindOfName
    conKindOfName (Induction -> KindOfName)
    -> (Ranged Induction -> Induction)
    -> Ranged Induction
    -> KindOfName
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Ranged Induction -> Induction
    forall a. Ranged a -> a
    rangedThing) Maybe (Ranged Induction)
    i

    instance DeclaredNames Declaration where
      declaredNames :: forall m. Collection KName m => Declaration -> m
    declaredNames = \case
          Axiom KindOfName
    _ DefInfo
    di ArgInfo
    _ Maybe [Occurrence]
    _ QName
    q Expr
    _           -> KName -> m
    forall el coll. Singleton el coll => el -> coll
    singleton (KName -> m) -> (KindOfName -> KName) -> KindOfName -> m
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (KindOfName -> QName -> KName
    forall a. KindOfName -> a -> WithKind a
    `WithKind` QName
    q) (KindOfName -> m) -> KindOfName -> m
    forall a b. (a -> b) -> a -> b
    $
                                          case DefInfo -> IsMacro
    forall t. DefInfo' t -> IsMacro
    defMacro DefInfo
    di of
                                            IsMacro
    MacroDef    -> KindOfName
    MacroName
                                            IsMacro
    NotMacroDef -> KindOfName
    AxiomName
          Generalize Set QName
    _ DefInfo
    _ ArgInfo
    _ QName
    q Expr
    _         -> KName -> m
    forall el coll. Singleton el coll => el -> coll
    singleton (KindOfName -> QName -> KName
    forall a. KindOfName -> a -> WithKind a
    WithKind KindOfName
    GeneralizeName QName
    q)
          Field DefInfo
    _ QName
    q Arg Expr
    _                  -> KName -> m
    forall el coll. Singleton el coll => el -> coll
    singleton (KindOfName -> QName -> KName
    forall a. KindOfName -> a -> WithKind a
    WithKind KindOfName
    FldName QName
    q)
          Primitive DefInfo
    _ QName
    q Arg Expr
    _              -> KName -> m
    forall el coll. Singleton el coll => el -> coll
    singleton (KindOfName -> QName -> KName
    forall a. KindOfName -> a -> WithKind a
    WithKind KindOfName
    PrimName QName
    q)
          Mutual MutualInfo
    _ [Declaration]
    decls               -> [Declaration] -> m
    forall a m. (DeclaredNames a, Collection KName m) => a -> m
    declaredNames [Declaration]
    decls
          DataSig DefInfo
    _ QName
    q GeneralizeTelescope
    _ Expr
    _              -> KName -> m
    forall el coll. Singleton el coll => el -> coll
    singleton (KindOfName -> QName -> KName
    forall a. KindOfName -> a -> WithKind a
    WithKind KindOfName
    DataName QName
    q)
          DataDef DefInfo
    _ QName
    q UniverseCheck
    _ DataDefParams
    _ [Declaration]
    decls        -> KName -> m
    forall el coll. Singleton el coll => el -> coll
    singleton (KindOfName -> QName -> KName
    forall a. KindOfName -> a -> WithKind a
    WithKind KindOfName
    DataName QName
    q) m -> m -> m
    forall a. Semigroup a => a -> a -> a
    <> (Declaration -> m) -> [Declaration] -> m
    forall (t :: * -> *) m a.
    (Foldable t, Monoid m) =>
    (a -> m) -> t a -> m
    foldMap Declaration -> m
    con [Declaration]
    decls
          RecSig DefInfo
    _ QName
    q GeneralizeTelescope
    _ Expr
    _               -> KName -> m
    forall el coll. Singleton el coll => el -> coll
    singleton (KindOfName -> QName -> KName
    forall a. KindOfName -> a -> WithKind a
    WithKind KindOfName
    RecName QName
    q)
          RecDef DefInfo
    _ QName
    q UniverseCheck
    _ RecordDirectives
    dir DataDefParams
    _ Expr
    _ [Declaration]
    decls   -> KName -> m
    forall el coll. Singleton el coll => el -> coll
    singleton (KindOfName -> QName -> KName
    forall a. KindOfName -> a -> WithKind a
    WithKind KindOfName
    RecName QName
    q) m -> m -> m
    forall a. Semigroup a => a -> a -> a
    <> RecordDirectives -> m
    forall a m. (DeclaredNames a, Collection KName m) => a -> m
    declaredNames RecordDirectives
    dir m -> m -> m
    forall a. Semigroup a => a -> a -> a
    <> [Declaration] -> m
    forall a m. (DeclaredNames a, Collection KName m) => a -> m
    declaredNames [Declaration]
    decls
          PatternSynDef QName
    q [Arg BindName]
    _ Pattern' Void
    _          -> KName -> m
    forall el coll. Singleton el coll => el -> coll
    singleton (KindOfName -> QName -> KName
    forall a. KindOfName -> a -> WithKind a
    WithKind KindOfName
    PatternSynName QName
    q)
          UnquoteDecl MutualInfo
    _ [DefInfo]
    _ [QName]
    qs Expr
    _         -> [KName] -> m
    forall el coll. Collection el coll => [el] -> coll
    fromList ([KName] -> m) -> [KName] -> m
    forall a b. (a -> b) -> a -> b
    $ (QName -> KName) -> [QName] -> [KName]
    forall a b. (a -> b) -> [a] -> [b]
    map (KindOfName -> QName -> KName
    forall a. KindOfName -> a -> WithKind a
    WithKind KindOfName
    OtherDefName) [QName]
    qs  -- could be Fun or Axiom
          UnquoteDef [DefInfo]
    _ [QName]
    qs Expr
    _            -> [KName] -> m
    forall el coll. Collection el coll => [el] -> coll
    fromList ([KName] -> m) -> [KName] -> m
    forall a b. (a -> b) -> a -> b
    $ (QName -> KName) -> [QName] -> [KName]
    forall a b. (a -> b) -> [a] -> [b]
    map (KindOfName -> QName -> KName
    forall a. KindOfName -> a -> WithKind a
    WithKind KindOfName
    FunName) [QName]
    qs       -- cannot be Axiom
          FunDef DefInfo
    _ QName
    q Delayed
    _ [Clause]
    cls             -> KName -> m
    forall el coll. Singleton el coll => el -> coll
    singleton (KindOfName -> QName -> KName
    forall a. KindOfName -> a -> WithKind a
    WithKind KindOfName
    FunName QName
    q) m -> m -> m
    forall a. Semigroup a => a -> a -> a
    <> [Clause] -> m
    forall a m. (DeclaredNames a, Collection KName m) => a -> m
    declaredNames [Clause]
    cls
          ScopedDecl ScopeInfo
    _ [Declaration]
    decls           -> [Declaration] -> m
    forall a m. (DeclaredNames a, Collection KName m) => a -> m
    declaredNames [Declaration]
    decls
          Section Range
    _ ModuleName
    _ GeneralizeTelescope
    _ [Declaration]
    decls          -> [Declaration] -> m
    forall a m. (DeclaredNames a, Collection KName m) => a -> m
    declaredNames [Declaration]
    decls
          Pragma Range
    _ Pragma
    pragma              -> Pragma -> m
    forall a m. (DeclaredNames a, Collection KName m) => a -> m
    declaredNames Pragma
    pragma
          Apply{}                      -> m
    forall a. Monoid a => a
    mempty
          Import{}                     -> m
    forall a. Monoid a => a
    mempty
          Open{}                       -> m
    forall a. Monoid a => a
    mempty
        where
        con :: Declaration -> m
    con = \case
          Axiom KindOfName
    _ DefInfo
    _ ArgInfo
    _ Maybe [Occurrence]
    _ QName
    q Expr
    _ -> KName -> m
    forall el coll. Singleton el coll => el -> coll
    singleton (KName -> m) -> KName -> m
    forall a b. (a -> b) -> a -> b
    $ KindOfName -> QName -> KName
    forall a. KindOfName -> a -> WithKind a
    WithKind KindOfName
    ConName QName
    q
          Declaration
    _ -> m
    forall a. HasCallStack => a
    __IMPOSSIBLE__

    instance DeclaredNames Pragma where
      declaredNames :: forall m. Collection KName m => Pragma -> m
    declaredNames = \case
        BuiltinNoDefPragma RString
    _b KindOfName
    kind QName
    x -> KName -> m
    forall el coll. Singleton el coll => el -> coll
    singleton (KName -> m) -> KName -> m
    forall a b. (a -> b) -> a -> b
    $ KindOfName -> QName -> KName
    forall a. KindOfName -> a -> WithKind a
    WithKind KindOfName
    kind QName
    x
        BuiltinPragma{}         -> m
    forall a. Monoid a => a
    mempty
        CompilePragma{}         -> m
    forall a. Monoid a => a
    mempty
        RewritePragma{}         -> m
    forall a. Monoid a => a
    mempty
        StaticPragma{}          -> m
    forall a. Monoid a => a
    mempty
        EtaPragma{}             -> m
    forall a. Monoid a => a
    mempty
        InjectivePragma{}       -> m
    forall a. Monoid a => a
    mempty
        InlinePragma{}          -> m
    forall a. Monoid a => a
    mempty
        DisplayPragma{}         -> m
    forall a. Monoid a => a
    mempty
        OptionsPragma{}         -> m
    forall a. Monoid a => a
    mempty

    instance DeclaredNames Clause where
      declaredNames :: forall m. Collection KName m => Clause -> m
    declaredNames (Clause LHS
    _ [ProblemEq]
    _ RHS
    rhs WhereDeclarations
    decls Bool
    _) = RHS -> m
    forall a m. (DeclaredNames a, Collection KName m) => a -> m
    declaredNames RHS
    rhs m -> m -> m
    forall a. Semigroup a => a -> a -> a
    <> WhereDeclarations -> m
    forall a m. (DeclaredNames a, Collection KName m) => a -> m
    declaredNames WhereDeclarations
    decls

    instance DeclaredNames WhereDeclarations where
      declaredNames :: forall m. Collection KName m => WhereDeclarations -> m
    declaredNames (WhereDecls Maybe ModuleName
    _ Maybe Declaration
    ds) = Maybe Declaration -> m
    forall a m. (DeclaredNames a, Collection KName m) => a -> m
    declaredNames Maybe Declaration
    ds

    instance DeclaredNames RHS where
      declaredNames :: forall m. Collection KName m => RHS -> m
    declaredNames = \case
        RHS Expr
    _ Maybe Expr
    _                   -> m
    forall a. Monoid a => a
    mempty
        RHS
    AbsurdRHS                 -> m
    forall a. Monoid a => a
    mempty
        WithRHS QName
    _q [WithExpr]
    _es [Clause]
    cls        -> [Clause] -> m
    forall a m. (DeclaredNames a, Collection KName m) => a -> m
    declaredNames [Clause]
    cls
        RewriteRHS [RewriteEqn]
    _qes [ProblemEq]
    _ RHS
    rhs WhereDeclarations
    cls -> RHS -> m
    forall a m. (DeclaredNames a, Collection KName m) => a -> m
    declaredNames RHS
    rhs m -> m -> m
    forall a. Semigroup a => a -> a -> a
    <> WhereDeclarations -> m
    forall a m. (DeclaredNames a, Collection KName m) => a -> m
    declaredNames WhereDeclarations
    cls

    -- Andreas, 2020-04-13: Migration from Agda.Syntax.Abstract.AllNames
    --
    -- Since we are not interested in names of extended lambdas, we do not
    -- traverse into expression.
    --
    -- However, we keep this code (originally Agda.Syntax.Abstract.AllNames) around
    -- should arise a need to collect extended lambda names.

    -- instance (DeclaredNames a, DeclaredNames b, DeclaredNames c) => DeclaredNames (a,b,c) where
    --   declaredNames (a,b,c) = declaredNames a <> declaredNames b <> declaredNames c

    -- instance DeclaredNames RHS where
    --   declaredNames = \case
    --     RHS e _                  -> declaredNames e
    --     AbsurdRHS{}              -> mempty
    --     WithRHS q _ cls          -> singleton (WithKind FunName q) <> declaredNames cls
    --     RewriteRHS qes _ rhs cls -> declaredNames (qes, rhs, cls)

    -- instance DeclaredNames ModuleName where
    --   declaredNames _ = mempty

    -- instance (DeclaredNames qn, DeclaredNames e) => DeclaredNames (RewriteEqn' qn p e) where
    --   declaredNames = \case
    --     Rewrite es    -> declaredNames es
    --     Invert qn pes -> declaredNames qn <> declaredNames pes

    -- instance DeclaredNames Expr where
    --   declaredNames = \case
    --     Var{}                 -> mempty
    --     Def{}                 -> mempty
    --     Proj{}                -> mempty
    --     Con{}                 -> mempty
    --     Lit{}                 -> mempty
    --     QuestionMark{}        -> mempty
    --     Underscore{}          -> mempty
    --     Dot _ e               -> declaredNames e
    --     App _ e1 e2           -> declaredNames e1 <> declaredNames e2
    --     WithApp _ e es        -> declaredNames e <> declaredNames es
    --     Lam _ b e             -> declaredNames b <> declaredNames e
    --     AbsurdLam{}           -> mempty
    --     ExtendedLam _ _ q cls -> singleton (WithKind FunName q) <> declaredNames cls
    --     Pi _ tel e            -> declaredNames tel <> declaredNames e
    --     Generalized s e       -> declaredNames e  -- NOT: fromList (map (WithKind GeneralizeName) $ Set.toList s) <> declaredNames e
    --     Fun _ e1 e2           -> declaredNames e1 <> declaredNames e2
    --     Set{}                 -> mempty
    --     Prop{}                -> mempty
    --     Let _ lbs e           -> declaredNames lbs <> declaredNames e
    --     ETel{}                -> __IMPOSSIBLE__
    --     Rec _ fields          -> declaredNames fields
    --     RecUpdate _ e fs      -> declaredNames e <> declaredNames fs
    --     ScopedExpr _ e        -> declaredNames e
    --     Quote{}               -> mempty
    --     QuoteTerm{}           -> mempty
    --     Unquote{}             -> mempty
    --     DontCare{}            -> mempty
    --     PatternSyn{}          -> mempty
    --     Macro{}               -> mempty

    -- instance DeclaredNames LamBinding where
    --   declaredNames DomainFree{}       = mempty
    --   declaredNames (DomainFull binds) = declaredNames binds

    -- instance DeclaredNames TypedBinding where
    --   declaredNames (TBind _ t _ e) = declaredNames (t, e)
    --   declaredNames (TLet _ lbs)    = declaredNames lbs

    -- instance DeclaredNames LetBinding where
    --   declaredNames (LetBind _ _ _ e1 e2)   = declaredNames e1 <> declaredNames e2
    --   declaredNames (LetPatBind _ _ e)      = declaredNames e
    --   declaredNames (LetApply _ _ app _ _)  = declaredNames app
    --   declaredNames LetOpen{}               = mempty
    --   declaredNames (LetDeclaredVariable _) = mempty

    -- instance DeclaredNames ModuleApplication where
    --   declaredNames (SectionApp bindss _ es) = declaredNames bindss <> declaredNames es
    --   declaredNames RecordModuleInstance{}   = mempty