    module Agda.Syntax.Abstract.Views where

    import Prelude hiding (null)

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

    import Data.Foldable (foldMap)
    import qualified Data.DList as DL
    import Data.Semigroup ((<>))
    import Data.Void

    import Agda.Syntax.Common
    import Agda.Syntax.Abstract as A
    import Agda.Syntax.Concrete (FieldAssignment', exprFieldA, TacticAttribute')
    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
    $cfmap :: forall a b. (a -> b) -> AppView' a -> AppView' b
    fmap :: forall a b. (a -> b) -> AppView' a -> AppView' b
    $c<$ :: forall a b. a -> AppView' b -> AppView' a
    <$ :: forall a b. a -> AppView' b -> AppView' a
    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 :: Type -> AppView
    appView = ((AppInfo, Type) -> Type) -> AppView' (AppInfo, Type) -> AppView
    forall a b. (a -> b) -> AppView' a -> AppView' b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (AppInfo, Type) -> Type
    forall a b. (a, b) -> b
    snd (AppView' (AppInfo, Type) -> AppView)
    -> (Type -> AppView' (AppInfo, Type)) -> Type -> AppView
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Type -> AppView' (AppInfo, Type)
    appView'

    appView' :: Expr -> AppView' (AppInfo, Expr)
    appView' :: Type -> AppView' (AppInfo, Type)
    appView' Type
    e = [NamedArg (AppInfo, Type)] -> AppView' (AppInfo, Type)
    f (DList (NamedArg (AppInfo, Type)) -> [NamedArg (AppInfo, Type)]
    forall a. DList a -> [a]
    DL.toList DList (NamedArg (AppInfo, Type))
    es)
      where
      ([NamedArg (AppInfo, Type)] -> AppView' (AppInfo, Type)
    f, DList (NamedArg (AppInfo, Type))
    es) = Type
    -> ([NamedArg (AppInfo, Type)] -> AppView' (AppInfo, Type),
        DList (NamedArg (AppInfo, Type)))
    forall {arg}.
    Type
    -> ([NamedArg arg] -> AppView' arg,
        DList (NamedArg (AppInfo, Type)))
    appView'' Type
    e

      appView'' :: Type
    -> ([NamedArg arg] -> AppView' arg,
        DList (NamedArg (AppInfo, Type)))
    appView'' = \case
        App AppInfo
    i Type
    e1 NamedArg Type
    e2
          | Dot ExprInfo
    _ Type
    e2' <- Type -> Type
    unScope (Type -> Type) -> Type -> Type
    forall a b. (a -> b) -> a -> b
    $ NamedArg Type -> Type
    forall a. NamedArg a -> a
    namedArg NamedArg Type
    e2
          , Just Type
    f <- Type -> Maybe Type
    maybeProjTurnPostfix Type
    e2'
          , NamedArg Type -> Hiding
    forall a. LensHiding a => a -> Hiding
    getHiding NamedArg Type
    e2 Hiding -> Hiding -> Bool
    forall a. Eq a => a -> a -> Bool
    == Hiding
    NotHidden -- Jesper, 2018-12-13: postfix projections shouldn't be hidden
          -> (Type -> [NamedArg arg] -> AppView' arg
    forall arg. Type -> [NamedArg arg] -> AppView' arg
    Application Type
    f, NamedArg (AppInfo, Type) -> DList (NamedArg (AppInfo, Type))
    forall el coll. Singleton el coll => el -> coll
    singleton ((AppInfo, Type) -> NamedArg (AppInfo, Type)
    forall a. a -> NamedArg a
    defaultNamedArg (AppInfo
    i, Type
    e1)))
        App AppInfo
    i Type
    e1 NamedArg Type
    arg | ([NamedArg arg] -> AppView' arg
    f, DList (NamedArg (AppInfo, Type))
    es) <- Type
    -> ([NamedArg arg] -> AppView' arg,
        DList (NamedArg (AppInfo, Type)))
    appView'' Type
    e1 ->
          ([NamedArg arg] -> AppView' arg
    f, DList (NamedArg (AppInfo, Type))
    es DList (NamedArg (AppInfo, Type))
    -> NamedArg (AppInfo, Type) -> DList (NamedArg (AppInfo, Type))
    forall a. DList a -> a -> DList a
    `DL.snoc` ((Named NamedName Type -> Named NamedName (AppInfo, Type))
    -> NamedArg Type -> NamedArg (AppInfo, Type)
    forall a b. (a -> b) -> Arg a -> Arg b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap ((Named NamedName Type -> Named NamedName (AppInfo, Type))
     -> NamedArg Type -> NamedArg (AppInfo, Type))
    -> ((Type -> (AppInfo, Type))
        -> Named NamedName Type -> Named NamedName (AppInfo, Type))
    -> (Type -> (AppInfo, Type))
    -> NamedArg Type
    -> NamedArg (AppInfo, Type)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Type -> (AppInfo, Type))
    -> Named NamedName Type -> Named NamedName (AppInfo, Type)
    forall a b. (a -> b) -> Named NamedName a -> Named NamedName b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap) (AppInfo
    i,) NamedArg Type
    arg)
        ScopedExpr ScopeInfo
    _ Type
    e -> Type
    -> ([NamedArg arg] -> AppView' arg,
        DList (NamedArg (AppInfo, Type)))
    appView'' Type
    e
        Type
    e              -> (Type -> [NamedArg arg] -> AppView' arg
    forall arg. Type -> [NamedArg arg] -> AppView' arg
    Application Type
    e, DList (NamedArg (AppInfo, Type))
    forall a. Monoid a => a
    mempty)

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

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

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

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

    -- | Collect @A.Pi@s.
    data PiView = PiView [(ExprInfo, Telescope1)] Type

    piView :: Expr -> PiView
    piView :: Type -> PiView
    piView = \case
       Pi ExprInfo
    i Telescope1
    tel Type
    b -> PiView -> PiView
    cons (PiView -> PiView) -> PiView -> PiView
    forall a b. (a -> b) -> a -> b
    $ Type -> PiView
    piView Type
    b
         where cons :: PiView -> PiView
    cons (PiView [(ExprInfo, Telescope1)]
    tels Type
    t) = [(ExprInfo, Telescope1)] -> Type -> PiView
    PiView ((ExprInfo
    i,Telescope1
    tel) (ExprInfo, Telescope1)
    -> [(ExprInfo, Telescope1)] -> [(ExprInfo, Telescope1)]
    forall a. a -> [a] -> [a]
    : [(ExprInfo, Telescope1)]
    tels) Type
    t
       Type
    e -> [(ExprInfo, Telescope1)] -> Type -> PiView
    PiView [] Type
    e

    unPiView :: PiView -> Expr
    unPiView :: PiView -> Type
    unPiView (PiView [(ExprInfo, Telescope1)]
    tels Type
    t) = ((ExprInfo, Telescope1) -> Type -> Type)
    -> Type -> [(ExprInfo, Telescope1)] -> Type
    forall a b. (a -> b -> b) -> b -> [a] -> b
    forall (t :: * -> *) a b.
    Foldable t =>
    (a -> b -> b) -> b -> t a -> b
    foldr ((ExprInfo -> Telescope1 -> Type -> Type)
    -> (ExprInfo, Telescope1) -> Type -> Type
    forall a b c. (a -> b -> c) -> (a, b) -> c
    uncurry ExprInfo -> Telescope1 -> Type -> Type
    Pi) Type
    t [(ExprInfo, Telescope1)]
    tels

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

    -- | Remove top 'ScopedExpr' wrappers.
    unScope :: Expr -> Expr
    unScope :: Type -> Type
    unScope (ScopedExpr ScopeInfo
    scope Type
    e) = Type -> Type
    unScope Type
    e
    unScope (QuestionMark MetaInfo
    i InteractionId
    ii)  = MetaInfo -> InteractionId -> Type
    QuestionMark (MetaInfo
    i {metaScope = empty}) InteractionId
    ii
    unScope (Underscore MetaInfo
    i)       = MetaInfo -> Type
    Underscore (MetaInfo
    i {metaScope = empty})
    unScope Type
    e                    = Type
    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 = (Type -> Type) -> a -> a
    forall a. ExprLike a => (Type -> Type) -> a -> a
    mapExpr Type -> Type
    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 = \case
      A.ScopedDecl ScopeInfo
    _ [Declaration]
    ds           -> [Declaration] -> [Declaration]
    deepUnscopeDecls [Declaration]
    ds
      A.Mutual MutualInfo
    i [Declaration]
    ds               -> [MutualInfo -> [Declaration] -> Declaration
    A.Mutual MutualInfo
    i ([Declaration] -> [Declaration]
    deepUnscopeDecls [Declaration]
    ds)]
      A.Section Range
    i Erased
    e ModuleName
    m GeneralizeTelescope
    tel [Declaration]
    ds      -> [Range
    -> Erased
    -> ModuleName
    -> GeneralizeTelescope
    -> [Declaration]
    -> Declaration
    A.Section Range
    i Erased
    e ModuleName
    m (GeneralizeTelescope -> GeneralizeTelescope
    forall a. ExprLike a => a -> a
    deepUnscope GeneralizeTelescope
    tel)
                                       ([Declaration] -> [Declaration]
    deepUnscopeDecls [Declaration]
    ds)]
      A.RecDef DefInfo
    i QName
    x UniverseCheck
    uc RecordDirectives
    dir DataDefParams
    bs Type
    e [Declaration]
    ds -> [ DefInfo
    -> QName
    -> UniverseCheck
    -> RecordDirectives
    -> DataDefParams
    -> Type
    -> [Declaration]
    -> Declaration
    A.RecDef DefInfo
    i QName
    x UniverseCheck
    uc RecordDirectives
    dir (DataDefParams -> DataDefParams
    forall a. ExprLike a => a -> a
    deepUnscope DataDefParams
    bs)
                                         (Type -> Type
    forall a. ExprLike a => a -> a
    deepUnscope Type
    e)
                                         ([Declaration] -> [Declaration]
    deepUnscopeDecls [Declaration]
    ds) ]
      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') -> a -> m a
    (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)
    forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> f a -> f (f b)
    traverse ((a' -> m a') -> a -> m a)
    -> ((Type -> m Type -> m Type) -> a' -> m a')
    -> (Type -> m Type -> m Type)
    -> a
    -> m a
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Type -> m Type -> m Type) -> a' -> m a'
    forall a (m :: * -> *). ExprLike a => RecurseExprFn m a
    forall (m :: * -> *). RecurseExprFn m a'
    recurseExpr

      foldExpr :: FoldExprFn m a
      foldExpr Type -> 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
    . (Type -> Const m Type -> Const m Type) -> a -> Const m a
    forall a (m :: * -> *). ExprLike a => RecurseExprFn m a
    forall (m :: * -> *). RecurseExprFn m a
    recurseExpr (\ Type
    pre Const m Type
    post -> m -> Const m Type
    forall {k} a (b :: k). a -> Const a b
    Const (Type -> m
    f Type
    pre) Const m Type -> Const m Type -> Const m Type
    forall a b. Const m a -> Const m b -> Const m a
    forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
    <* Const m Type
    post)

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

      mapExpr :: (Expr -> Expr) -> (a -> a)
      mapExpr Type -> Type
    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
    . (Type -> Identity Type) -> a -> Identity a
    forall a (m :: * -> *). ExprLike a => TraverseExprFn m a
    forall (m :: * -> *). TraverseExprFn m a
    traverseExpr (Type -> Identity Type
    forall a. a -> Identity a
    Identity (Type -> Identity Type) -> (Type -> Type) -> Type -> Identity Type
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Type -> Type
    f)

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

      foldExpr :: forall m. FoldExprFn m Expr
      foldExpr :: forall m. FoldExprFn m Type
    foldExpr Type -> m
    f Type
    e =
        case Type
    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
    _ Type
    e                -> m
    m m -> m -> m
    forall a. Monoid a => a -> a -> a
    `mappend` Type -> m
    FoldExprRecFn m
    fold Type
    e
          App AppInfo
    _ Type
    e NamedArg Type
    e'             -> m
    m m -> m -> m
    forall a. Monoid a => a -> a -> a
    `mappend` Type -> m
    FoldExprRecFn m
    fold Type
    e m -> m -> m
    forall a. Monoid a => a -> a -> a
    `mappend` NamedArg Type -> m
    FoldExprRecFn m
    fold NamedArg Type
    e'
          WithApp ExprInfo
    _ Type
    e List1 Type
    es         -> m
    m m -> m -> m
    forall a. Monoid a => a -> a -> a
    `mappend` Type -> m
    FoldExprRecFn m
    fold Type
    e m -> m -> m
    forall a. Monoid a => a -> a -> a
    `mappend` List1 Type -> m
    FoldExprRecFn m
    fold List1 Type
    es
          Lam ExprInfo
    _ LamBinding
    b Type
    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` Type -> m
    FoldExprRecFn m
    fold Type
    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 Type
    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` Type -> m
    FoldExprRecFn m
    fold Type
    e
          Generalized Set1 QName
    _ Type
    e        -> m
    m m -> m -> m
    forall a. Monoid a => a -> a -> a
    `mappend` Type -> m
    FoldExprRecFn m
    fold Type
    e
          Fun ExprInfo
    _ Arg Type
    e Type
    e'             -> m
    m m -> m -> m
    forall a. Monoid a => a -> a -> a
    `mappend` Arg Type -> m
    FoldExprRecFn m
    fold Arg Type
    e m -> m -> m
    forall a. Monoid a => a -> a -> a
    `mappend` Type -> m
    FoldExprRecFn m
    fold Type
    e'
          Let ExprInfo
    _ List1 LetBinding
    bs Type
    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` Type -> m
    FoldExprRecFn m
    fold Type
    e
          Rec KwRange
    _ ExprInfo
    _ RecordAssigns
    as             -> m
    m m -> m -> m
    forall a. Monoid a => a -> a -> a
    `mappend` RecordAssigns -> m
    FoldExprRecFn m
    fold RecordAssigns
    as
          RecUpdate KwRange
    _ ExprInfo
    _ Type
    e Assigns
    as     -> m
    m m -> m -> m
    forall a. Monoid a => a -> a -> a
    `mappend` Type -> m
    FoldExprRecFn m
    fold Type
    e m -> m -> m
    forall a. Monoid a => a -> a -> a
    `mappend` Assigns -> m
    FoldExprRecFn m
    fold Assigns
    as
          ScopedExpr ScopeInfo
    _ Type
    e         -> m
    m m -> m -> m
    forall a. Monoid a => a -> a -> a
    `mappend` Type -> m
    FoldExprRecFn m
    fold Type
    e
          Quote{}                -> m
    m
          QuoteTerm{}            -> m
    m
          Unquote{}              -> m
    m
          DontCare Type
    e             -> m
    m m -> m -> m
    forall a. Monoid a => a -> a -> a
    `mappend` Type -> m
    FoldExprRecFn m
    fold Type
    e
       where
         m :: m
    m = Type -> m
    f Type
    e
         fold :: FoldExprRecFn m
         fold :: FoldExprRecFn m
    fold = (Type -> m) -> a -> m
    forall m. FoldExprFn m a
    forall a m. ExprLike a => FoldExprFn m a
    foldExpr Type -> m
    f

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

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

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

    instance ExprLike Void where
      recurseExpr :: forall (m :: * -> *). RecurseExprFn m Void
    recurseExpr Type -> m Type -> m Type
    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 (f :: * -> *).
    Functor f =>
    (a -> f a) -> FieldAssignment' a -> f (FieldAssignment' a)
    exprFieldA ((a -> m a) -> FieldAssignment' a -> m (FieldAssignment' a))
    -> ((Type -> m Type -> m Type) -> a -> m a)
    -> (Type -> m Type -> m Type)
    -> FieldAssignment' a
    -> m (FieldAssignment' a)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Type -> m Type -> m Type) -> a -> m a
    forall a (m :: * -> *). ExprLike a => RecurseExprFn m a
    forall (m :: * -> *). RecurseExprFn m a
    recurseExpr

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

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

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

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

    instance ExprLike LamBinding where
      recurseExpr :: forall (m :: * -> *). RecurseExprFn m LamBinding
    recurseExpr Type -> m Type -> m Type
    f LamBinding
    e =
        case LamBinding
    e of
          DomainFree TacticAttribute
    t NamedArg Binder
    x -> TacticAttribute -> NamedArg Binder -> LamBinding
    DomainFree (TacticAttribute -> NamedArg Binder -> LamBinding)
    -> m TacticAttribute -> m (NamedArg Binder -> LamBinding)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (Type -> m Type -> m Type) -> TacticAttribute -> m TacticAttribute
    forall a (m :: * -> *). ExprLike a => RecurseExprFn m a
    forall (m :: * -> *). RecurseExprFn m TacticAttribute
    recurseExpr Type -> m Type -> m Type
    f TacticAttribute
    t m (NamedArg Binder -> LamBinding)
    -> m (NamedArg Binder) -> m LamBinding
    forall a b. m (a -> b) -> m a -> m b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> NamedArg Binder -> m (NamedArg Binder)
    forall a. a -> m a
    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
    <$> (Type -> m Type -> m Type) -> TypedBinding -> m TypedBinding
    forall a (m :: * -> *). ExprLike a => RecurseExprFn m a
    forall (m :: * -> *). RecurseExprFn m TypedBinding
    recurseExpr Type -> m Type -> m Type
    f TypedBinding
    bs
      foldExpr :: forall m. FoldExprFn m LamBinding
    foldExpr Type -> m
    f LamBinding
    e =
        case LamBinding
    e of
          DomainFree TacticAttribute
    t NamedArg Binder
    _ -> (Type -> m) -> TacticAttribute -> m
    forall m. FoldExprFn m TacticAttribute
    forall a m. ExprLike a => FoldExprFn m a
    foldExpr Type -> m
    f TacticAttribute
    t
          DomainFull TypedBinding
    bs -> (Type -> m) -> TypedBinding -> m
    forall m. FoldExprFn m TypedBinding
    forall a m. ExprLike a => FoldExprFn m a
    foldExpr Type -> m
    f TypedBinding
    bs
      traverseExpr :: forall (m :: * -> *). TraverseExprFn m LamBinding
    traverseExpr Type -> m Type
    f LamBinding
    e =
        case LamBinding
    e of
          DomainFree TacticAttribute
    t NamedArg Binder
    x -> TacticAttribute -> NamedArg Binder -> LamBinding
    DomainFree (TacticAttribute -> NamedArg Binder -> LamBinding)
    -> m TacticAttribute -> m (NamedArg Binder -> LamBinding)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (Type -> m Type) -> TacticAttribute -> m TacticAttribute
    forall a (m :: * -> *). ExprLike a => TraverseExprFn m a
    forall (m :: * -> *). TraverseExprFn m TacticAttribute
    traverseExpr Type -> m Type
    f TacticAttribute
    t m (NamedArg Binder -> LamBinding)
    -> m (NamedArg Binder) -> m LamBinding
    forall a b. m (a -> b) -> m a -> m b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> NamedArg Binder -> m (NamedArg Binder)
    forall a. a -> m a
    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
    <$> (Type -> m Type) -> TypedBinding -> m TypedBinding
    forall a (m :: * -> *). ExprLike a => TraverseExprFn m a
    forall (m :: * -> *). TraverseExprFn m TypedBinding
    traverseExpr Type -> m Type
    f TypedBinding
    bs

    instance ExprLike GeneralizeTelescope where
      recurseExpr :: forall (m :: * -> *). RecurseExprFn m GeneralizeTelescope
    recurseExpr  Type -> m Type -> m Type
    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
    <$> (Type -> m Type -> m Type) -> Telescope -> m Telescope
    forall a (m :: * -> *). ExprLike a => RecurseExprFn m a
    forall (m :: * -> *). RecurseExprFn m Telescope
    recurseExpr Type -> m Type -> m Type
    f Telescope
    tel
      foldExpr :: forall m. FoldExprFn m GeneralizeTelescope
    foldExpr     Type -> m
    f (GeneralizeTel Map QName Name
    s Telescope
    tel) = (Type -> m) -> Telescope -> m
    forall m. FoldExprFn m Telescope
    forall a m. ExprLike a => FoldExprFn m a
    foldExpr Type -> m
    f Telescope
    tel
      traverseExpr :: forall (m :: * -> *). TraverseExprFn m GeneralizeTelescope
    traverseExpr Type -> m Type
    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
    <$> (Type -> m Type) -> Telescope -> m Telescope
    forall a (m :: * -> *). ExprLike a => TraverseExprFn m a
    forall (m :: * -> *). TraverseExprFn m Telescope
    traverseExpr Type -> m Type
    f Telescope
    tel

    instance ExprLike DataDefParams where
      recurseExpr :: forall (m :: * -> *). RecurseExprFn m DataDefParams
    recurseExpr  Type -> m Type -> m Type
    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
    <$> (Type -> m Type -> m Type) -> [LamBinding] -> m [LamBinding]
    forall a (m :: * -> *). ExprLike a => RecurseExprFn m a
    forall (m :: * -> *). RecurseExprFn m [LamBinding]
    recurseExpr Type -> m Type -> m Type
    f [LamBinding]
    tel
      foldExpr :: forall m. FoldExprFn m DataDefParams
    foldExpr     Type -> m
    f (DataDefParams Set Name
    s [LamBinding]
    tel) = (Type -> m) -> [LamBinding] -> m
    forall m. FoldExprFn m [LamBinding]
    forall a m. ExprLike a => FoldExprFn m a
    foldExpr Type -> m
    f [LamBinding]
    tel
      traverseExpr :: forall (m :: * -> *). TraverseExprFn m DataDefParams
    traverseExpr Type -> m Type
    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
    <$> (Type -> m Type) -> [LamBinding] -> m [LamBinding]
    forall a (m :: * -> *). ExprLike a => TraverseExprFn m a
    forall (m :: * -> *). TraverseExprFn m [LamBinding]
    traverseExpr Type -> m Type
    f [LamBinding]
    tel

    instance ExprLike TypedBindingInfo where
      recurseExpr :: forall (m :: * -> *). RecurseExprFn m TypedBindingInfo
    recurseExpr Type -> m Type -> m Type
    f (TypedBindingInfo TacticAttribute
    s Bool
    t)  = TacticAttribute -> Bool -> TypedBindingInfo
    TypedBindingInfo (TacticAttribute -> Bool -> TypedBindingInfo)
    -> m TacticAttribute -> m (Bool -> TypedBindingInfo)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (Type -> m Type -> m Type) -> TacticAttribute -> m TacticAttribute
    forall a (m :: * -> *). ExprLike a => RecurseExprFn m a
    forall (m :: * -> *). RecurseExprFn m TacticAttribute
    recurseExpr Type -> m Type -> m Type
    f TacticAttribute
    s m (Bool -> TypedBindingInfo) -> m Bool -> m TypedBindingInfo
    forall a b. m (a -> b) -> m a -> m b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> Bool -> m Bool
    forall a. a -> m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Bool
    t
      foldExpr :: forall m. FoldExprFn m TypedBindingInfo
    foldExpr Type -> m
    f (TypedBindingInfo TacticAttribute
    s Bool
    t)     = (Type -> m) -> TacticAttribute -> m
    forall m. FoldExprFn m TacticAttribute
    forall a m. ExprLike a => FoldExprFn m a
    foldExpr Type -> m
    f TacticAttribute
    s
      traverseExpr :: forall (m :: * -> *). TraverseExprFn m TypedBindingInfo
    traverseExpr Type -> m Type
    f (TypedBindingInfo TacticAttribute
    s Bool
    t) = TacticAttribute -> Bool -> TypedBindingInfo
    TypedBindingInfo (TacticAttribute -> Bool -> TypedBindingInfo)
    -> m TacticAttribute -> m (Bool -> TypedBindingInfo)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (Type -> m Type) -> TacticAttribute -> m TacticAttribute
    forall a (m :: * -> *). ExprLike a => TraverseExprFn m a
    forall (m :: * -> *). TraverseExprFn m TacticAttribute
    traverseExpr Type -> m Type
    f TacticAttribute
    s m (Bool -> TypedBindingInfo) -> m Bool -> m TypedBindingInfo
    forall a b. m (a -> b) -> m a -> m b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> Bool -> m Bool
    forall a. a -> m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Bool
    t

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

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

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

      traverseExpr :: forall m. TraverseExprFn m LetBinding
      traverseExpr :: forall (m :: * -> *). TraverseExprFn m LetBinding
    traverseExpr Type -> m Type
    f LetBinding
    e = do
        let
          trav :: TraverseExprRecFn m
          trav :: TraverseExprRecFn m
    trav a
    e = (Type -> m Type) -> a -> m a
    forall a (m :: * -> *). ExprLike a => TraverseExprFn m a
    forall (m :: * -> *). TraverseExprFn m a
    traverseExpr Type -> m Type
    f a
    e
        case LetBinding
    e of
          LetBind LetInfo
    li ArgInfo
    ai BindName
    x Type
    e Type
    e'  -> LetInfo -> ArgInfo -> BindName -> Type -> Type -> LetBinding
    LetBind LetInfo
    li ArgInfo
    ai BindName
    x (Type -> Type -> LetBinding) -> m Type -> m (Type -> LetBinding)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Type -> m Type
    TraverseExprRecFn m
    trav Type
    e m (Type -> LetBinding) -> m Type -> m LetBinding
    forall a b. m (a -> b) -> m a -> m b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> Type -> m Type
    TraverseExprRecFn m
    trav Type
    e'
          LetAxiom LetInfo
    li ArgInfo
    ai BindName
    x Type
    e    -> LetInfo -> ArgInfo -> BindName -> Type -> LetBinding
    LetAxiom LetInfo
    li ArgInfo
    ai BindName
    x (Type -> LetBinding) -> m Type -> m LetBinding
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Type -> m Type
    TraverseExprRecFn m
    trav Type
    e
          LetPatBind LetInfo
    li Pattern
    p Type
    e     -> LetInfo -> Pattern -> Type -> LetBinding
    LetPatBind LetInfo
    li (Pattern -> Type -> LetBinding)
    -> m Pattern -> m (Type -> LetBinding)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Pattern -> m Pattern
    TraverseExprRecFn m
    trav Pattern
    p m (Type -> LetBinding) -> m Type -> m LetBinding
    forall a b. m (a -> b) -> m a -> m b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> Type -> m Type
    TraverseExprRecFn m
    trav Type
    e
          LetApply{}            -> LetBinding -> m LetBinding
    forall a. a -> m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure LetBinding
    e
          LetOpen{}             -> LetBinding -> m LetBinding
    forall a. a -> m a
    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 Type -> m Type -> m Type
    f (Clause a
    lhs [ProblemEq]
    spats RHS
    rhs WhereDeclarations
    ds Catchall
    ca) = a
    -> [ProblemEq] -> RHS -> WhereDeclarations -> Catchall -> Clause' a
    forall lhs.
    lhs
    -> [ProblemEq]
    -> RHS
    -> WhereDeclarations
    -> Catchall
    -> Clause' lhs
    Clause (a
     -> [ProblemEq]
     -> RHS
     -> WhereDeclarations
     -> Catchall
     -> Clause' a)
    -> m a
    -> m ([ProblemEq]
          -> RHS -> WhereDeclarations -> Catchall -> 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 -> Catchall -> Clause' a)
    -> m [ProblemEq]
    -> m (RHS -> WhereDeclarations -> Catchall -> Clause' a)
    forall a b. m (a -> b) -> m a -> m b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> [ProblemEq] -> m [ProblemEq]
    forall a. a -> m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure [ProblemEq]
    spats m (RHS -> WhereDeclarations -> Catchall -> Clause' a)
    -> m RHS -> m (WhereDeclarations -> Catchall -> Clause' a)
    forall a b. m (a -> b) -> m a -> m b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> RHS -> m RHS
    RecurseExprRecFn m
    rec RHS
    rhs m (WhereDeclarations -> Catchall -> Clause' a)
    -> m WhereDeclarations -> m (Catchall -> Clause' a)
    forall a b. m (a -> b) -> m a -> m b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> WhereDeclarations -> m WhereDeclarations
    RecurseExprRecFn m
    rec WhereDeclarations
    ds m (Catchall -> Clause' a) -> m Catchall -> m (Clause' a)
    forall a b. m (a -> b) -> m a -> m b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> Catchall -> m Catchall
    forall a. a -> m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Catchall
    ca
        where
          rec :: RecurseExprRecFn m
          rec :: RecurseExprRecFn m
    rec = (Type -> m Type -> m Type) -> a -> m a
    forall a (m :: * -> *). ExprLike a => RecurseExprFn m a
    forall (m :: * -> *). RecurseExprFn m a
    recurseExpr Type -> m Type -> m Type
    f

    instance ExprLike RHS where
      recurseExpr :: forall m. RecurseExprFn m RHS
      recurseExpr :: forall (m :: * -> *). RecurseExprFn m RHS
    recurseExpr Type -> m Type -> m Type
    f RHS
    rhs =
        case RHS
    rhs of
          RHS Type
    e Maybe Expr
    c                 -> Type -> Maybe Expr -> RHS
    RHS (Type -> Maybe Expr -> RHS) -> m Type -> m (Maybe Expr -> RHS)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Type -> m Type
    RecurseExprRecFn m
    rec Type
    e m (Maybe Expr -> RHS) -> m (Maybe Expr) -> m RHS
    forall a b. m (a -> b) -> m a -> m b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> Maybe Expr -> m (Maybe Expr)
    forall a. a -> m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Maybe Expr
    c
          AbsurdRHS{}             -> RHS -> m RHS
    forall a. a -> m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure RHS
    rhs
          WithRHS QName
    x List1 WithExpr
    es List1 Clause
    cs         -> QName -> List1 WithExpr -> List1 Clause -> RHS
    WithRHS QName
    x (List1 WithExpr -> List1 Clause -> RHS)
    -> m (List1 WithExpr) -> m (List1 Clause -> RHS)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> List1 WithExpr -> m (List1 WithExpr)
    RecurseExprRecFn m
    rec List1 WithExpr
    es m (List1 Clause -> RHS) -> m (List1 Clause) -> m RHS
    forall a b. m (a -> b) -> m a -> m b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> List1 Clause -> m (List1 Clause)
    RecurseExprRecFn m
    rec List1 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 a b. m (a -> b) -> m a -> m b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> [ProblemEq] -> m [ProblemEq]
    forall a. a -> m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure [ProblemEq]
    spats m (RHS -> WhereDeclarations -> RHS)
    -> m RHS -> m (WhereDeclarations -> RHS)
    forall a b. m (a -> b) -> m a -> m b
    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 a b. m (a -> b) -> m a -> m b
    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 = (Type -> m Type -> m Type) -> a -> m a
    forall a (m :: * -> *). ExprLike a => RecurseExprFn m a
    forall (m :: * -> *). RecurseExprFn m a
    recurseExpr Type -> m Type -> m Type
    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 Type -> m Type -> m Type
    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
    <$> (Type -> m Type -> m Type) -> List1 (qn, e) -> m (List1 (qn, e))
    forall a (m :: * -> *). ExprLike a => RecurseExprFn m a
    forall (m :: * -> *). RecurseExprFn m (List1 (qn, e))
    recurseExpr Type -> m Type -> m Type
    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
    <$> (Type -> m Type -> m Type) -> qn -> m qn
    forall a (m :: * -> *). ExprLike a => RecurseExprFn m a
    forall (m :: * -> *). RecurseExprFn m qn
    recurseExpr Type -> m Type -> m Type
    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 a b. m (a -> b) -> m a -> m b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> (Type -> m Type -> m Type)
    -> List1 (Named nm (p, e)) -> m (List1 (Named nm (p, e)))
    forall a (m :: * -> *). ExprLike a => RecurseExprFn m a
    forall (m :: * -> *). RecurseExprFn m (List1 (Named nm (p, e)))
    recurseExpr Type -> m Type -> m Type
    f List1 (Named nm (p, e))
    pes
        LeftLet List1 (p, e)
    pes   -> List1 (p, e) -> RewriteEqn' qn nm p e
    forall qn nm p e. List1 (p, e) -> RewriteEqn' qn nm p e
    LeftLet (List1 (p, e) -> RewriteEqn' qn nm p e)
    -> m (List1 (p, e)) -> m (RewriteEqn' qn nm p e)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (Type -> m Type -> m Type) -> List1 (p, e) -> m (List1 (p, e))
    forall a (m :: * -> *). ExprLike a => RecurseExprFn m a
    forall (m :: * -> *). RecurseExprFn m (List1 (p, e))
    recurseExpr Type -> m Type -> m Type
    f List1 (p, e)
    pes

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

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

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

    instance ExprLike LHS where
      recurseExpr :: forall (m :: * -> *). RecurseExprFn m LHS
    recurseExpr Type -> m Type -> m Type
    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
    <$> (Type -> m Type -> m Type) -> LHSCore -> m LHSCore
    forall a (m :: * -> *). ExprLike a => RecurseExprFn m a
    forall (m :: * -> *). RecurseExprFn m LHSCore
    recurseExpr Type -> m Type -> m Type
    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 Type -> m Type -> m Type
    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
    <$> (Type -> m Type -> m Type)
    -> [NamedArg Pattern] -> m [NamedArg Pattern]
    forall a (m :: * -> *). ExprLike a => RecurseExprFn m a
    forall (m :: * -> *). RecurseExprFn m [NamedArg Pattern]
    recurseExpr Type -> m Type -> m Type
    f [NamedArg Pattern]
    ps

    instance ExprLike Declaration where
      recurseExpr :: forall m. RecurseExprFn m Declaration
      recurseExpr :: forall (m :: * -> *). RecurseExprFn m Declaration
    recurseExpr Type -> m Type -> m Type
    f Declaration
    d =
        case Declaration
    d of
          Axiom KindOfName
    a DefInfo
    d ArgInfo
    i Maybe PragmaPolarities
    mp QName
    x Type
    e        -> KindOfName
    -> DefInfo
    -> ArgInfo
    -> Maybe PragmaPolarities
    -> QName
    -> Type
    -> Declaration
    Axiom KindOfName
    a DefInfo
    d ArgInfo
    i Maybe PragmaPolarities
    mp QName
    x (Type -> Declaration) -> m Type -> m Declaration
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Type -> m Type
    RecurseExprRecFn m
    rec Type
    e
          Generalize Set QName
    s DefInfo
    i ArgInfo
    j QName
    x Type
    e      -> Set QName -> DefInfo -> ArgInfo -> QName -> Type -> Declaration
    Generalize Set QName
    s DefInfo
    i ArgInfo
    j QName
    x (Type -> Declaration) -> m Type -> m Declaration
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Type -> m Type
    RecurseExprRecFn m
    rec Type
    e
          Field DefInfo
    i QName
    x Arg Type
    e               -> DefInfo -> QName -> Arg Type -> Declaration
    Field DefInfo
    i QName
    x (Arg Type -> Declaration) -> m (Arg Type) -> m Declaration
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Arg Type -> m (Arg Type)
    RecurseExprRecFn m
    rec Arg Type
    e
          Primitive DefInfo
    i QName
    x Arg Type
    e           -> DefInfo -> QName -> Arg Type -> Declaration
    Primitive DefInfo
    i QName
    x (Arg Type -> Declaration) -> m (Arg Type) -> m Declaration
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Arg Type -> m (Arg Type)
    RecurseExprRecFn m
    rec Arg Type
    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 Erased
    e ModuleName
    m GeneralizeTelescope
    tel [Declaration]
    ds      -> Range
    -> Erased
    -> ModuleName
    -> GeneralizeTelescope
    -> [Declaration]
    -> Declaration
    Section Range
    i Erased
    e 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 a b. m (a -> b) -> m a -> m b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> [Declaration] -> m [Declaration]
    RecurseExprRecFn m
    rec [Declaration]
    ds
          Apply ModuleInfo
    i Erased
    e ModuleName
    m ModuleApplication
    a ScopeCopyInfo
    ci ImportDirective
    d        -> (\ModuleApplication
    a -> ModuleInfo
    -> Erased
    -> ModuleName
    -> ModuleApplication
    -> ScopeCopyInfo
    -> ImportDirective
    -> Declaration
    Apply ModuleInfo
    i Erased
    e 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 a. a -> m a
    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 a. a -> m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Declaration
    d
          FunDef DefInfo
    i QName
    f [Clause]
    cs             -> DefInfo -> QName -> [Clause] -> Declaration
    FunDef DefInfo
    i QName
    f ([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 Erased
    er QName
    d GeneralizeTelescope
    tel Type
    e      -> DefInfo
    -> Erased -> QName -> GeneralizeTelescope -> Type -> Declaration
    DataSig DefInfo
    i Erased
    er QName
    d (GeneralizeTelescope -> Type -> Declaration)
    -> m GeneralizeTelescope -> m (Type -> Declaration)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> GeneralizeTelescope -> m GeneralizeTelescope
    RecurseExprRecFn m
    rec GeneralizeTelescope
    tel m (Type -> Declaration) -> m Type -> m Declaration
    forall a b. m (a -> b) -> m a -> m b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> Type -> m Type
    RecurseExprRecFn m
    rec Type
    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 a b. m (a -> b) -> m a -> m b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> [Declaration] -> m [Declaration]
    RecurseExprRecFn m
    rec [Declaration]
    cs
          RecSig DefInfo
    i Erased
    er QName
    r GeneralizeTelescope
    tel Type
    e       -> DefInfo
    -> Erased -> QName -> GeneralizeTelescope -> Type -> Declaration
    RecSig DefInfo
    i Erased
    er QName
    r (GeneralizeTelescope -> Type -> Declaration)
    -> m GeneralizeTelescope -> m (Type -> Declaration)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> GeneralizeTelescope -> m GeneralizeTelescope
    RecurseExprRecFn m
    rec GeneralizeTelescope
    tel m (Type -> Declaration) -> m Type -> m Declaration
    forall a b. m (a -> b) -> m a -> m b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> Type -> m Type
    RecurseExprRecFn m
    rec Type
    e
          RecDef DefInfo
    i QName
    r UniverseCheck
    uc RecordDirectives
    dir DataDefParams
    bs Type
    e [Declaration]
    ds -> DefInfo
    -> QName
    -> UniverseCheck
    -> RecordDirectives
    -> DataDefParams
    -> Type
    -> [Declaration]
    -> Declaration
    RecDef DefInfo
    i QName
    r UniverseCheck
    uc RecordDirectives
    dir (DataDefParams -> Type -> [Declaration] -> Declaration)
    -> m DataDefParams -> m (Type -> [Declaration] -> Declaration)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> DataDefParams -> m DataDefParams
    RecurseExprRecFn m
    rec DataDefParams
    bs m (Type -> [Declaration] -> Declaration)
    -> m Type -> m ([Declaration] -> Declaration)
    forall a b. m (a -> b) -> m a -> m b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> Type -> m Type
    RecurseExprRecFn m
    rec Type
    e m ([Declaration] -> Declaration)
    -> m [Declaration] -> m Declaration
    forall a b. m (a -> b) -> m a -> m b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> [Declaration] -> m [Declaration]
    RecurseExprRecFn m
    rec [Declaration]
    ds
          PatternSynDef QName
    f [WithHiding BindName]
    xs Pattern' Void
    p      -> QName -> [WithHiding BindName] -> Pattern' Void -> Declaration
    PatternSynDef QName
    f [WithHiding 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 Type
    e     -> MutualInfo -> [DefInfo] -> [QName] -> Type -> Declaration
    UnquoteDecl MutualInfo
    i [DefInfo]
    is [QName]
    xs (Type -> Declaration) -> m Type -> m Declaration
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Type -> m Type
    RecurseExprRecFn m
    rec Type
    e
          UnquoteDef [DefInfo]
    i [QName]
    xs Type
    e         -> [DefInfo] -> [QName] -> Type -> Declaration
    UnquoteDef [DefInfo]
    i [QName]
    xs (Type -> Declaration) -> m Type -> m Declaration
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Type -> m Type
    RecurseExprRecFn m
    rec Type
    e
          UnquoteData [DefInfo]
    i QName
    xs UniverseCheck
    uc [DefInfo]
    j [QName]
    cs Type
    e -> [DefInfo]
    -> QName
    -> UniverseCheck
    -> [DefInfo]
    -> [QName]
    -> Type
    -> Declaration
    UnquoteData [DefInfo]
    i QName
    xs UniverseCheck
    uc [DefInfo]
    j [QName]
    cs (Type -> Declaration) -> m Type -> m Declaration
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Type -> m Type
    RecurseExprRecFn m
    rec Type
    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
          UnfoldingDecl Range
    r [QName]
    ds        -> Range -> [QName] -> Declaration
    UnfoldingDecl Range
    r ([QName] -> Declaration) -> m [QName] -> m Declaration
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> [QName] -> m [QName]
    RecurseExprRecFn m
    rec [QName]
    ds
        where
          rec :: RecurseExprRecFn m
          rec :: RecurseExprRecFn m
    rec a
    e = (Type -> m Type -> m Type) -> a -> m a
    forall a (m :: * -> *). ExprLike a => RecurseExprFn m a
    forall (m :: * -> *). RecurseExprFn m a
    recurseExpr Type -> m Type -> m Type
    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 m a. Monoid m => (a -> m) -> t a -> m
    forall (t :: * -> *) m a.
    (Foldable t, Monoid m) =>
    (a -> m) -> t a -> m
    foldMap b -> m
    forall m. Collection KName m => 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 m. Collection KName m => a -> m
    forall a m. (DeclaredNames a, Collection KName m) => a -> m
    declaredNames b -> m
    forall m. Collection KName m => 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 m. Collection KName m => 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 m. Collection KName m => 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 (Ranged HasEta0)
    _ Maybe Range
    _ RecordConName
    c) = m
    kc where
        kc :: m
    kc = case RecordConName
    c of
          NamedRecCon QName
    c -> 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
    k QName
    c
          FreshRecCon{} -> m
    forall a. Monoid a => a
    mempty
        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 PragmaPolarities
    _ QName
    q Type
    _           -> 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 Type
    _         -> 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 Type
    _                  -> 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 Type
    _              -> 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 m. Collection KName m => [Declaration] -> m
    forall a m. (DeclaredNames a, Collection KName m) => a -> m
    declaredNames [Declaration]
    decls
          DataSig DefInfo
    _ Erased
    _ QName
    q GeneralizeTelescope
    _ Type
    _            -> 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 m a. Monoid m => (a -> m) -> [a] -> m
    forall (t :: * -> *) m a.
    (Foldable t, Monoid m) =>
    (a -> m) -> t a -> m
    foldMap Declaration -> m
    con [Declaration]
    decls
          RecSig DefInfo
    _ Erased
    _ QName
    q GeneralizeTelescope
    _ Type
    _             -> 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
    _ Type
    _ [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 m. Collection KName m => 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 m. Collection KName m => [Declaration] -> m
    forall a m. (DeclaredNames a, Collection KName m) => a -> m
    declaredNames [Declaration]
    decls
          PatternSynDef QName
    q [WithHiding 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 Type
    _         -> [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 Type
    _            -> [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
          UnquoteData [DefInfo]
    _ QName
    d UniverseCheck
    _ [DefInfo]
    _ [QName]
    cs Type
    _     -> KName -> m
    forall el coll. Singleton el coll => el -> coll
    singleton (KindOfName -> QName -> KName
    forall a. KindOfName -> a -> WithKind a
    WithKind KindOfName
    DataName QName
    d) m -> m -> m
    forall a. Semigroup a => a -> a -> a
    <> [KName] -> m
    forall el coll. Collection el coll => [el] -> coll
    fromList ((QName -> KName) -> [QName] -> [KName]
    forall a b. (a -> b) -> [a] -> [b]
    map (KindOfName -> QName -> KName
    forall a. KindOfName -> a -> WithKind a
    WithKind KindOfName
    ConName) [QName]
    cs) -- singleton _ <> map (WithKind ConName) cs
          FunDef DefInfo
    _ QName
    q [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 m. Collection KName m => [Clause] -> m
    forall a m. (DeclaredNames a, Collection KName m) => a -> m
    declaredNames [Clause]
    cls
          ScopedDecl ScopeInfo
    _ [Declaration]
    decls           -> [Declaration] -> m
    forall m. Collection KName m => [Declaration] -> m
    forall a m. (DeclaredNames a, Collection KName m) => a -> m
    declaredNames [Declaration]
    decls
          Section Range
    _ Erased
    _ ModuleName
    _ GeneralizeTelescope
    _ [Declaration]
    decls        -> [Declaration] -> m
    forall m. Collection KName m => [Declaration] -> m
    forall a m. (DeclaredNames a, Collection KName m) => a -> m
    declaredNames [Declaration]
    decls
          Pragma Range
    _ Pragma
    pragma              -> Pragma -> m
    forall m. Collection KName m => 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
          UnfoldingDecl{}              -> m
    forall a. Monoid a => a
    mempty
        where
        con :: Declaration -> m
    con = \case
          Axiom KindOfName
    _ DefInfo
    _ ArgInfo
    _ Maybe PragmaPolarities
    _ QName
    q Type
    _ -> 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
        InjectiveForInferencePragma{} -> m
    forall a. Monoid a => a
    mempty
        InlinePragma{}            -> m
    forall a. Monoid a => a
    mempty
        NotProjectionLikePragma{} -> m
    forall a. Monoid a => a
    mempty
        DisplayPragma{}           -> m
    forall a. Monoid a => a
    mempty
        OptionsPragma{}           -> m
    forall a. Monoid a => a
    mempty
        OverlapPragma{}           -> 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 Catchall
    _) = RHS -> m
    forall m. Collection KName m => 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 m. Collection KName m => 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
    _ Bool
    _ Maybe Declaration
    ds) = Maybe Declaration -> m
    forall m. Collection KName m => 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 Type
    _ Maybe Expr
    _                   -> m
    forall a. Monoid a => a
    mempty
        RHS
    AbsurdRHS                 -> m
    forall a. Monoid a => a
    mempty
        WithRHS QName
    _q List1 WithExpr
    _es List1 Clause
    cls        -> List1 Clause -> m
    forall m. Collection KName m => List1 Clause -> m
    forall a m. (DeclaredNames a, Collection KName m) => a -> m
    declaredNames List1 Clause
    cls
        RewriteRHS [RewriteEqn]
    _qes [ProblemEq]
    _ RHS
    rhs WhereDeclarations
    cls -> RHS -> m
    forall m. Collection KName m => 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 m. Collection KName m => 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
    --     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

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