    -- | Preprocess 'Agda.Syntax.Concrete.Declaration's, producing 'NiceDeclaration's.
    --
    --   * Attach fixity and syntax declarations to the definition they refer to.
    --
    --   * Distribute the following attributes to the individual definitions:
    --       @abstract@,
    --       @instance@,
    --       @postulate@,
    --       @primitive@,
    --       @private@,
    --       termination pragmas.
    --
    --   * Gather the function clauses belonging to one function definition.
    --
    --   * Expand ellipsis @...@ in function clauses following @with@.
    --
    --   * Infer mutual blocks.
    --     A block starts when a lone signature is encountered, and ends when
    --     all lone signatures have seen their definition.
    --
    --   * Handle interleaved mutual blocks.
    --     In an `interleaved mutual' block we:
    --     * leave the data and fun sigs in place
    --     * classify signatures in `constructor' block based on their return type
    --       and group them all as a data def at the position in the block where the
    --       first constructor for the data sig in question occured
    --     * classify fun clauses based on the declared function used and group them
    --       all as a fundef at the position in the block where the first such fun
    --       clause appeared
    --
    --   * Report basic well-formedness error,
    --     when one of the above transformation fails.
    --     When possible, errors should be deferred to the scope checking phase
    --     (ConcreteToAbstract), where we are in the TCM and can produce more
    --     informative error messages.

    module Agda.Syntax.Concrete.Definitions
        ( NiceDeclaration(..)
        , NiceConstructor, NiceTypeSignature
        , Clause(..)
        , DeclarationException(..)
        , DeclarationWarning(..), DeclarationWarning'(..), unsafeDeclarationWarning
        , Nice, NiceEnv(..), runNice
        , niceDeclarations
        , notSoNiceDeclarations
        , niceHasAbstract
        , Measure
        , declarationWarningName
        ) where

    import Prelude hiding (null)

    import Control.Monad.Except  ( )
    import Control.Monad.Reader  ( asks )
    import Control.Monad.State   ( MonadState(..), gets, StateT, runStateT )
    import Control.Monad.Trans   ( lift )

    import Data.Bifunctor
    import Data.Either (isLeft, isRight)
    import Data.Function (on)
    import qualified Data.Map as Map
    import Data.Map (Map)
    import Data.Maybe
    import Data.Semigroup ( Semigroup(..) )
    import qualified Data.List as List
    import qualified Data.Foldable as Fold
    import qualified Data.Traversable as Trav

    import Agda.Syntax.Concrete
    import Agda.Syntax.Concrete.Pattern
    import Agda.Syntax.Common hiding (TerminationCheck())
    import qualified Agda.Syntax.Common as Common
    import Agda.Syntax.Position
    import Agda.Syntax.Notation
    import Agda.Syntax.Concrete.Pretty () --instance only
    import Agda.Syntax.Concrete.Fixity
    import Agda.Syntax.Common.Pretty

    import Agda.Syntax.Concrete.Definitions.Errors
    import Agda.Syntax.Concrete.Definitions.Monad
    import Agda.Syntax.Concrete.Definitions.Types

    import Agda.Utils.AffineHole
    import Agda.Utils.CallStack ( CallStack, HasCallStack, withCallerCallStack )
    import Agda.Utils.Functor
    import Agda.Utils.Lens
    import Agda.Utils.List (spanJust)
    import Agda.Utils.List1 (List1, pattern (:|), (<|))
    import qualified Agda.Utils.List1 as List1
    import Agda.Utils.Maybe
    import Agda.Utils.Monad
    import Agda.Utils.Null
    import Agda.Utils.Singleton
    import Agda.Utils.Three
    import Agda.Utils.Tuple
    import Agda.Utils.Update

    import Agda.Utils.Impossible

    {--------------------------------------------------------------------------
        The niceifier
     --------------------------------------------------------------------------}

    -- | Check that declarations in a mutual block are consistently
    --   equipped with MEASURE pragmas, or whether there is a
    --   NO_TERMINATION_CHECK pragma.
    combineTerminationChecks :: Range -> [TerminationCheck] -> Nice TerminationCheck
    combineTerminationChecks :: Range -> [TerminationCheck] -> Nice TerminationCheck
    combineTerminationChecks Range
    r = [TerminationCheck] -> Nice TerminationCheck
    loop
      where
      loop :: [TerminationCheck] -> Nice TerminationCheck
      loop :: [TerminationCheck] -> Nice TerminationCheck
    loop []         = TerminationCheck -> Nice TerminationCheck
    forall a. a -> Nice a
    forall (m :: * -> *) a. Monad m => a -> m a
    return TerminationCheck
    forall m. TerminationCheck m
    TerminationCheck
      loop (TerminationCheck
    tc : [TerminationCheck]
    tcs) = do
        tc' <- [TerminationCheck] -> Nice TerminationCheck
    loop [TerminationCheck]
    tcs
        case (tc, tc') of
          (TerminationCheck
    TerminationCheck      , TerminationCheck
    tc'                   ) -> TerminationCheck -> Nice TerminationCheck
    forall a. a -> Nice a
    forall (m :: * -> *) a. Monad m => a -> m a
    return TerminationCheck
    tc'
          (TerminationCheck
    tc                    , TerminationCheck
    TerminationCheck      ) -> TerminationCheck -> Nice TerminationCheck
    forall a. a -> Nice a
    forall (m :: * -> *) a. Monad m => a -> m a
    return TerminationCheck
    tc
          (TerminationCheck
    NonTerminating        , TerminationCheck
    NonTerminating        ) -> TerminationCheck -> Nice TerminationCheck
    forall a. a -> Nice a
    forall (m :: * -> *) a. Monad m => a -> m a
    return TerminationCheck
    forall m. TerminationCheck m
    NonTerminating
          (TerminationCheck
    NoTerminationCheck    , TerminationCheck
    NoTerminationCheck    ) -> TerminationCheck -> Nice TerminationCheck
    forall a. a -> Nice a
    forall (m :: * -> *) a. Monad m => a -> m a
    return TerminationCheck
    forall m. TerminationCheck m
    NoTerminationCheck
          (TerminationCheck
    NoTerminationCheck    , TerminationCheck
    Terminating           ) -> TerminationCheck -> Nice TerminationCheck
    forall a. a -> Nice a
    forall (m :: * -> *) a. Monad m => a -> m a
    return TerminationCheck
    forall m. TerminationCheck m
    Terminating
          (TerminationCheck
    Terminating           , TerminationCheck
    NoTerminationCheck    ) -> TerminationCheck -> Nice TerminationCheck
    forall a. a -> Nice a
    forall (m :: * -> *) a. Monad m => a -> m a
    return TerminationCheck
    forall m. TerminationCheck m
    Terminating
          (TerminationCheck
    Terminating           , TerminationCheck
    Terminating           ) -> TerminationCheck -> Nice TerminationCheck
    forall a. a -> Nice a
    forall (m :: * -> *) a. Monad m => a -> m a
    return TerminationCheck
    forall m. TerminationCheck m
    Terminating
          (TerminationMeasure{}  , TerminationMeasure{}  ) -> TerminationCheck -> Nice TerminationCheck
    forall a. a -> Nice a
    forall (m :: * -> *) a. Monad m => a -> m a
    return TerminationCheck
    tc
          (TerminationMeasure Range
    r Name
    _, TerminationCheck
    NoTerminationCheck    ) -> Range -> Nice TerminationCheck
    forall {a}. Range -> Nice a
    failure Range
    r
          (TerminationMeasure Range
    r Name
    _, TerminationCheck
    Terminating           ) -> Range -> Nice TerminationCheck
    forall {a}. Range -> Nice a
    failure Range
    r
          (TerminationCheck
    NoTerminationCheck    , TerminationMeasure Range
    r Name
    _) -> Range -> Nice TerminationCheck
    forall {a}. Range -> Nice a
    failure Range
    r
          (TerminationCheck
    Terminating           , TerminationMeasure Range
    r Name
    _) -> Range -> Nice TerminationCheck
    forall {a}. Range -> Nice a
    failure Range
    r
          (TerminationMeasure Range
    r Name
    _, TerminationCheck
    NonTerminating        ) -> Range -> Nice TerminationCheck
    forall {a}. Range -> Nice a
    failure Range
    r
          (TerminationCheck
    NonTerminating        , TerminationMeasure Range
    r Name
    _) -> Range -> Nice TerminationCheck
    forall {a}. Range -> Nice a
    failure Range
    r
          (TerminationCheck
    NoTerminationCheck    , TerminationCheck
    NonTerminating        ) -> Range -> Nice TerminationCheck
    forall {a}. Range -> Nice a
    failure Range
    r
          (TerminationCheck
    Terminating           , TerminationCheck
    NonTerminating        ) -> Range -> Nice TerminationCheck
    forall {a}. Range -> Nice a
    failure Range
    r
          (TerminationCheck
    NonTerminating        , TerminationCheck
    NoTerminationCheck    ) -> Range -> Nice TerminationCheck
    forall {a}. Range -> Nice a
    failure Range
    r
          (TerminationCheck
    NonTerminating        , TerminationCheck
    Terminating           ) -> Range -> Nice TerminationCheck
    forall {a}. Range -> Nice a
    failure Range
    r
      failure :: Range -> Nice a
    failure Range
    r = DeclarationException' -> Nice a
    forall a. HasCallStack => DeclarationException' -> Nice a
    declarationException (DeclarationException' -> Nice a)
    -> DeclarationException' -> Nice a
    forall a b. (a -> b) -> a -> b
    $ Range -> DeclarationException'
    InvalidMeasureMutual Range
    r

    combineCoverageChecks :: [CoverageCheck] -> CoverageCheck
    combineCoverageChecks :: [CoverageCheck] -> CoverageCheck
    combineCoverageChecks = [CoverageCheck] -> CoverageCheck
    forall m. Monoid m => [m] -> m
    forall (t :: * -> *) m. (Foldable t, Monoid m) => t m -> m
    Fold.fold

    combinePositivityChecks :: [PositivityCheck] -> PositivityCheck
    combinePositivityChecks :: [PositivityCheck] -> PositivityCheck
    combinePositivityChecks = [PositivityCheck] -> PositivityCheck
    forall m. Monoid m => [m] -> m
    forall (t :: * -> *) m. (Foldable t, Monoid m) => t m -> m
    Fold.fold

    data DeclKind
        = LoneSigDecl Range DataRecOrFun Name
        | LoneDefs DataRecOrFun [Name]
        | OtherDecl
      deriving (DeclKind -> DeclKind -> Bool
    (DeclKind -> DeclKind -> Bool)
    -> (DeclKind -> DeclKind -> Bool) -> Eq DeclKind
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    $c== :: DeclKind -> DeclKind -> Bool
    == :: DeclKind -> DeclKind -> Bool
    $c/= :: DeclKind -> DeclKind -> Bool
    /= :: DeclKind -> DeclKind -> Bool
    Eq, Int -> DeclKind -> ShowS
    [DeclKind] -> ShowS
    DeclKind -> String
    (Int -> DeclKind -> ShowS)
    -> (DeclKind -> String) -> ([DeclKind] -> ShowS) -> Show DeclKind
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    $cshowsPrec :: Int -> DeclKind -> ShowS
    showsPrec :: Int -> DeclKind -> ShowS
    $cshow :: DeclKind -> String
    show :: DeclKind -> String
    $cshowList :: [DeclKind] -> ShowS
    showList :: [DeclKind] -> ShowS
    Show)

    declKind :: NiceDeclaration -> DeclKind
    declKind :: NiceDeclaration -> DeclKind
    declKind (FunSig Range
    r Access
    _ IsAbstract
    _ IsInstance
    _ IsMacro
    _ ArgInfo
    _ TerminationCheck
    tc CoverageCheck
    cc Name
    x Expr
    _)      = Range -> DataRecOrFun -> Name -> DeclKind
    LoneSigDecl Range
    r (TerminationCheck -> CoverageCheck -> DataRecOrFun
    FunName TerminationCheck
    tc CoverageCheck
    cc) Name
    x
    declKind (NiceRecSig Range
    r Erased
    _ Access
    _ IsAbstract
    _ PositivityCheck
    pc UniverseCheck
    uc Name
    x [LamBinding]
    _ Expr
    _)    = Range -> DataRecOrFun -> Name -> DeclKind
    LoneSigDecl Range
    r (PositivityCheck -> UniverseCheck -> DataRecOrFun
    RecName PositivityCheck
    pc UniverseCheck
    uc) Name
    x
    declKind (NiceDataSig Range
    r Erased
    _ Access
    _ IsAbstract
    _ PositivityCheck
    pc UniverseCheck
    uc Name
    x [LamBinding]
    _ Expr
    _)   = Range -> DataRecOrFun -> Name -> DeclKind
    LoneSigDecl Range
    r (PositivityCheck -> UniverseCheck -> DataRecOrFun
    DataName PositivityCheck
    pc UniverseCheck
    uc) Name
    x
    declKind (FunDef Range
    r [Declaration]
    _ IsAbstract
    abs IsInstance
    ins TerminationCheck
    tc CoverageCheck
    cc Name
    x [Clause]
    _)      = DataRecOrFun -> [Name] -> DeclKind
    LoneDefs (TerminationCheck -> CoverageCheck -> DataRecOrFun
    FunName TerminationCheck
    tc CoverageCheck
    cc) [Name
    x]
    declKind (NiceDataDef Range
    _ Origin
    _ IsAbstract
    _ PositivityCheck
    pc UniverseCheck
    uc Name
    x [LamBinding]
    pars [NiceDeclaration]
    _)  = DataRecOrFun -> [Name] -> DeclKind
    LoneDefs (PositivityCheck -> UniverseCheck -> DataRecOrFun
    DataName PositivityCheck
    pc UniverseCheck
    uc) [Name
    x]
    declKind (NiceUnquoteData Range
    _ Access
    _ IsAbstract
    _ PositivityCheck
    pc UniverseCheck
    uc Name
    x [Name]
    _ Expr
    _) = DataRecOrFun -> [Name] -> DeclKind
    LoneDefs (PositivityCheck -> UniverseCheck -> DataRecOrFun
    DataName PositivityCheck
    pc UniverseCheck
    uc) [Name
    x]
    declKind (NiceRecDef Range
    _ Origin
    _ IsAbstract
    _ PositivityCheck
    pc UniverseCheck
    uc Name
    x [RecordDirective]
    _ [LamBinding]
    pars [Declaration]
    _) = DataRecOrFun -> [Name] -> DeclKind
    LoneDefs (PositivityCheck -> UniverseCheck -> DataRecOrFun
    RecName PositivityCheck
    pc UniverseCheck
    uc) [Name
    x]
    declKind (NiceUnquoteDef Range
    _ Access
    _ IsAbstract
    _ TerminationCheck
    tc CoverageCheck
    cc [Name]
    xs Expr
    _)   = DataRecOrFun -> [Name] -> DeclKind
    LoneDefs (TerminationCheck -> CoverageCheck -> DataRecOrFun
    FunName TerminationCheck
    tc CoverageCheck
    cc) [Name]
    xs
    declKind Axiom{}                             = DeclKind
    OtherDecl
    declKind NiceField{}                         = DeclKind
    OtherDecl
    declKind PrimitiveFunction{}                 = DeclKind
    OtherDecl
    declKind NiceMutual{}                        = DeclKind
    OtherDecl
    declKind NiceModule{}                        = DeclKind
    OtherDecl
    declKind NiceModuleMacro{}                   = DeclKind
    OtherDecl
    declKind NiceOpen{}                          = DeclKind
    OtherDecl
    declKind NiceImport{}                        = DeclKind
    OtherDecl
    declKind NicePragma{}                        = DeclKind
    OtherDecl
    declKind NiceFunClause{}                     = DeclKind
    OtherDecl
    declKind NicePatternSyn{}                    = DeclKind
    OtherDecl
    declKind NiceGeneralize{}                    = DeclKind
    OtherDecl
    declKind NiceUnquoteDecl{}                   = DeclKind
    OtherDecl
    declKind NiceLoneConstructor{}               = DeclKind
    OtherDecl
    declKind NiceOpaque{}                        = DeclKind
    OtherDecl

    -- | Replace (Data/Rec/Fun)Sigs with Axioms for postulated names
    --   The first argument is a list of axioms only.
    replaceSigs
      :: LoneSigs               -- ^ Lone signatures to be turned into Axioms
      -> [NiceDeclaration]      -- ^ Declarations containing them
      -> [NiceDeclaration]      -- ^ In the output, everything should be defined
    replaceSigs :: LoneSigs -> [NiceDeclaration] -> [NiceDeclaration]
    replaceSigs LoneSigs
    ps = if LoneSigs -> Bool
    forall k a. Map k a -> Bool
    Map.null LoneSigs
    ps then [NiceDeclaration] -> [NiceDeclaration]
    forall a. a -> a
    id else \case
      []     -> [NiceDeclaration]
    forall a. HasCallStack => a
    __IMPOSSIBLE__
      (NiceDeclaration
    d:[NiceDeclaration]
    ds) ->
        case NiceDeclaration -> Maybe (Name, NiceDeclaration)
    replaceable NiceDeclaration
    d of
          -- If declaration d of x is mentioned in the map of lone signatures then replace
          -- it with an axiom
          Just (Name
    x, NiceDeclaration
    axiom)
            | (Just (LoneSig Range
    _ Name
    x' DataRecOrFun
    _), LoneSigs
    ps') <- (Name -> LoneSig -> Maybe LoneSig)
    -> Name -> LoneSigs -> (Maybe LoneSig, LoneSigs)
    forall k a.
    Ord k =>
    (k -> a -> Maybe a) -> k -> Map k a -> (Maybe a, Map k a)
    Map.updateLookupWithKey (\ Name
    _ LoneSig
    _ -> Maybe LoneSig
    forall a. Maybe a
    Nothing) Name
    x LoneSigs
    ps
            , Name -> Range
    forall a. HasRange a => a -> Range
    getRange Name
    x Range -> Range -> Bool
    forall a. Eq a => a -> a -> Bool
    == Name -> Range
    forall a. HasRange a => a -> Range
    getRange Name
    x'
                -- Use the range as UID to ensure we do not replace the wrong signature.
                -- This could happen if the user wrote a duplicate definition.
            -> NiceDeclaration
    axiom NiceDeclaration -> [NiceDeclaration] -> [NiceDeclaration]
    forall a. a -> [a] -> [a]
    : LoneSigs -> [NiceDeclaration] -> [NiceDeclaration]
    replaceSigs LoneSigs
    ps' [NiceDeclaration]
    ds
          Maybe (Name, NiceDeclaration)
    _ -> NiceDeclaration
    d     NiceDeclaration -> [NiceDeclaration] -> [NiceDeclaration]
    forall a. a -> [a] -> [a]
    : LoneSigs -> [NiceDeclaration] -> [NiceDeclaration]
    replaceSigs LoneSigs
    ps  [NiceDeclaration]
    ds

      where

        -- A @replaceable@ declaration is a signature. It has a name and we can make an
        -- @Axiom@ out of it.
        replaceable :: NiceDeclaration -> Maybe (Name, NiceDeclaration)
        replaceable :: NiceDeclaration -> Maybe (Name, NiceDeclaration)
    replaceable = \case
          FunSig Range
    r Access
    acc IsAbstract
    abst IsInstance
    inst IsMacro
    _ ArgInfo
    argi TerminationCheck
    _ CoverageCheck
    _ Name
    x' Expr
    e ->
            -- #4881: Don't use the unique NameId for NoName lookups.
            let x :: Name
    x = if Name -> Bool
    forall a. IsNoName a => a -> Bool
    isNoName Name
    x' then Range -> Name
    noName (Name -> Range
    nameRange Name
    x') else Name
    x' in
            (Name, NiceDeclaration) -> Maybe (Name, NiceDeclaration)
    forall a. a -> Maybe a
    Just (Name
    x, Range
    -> Access
    -> IsAbstract
    -> IsInstance
    -> ArgInfo
    -> Name
    -> Expr
    -> NiceDeclaration
    Axiom Range
    r Access
    acc IsAbstract
    abst IsInstance
    inst (Origin -> ArgInfo -> ArgInfo
    forall a. LensOrigin a => Origin -> a -> a
    setOrigin Origin
    Inserted ArgInfo
    argi) Name
    x' Expr
    e)
          NiceRecSig Range
    r Erased
    erased Access
    acc IsAbstract
    abst PositivityCheck
    _ UniverseCheck
    _ Name
    x [LamBinding]
    pars Expr
    t ->
            let e :: Expr
    e = Expr -> Expr
    Generalized (Expr -> Expr) -> Expr -> Expr
    forall a b. (a -> b) -> a -> b
    $ Telescope -> Expr -> Expr
    makePi (Range -> [LamBinding] -> Telescope
    lamBindingsToTelescope Range
    r [LamBinding]
    pars) Expr
    t in
            (Name, NiceDeclaration) -> Maybe (Name, NiceDeclaration)
    forall a. a -> Maybe a
    Just (Name
    x, Range
    -> Access
    -> IsAbstract
    -> IsInstance
    -> ArgInfo
    -> Name
    -> Expr
    -> NiceDeclaration
    Axiom Range
    r Access
    acc IsAbstract
    abst IsInstance
    NotInstanceDef
                       (Origin -> ArgInfo -> ArgInfo
    forall a. LensOrigin a => Origin -> a -> a
    setOrigin Origin
    Inserted (Quantity -> ArgInfo -> ArgInfo
    forall a. LensQuantity a => Quantity -> a -> a
    setQuantity (Erased -> Quantity
    asQuantity Erased
    erased) ArgInfo
    defaultArgInfo)) Name
    x Expr
    e)
          NiceDataSig Range
    r Erased
    erased Access
    acc IsAbstract
    abst PositivityCheck
    _ UniverseCheck
    _ Name
    x [LamBinding]
    pars Expr
    t ->
            let e :: Expr
    e = Expr -> Expr
    Generalized (Expr -> Expr) -> Expr -> Expr
    forall a b. (a -> b) -> a -> b
    $ Telescope -> Expr -> Expr
    makePi (Range -> [LamBinding] -> Telescope
    lamBindingsToTelescope Range
    r [LamBinding]
    pars) Expr
    t in
            (Name, NiceDeclaration) -> Maybe (Name, NiceDeclaration)
    forall a. a -> Maybe a
    Just (Name
    x, Range
    -> Access
    -> IsAbstract
    -> IsInstance
    -> ArgInfo
    -> Name
    -> Expr
    -> NiceDeclaration
    Axiom Range
    r Access
    acc IsAbstract
    abst IsInstance
    NotInstanceDef
                       (Origin -> ArgInfo -> ArgInfo
    forall a. LensOrigin a => Origin -> a -> a
    setOrigin Origin
    Inserted (Quantity -> ArgInfo -> ArgInfo
    forall a. LensQuantity a => Quantity -> a -> a
    setQuantity (Erased -> Quantity
    asQuantity Erased
    erased) ArgInfo
    defaultArgInfo)) Name
    x Expr
    e)
          NiceDeclaration
    _ -> Maybe (Name, NiceDeclaration)
    forall a. Maybe a
    Nothing

    -- | Main. Fixities (or more precisely syntax declarations) are needed when
    --   grouping function clauses.
    niceDeclarations :: Fixities -> [Declaration] -> Nice [NiceDeclaration]
    niceDeclarations :: Fixities -> [Declaration] -> Nice [NiceDeclaration]
    niceDeclarations Fixities
    fixs [Declaration]
    ds = do

      -- Run the nicifier in an initial environment. But keep the warnings.
      st <- Nice NiceState
    forall s (m :: * -> *). MonadState s m => m s
    get
      put $ initNiceState { niceWarn = niceWarn st }
      nds <- nice ds

      -- Check that every signature got its definition.
      ps <- use loneSigs
      checkLoneSigs ps
      -- We postulate the missing ones and insert them in place of the corresponding @FunSig@
      let ds = LoneSigs -> [NiceDeclaration] -> [NiceDeclaration]
    replaceSigs LoneSigs
    ps [NiceDeclaration]
    nds

      -- Note that loneSigs is ensured to be empty.
      -- (Important, since inferMutualBlocks also uses loneSigs state).
      res <- inferMutualBlocks ds

      -- Restore the old state, but keep the warnings.
      warns <- gets niceWarn
      put $ st { niceWarn = warns }
      return res

      where

        inferMutualBlocks :: [NiceDeclaration] -> Nice [NiceDeclaration]
        inferMutualBlocks :: [NiceDeclaration] -> Nice [NiceDeclaration]
    inferMutualBlocks [] = [NiceDeclaration] -> Nice [NiceDeclaration]
    forall a. a -> Nice a
    forall (m :: * -> *) a. Monad m => a -> m a
    return []
        inferMutualBlocks (NiceDeclaration
    d : [NiceDeclaration]
    ds) =
          case NiceDeclaration -> DeclKind
    declKind NiceDeclaration
    d of
            DeclKind
    OtherDecl    -> (NiceDeclaration
    d NiceDeclaration -> [NiceDeclaration] -> [NiceDeclaration]
    forall a. a -> [a] -> [a]
    :) ([NiceDeclaration] -> [NiceDeclaration])
    -> Nice [NiceDeclaration] -> Nice [NiceDeclaration]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> [NiceDeclaration] -> Nice [NiceDeclaration]
    inferMutualBlocks [NiceDeclaration]
    ds
            LoneDefs{}   -> (NiceDeclaration
    d NiceDeclaration -> [NiceDeclaration] -> [NiceDeclaration]
    forall a. a -> [a] -> [a]
    :) ([NiceDeclaration] -> [NiceDeclaration])
    -> Nice [NiceDeclaration] -> Nice [NiceDeclaration]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> [NiceDeclaration] -> Nice [NiceDeclaration]
    inferMutualBlocks [NiceDeclaration]
    ds  -- Andreas, 2017-10-09, issue #2576: report error in ConcreteToAbstract
            LoneSigDecl Range
    r DataRecOrFun
    k Name
    x  -> do
              _ <- Range -> Name -> DataRecOrFun -> Nice Name
    addLoneSig Range
    r Name
    x DataRecOrFun
    k
              InferredMutual checks nds0 ds1 <- untilAllDefined (mutualChecks k) ds
              -- If we still have lone signatures without any accompanying definition,
              -- we postulate the definition and substitute the axiom for the lone signature
              ps <- use loneSigs
              checkLoneSigs ps
              let ds0 = LoneSigs -> [NiceDeclaration] -> [NiceDeclaration]
    replaceSigs LoneSigs
    ps (NiceDeclaration
    d NiceDeclaration -> [NiceDeclaration] -> [NiceDeclaration]
    forall a. a -> [a] -> [a]
    : [NiceDeclaration]
    nds0) -- NB: don't forget the LoneSig the block started with!
              -- We then keep processing the rest of the block
              tc <- combineTerminationChecks (getRange d) (mutualTermination checks)
              let cc = [CoverageCheck] -> CoverageCheck
    combineCoverageChecks              (MutualChecks -> [CoverageCheck]
    mutualCoverage MutualChecks
    checks)
              let pc = [PositivityCheck] -> PositivityCheck
    combinePositivityChecks            (MutualChecks -> [PositivityCheck]
    mutualPositivity MutualChecks
    checks)
              (NiceMutual empty tc cc pc ds0 :) <$> inferMutualBlocks ds1
          where
            untilAllDefined :: MutualChecks -> [NiceDeclaration] -> Nice InferredMutual
            untilAllDefined :: MutualChecks -> [NiceDeclaration] -> Nice InferredMutual
    untilAllDefined MutualChecks
    checks [NiceDeclaration]
    ds = do
              done <- Nice Bool
    noLoneSigs
              if done then return (InferredMutual checks [] ds) else
                case ds of
                  []     -> InferredMutual -> Nice InferredMutual
    forall a. a -> Nice a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (MutualChecks
    -> [NiceDeclaration] -> [NiceDeclaration] -> InferredMutual
    InferredMutual MutualChecks
    checks [] [NiceDeclaration]
    ds)
                  NiceDeclaration
    d : [NiceDeclaration]
    ds -> case NiceDeclaration -> DeclKind
    declKind NiceDeclaration
    d of
                    LoneSigDecl Range
    r DataRecOrFun
    k Name
    x -> do
                      Nice Name -> Nice ()
    forall (f :: * -> *) a. Functor f => f a -> f ()
    void (Nice Name -> Nice ()) -> Nice Name -> Nice ()
    forall a b. (a -> b) -> a -> b
    $ Range -> Name -> DataRecOrFun -> Nice Name
    addLoneSig Range
    r Name
    x DataRecOrFun
    k
                      NiceDeclaration -> InferredMutual -> InferredMutual
    extendInferredBlock  NiceDeclaration
    d (InferredMutual -> InferredMutual)
    -> Nice InferredMutual -> Nice InferredMutual
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> MutualChecks -> [NiceDeclaration] -> Nice InferredMutual
    untilAllDefined (DataRecOrFun -> MutualChecks
    mutualChecks DataRecOrFun
    k MutualChecks -> MutualChecks -> MutualChecks
    forall a. Semigroup a => a -> a -> a
    <> MutualChecks
    checks) [NiceDeclaration]
    ds
                    LoneDefs DataRecOrFun
    k [Name]
    xs -> do
                      (Name -> Nice ()) -> [Name] -> Nice ()
    forall (t :: * -> *) (m :: * -> *) a b.
    (Foldable t, Monad m) =>
    (a -> m b) -> t a -> m ()
    mapM_ Name -> Nice ()
    removeLoneSig [Name]
    xs
                      NiceDeclaration -> InferredMutual -> InferredMutual
    extendInferredBlock  NiceDeclaration
    d (InferredMutual -> InferredMutual)
    -> Nice InferredMutual -> Nice InferredMutual
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> MutualChecks -> [NiceDeclaration] -> Nice InferredMutual
    untilAllDefined (DataRecOrFun -> MutualChecks
    mutualChecks DataRecOrFun
    k MutualChecks -> MutualChecks -> MutualChecks
    forall a. Semigroup a => a -> a -> a
    <> MutualChecks
    checks) [NiceDeclaration]
    ds
                    DeclKind
    OtherDecl -> NiceDeclaration -> InferredMutual -> InferredMutual
    extendInferredBlock NiceDeclaration
    d (InferredMutual -> InferredMutual)
    -> Nice InferredMutual -> Nice InferredMutual
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> MutualChecks -> [NiceDeclaration] -> Nice InferredMutual
    untilAllDefined MutualChecks
    checks [NiceDeclaration]
    ds

        nice :: [Declaration] -> Nice [NiceDeclaration]
        nice :: [Declaration] -> Nice [NiceDeclaration]
    nice [] = [NiceDeclaration] -> Nice [NiceDeclaration]
    forall a. a -> Nice a
    forall (m :: * -> *) a. Monad m => a -> m a
    return []
        nice [Declaration]
    ds = do
          (xs , ys) <- [Declaration] -> Nice ([NiceDeclaration], [Declaration])
    nice1 [Declaration]
    ds
          (xs ++) <$> nice ys

        nice1 :: [Declaration] -> Nice ([NiceDeclaration], [Declaration])
        nice1 :: [Declaration] -> Nice ([NiceDeclaration], [Declaration])
    nice1 []     = ([NiceDeclaration], [Declaration])
    -> Nice ([NiceDeclaration], [Declaration])
    forall a. a -> Nice a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([], []) -- Andreas, 2017-09-16, issue #2759: no longer __IMPOSSIBLE__
        nice1 (Declaration
    d:[Declaration]
    ds) = do
          let justWarning :: HasCallStack => DeclarationWarning' -> Nice ([NiceDeclaration], [Declaration])
              justWarning :: HasCallStack =>
    DeclarationWarning' -> Nice ([NiceDeclaration], [Declaration])
    justWarning DeclarationWarning'
    w = do
                -- NOTE: This is the location of the invoker of justWarning, not here.
                (CallStack -> Nice ()) -> Nice ()
    forall b. HasCallStack => (CallStack -> b) -> b
    withCallerCallStack ((CallStack -> Nice ()) -> Nice ())
    -> (CallStack -> Nice ()) -> Nice ()
    forall a b. (a -> b) -> a -> b
    $ DeclarationWarning' -> CallStack -> Nice ()
    declarationWarning' DeclarationWarning'
    w
                [Declaration] -> Nice ([NiceDeclaration], [Declaration])
    nice1 [Declaration]
    ds

          case Declaration
    d of

            TypeSig ArgInfo
    info TacticAttribute
    _tac Name
    x Expr
    t -> do
              termCheck <- Lens' NiceState TerminationCheck -> Nice TerminationCheck
    forall o (m :: * -> *) i. MonadState o m => Lens' o i -> m i
    use (TerminationCheck -> f TerminationCheck)
    -> NiceState -> f NiceState
    Lens' NiceState TerminationCheck
    terminationCheckPragma
              covCheck  <- use coverageCheckPragma
              -- Andreas, 2020-09-28, issue #4950: take only range of identifier,
              -- since parser expands type signatures with several identifiers
              -- (like @x y z : A@) into several type signatures (with imprecise ranges).
              let r = Name -> Range
    forall a. HasRange a => a -> Range
    getRange Name
    x
              -- register x as lone type signature, to recognize clauses later
              x' <- addLoneSig r x $ FunName termCheck covCheck
              return ([FunSig r PublicAccess ConcreteDef NotInstanceDef NotMacroDef info termCheck covCheck x' t] , ds)

            -- Should not show up: all FieldSig are part of a Field block
            FieldSig{} -> Nice ([NiceDeclaration], [Declaration])
    forall a. HasCallStack => a
    __IMPOSSIBLE__

            Generalize KwRange
    r [] -> HasCallStack =>
    DeclarationWarning' -> Nice ([NiceDeclaration], [Declaration])
    DeclarationWarning' -> Nice ([NiceDeclaration], [Declaration])
    justWarning (DeclarationWarning' -> Nice ([NiceDeclaration], [Declaration]))
    -> DeclarationWarning' -> Nice ([NiceDeclaration], [Declaration])
    forall a b. (a -> b) -> a -> b
    $ KwRange -> DeclarationWarning'
    EmptyGeneralize KwRange
    r
            Generalize KwRange
    _ [Declaration]
    sigs -> do
              gs <- [Declaration]
    -> (Declaration -> Nice NiceDeclaration) -> Nice [NiceDeclaration]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    t a -> (a -> m b) -> m (t b)
    forM [Declaration]
    sigs ((Declaration -> Nice NiceDeclaration) -> Nice [NiceDeclaration])
    -> (Declaration -> Nice NiceDeclaration) -> Nice [NiceDeclaration]
    forall a b. (a -> b) -> a -> b
    $ \case
                sig :: Declaration
    sig@(TypeSig ArgInfo
    info TacticAttribute
    tac Name
    x Expr
    t) -> do
                  -- Andreas, 2022-03-25, issue #5850:
                  -- Warn about @variable {x} : A@ which is equivalent to @variable x : A@.
                  Bool -> Nice () -> Nice ()
    forall b (m :: * -> *). (IsBool b, Monad m) => b -> m () -> m ()
    when (ArgInfo -> Hiding
    forall a. LensHiding a => a -> Hiding
    getHiding ArgInfo
    info Hiding -> Hiding -> Bool
    forall a. Eq a => a -> a -> Bool
    == Hiding
    Hidden) (Nice () -> Nice ()) -> Nice () -> Nice ()
    forall a b. (a -> b) -> a -> b
    $
                    HasCallStack => DeclarationWarning' -> Nice ()
    DeclarationWarning' -> Nice ()
    declarationWarning (DeclarationWarning' -> Nice ()) -> DeclarationWarning' -> Nice ()
    forall a b. (a -> b) -> a -> b
    $ Range -> DeclarationWarning'
    HiddenGeneralize (Range -> DeclarationWarning') -> Range -> DeclarationWarning'
    forall a b. (a -> b) -> a -> b
    $ Name -> Range
    forall a. HasRange a => a -> Range
    getRange Name
    x
                  NiceDeclaration -> Nice NiceDeclaration
    forall a. a -> Nice a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (NiceDeclaration -> Nice NiceDeclaration)
    -> NiceDeclaration -> Nice NiceDeclaration
    forall a b. (a -> b) -> a -> b
    $ Range
    -> Access
    -> ArgInfo
    -> TacticAttribute
    -> Name
    -> Expr
    -> NiceDeclaration
    NiceGeneralize (Declaration -> Range
    forall a. HasRange a => a -> Range
    getRange Declaration
    sig) Access
    PublicAccess ArgInfo
    info TacticAttribute
    tac Name
    x Expr
    t
                Declaration
    _ -> Nice NiceDeclaration
    forall a. HasCallStack => a
    __IMPOSSIBLE__
              return (gs, ds)

            (FunClause LHS
    lhs RHS
    _ WhereClause
    _ Catchall
    _)         -> do
              termCheck <- Lens' NiceState TerminationCheck -> Nice TerminationCheck
    forall o (m :: * -> *) i. MonadState o m => Lens' o i -> m i
    use (TerminationCheck -> f TerminationCheck)
    -> NiceState -> f NiceState
    Lens' NiceState TerminationCheck
    terminationCheckPragma
              covCheck  <- use coverageCheckPragma
              catchall  <- popCatchallPragma
              xs <- loneFuns <$> use loneSigs
              -- for each type signature 'x' waiting for clauses, we try
              -- if we have some clauses for 'x'
              case [ (x, (x', fits, rest))
                   | (x, x') <- xs
                   , let (fits, rest) =
                          -- Anonymous declarations only have 1 clause each!
                          if isNoName x then ([d], ds)
                          else span (couldBeFunClauseOf (Map.lookup x fixs) x) (d : ds)
                   , not (null fits)
                   ] of

                -- case: clauses match none of the sigs
                [] -> case LHS
    lhs of
                  -- Subcase: The lhs is single identifier (potentially anonymous).
                  -- Treat it as a function clause without a type signature.
                  LHS Pattern
    p [] [] | Just Name
    x <- Pattern -> Maybe Name
    isSingleIdentifierP Pattern
    p -> do
                    d  <- ArgInfo
    -> TerminationCheck
    -> CoverageCheck
    -> Name
    -> Maybe Expr
    -> [Declaration]
    -> Nice [NiceDeclaration]
    mkFunDef (Origin -> ArgInfo -> ArgInfo
    forall a. LensOrigin a => Origin -> a -> a
    setOrigin Origin
    Inserted ArgInfo
    defaultArgInfo) TerminationCheck
    termCheck CoverageCheck
    covCheck Name
    x Maybe Expr
    forall a. Maybe a
    Nothing ([Declaration] -> Nice [NiceDeclaration])
    -> [Declaration] -> Nice [NiceDeclaration]
    forall a b. (a -> b) -> a -> b
    $ Declaration -> [Declaration]
    forall el coll. Singleton el coll => el -> coll
    singleton Declaration
    d -- fun def without type signature is relevant
                    return (d , ds)
                  -- Subcase: The lhs is a proper pattern.
                  -- This could be a let-pattern binding. Pass it on.
                  -- A missing type signature error might be raise in ConcreteToAbstract
                  LHS
    _ -> do
                    ([NiceDeclaration], [Declaration])
    -> Nice ([NiceDeclaration], [Declaration])
    forall a. a -> Nice a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([Range
    -> Access
    -> IsAbstract
    -> TerminationCheck
    -> CoverageCheck
    -> Catchall
    -> Declaration
    -> NiceDeclaration
    NiceFunClause (Declaration -> Range
    forall a. HasRange a => a -> Range
    getRange Declaration
    d) Access
    PublicAccess IsAbstract
    ConcreteDef TerminationCheck
    termCheck CoverageCheck
    covCheck Catchall
    catchall Declaration
    d] , [Declaration]
    ds)

                -- case: clauses match exactly one of the sigs
                [(Name
    x,(Name
    x',[Declaration]
    fits,[Declaration]
    rest))] -> do
                   -- The x'@NoName{} is the unique version of x@NoName{}.
                   Name -> Nice ()
    removeLoneSig Name
    x
                   ds  <- [Declaration] -> Nice [Declaration]
    expandEllipsis [Declaration]
    fits
                   cs  <- mkClauses x' ds empty
                   return ([FunDef (getRange fits) fits ConcreteDef NotInstanceDef termCheck covCheck x' cs] , rest)

                -- case: clauses match more than one sigs (ambiguity)
                (Name, (Name, [Declaration], [Declaration]))
    xf:[(Name, (Name, [Declaration], [Declaration]))]
    xfs -> DeclarationException' -> Nice ([NiceDeclaration], [Declaration])
    forall a. HasCallStack => DeclarationException' -> Nice a
    declarationException (DeclarationException' -> Nice ([NiceDeclaration], [Declaration]))
    -> DeclarationException' -> Nice ([NiceDeclaration], [Declaration])
    forall a b. (a -> b) -> a -> b
    $ LHS -> List1 Name -> DeclarationException'
    AmbiguousFunClauses LHS
    lhs (List1 Name -> DeclarationException')
    -> List1 Name -> DeclarationException'
    forall a b. (a -> b) -> a -> b
    $ List1 Name -> List1 Name
    forall a. NonEmpty a -> NonEmpty a
    List1.reverse (List1 Name -> List1 Name) -> List1 Name -> List1 Name
    forall a b. (a -> b) -> a -> b
    $ ((Name, (Name, [Declaration], [Declaration])) -> Name)
    -> NonEmpty (Name, (Name, [Declaration], [Declaration]))
    -> List1 Name
    forall a b. (a -> b) -> NonEmpty a -> NonEmpty b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (Name, (Name, [Declaration], [Declaration])) -> Name
    forall a b. (a, b) -> a
    fst (NonEmpty (Name, (Name, [Declaration], [Declaration]))
     -> List1 Name)
    -> NonEmpty (Name, (Name, [Declaration], [Declaration]))
    -> List1 Name
    forall a b. (a -> b) -> a -> b
    $ (Name, (Name, [Declaration], [Declaration]))
    xf (Name, (Name, [Declaration], [Declaration]))
    -> [(Name, (Name, [Declaration], [Declaration]))]
    -> NonEmpty (Name, (Name, [Declaration], [Declaration]))
    forall a. a -> [a] -> NonEmpty a
    :| [(Name, (Name, [Declaration], [Declaration]))]
    xfs
                     -- "ambiguous function clause; cannot assign it uniquely to one type signature"

            Field KwRange
    r [] -> HasCallStack =>
    DeclarationWarning' -> Nice ([NiceDeclaration], [Declaration])
    DeclarationWarning' -> Nice ([NiceDeclaration], [Declaration])
    justWarning (DeclarationWarning' -> Nice ([NiceDeclaration], [Declaration]))
    -> DeclarationWarning' -> Nice ([NiceDeclaration], [Declaration])
    forall a b. (a -> b) -> a -> b
    $ KwRange -> DeclarationWarning'
    EmptyField KwRange
    r
            Field KwRange
    _ [Declaration]
    fs -> (,[Declaration]
    ds) ([NiceDeclaration] -> ([NiceDeclaration], [Declaration]))
    -> Nice [NiceDeclaration]
    -> Nice ([NiceDeclaration], [Declaration])
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> KindOfBlock -> [Declaration] -> Nice [NiceDeclaration]
    niceAxioms KindOfBlock
    FieldBlock [Declaration]
    fs

            DataSig Range
    r Erased
    erased Name
    x [LamBinding]
    tel Expr
    t -> do
              pc <- Lens' NiceState PositivityCheck -> Nice PositivityCheck
    forall o (m :: * -> *) i. MonadState o m => Lens' o i -> m i
    use (PositivityCheck -> f PositivityCheck) -> NiceState -> f NiceState
    Lens' NiceState PositivityCheck
    positivityCheckPragma
              uc <- use universeCheckPragma
              _ <- addLoneSig r x $ DataName pc uc
              (,ds) <$> dataOrRec pc uc NiceDataDef
                          (flip NiceDataSig erased) (niceAxioms DataBlock) r
                          x (Just (tel, t)) Nothing

            Data Range
    r Erased
    erased Name
    x [LamBinding]
    tel Expr
    t [Declaration]
    cs -> do
              pc <- Lens' NiceState PositivityCheck -> Nice PositivityCheck
    forall o (m :: * -> *) i. MonadState o m => Lens' o i -> m i
    use (PositivityCheck -> f PositivityCheck) -> NiceState -> f NiceState
    Lens' NiceState PositivityCheck
    positivityCheckPragma
              -- Andreas, 2018-10-27, issue #3327
              -- Propagate {-# NO_UNIVERSE_CHECK #-} pragma from signature to definition.
              -- Universe check is performed if both the current value of
              -- 'universeCheckPragma' AND the one from the signature say so.
              uc <- use universeCheckPragma
              uc <- if uc == NoUniverseCheck then return uc else getUniverseCheckFromSig x
              mt <- defaultTypeSig (DataName pc uc) x (Just t)
              (,ds) <$> dataOrRec pc uc NiceDataDef
                          (flip NiceDataSig erased) (niceAxioms DataBlock) r
                          x ((tel,) <$> mt) (Just (tel, cs))

            DataDef Range
    r Name
    x [LamBinding]
    tel [Declaration]
    cs -> do
              pc <- Lens' NiceState PositivityCheck -> Nice PositivityCheck
    forall o (m :: * -> *) i. MonadState o m => Lens' o i -> m i
    use (PositivityCheck -> f PositivityCheck) -> NiceState -> f NiceState
    Lens' NiceState PositivityCheck
    positivityCheckPragma
              -- Andreas, 2018-10-27, issue #3327
              -- Propagate {-# NO_UNIVERSE_CHECK #-} pragma from signature to definition.
              -- Universe check is performed if both the current value of
              -- 'universeCheckPragma' AND the one from the signature say so.
              uc <- use universeCheckPragma
              uc <- if uc == NoUniverseCheck then return uc else getUniverseCheckFromSig x
              mt <- defaultTypeSig (DataName pc uc) x Nothing
              (,ds) <$> dataOrRec pc uc NiceDataDef
                          (flip NiceDataSig defaultErased)
                          (niceAxioms DataBlock) r x ((tel,) <$> mt)
                          (Just (tel, cs))

            RecordSig Range
    r Erased
    erased Name
    x [LamBinding]
    tel Expr
    t -> do
              pc <- Lens' NiceState PositivityCheck -> Nice PositivityCheck
    forall o (m :: * -> *) i. MonadState o m => Lens' o i -> m i
    use (PositivityCheck -> f PositivityCheck) -> NiceState -> f NiceState
    Lens' NiceState PositivityCheck
    positivityCheckPragma
              uc <- use universeCheckPragma
              _ <- addLoneSig r x $ RecName pc uc
              return ( [NiceRecSig r erased PublicAccess ConcreteDef pc uc x
                          tel t]
                     , ds
                     )

            Record Range
    r Erased
    erased Name
    x [RecordDirective]
    dir [LamBinding]
    tel Expr
    t [Declaration]
    cs -> do
              pc <- Lens' NiceState PositivityCheck -> Nice PositivityCheck
    forall o (m :: * -> *) i. MonadState o m => Lens' o i -> m i
    use (PositivityCheck -> f PositivityCheck) -> NiceState -> f NiceState
    Lens' NiceState PositivityCheck
    positivityCheckPragma
              -- Andreas, 2018-10-27, issue #3327
              -- Propagate {-# NO_UNIVERSE_CHECK #-} pragma from signature to definition.
              -- Universe check is performed if both the current value of
              -- 'universeCheckPragma' AND the one from the signature say so.
              uc <- use universeCheckPragma
              uc <- if uc == NoUniverseCheck then return uc else getUniverseCheckFromSig x
              mt <- defaultTypeSig (RecName pc uc) x (Just t)
              (,ds) <$> dataOrRec pc uc
                          (\Range
    r Origin
    o IsAbstract
    a PositivityCheck
    pc UniverseCheck
    uc Name
    x [LamBinding]
    tel [Declaration]
    cs ->
                            Range
    -> Origin
    -> IsAbstract
    -> PositivityCheck
    -> UniverseCheck
    -> Name
    -> [RecordDirective]
    -> [LamBinding]
    -> [Declaration]
    -> NiceDeclaration
    NiceRecDef Range
    r Origin
    o IsAbstract
    a PositivityCheck
    pc UniverseCheck
    uc Name
    x [RecordDirective]
    dir [LamBinding]
    tel [Declaration]
    cs)
                          (flip NiceRecSig erased) return r x
                          ((tel,) <$> mt) (Just (tel, cs))

            RecordDef Range
    r Name
    x [RecordDirective]
    dir [LamBinding]
    tel [Declaration]
    cs   -> do
              pc <- Lens' NiceState PositivityCheck -> Nice PositivityCheck
    forall o (m :: * -> *) i. MonadState o m => Lens' o i -> m i
    use (PositivityCheck -> f PositivityCheck) -> NiceState -> f NiceState
    Lens' NiceState PositivityCheck
    positivityCheckPragma
              -- Andreas, 2018-10-27, issue #3327
              -- Propagate {-# NO_UNIVERSE_CHECK #-} pragma from signature to definition.
              -- Universe check is performed if both the current value of
              -- 'universeCheckPragma' AND the one from the signature say so.
              uc <- use universeCheckPragma
              uc <- if uc == NoUniverseCheck then return uc else getUniverseCheckFromSig x
              mt <- defaultTypeSig (RecName pc uc) x Nothing
              (,ds) <$> dataOrRec pc uc
                          (\Range
    r Origin
    o IsAbstract
    a PositivityCheck
    pc UniverseCheck
    uc Name
    x [LamBinding]
    tel [Declaration]
    cs ->
                            Range
    -> Origin
    -> IsAbstract
    -> PositivityCheck
    -> UniverseCheck
    -> Name
    -> [RecordDirective]
    -> [LamBinding]
    -> [Declaration]
    -> NiceDeclaration
    NiceRecDef Range
    r Origin
    o IsAbstract
    a PositivityCheck
    pc UniverseCheck
    uc Name
    x [RecordDirective]
    dir [LamBinding]
    tel [Declaration]
    cs)
                          (flip NiceRecSig defaultErased) return r x
                          ((tel,) <$> mt) (Just (tel, cs))

            Mutual KwRange
    r [Declaration]
    ds' -> do
              -- The lone signatures encountered so far are not in scope
              -- for the mutual definition
              KwRange -> String -> Nice ()
    breakImplicitMutualBlock KwRange
    r String
    "`mutual` blocks"
              case [Declaration]
    ds' of
                [] -> HasCallStack =>
    DeclarationWarning' -> Nice ([NiceDeclaration], [Declaration])
    DeclarationWarning' -> Nice ([NiceDeclaration], [Declaration])
    justWarning (DeclarationWarning' -> Nice ([NiceDeclaration], [Declaration]))
    -> DeclarationWarning' -> Nice ([NiceDeclaration], [Declaration])
    forall a b. (a -> b) -> a -> b
    $ KwRange -> DeclarationWarning'
    EmptyMutual KwRange
    r
                [Declaration]
    _  -> (,[Declaration]
    ds) ([NiceDeclaration] -> ([NiceDeclaration], [Declaration]))
    -> Nice [NiceDeclaration]
    -> Nice ([NiceDeclaration], [Declaration])
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (NiceDeclaration -> [NiceDeclaration]
    forall el coll. Singleton el coll => el -> coll
    singleton (NiceDeclaration -> [NiceDeclaration])
    -> Nice NiceDeclaration -> Nice [NiceDeclaration]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (KwRange -> [NiceDeclaration] -> Nice NiceDeclaration
    mkOldMutual KwRange
    r ([NiceDeclaration] -> Nice NiceDeclaration)
    -> Nice [NiceDeclaration] -> Nice NiceDeclaration
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< [Declaration] -> Nice [NiceDeclaration]
    nice [Declaration]
    ds'))

            InterleavedMutual KwRange
    r [Declaration]
    ds' -> do
              -- The lone signatures encountered so far are not in scope
              -- for the mutual definition
              KwRange -> String -> Nice ()
    breakImplicitMutualBlock KwRange
    r String
    "`interleaved mutual` blocks"
              case [Declaration]
    ds' of
                [] -> HasCallStack =>
    DeclarationWarning' -> Nice ([NiceDeclaration], [Declaration])
    DeclarationWarning' -> Nice ([NiceDeclaration], [Declaration])
    justWarning (DeclarationWarning' -> Nice ([NiceDeclaration], [Declaration]))
    -> DeclarationWarning' -> Nice ([NiceDeclaration], [Declaration])
    forall a b. (a -> b) -> a -> b
    $ KwRange -> DeclarationWarning'
    EmptyMutual KwRange
    r
                [Declaration]
    _  -> (,[Declaration]
    ds) ([NiceDeclaration] -> ([NiceDeclaration], [Declaration]))
    -> Nice [NiceDeclaration]
    -> Nice ([NiceDeclaration], [Declaration])
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (NiceDeclaration -> [NiceDeclaration]
    forall el coll. Singleton el coll => el -> coll
    singleton (NiceDeclaration -> [NiceDeclaration])
    -> Nice NiceDeclaration -> Nice [NiceDeclaration]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (KwRange -> [NiceDeclaration] -> Nice NiceDeclaration
    mkInterleavedMutual KwRange
    r ([NiceDeclaration] -> Nice NiceDeclaration)
    -> Nice [NiceDeclaration] -> Nice NiceDeclaration
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< [Declaration] -> Nice [NiceDeclaration]
    nice [Declaration]
    ds'))

            LoneConstructor KwRange
    r [] -> HasCallStack =>
    DeclarationWarning' -> Nice ([NiceDeclaration], [Declaration])
    DeclarationWarning' -> Nice ([NiceDeclaration], [Declaration])
    justWarning (DeclarationWarning' -> Nice ([NiceDeclaration], [Declaration]))
    -> DeclarationWarning' -> Nice ([NiceDeclaration], [Declaration])
    forall a b. (a -> b) -> a -> b
    $ KwRange -> DeclarationWarning'
    EmptyConstructor KwRange
    r
            LoneConstructor KwRange
    r [Declaration]
    ds' ->
              ((,[Declaration]
    ds) ([NiceDeclaration] -> ([NiceDeclaration], [Declaration]))
    -> ([NiceDeclaration] -> [NiceDeclaration])
    -> [NiceDeclaration]
    -> ([NiceDeclaration], [Declaration])
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . NiceDeclaration -> [NiceDeclaration]
    forall el coll. Singleton el coll => el -> coll
    singleton (NiceDeclaration -> [NiceDeclaration])
    -> ([NiceDeclaration] -> NiceDeclaration)
    -> [NiceDeclaration]
    -> [NiceDeclaration]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . KwRange -> [NiceDeclaration] -> NiceDeclaration
    NiceLoneConstructor KwRange
    r) ([NiceDeclaration] -> ([NiceDeclaration], [Declaration]))
    -> Nice [NiceDeclaration]
    -> Nice ([NiceDeclaration], [Declaration])
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> KindOfBlock -> [Declaration] -> Nice [NiceDeclaration]
    niceAxioms KindOfBlock
    ConstructorBlock [Declaration]
    ds'

            Abstract KwRange
    r []  -> HasCallStack =>
    DeclarationWarning' -> Nice ([NiceDeclaration], [Declaration])
    DeclarationWarning' -> Nice ([NiceDeclaration], [Declaration])
    justWarning (DeclarationWarning' -> Nice ([NiceDeclaration], [Declaration]))
    -> DeclarationWarning' -> Nice ([NiceDeclaration], [Declaration])
    forall a b. (a -> b) -> a -> b
    $ KwRange -> DeclarationWarning'
    EmptyAbstract KwRange
    r
            Abstract KwRange
    r [Declaration]
    ds' ->
              (,[Declaration]
    ds) ([NiceDeclaration] -> ([NiceDeclaration], [Declaration]))
    -> Nice [NiceDeclaration]
    -> Nice ([NiceDeclaration], [Declaration])
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (KwRange -> [NiceDeclaration] -> Nice [NiceDeclaration]
    abstractBlock KwRange
    r ([NiceDeclaration] -> Nice [NiceDeclaration])
    -> Nice [NiceDeclaration] -> Nice [NiceDeclaration]
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< [Declaration] -> Nice [NiceDeclaration]
    nice [Declaration]
    ds')

            Private KwRange
    r Origin
    UserWritten []  -> HasCallStack =>
    DeclarationWarning' -> Nice ([NiceDeclaration], [Declaration])
    DeclarationWarning' -> Nice ([NiceDeclaration], [Declaration])
    justWarning (DeclarationWarning' -> Nice ([NiceDeclaration], [Declaration]))
    -> DeclarationWarning' -> Nice ([NiceDeclaration], [Declaration])
    forall a b. (a -> b) -> a -> b
    $ KwRange -> DeclarationWarning'
    EmptyPrivate KwRange
    r
            Private KwRange
    r Origin
    o [Declaration]
    ds' ->
              (,[Declaration]
    ds) ([NiceDeclaration] -> ([NiceDeclaration], [Declaration]))
    -> Nice [NiceDeclaration]
    -> Nice ([NiceDeclaration], [Declaration])
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (KwRange -> Origin -> [NiceDeclaration] -> Nice [NiceDeclaration]
    privateBlock KwRange
    r Origin
    o ([NiceDeclaration] -> Nice [NiceDeclaration])
    -> Nice [NiceDeclaration] -> Nice [NiceDeclaration]
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< [Declaration] -> Nice [NiceDeclaration]
    nice [Declaration]
    ds')

            InstanceB KwRange
    r []  -> HasCallStack =>
    DeclarationWarning' -> Nice ([NiceDeclaration], [Declaration])
    DeclarationWarning' -> Nice ([NiceDeclaration], [Declaration])
    justWarning (DeclarationWarning' -> Nice ([NiceDeclaration], [Declaration]))
    -> DeclarationWarning' -> Nice ([NiceDeclaration], [Declaration])
    forall a b. (a -> b) -> a -> b
    $ KwRange -> DeclarationWarning'
    EmptyInstance KwRange
    r
            InstanceB KwRange
    r [Declaration]
    ds' ->
              (,[Declaration]
    ds) ([NiceDeclaration] -> ([NiceDeclaration], [Declaration]))
    -> Nice [NiceDeclaration]
    -> Nice ([NiceDeclaration], [Declaration])
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (KwRange -> [NiceDeclaration] -> Nice [NiceDeclaration]
    instanceBlock KwRange
    r ([NiceDeclaration] -> Nice [NiceDeclaration])
    -> Nice [NiceDeclaration] -> Nice [NiceDeclaration]
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< [Declaration] -> Nice [NiceDeclaration]
    nice [Declaration]
    ds')

            Macro KwRange
    r []  -> HasCallStack =>
    DeclarationWarning' -> Nice ([NiceDeclaration], [Declaration])
    DeclarationWarning' -> Nice ([NiceDeclaration], [Declaration])
    justWarning (DeclarationWarning' -> Nice ([NiceDeclaration], [Declaration]))
    -> DeclarationWarning' -> Nice ([NiceDeclaration], [Declaration])
    forall a b. (a -> b) -> a -> b
    $ KwRange -> DeclarationWarning'
    EmptyMacro KwRange
    r
            Macro KwRange
    r [Declaration]
    ds' ->
              (,[Declaration]
    ds) ([NiceDeclaration] -> ([NiceDeclaration], [Declaration]))
    -> Nice [NiceDeclaration]
    -> Nice ([NiceDeclaration], [Declaration])
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (KwRange -> [NiceDeclaration] -> Nice [NiceDeclaration]
    macroBlock KwRange
    r ([NiceDeclaration] -> Nice [NiceDeclaration])
    -> Nice [NiceDeclaration] -> Nice [NiceDeclaration]
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< [Declaration] -> Nice [NiceDeclaration]
    nice [Declaration]
    ds')

            Postulate KwRange
    r []  -> HasCallStack =>
    DeclarationWarning' -> Nice ([NiceDeclaration], [Declaration])
    DeclarationWarning' -> Nice ([NiceDeclaration], [Declaration])
    justWarning (DeclarationWarning' -> Nice ([NiceDeclaration], [Declaration]))
    -> DeclarationWarning' -> Nice ([NiceDeclaration], [Declaration])
    forall a b. (a -> b) -> a -> b
    $ KwRange -> DeclarationWarning'
    EmptyPostulate KwRange
    r
            Postulate KwRange
    _ [Declaration]
    ds' ->
              (,[Declaration]
    ds) ([NiceDeclaration] -> ([NiceDeclaration], [Declaration]))
    -> Nice [NiceDeclaration]
    -> Nice ([NiceDeclaration], [Declaration])
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> KindOfBlock -> [Declaration] -> Nice [NiceDeclaration]
    niceAxioms KindOfBlock
    PostulateBlock [Declaration]
    ds'

            Primitive KwRange
    r []  -> HasCallStack =>
    DeclarationWarning' -> Nice ([NiceDeclaration], [Declaration])
    DeclarationWarning' -> Nice ([NiceDeclaration], [Declaration])
    justWarning (DeclarationWarning' -> Nice ([NiceDeclaration], [Declaration]))
    -> DeclarationWarning' -> Nice ([NiceDeclaration], [Declaration])
    forall a b. (a -> b) -> a -> b
    $ KwRange -> DeclarationWarning'
    EmptyPrimitive KwRange
    r
            Primitive KwRange
    _ [Declaration]
    ds' -> (,[Declaration]
    ds) ([NiceDeclaration] -> ([NiceDeclaration], [Declaration]))
    -> Nice [NiceDeclaration]
    -> Nice ([NiceDeclaration], [Declaration])
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> ((NiceDeclaration -> NiceDeclaration)
    -> [NiceDeclaration] -> [NiceDeclaration]
    forall a b. (a -> b) -> [a] -> [b]
    map NiceDeclaration -> NiceDeclaration
    toPrim ([NiceDeclaration] -> [NiceDeclaration])
    -> Nice [NiceDeclaration] -> Nice [NiceDeclaration]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> KindOfBlock -> [Declaration] -> Nice [NiceDeclaration]
    niceAxioms KindOfBlock
    PrimitiveBlock [Declaration]
    ds')

            Module Range
    r Erased
    erased QName
    x Telescope
    tel [Declaration]
    ds' -> ([NiceDeclaration], [Declaration])
    -> Nice ([NiceDeclaration], [Declaration])
    forall a. a -> Nice a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (([NiceDeclaration], [Declaration])
     -> Nice ([NiceDeclaration], [Declaration]))
    -> ([NiceDeclaration], [Declaration])
    -> Nice ([NiceDeclaration], [Declaration])
    forall a b. (a -> b) -> a -> b
    $
              ([Range
    -> Access
    -> IsAbstract
    -> Erased
    -> QName
    -> Telescope
    -> [Declaration]
    -> NiceDeclaration
    NiceModule Range
    r Access
    PublicAccess IsAbstract
    ConcreteDef Erased
    erased QName
    x Telescope
    tel [Declaration]
    ds'], [Declaration]
    ds)

            ModuleMacro Range
    r Erased
    erased Name
    x ModuleApplication
    modapp OpenShortHand
    op ImportDirective
    is -> ([NiceDeclaration], [Declaration])
    -> Nice ([NiceDeclaration], [Declaration])
    forall a. a -> Nice a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (([NiceDeclaration], [Declaration])
     -> Nice ([NiceDeclaration], [Declaration]))
    -> ([NiceDeclaration], [Declaration])
    -> Nice ([NiceDeclaration], [Declaration])
    forall a b. (a -> b) -> a -> b
    $
              ([Range
    -> Access
    -> Erased
    -> Name
    -> ModuleApplication
    -> OpenShortHand
    -> ImportDirective
    -> NiceDeclaration
    NiceModuleMacro Range
    r Access
    PublicAccess Erased
    erased Name
    x ModuleApplication
    modapp OpenShortHand
    op ImportDirective
    is], [Declaration]
    ds)

            -- Fixity and syntax declarations and polarity pragmas have
            -- already been processed.
            Infix Fixity
    _ List1 Name
    _  -> ([NiceDeclaration], [Declaration])
    -> Nice ([NiceDeclaration], [Declaration])
    forall a. a -> Nice a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([], [Declaration]
    ds)
            Syntax Name
    _ Notation
    _ -> ([NiceDeclaration], [Declaration])
    -> Nice ([NiceDeclaration], [Declaration])
    forall a. a -> Nice a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([], [Declaration]
    ds)

            PatternSyn Range
    r Name
    n [WithHiding Name]
    as Pattern
    p -> do
              ([NiceDeclaration], [Declaration])
    -> Nice ([NiceDeclaration], [Declaration])
    forall a. a -> Nice a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([Range
    -> Access
    -> Name
    -> [WithHiding Name]
    -> Pattern
    -> NiceDeclaration
    NicePatternSyn Range
    r Access
    PublicAccess Name
    n [WithHiding Name]
    as Pattern
    p] , [Declaration]
    ds)
            Open Range
    r QName
    x ImportDirective
    is         -> ([NiceDeclaration], [Declaration])
    -> Nice ([NiceDeclaration], [Declaration])
    forall a. a -> Nice a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([Range -> QName -> ImportDirective -> NiceDeclaration
    NiceOpen Range
    r QName
    x ImportDirective
    is] , [Declaration]
    ds)
            Import Range
    r QName
    x Maybe AsName
    as OpenShortHand
    op ImportDirective
    is -> ([NiceDeclaration], [Declaration])
    -> Nice ([NiceDeclaration], [Declaration])
    forall a. a -> Nice a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([Range
    -> QName
    -> Maybe AsName
    -> OpenShortHand
    -> ImportDirective
    -> NiceDeclaration
    NiceImport Range
    r QName
    x Maybe AsName
    as OpenShortHand
    op ImportDirective
    is] , [Declaration]
    ds)

            UnquoteDecl Range
    r [Name]
    xs Expr
    e -> do
              tc <- Lens' NiceState TerminationCheck -> Nice TerminationCheck
    forall o (m :: * -> *) i. MonadState o m => Lens' o i -> m i
    use (TerminationCheck -> f TerminationCheck)
    -> NiceState -> f NiceState
    Lens' NiceState TerminationCheck
    terminationCheckPragma
              cc <- use coverageCheckPragma
              return ([NiceUnquoteDecl r PublicAccess ConcreteDef NotInstanceDef tc cc xs e] , ds)

            UnquoteDef Range
    r [Name]
    xs Expr
    e -> do
              sigs <- ((Name, Name) -> Name) -> [(Name, Name)] -> [Name]
    forall a b. (a -> b) -> [a] -> [b]
    map (Name, Name) -> Name
    forall a b. (a, b) -> a
    fst ([(Name, Name)] -> [Name])
    -> (LoneSigs -> [(Name, Name)]) -> LoneSigs -> [Name]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . LoneSigs -> [(Name, Name)]
    loneFuns (LoneSigs -> [Name]) -> Nice LoneSigs -> Nice [Name]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Lens' NiceState LoneSigs -> Nice LoneSigs
    forall o (m :: * -> *) i. MonadState o m => Lens' o i -> m i
    use (LoneSigs -> f LoneSigs) -> NiceState -> f NiceState
    Lens' NiceState LoneSigs
    loneSigs
              List1.ifNotNull (filter (`notElem` sigs) xs)
                {-then-} (declarationException . UnquoteDefRequiresSignature)
                {-else-} $ do
                  mapM_ removeLoneSig xs
                  return ([NiceUnquoteDef r PublicAccess ConcreteDef TerminationCheck YesCoverageCheck xs e] , ds)

            UnquoteData Range
    r Name
    xs [Name]
    cs Expr
    e -> do
              pc <- Lens' NiceState PositivityCheck -> Nice PositivityCheck
    forall o (m :: * -> *) i. MonadState o m => Lens' o i -> m i
    use (PositivityCheck -> f PositivityCheck) -> NiceState -> f NiceState
    Lens' NiceState PositivityCheck
    positivityCheckPragma
              uc <- use universeCheckPragma
              return ([NiceUnquoteData r PublicAccess ConcreteDef pc uc xs cs e], ds)

            Pragma Pragma
    p -> do
              -- Warn about unsafe pragmas unless we are in a builtin module.
              Nice Bool -> Nice () -> Nice ()
    forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
    whenM ((NiceEnv -> Bool) -> Nice Bool
    forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
    asks NiceEnv -> Bool
    safeButNotBuiltin) (Nice () -> Nice ()) -> Nice () -> Nice ()
    forall a b. (a -> b) -> a -> b
    $
                Maybe DeclarationWarning'
    -> (DeclarationWarning' -> Nice ()) -> Nice ()
    forall (m :: * -> *) a. Monad m => Maybe a -> (a -> m ()) -> m ()
    whenJust (Pragma -> Maybe DeclarationWarning'
    forall m. CMaybe DeclarationWarning' m => Pragma -> m
    unsafePragma Pragma
    p) ((DeclarationWarning' -> Nice ()) -> Nice ())
    -> (DeclarationWarning' -> Nice ()) -> Nice ()
    forall a b. (a -> b) -> a -> b
    $ \ DeclarationWarning'
    w ->
                  HasCallStack => DeclarationWarning' -> Nice ()
    DeclarationWarning' -> Nice ()
    declarationWarning DeclarationWarning'
    w
              Pragma -> [Declaration] -> Nice ([NiceDeclaration], [Declaration])
    nicePragma Pragma
    p [Declaration]
    ds

            Opaque KwRange
    r [Declaration]
    ds' -> do
              KwRange -> String -> Nice ()
    breakImplicitMutualBlock KwRange
    r String
    "`opaque` blocks"

              -- Split the enclosed declarations into an initial run of
              -- 'unfolding' statements and the rest of the body.
              let
                ([[QName]]
    unfoldings, [Declaration]
    body) = ((Declaration -> Maybe [QName])
     -> [Declaration] -> ([[QName]], [Declaration]))
    -> [Declaration]
    -> (Declaration -> Maybe [QName])
    -> ([[QName]], [Declaration])
    forall a b c. (a -> b -> c) -> b -> a -> c
    flip (Declaration -> Maybe [QName])
    -> [Declaration] -> ([[QName]], [Declaration])
    forall a b. (a -> Maybe b) -> [a] -> ([b], [a])
    spanMaybe [Declaration]
    ds' ((Declaration -> Maybe [QName]) -> ([[QName]], [Declaration]))
    -> (Declaration -> Maybe [QName]) -> ([[QName]], [Declaration])
    forall a b. (a -> b) -> a -> b
    $ \case
                  Unfolding KwRange
    _ [QName]
    ns -> [QName] -> Maybe [QName]
    forall a. a -> Maybe a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure [QName]
    ns
                  Declaration
    _ -> Maybe [QName]
    forall a. Maybe a
    Nothing

              -- The body of an 'opaque' definition can have mutual
              -- recursion by interleaving type signatures and definitions,
              -- just like the body of a module.
              decls0 <- [Declaration] -> Nice [NiceDeclaration]
    nice [Declaration]
    body
              ps <- use loneSigs
              checkLoneSigs ps
              let decls = LoneSigs -> [NiceDeclaration] -> [NiceDeclaration]
    replaceSigs LoneSigs
    ps [NiceDeclaration]
    decls0
              body <- inferMutualBlocks decls
              pure ([NiceOpaque r (concat unfoldings) body], ds)

            Unfolding KwRange
    r [QName]
    _ -> DeclarationException' -> Nice ([NiceDeclaration], [Declaration])
    forall a. HasCallStack => DeclarationException' -> Nice a
    declarationException (DeclarationException' -> Nice ([NiceDeclaration], [Declaration]))
    -> DeclarationException' -> Nice ([NiceDeclaration], [Declaration])
    forall a b. (a -> b) -> a -> b
    $ KwRange -> DeclarationException'
    UnfoldingOutsideOpaque KwRange
    r

        nicePragma :: Pragma -> [Declaration] -> Nice ([NiceDeclaration], [Declaration])

        nicePragma :: Pragma -> [Declaration] -> Nice ([NiceDeclaration], [Declaration])
    nicePragma (TerminationCheckPragma Range
    r (TerminationMeasure Range
    _ Name
    x)) [Declaration]
    ds =
          if [Declaration] -> Bool
    canHaveTerminationMeasure [Declaration]
    ds then
            TerminationCheck
    -> Nice ([NiceDeclaration], [Declaration])
    -> Nice ([NiceDeclaration], [Declaration])
    forall a. TerminationCheck -> Nice a -> Nice a
    withTerminationCheckPragma (Range -> Name -> TerminationCheck
    forall m. Range -> m -> TerminationCheck m
    TerminationMeasure Range
    r Name
    x) (Nice ([NiceDeclaration], [Declaration])
     -> Nice ([NiceDeclaration], [Declaration]))
    -> Nice ([NiceDeclaration], [Declaration])
    -> Nice ([NiceDeclaration], [Declaration])
    forall a b. (a -> b) -> a -> b
    $ [Declaration] -> Nice ([NiceDeclaration], [Declaration])
    nice1 [Declaration]
    ds
          else do
            HasCallStack => DeclarationWarning' -> Nice ()
    DeclarationWarning' -> Nice ()
    declarationWarning (DeclarationWarning' -> Nice ()) -> DeclarationWarning' -> Nice ()
    forall a b. (a -> b) -> a -> b
    $ Range -> DeclarationWarning'
    InvalidTerminationCheckPragma Range
    r
            [Declaration] -> Nice ([NiceDeclaration], [Declaration])
    nice1 [Declaration]
    ds

        nicePragma (TerminationCheckPragma Range
    r TerminationCheck
    NoTerminationCheck) [Declaration]
    ds = do
          -- This PRAGMA has been deprecated in favour of (NON_)TERMINATING
          -- We warn the user about it and then assume the function is NON_TERMINATING.
          HasCallStack => DeclarationWarning' -> Nice ()
    DeclarationWarning' -> Nice ()
    declarationWarning (DeclarationWarning' -> Nice ()) -> DeclarationWarning' -> Nice ()
    forall a b. (a -> b) -> a -> b
    $ Range -> DeclarationWarning'
    PragmaNoTerminationCheck Range
    r
          Pragma -> [Declaration] -> Nice ([NiceDeclaration], [Declaration])
    nicePragma (Range -> TerminationCheck -> Pragma
    TerminationCheckPragma Range
    r TerminationCheck
    forall m. TerminationCheck m
    NonTerminating) [Declaration]
    ds

        nicePragma (TerminationCheckPragma Range
    r TerminationCheck
    tc) [Declaration]
    ds =
          if [Declaration] -> Bool
    canHaveTerminationCheckPragma [Declaration]
    ds then
            TerminationCheck
    -> Nice ([NiceDeclaration], [Declaration])
    -> Nice ([NiceDeclaration], [Declaration])
    forall a. TerminationCheck -> Nice a -> Nice a
    withTerminationCheckPragma TerminationCheck
    tc (Nice ([NiceDeclaration], [Declaration])
     -> Nice ([NiceDeclaration], [Declaration]))
    -> Nice ([NiceDeclaration], [Declaration])
    -> Nice ([NiceDeclaration], [Declaration])
    forall a b. (a -> b) -> a -> b
    $ [Declaration] -> Nice ([NiceDeclaration], [Declaration])
    nice1 [Declaration]
    ds
          else do
            HasCallStack => DeclarationWarning' -> Nice ()
    DeclarationWarning' -> Nice ()
    declarationWarning (DeclarationWarning' -> Nice ()) -> DeclarationWarning' -> Nice ()
    forall a b. (a -> b) -> a -> b
    $ Range -> DeclarationWarning'
    InvalidTerminationCheckPragma Range
    r
            [Declaration] -> Nice ([NiceDeclaration], [Declaration])
    nice1 [Declaration]
    ds

        nicePragma (NoCoverageCheckPragma Range
    r) [Declaration]
    ds =
          if [Declaration] -> Bool
    canHaveCoverageCheckPragma [Declaration]
    ds then
            CoverageCheck
    -> Nice ([NiceDeclaration], [Declaration])
    -> Nice ([NiceDeclaration], [Declaration])
    forall a. CoverageCheck -> Nice a -> Nice a
    withCoverageCheckPragma CoverageCheck
    NoCoverageCheck (Nice ([NiceDeclaration], [Declaration])
     -> Nice ([NiceDeclaration], [Declaration]))
    -> Nice ([NiceDeclaration], [Declaration])
    -> Nice ([NiceDeclaration], [Declaration])
    forall a b. (a -> b) -> a -> b
    $ [Declaration] -> Nice ([NiceDeclaration], [Declaration])
    nice1 [Declaration]
    ds
          else do
            HasCallStack => DeclarationWarning' -> Nice ()
    DeclarationWarning' -> Nice ()
    declarationWarning (DeclarationWarning' -> Nice ()) -> DeclarationWarning' -> Nice ()
    forall a b. (a -> b) -> a -> b
    $ Range -> DeclarationWarning'
    InvalidCoverageCheckPragma Range
    r
            [Declaration] -> Nice ([NiceDeclaration], [Declaration])
    nice1 [Declaration]
    ds

        nicePragma (CatchallPragma Range
    r) [Declaration]
    ds =
          if [Declaration] -> Bool
    canHaveCatchallPragma [Declaration]
    ds then
            Catchall
    -> Nice ([NiceDeclaration], [Declaration])
    -> Nice ([NiceDeclaration], [Declaration])
    forall a. Catchall -> Nice a -> Nice a
    withCatchallPragma (Range -> Catchall
    YesCatchall Range
    r) (Nice ([NiceDeclaration], [Declaration])
     -> Nice ([NiceDeclaration], [Declaration]))
    -> Nice ([NiceDeclaration], [Declaration])
    -> Nice ([NiceDeclaration], [Declaration])
    forall a b. (a -> b) -> a -> b
    $ [Declaration] -> Nice ([NiceDeclaration], [Declaration])
    nice1 [Declaration]
    ds
          else do
            HasCallStack => DeclarationWarning' -> Nice ()
    DeclarationWarning' -> Nice ()
    declarationWarning (DeclarationWarning' -> Nice ()) -> DeclarationWarning' -> Nice ()
    forall a b. (a -> b) -> a -> b
    $ Range -> DeclarationWarning'
    InvalidCatchallPragma Range
    r
            [Declaration] -> Nice ([NiceDeclaration], [Declaration])
    nice1 [Declaration]
    ds

        nicePragma (NoPositivityCheckPragma Range
    r) [Declaration]
    ds =
          if [Declaration] -> Bool
    canHaveNoPositivityCheckPragma [Declaration]
    ds then
            PositivityCheck
    -> Nice ([NiceDeclaration], [Declaration])
    -> Nice ([NiceDeclaration], [Declaration])
    forall a. PositivityCheck -> Nice a -> Nice a
    withPositivityCheckPragma PositivityCheck
    NoPositivityCheck (Nice ([NiceDeclaration], [Declaration])
     -> Nice ([NiceDeclaration], [Declaration]))
    -> Nice ([NiceDeclaration], [Declaration])
    -> Nice ([NiceDeclaration], [Declaration])
    forall a b. (a -> b) -> a -> b
    $ [Declaration] -> Nice ([NiceDeclaration], [Declaration])
    nice1 [Declaration]
    ds
          else do
            HasCallStack => DeclarationWarning' -> Nice ()
    DeclarationWarning' -> Nice ()
    declarationWarning (DeclarationWarning' -> Nice ()) -> DeclarationWarning' -> Nice ()
    forall a b. (a -> b) -> a -> b
    $ Range -> DeclarationWarning'
    InvalidNoPositivityCheckPragma Range
    r
            [Declaration] -> Nice ([NiceDeclaration], [Declaration])
    nice1 [Declaration]
    ds

        nicePragma (NoUniverseCheckPragma Range
    r) [Declaration]
    ds =
          if [Declaration] -> Bool
    canHaveNoUniverseCheckPragma [Declaration]
    ds then
            UniverseCheck
    -> Nice ([NiceDeclaration], [Declaration])
    -> Nice ([NiceDeclaration], [Declaration])
    forall a. UniverseCheck -> Nice a -> Nice a
    withUniverseCheckPragma UniverseCheck
    NoUniverseCheck (Nice ([NiceDeclaration], [Declaration])
     -> Nice ([NiceDeclaration], [Declaration]))
    -> Nice ([NiceDeclaration], [Declaration])
    -> Nice ([NiceDeclaration], [Declaration])
    forall a b. (a -> b) -> a -> b
    $ [Declaration] -> Nice ([NiceDeclaration], [Declaration])
    nice1 [Declaration]
    ds
          else do
            HasCallStack => DeclarationWarning' -> Nice ()
    DeclarationWarning' -> Nice ()
    declarationWarning (DeclarationWarning' -> Nice ()) -> DeclarationWarning' -> Nice ()
    forall a b. (a -> b) -> a -> b
    $ Range -> DeclarationWarning'
    InvalidNoUniverseCheckPragma Range
    r
            [Declaration] -> Nice ([NiceDeclaration], [Declaration])
    nice1 [Declaration]
    ds

        nicePragma p :: Pragma
    p@CompilePragma{} [Declaration]
    ds = do
          ([NiceDeclaration], [Declaration])
    -> Nice ([NiceDeclaration], [Declaration])
    forall a. a -> Nice a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([Range -> Pragma -> NiceDeclaration
    NicePragma (Pragma -> Range
    forall a. HasRange a => a -> Range
    getRange Pragma
    p) Pragma
    p], [Declaration]
    ds)

        nicePragma (PolarityPragma{}) [Declaration]
    ds = ([NiceDeclaration], [Declaration])
    -> Nice ([NiceDeclaration], [Declaration])
    forall a. a -> Nice a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([], [Declaration]
    ds)

        nicePragma (BuiltinPragma Range
    r RString
    str qn :: QName
    qn@(QName Name
    x)) [Declaration]
    ds = do
          ([NiceDeclaration], [Declaration])
    -> Nice ([NiceDeclaration], [Declaration])
    forall a. a -> Nice a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([Range -> Pragma -> NiceDeclaration
    NicePragma Range
    r (Range -> RString -> QName -> Pragma
    BuiltinPragma Range
    r RString
    str QName
    qn)], [Declaration]
    ds)

        nicePragma p :: Pragma
    p@RewritePragma{} [Declaration]
    ds = ([NiceDeclaration], [Declaration])
    -> Nice ([NiceDeclaration], [Declaration])
    forall a. a -> Nice a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([Range -> Pragma -> NiceDeclaration
    NicePragma (Pragma -> Range
    forall a. HasRange a => a -> Range
    getRange Pragma
    p) Pragma
    p], [Declaration]
    ds)
        nicePragma Pragma
    p [Declaration]
    ds = ([NiceDeclaration], [Declaration])
    -> Nice ([NiceDeclaration], [Declaration])
    forall a. a -> Nice a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([Range -> Pragma -> NiceDeclaration
    NicePragma (Pragma -> Range
    forall a. HasRange a => a -> Range
    getRange Pragma
    p) Pragma
    p], [Declaration]
    ds)

        canHaveTerminationMeasure :: [Declaration] -> Bool
        canHaveTerminationMeasure :: [Declaration] -> Bool
    canHaveTerminationMeasure [] = Bool
    False
        canHaveTerminationMeasure (Declaration
    d:[Declaration]
    ds) = case Declaration
    d of
          TypeSig{} -> Bool
    True
          (Pragma Pragma
    p) | Pragma -> Bool
    isAttachedPragma Pragma
    p -> [Declaration] -> Bool
    canHaveTerminationMeasure [Declaration]
    ds
          Declaration
    _         -> Bool
    False

        canHaveTerminationCheckPragma :: [Declaration] -> Bool
        canHaveTerminationCheckPragma :: [Declaration] -> Bool
    canHaveTerminationCheckPragma []     = Bool
    False
        canHaveTerminationCheckPragma (Declaration
    d:[Declaration]
    ds) = case Declaration
    d of
          Mutual KwRange
    _ [Declaration]
    ds   -> (Declaration -> Bool) -> [Declaration] -> Bool
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
    any ([Declaration] -> Bool
    canHaveTerminationCheckPragma ([Declaration] -> Bool)
    -> (Declaration -> [Declaration]) -> Declaration -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Declaration -> [Declaration]
    forall el coll. Singleton el coll => el -> coll
    singleton) [Declaration]
    ds
          TypeSig{}     -> Bool
    True
          FunClause{}   -> Bool
    True
          UnquoteDecl{} -> Bool
    True
          (Pragma Pragma
    p) | Pragma -> Bool
    isAttachedPragma Pragma
    p -> [Declaration] -> Bool
    canHaveTerminationCheckPragma [Declaration]
    ds
          Declaration
    _             -> Bool
    False

        canHaveCoverageCheckPragma :: [Declaration] -> Bool
        canHaveCoverageCheckPragma :: [Declaration] -> Bool
    canHaveCoverageCheckPragma = [Declaration] -> Bool
    canHaveTerminationCheckPragma

        canHaveCatchallPragma :: [Declaration] -> Bool
        canHaveCatchallPragma :: [Declaration] -> Bool
    canHaveCatchallPragma []     = Bool
    False
        canHaveCatchallPragma (Declaration
    d:[Declaration]
    ds) = case Declaration
    d of
          FunClause{} -> Bool
    True
          (Pragma Pragma
    p) | Pragma -> Bool
    isAttachedPragma Pragma
    p -> [Declaration] -> Bool
    canHaveCatchallPragma [Declaration]
    ds
          Declaration
    _           -> Bool
    False

        canHaveNoPositivityCheckPragma :: [Declaration] -> Bool
        canHaveNoPositivityCheckPragma :: [Declaration] -> Bool
    canHaveNoPositivityCheckPragma []     = Bool
    False
        canHaveNoPositivityCheckPragma (Declaration
    d:[Declaration]
    ds) = case Declaration
    d of
          Mutual KwRange
    _ [Declaration]
    ds                   -> (Declaration -> Bool) -> [Declaration] -> Bool
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
    any ([Declaration] -> Bool
    canHaveNoPositivityCheckPragma ([Declaration] -> Bool)
    -> (Declaration -> [Declaration]) -> Declaration -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Declaration -> [Declaration]
    forall el coll. Singleton el coll => el -> coll
    singleton) [Declaration]
    ds
          Data{}                        -> Bool
    True
          DataSig{}                     -> Bool
    True
          DataDef{}                     -> Bool
    True
          Record{}                      -> Bool
    True
          RecordSig{}                   -> Bool
    True
          RecordDef{}                   -> Bool
    True
          Pragma Pragma
    p | Pragma -> Bool
    isAttachedPragma Pragma
    p -> [Declaration] -> Bool
    canHaveNoPositivityCheckPragma [Declaration]
    ds
          Declaration
    _                             -> Bool
    False

        canHaveNoUniverseCheckPragma :: [Declaration] -> Bool
        canHaveNoUniverseCheckPragma :: [Declaration] -> Bool
    canHaveNoUniverseCheckPragma []     = Bool
    False
        canHaveNoUniverseCheckPragma (Declaration
    d:[Declaration]
    ds) = case Declaration
    d of
          Data{}                        -> Bool
    True
          DataSig{}                     -> Bool
    True
          DataDef{}                     -> Bool
    True
          Record{}                      -> Bool
    True
          RecordSig{}                   -> Bool
    True
          RecordDef{}                   -> Bool
    True
          Pragma Pragma
    p | Pragma -> Bool
    isAttachedPragma Pragma
    p -> [Declaration] -> Bool
    canHaveNoPositivityCheckPragma [Declaration]
    ds
          Declaration
    _                             -> Bool
    False

        -- Pragma that attaches to the following declaration.
        isAttachedPragma :: Pragma -> Bool
        isAttachedPragma :: Pragma -> Bool
    isAttachedPragma = \case
          TerminationCheckPragma{}  -> Bool
    True
          CatchallPragma{}          -> Bool
    True
          NoPositivityCheckPragma{} -> Bool
    True
          NoUniverseCheckPragma{}   -> Bool
    True
          Pragma
    _                         -> Bool
    False

        -- We could add a default type signature here, but at the moment we can't
        -- infer the type of a record or datatype, so better to just fail here.
        defaultTypeSig :: DataRecOrFun -> Name -> Maybe Expr -> Nice (Maybe Expr)
        defaultTypeSig :: DataRecOrFun -> Name -> Maybe Expr -> Nice (Maybe Expr)
    defaultTypeSig DataRecOrFun
    k Name
    x t :: Maybe Expr
    t@Just{} = Maybe Expr -> Nice (Maybe Expr)
    forall a. a -> Nice a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Maybe Expr
    t
        defaultTypeSig DataRecOrFun
    k Name
    x Maybe Expr
    Nothing  = do
          Nice (Maybe DataRecOrFun)
    -> Nice (Maybe Expr)
    -> (DataRecOrFun -> Nice (Maybe Expr))
    -> Nice (Maybe Expr)
    forall (m :: * -> *) a b.
    Monad m =>
    m (Maybe a) -> m b -> (a -> m b) -> m b
    caseMaybeM (Name -> Nice (Maybe DataRecOrFun)
    getSig Name
    x) (Maybe Expr -> Nice (Maybe Expr)
    forall a. a -> Nice a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Maybe Expr
    forall a. Maybe a
    Nothing) ((DataRecOrFun -> Nice (Maybe Expr)) -> Nice (Maybe Expr))
    -> (DataRecOrFun -> Nice (Maybe Expr)) -> Nice (Maybe Expr)
    forall a b. (a -> b) -> a -> b
    $ \ DataRecOrFun
    k' -> do
            Bool -> Nice () -> Nice ()
    forall b (m :: * -> *). (IsBool b, Monad m) => b -> m () -> m ()
    unless (DataRecOrFun -> DataRecOrFun -> Bool
    sameKind DataRecOrFun
    k DataRecOrFun
    k') (Nice () -> Nice ()) -> Nice () -> Nice ()
    forall a b. (a -> b) -> a -> b
    $ DeclarationException' -> Nice ()
    forall a. HasCallStack => DeclarationException' -> Nice a
    declarationException (DeclarationException' -> Nice ())
    -> DeclarationException' -> Nice ()
    forall a b. (a -> b) -> a -> b
    $ Name -> DataRecOrFun -> DataRecOrFun -> DeclarationException'
    WrongDefinition Name
    x DataRecOrFun
    k' DataRecOrFun
    k
            Maybe Expr
    forall a. Maybe a
    Nothing Maybe Expr -> Nice () -> Nice (Maybe Expr)
    forall a b. a -> Nice b -> Nice a
    forall (f :: * -> *) a b. Functor f => a -> f b -> f a
    <$ Name -> Nice ()
    removeLoneSig Name
    x

        dataOrRec
          :: forall a decl
          .  PositivityCheck
          -> UniverseCheck
          -> (Range -> Origin -> IsAbstract -> PositivityCheck -> UniverseCheck -> Name -> [LamBinding] -> [decl] -> NiceDeclaration)
             -- Construct definition.
          -> (Range -> Access -> IsAbstract -> PositivityCheck -> UniverseCheck -> Name -> [LamBinding] -> Expr -> NiceDeclaration)
             -- Construct signature.
          -> ([a] -> Nice [decl])        -- Constructor checking.
          -> Range
          -> Name                        -- Data/record type name.
          -> Maybe ([LamBinding], Expr)  -- Parameters and type.  If not @Nothing@ a signature is created.
          -> Maybe ([LamBinding], [a])   -- Parameters and constructors.  If not @Nothing@, a definition body is created.
          -> Nice [NiceDeclaration]
        dataOrRec :: forall a decl.
    PositivityCheck
    -> UniverseCheck
    -> (Range
        -> Origin
        -> IsAbstract
        -> PositivityCheck
        -> UniverseCheck
        -> Name
        -> [LamBinding]
        -> [decl]
        -> NiceDeclaration)
    -> (Range
        -> Access
        -> IsAbstract
        -> PositivityCheck
        -> UniverseCheck
        -> Name
        -> [LamBinding]
        -> Expr
        -> NiceDeclaration)
    -> ([a] -> Nice [decl])
    -> Range
    -> Name
    -> Maybe ([LamBinding], Expr)
    -> Maybe ([LamBinding], [a])
    -> Nice [NiceDeclaration]
    dataOrRec PositivityCheck
    pc UniverseCheck
    uc Range
    -> Origin
    -> IsAbstract
    -> PositivityCheck
    -> UniverseCheck
    -> Name
    -> [LamBinding]
    -> [decl]
    -> NiceDeclaration
    mkDef Range
    -> Access
    -> IsAbstract
    -> PositivityCheck
    -> UniverseCheck
    -> Name
    -> [LamBinding]
    -> Expr
    -> NiceDeclaration
    mkSig [a] -> Nice [decl]
    niceD Range
    r Name
    x Maybe ([LamBinding], Expr)
    mt Maybe ([LamBinding], [a])
    mcs = do
          mds <- Maybe ([LamBinding], [a])
    -> (([LamBinding], [a]) -> Nice ([LamBinding], [decl]))
    -> Nice (Maybe ([LamBinding], [decl]))
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    t a -> (a -> m b) -> m (t b)
    Trav.forM Maybe ([LamBinding], [a])
    mcs ((([LamBinding], [a]) -> Nice ([LamBinding], [decl]))
     -> Nice (Maybe ([LamBinding], [decl])))
    -> (([LamBinding], [a]) -> Nice ([LamBinding], [decl]))
    -> Nice (Maybe ([LamBinding], [decl]))
    forall a b. (a -> b) -> a -> b
    $ \ ([LamBinding]
    tel, [a]
    cs) -> ([LamBinding]
    tel,) ([decl] -> ([LamBinding], [decl]))
    -> Nice [decl] -> Nice ([LamBinding], [decl])
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> [a] -> Nice [decl]
    niceD [a]
    cs
          -- We set origin to UserWritten if the user split the data/rec herself,
          -- and to Inserted if the she wrote a single declaration that we're
          -- splitting up here. We distinguish these because the scoping rules for
          -- generalizable variables differ in these cases.
          let o | Maybe ([LamBinding], Expr) -> Bool
    forall a. Maybe a -> Bool
    isJust Maybe ([LamBinding], Expr)
    mt Bool -> Bool -> Bool
    && Maybe ([LamBinding], [a]) -> Bool
    forall a. Maybe a -> Bool
    isJust Maybe ([LamBinding], [a])
    mcs = Origin
    Inserted
                | Bool
    otherwise               = Origin
    UserWritten
          return $ catMaybes $
            [ mt  <&> \ ([LamBinding]
    tel, Expr
    t)  -> Range
    -> Access
    -> IsAbstract
    -> PositivityCheck
    -> UniverseCheck
    -> Name
    -> [LamBinding]
    -> Expr
    -> NiceDeclaration
    mkSig (Name -> Expr -> Range
    forall u t. (HasRange u, HasRange t) => u -> t -> Range
    fuseRange Name
    x Expr
    t) Access
    PublicAccess IsAbstract
    ConcreteDef PositivityCheck
    pc UniverseCheck
    uc Name
    x [LamBinding]
    tel Expr
    t
            , mds <&> \ ([LamBinding]
    tel, [decl]
    ds) -> Range
    -> Origin
    -> IsAbstract
    -> PositivityCheck
    -> UniverseCheck
    -> Name
    -> [LamBinding]
    -> [decl]
    -> NiceDeclaration
    mkDef Range
    r Origin
    o IsAbstract
    ConcreteDef PositivityCheck
    pc UniverseCheck
    uc Name
    x (Maybe ([LamBinding], Expr)
    -> [LamBinding]
    -> (([LamBinding], Expr) -> [LamBinding])
    -> [LamBinding]
    forall a b. Maybe a -> b -> (a -> b) -> b
    caseMaybe Maybe ([LamBinding], Expr)
    mt [LamBinding]
    tel ((([LamBinding], Expr) -> [LamBinding]) -> [LamBinding])
    -> (([LamBinding], Expr) -> [LamBinding]) -> [LamBinding]
    forall a b. (a -> b) -> a -> b
    $ [LamBinding] -> ([LamBinding], Expr) -> [LamBinding]
    forall a b. a -> b -> a
    const ([LamBinding] -> ([LamBinding], Expr) -> [LamBinding])
    -> [LamBinding] -> ([LamBinding], Expr) -> [LamBinding]
    forall a b. (a -> b) -> a -> b
    $ (LamBinding -> [LamBinding]) -> [LamBinding] -> [LamBinding]
    forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
    concatMap LamBinding -> [LamBinding]
    dropTypeAndModality [LamBinding]
    tel) [decl]
    ds
              -- If a type is given (mt /= Nothing), we have to delete the types in @tel@
              -- for the data definition, lest we duplicate them. And also drop modalities (#1886).
            ]
        -- Translate axioms
        niceAxioms :: KindOfBlock -> [TypeSignatureOrInstanceBlock] -> Nice [NiceDeclaration]
        niceAxioms :: KindOfBlock -> [Declaration] -> Nice [NiceDeclaration]
    niceAxioms KindOfBlock
    b [Declaration]
    ds = [[NiceDeclaration]] -> [NiceDeclaration]
    forall (t :: * -> *) a. Foldable t => t [a] -> [a]
    List.concat ([[NiceDeclaration]] -> [NiceDeclaration])
    -> Nice [[NiceDeclaration]] -> Nice [NiceDeclaration]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (Declaration -> Nice [NiceDeclaration])
    -> [Declaration] -> Nice [[NiceDeclaration]]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
    mapM (KindOfBlock -> Declaration -> Nice [NiceDeclaration]
    niceAxiom KindOfBlock
    b) [Declaration]
    ds

        niceAxiom :: KindOfBlock -> TypeSignatureOrInstanceBlock -> Nice [NiceDeclaration]
        niceAxiom :: KindOfBlock -> Declaration -> Nice [NiceDeclaration]
    niceAxiom KindOfBlock
    b = \case
          d :: Declaration
    d@(TypeSig ArgInfo
    rel TacticAttribute
    _tac Name
    x Expr
    t) -> do
            [NiceDeclaration] -> Nice [NiceDeclaration]
    forall a. a -> Nice a
    forall (m :: * -> *) a. Monad m => a -> m a
    return [ Range
    -> Access
    -> IsAbstract
    -> IsInstance
    -> ArgInfo
    -> Name
    -> Expr
    -> NiceDeclaration
    Axiom (Declaration -> Range
    forall a. HasRange a => a -> Range
    getRange Declaration
    d) Access
    PublicAccess IsAbstract
    ConcreteDef IsInstance
    NotInstanceDef ArgInfo
    rel Name
    x Expr
    t ]
          d :: Declaration
    d@(FieldSig IsInstance
    i TacticAttribute
    tac Name
    x Arg Expr
    argt) | KindOfBlock
    b KindOfBlock -> KindOfBlock -> Bool
    forall a. Eq a => a -> a -> Bool
    == KindOfBlock
    FieldBlock -> do
            [NiceDeclaration] -> Nice [NiceDeclaration]
    forall a. a -> Nice a
    forall (m :: * -> *) a. Monad m => a -> m a
    return [ Range
    -> Access
    -> IsAbstract
    -> IsInstance
    -> TacticAttribute
    -> Name
    -> Arg Expr
    -> NiceDeclaration
    NiceField (Declaration -> Range
    forall a. HasRange a => a -> Range
    getRange Declaration
    d) Access
    PublicAccess IsAbstract
    ConcreteDef IsInstance
    i TacticAttribute
    tac Name
    x Arg Expr
    argt ]
          InstanceB KwRange
    r [Declaration]
    decls -> do
            KwRange -> [NiceDeclaration] -> Nice [NiceDeclaration]
    instanceBlock KwRange
    r ([NiceDeclaration] -> Nice [NiceDeclaration])
    -> Nice [NiceDeclaration] -> Nice [NiceDeclaration]
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< KindOfBlock -> [Declaration] -> Nice [NiceDeclaration]
    niceAxioms KindOfBlock
    InstanceBlock [Declaration]
    decls
          Private KwRange
    r Origin
    o [Declaration]
    decls | KindOfBlock
    PostulateBlock <- KindOfBlock
    b -> do
            KwRange -> Origin -> [NiceDeclaration] -> Nice [NiceDeclaration]
    privateBlock KwRange
    r Origin
    o ([NiceDeclaration] -> Nice [NiceDeclaration])
    -> Nice [NiceDeclaration] -> Nice [NiceDeclaration]
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< KindOfBlock -> [Declaration] -> Nice [NiceDeclaration]
    niceAxioms KindOfBlock
    b [Declaration]
    decls
          Pragma p :: Pragma
    p@(RewritePragma Range
    r Range
    _ [QName]
    _) -> [NiceDeclaration] -> Nice [NiceDeclaration]
    forall a. a -> Nice a
    forall (m :: * -> *) a. Monad m => a -> m a
    return [ Range -> Pragma -> NiceDeclaration
    NicePragma Range
    r Pragma
    p ]
          Pragma p :: Pragma
    p@(OverlapPragma Range
    r [QName]
    _ OverlapMode
    _) -> [NiceDeclaration] -> Nice [NiceDeclaration]
    forall a. a -> Nice a
    forall (m :: * -> *) a. Monad m => a -> m a
    return [ Range -> Pragma -> NiceDeclaration
    NicePragma Range
    r Pragma
    p ]
          Declaration
    d -> DeclarationException' -> Nice [NiceDeclaration]
    forall a. HasCallStack => DeclarationException' -> Nice a
    declarationException (DeclarationException' -> Nice [NiceDeclaration])
    -> DeclarationException' -> Nice [NiceDeclaration]
    forall a b. (a -> b) -> a -> b
    $ KindOfBlock -> Range -> DeclarationException'
    WrongContentBlock KindOfBlock
    b (Range -> DeclarationException') -> Range -> DeclarationException'
    forall a b. (a -> b) -> a -> b
    $ Declaration -> Range
    forall a. HasRange a => a -> Range
    getRange Declaration
    d

        toPrim :: NiceDeclaration -> NiceDeclaration
        toPrim :: NiceDeclaration -> NiceDeclaration
    toPrim (Axiom Range
    r Access
    p IsAbstract
    a IsInstance
    i ArgInfo
    rel Name
    x Expr
    t) = Range
    -> Access -> IsAbstract -> Name -> Arg Expr -> NiceDeclaration
    PrimitiveFunction Range
    r Access
    p IsAbstract
    a Name
    x (ArgInfo -> Expr -> Arg Expr
    forall e. ArgInfo -> e -> Arg e
    Arg ArgInfo
    rel Expr
    t)
        toPrim NiceDeclaration
    _                       = NiceDeclaration
    forall a. HasCallStack => a
    __IMPOSSIBLE__

        -- Create a function definition.
        mkFunDef :: ArgInfo
    -> TerminationCheck
    -> CoverageCheck
    -> Name
    -> Maybe Expr
    -> [Declaration]
    -> Nice [NiceDeclaration]
    mkFunDef ArgInfo
    info TerminationCheck
    termCheck CoverageCheck
    covCheck Name
    x Maybe Expr
    mt [Declaration]
    ds0 = do
          ds <- [Declaration] -> Nice [Declaration]
    expandEllipsis [Declaration]
    ds0
          cs <- mkClauses x ds empty
          return [ FunSig (fuseRange x t) PublicAccess ConcreteDef NotInstanceDef NotMacroDef info termCheck covCheck x t
                 , FunDef (getRange ds0) ds0 ConcreteDef NotInstanceDef termCheck covCheck x cs ]
            where
              t :: Expr
    t = Expr -> Maybe Expr -> Expr
    forall a. a -> Maybe a -> a
    fromMaybe (Range -> Expr
    underscore (Name -> Range
    forall a. HasRange a => a -> Range
    getRange Name
    x)) Maybe Expr
    mt

        underscore :: Range -> Expr
    underscore Range
    r = Range -> Maybe String -> Expr
    Underscore Range
    r Maybe String
    forall a. Maybe a
    Nothing

        -- Search for the first clause that does not have an ellipsis (usually the very first one)
        -- and then use its lhs pattern to replace ellipses in the subsequent clauses (if any).
        expandEllipsis :: [Declaration] -> Nice [Declaration]
        expandEllipsis :: [Declaration] -> Nice [Declaration]
    expandEllipsis [] = [Declaration] -> Nice [Declaration]
    forall a. a -> Nice a
    forall (m :: * -> *) a. Monad m => a -> m a
    return []
        expandEllipsis (d :: Declaration
    d@(FunClause lhs :: LHS
    lhs@(LHS Pattern
    p [RewriteEqn]
    _ [WithExpr]
    _) RHS
    _ WhereClause
    _ Catchall
    _) : [Declaration]
    ds)
          | Pattern -> Bool
    forall a. HasEllipsis a => a -> Bool
    hasEllipsis Pattern
    p = (Declaration
    d Declaration -> [Declaration] -> [Declaration]
    forall a. a -> [a] -> [a]
    :) ([Declaration] -> [Declaration])
    -> Nice [Declaration] -> Nice [Declaration]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> [Declaration] -> Nice [Declaration]
    expandEllipsis [Declaration]
    ds
          | Bool
    otherwise     = (Declaration
    d Declaration -> [Declaration] -> [Declaration]
    forall a. a -> [a] -> [a]
    :) ([Declaration] -> [Declaration])
    -> Nice [Declaration] -> Nice [Declaration]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Pattern -> [Declaration] -> Nice [Declaration]
    expand (KillRangeT Pattern
    forall a. KillRange a => KillRangeT a
    killRange Pattern
    p) [Declaration]
    ds
          where
            expand :: Pattern -> [Declaration] -> Nice [Declaration]
            expand :: Pattern -> [Declaration] -> Nice [Declaration]
    expand Pattern
    _ [] = [Declaration] -> Nice [Declaration]
    forall a. a -> Nice a
    forall (m :: * -> *) a. Monad m => a -> m a
    return []
            expand Pattern
    p (Declaration
    d : [Declaration]
    ds) = do
              case Declaration
    d of
                Pragma (CatchallPragma Range
    _) -> do
                      (Declaration
    d Declaration -> [Declaration] -> [Declaration]
    forall a. a -> [a] -> [a]
    :) ([Declaration] -> [Declaration])
    -> Nice [Declaration] -> Nice [Declaration]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Pattern -> [Declaration] -> Nice [Declaration]
    expand Pattern
    p [Declaration]
    ds
                FunClause (LHS Pattern
    p0 [RewriteEqn]
    eqs [WithExpr]
    es) RHS
    rhs WhereClause
    wh Catchall
    ca -> do
                  case Pattern -> AffineHole Pattern Pattern
    forall p. CPatternLike p => p -> AffineHole Pattern p
    hasEllipsis' Pattern
    p0 of
                    AffineHole Pattern Pattern
    ManyHoles -> DeclarationException' -> Nice [Declaration]
    forall a. HasCallStack => DeclarationException' -> Nice a
    declarationException (DeclarationException' -> Nice [Declaration])
    -> DeclarationException' -> Nice [Declaration]
    forall a b. (a -> b) -> a -> b
    $ Pattern -> DeclarationException'
    MultipleEllipses Pattern
    p0
                    OneHole KillRangeT Pattern
    cxt ~(EllipsisP Range
    r Maybe Pattern
    Nothing) -> do
                      -- Replace the ellipsis by @p@.
                      let p1 :: Pattern
    p1 = KillRangeT Pattern
    cxt KillRangeT Pattern -> KillRangeT Pattern
    forall a b. (a -> b) -> a -> b
    $ Range -> Maybe Pattern -> Pattern
    EllipsisP Range
    r (Maybe Pattern -> Pattern) -> Maybe Pattern -> Pattern
    forall a b. (a -> b) -> a -> b
    $ Pattern -> Maybe Pattern
    forall a. a -> Maybe a
    Just (Pattern -> Maybe Pattern) -> Pattern -> Maybe Pattern
    forall a b. (a -> b) -> a -> b
    $ Range -> KillRangeT Pattern
    forall a. SetRange a => Range -> a -> a
    setRange Range
    r Pattern
    p
                      let d' :: Declaration
    d' = LHS -> RHS -> WhereClause -> Catchall -> Declaration
    FunClause (Pattern -> [RewriteEqn] -> [WithExpr] -> LHS
    LHS Pattern
    p1 [RewriteEqn]
    eqs [WithExpr]
    es) RHS
    rhs WhereClause
    wh Catchall
    ca
                      -- If we have with-expressions (es /= []) then the following
                      -- ellipses also get the additional patterns in p0.
                      (Declaration
    d' Declaration -> [Declaration] -> [Declaration]
    forall a. a -> [a] -> [a]
    :) ([Declaration] -> [Declaration])
    -> Nice [Declaration] -> Nice [Declaration]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Pattern -> [Declaration] -> Nice [Declaration]
    expand (if [WithExpr] -> Bool
    forall a. Null a => a -> Bool
    null [WithExpr]
    es then Pattern
    p else KillRangeT Pattern
    forall a. KillRange a => KillRangeT a
    killRange Pattern
    p1) [Declaration]
    ds
                    ZeroHoles Pattern
    _ -> do
                      -- We can have ellipses after a fun clause without.
                      -- They refer to the last clause that introduced new with-expressions.
                      -- Same here: If we have new with-expressions, the next ellipses will
                      -- refer to us.
                      -- Andreas, Jesper, 2017-05-13, issue #2578
                      -- Need to update the range also on the next with-patterns.
                      (Declaration
    d Declaration -> [Declaration] -> [Declaration]
    forall a. a -> [a] -> [a]
    :) ([Declaration] -> [Declaration])
    -> Nice [Declaration] -> Nice [Declaration]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Pattern -> [Declaration] -> Nice [Declaration]
    expand (if [WithExpr] -> Bool
    forall a. Null a => a -> Bool
    null [WithExpr]
    es then Pattern
    p else KillRangeT Pattern
    forall a. KillRange a => KillRangeT a
    killRange Pattern
    p0) [Declaration]
    ds
                Declaration
    _ -> Nice [Declaration]
    forall a. HasCallStack => a
    __IMPOSSIBLE__
        expandEllipsis [Declaration]
    _ = Nice [Declaration]
    forall a. HasCallStack => a
    __IMPOSSIBLE__

        -- Turn function clauses into nice function clauses.
        mkClauses :: Name -> [Declaration] -> Catchall -> Nice [Clause]
        mkClauses :: Name -> [Declaration] -> Catchall -> Nice [Clause]
    mkClauses Name
    _ [] Catchall
    _ = [Clause] -> Nice [Clause]
    forall a. a -> Nice a
    forall (m :: * -> *) a. Monad m => a -> m a
    return []

        -- A CATCHALL pragma after the last clause is useless.
        mkClauses Name
    x [Pragma (CatchallPragma Range
    r)] Catchall
    _ = [] [Clause] -> Nice () -> Nice [Clause]
    forall a b. a -> Nice b -> Nice a
    forall (f :: * -> *) a b. Functor f => a -> f b -> f a
    <$ do
          HasCallStack => DeclarationWarning' -> Nice ()
    DeclarationWarning' -> Nice ()
    declarationWarning (DeclarationWarning' -> Nice ()) -> DeclarationWarning' -> Nice ()
    forall a b. (a -> b) -> a -> b
    $ Range -> DeclarationWarning'
    InvalidCatchallPragma Range
    r

        mkClauses Name
    x (Pragma (CatchallPragma Range
    r) : [Declaration]
    cs) Catchall
    catchall = do
          -- Warn about consecutive CATCHALL pragmas
          Bool -> Nice () -> Nice ()
    forall b (m :: * -> *). (IsBool b, Monad m) => b -> m () -> m ()
    unless (Catchall -> Bool
    forall a. Null a => a -> Bool
    null Catchall
    catchall) (Nice () -> Nice ()) -> Nice () -> Nice ()
    forall a b. (a -> b) -> a -> b
    $ HasCallStack => DeclarationWarning' -> Nice ()
    DeclarationWarning' -> Nice ()
    declarationWarning (DeclarationWarning' -> Nice ()) -> DeclarationWarning' -> Nice ()
    forall a b. (a -> b) -> a -> b
    $ Range -> DeclarationWarning'
    InvalidCatchallPragma Range
    r
          Name -> [Declaration] -> Catchall -> Nice [Clause]
    mkClauses Name
    x [Declaration]
    cs (Range -> Catchall
    YesCatchall Range
    r)

        mkClauses Name
    x (FunClause LHS
    lhs RHS
    rhs WhereClause
    wh Catchall
    ca : [Declaration]
    cs) Catchall
    catchall
          | [WithExpr] -> Bool
    forall a. Null a => a -> Bool
    null (LHS -> [WithExpr]
    lhsWithExpr LHS
    lhs) Bool -> Bool -> Bool
    || LHS -> Bool
    forall a. HasEllipsis a => a -> Bool
    hasEllipsis LHS
    lhs  =
          (Name -> Catchall -> LHS -> RHS -> WhereClause -> [Clause] -> Clause
    Clause Name
    x (Catchall
    ca Catchall -> Catchall -> Catchall
    forall a. Semigroup a => a -> a -> a
    <> Catchall
    catchall) LHS
    lhs RHS
    rhs WhereClause
    wh [] Clause -> [Clause] -> [Clause]
    forall a. a -> [a] -> [a]
    :) ([Clause] -> [Clause]) -> Nice [Clause] -> Nice [Clause]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Name -> [Declaration] -> Catchall -> Nice [Clause]
    mkClauses Name
    x [Declaration]
    cs Catchall
    forall a. Null a => a
    empty   -- Will result in an error later.

        mkClauses Name
    x (FunClause LHS
    lhs RHS
    rhs WhereClause
    wh Catchall
    ca : [Declaration]
    cs) Catchall
    catchall = do
          Bool -> Nice () -> Nice ()
    forall b (m :: * -> *). (IsBool b, Monad m) => b -> m () -> m ()
    when ([Declaration] -> Bool
    forall a. Null a => a -> Bool
    null [Declaration]
    withClauses) (Nice () -> Nice ()) -> Nice () -> Nice ()
    forall a b. (a -> b) -> a -> b
    $ DeclarationException' -> Nice ()
    forall a. HasCallStack => DeclarationException' -> Nice a
    declarationException (DeclarationException' -> Nice ())
    -> DeclarationException' -> Nice ()
    forall a b. (a -> b) -> a -> b
    $ Name -> LHS -> DeclarationException'
    MissingWithClauses Name
    x LHS
    lhs
          wcs <- Name -> [Declaration] -> Catchall -> Nice [Clause]
    mkClauses Name
    x [Declaration]
    withClauses Catchall
    forall a. Null a => a
    empty
          (Clause x (ca <> catchall) lhs rhs wh wcs :) <$> mkClauses x cs' empty
          where
            ([Declaration]
    withClauses, [Declaration]
    cs') = [Declaration] -> ([Declaration], [Declaration])
    subClauses [Declaration]
    cs

            -- A clause is a subclause if the number of with-patterns is
            -- greater or equal to the current number of with-patterns plus the
            -- number of with arguments.
            numWith :: Int
    numWith = Pattern -> Int
    forall p. CPatternLike p => p -> Int
    numberOfWithPatterns Pattern
    p Int -> Int -> Int
    forall a. Num a => a -> a -> a
    + [WithExpr] -> Int
    forall a. [a] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length ((WithExpr -> Bool) -> [WithExpr] -> [WithExpr]
    forall a. (a -> Bool) -> [a] -> [a]
    filter WithExpr -> Bool
    forall a. LensHiding a => a -> Bool
    visible [WithExpr]
    es) where LHS Pattern
    p [RewriteEqn]
    _ [WithExpr]
    es = LHS
    lhs

            subClauses :: [Declaration] -> ([Declaration],[Declaration])
            subClauses :: [Declaration] -> ([Declaration], [Declaration])
    subClauses (c :: Declaration
    c@(FunClause (LHS Pattern
    p0 [RewriteEqn]
    _ [WithExpr]
    _) RHS
    _ WhereClause
    _ Catchall
    _) : [Declaration]
    cs)
             | Pattern -> Bool
    forall a. IsEllipsis a => a -> Bool
    isEllipsis Pattern
    p0 Bool -> Bool -> Bool
    ||
               Pattern -> Int
    forall p. CPatternLike p => p -> Int
    numberOfWithPatterns Pattern
    p0 Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    >= Int
    numWith = ([Declaration] -> [Declaration])
    -> ([Declaration], [Declaration]) -> ([Declaration], [Declaration])
    forall a c b. (a -> c) -> (a, b) -> (c, b)
    mapFst (Declaration
    cDeclaration -> [Declaration] -> [Declaration]
    forall a. a -> [a] -> [a]
    :) ([Declaration] -> ([Declaration], [Declaration])
    subClauses [Declaration]
    cs)
             | Bool
    otherwise                           = ([], Declaration
    cDeclaration -> [Declaration] -> [Declaration]
    forall a. a -> [a] -> [a]
    :[Declaration]
    cs)
            subClauses (c :: Declaration
    c@(Pragma (CatchallPragma Range
    r)) : [Declaration]
    cs) = case [Declaration] -> ([Declaration], [Declaration])
    subClauses [Declaration]
    cs of
              ([], [Declaration]
    cs') -> ([], Declaration
    cDeclaration -> [Declaration] -> [Declaration]
    forall a. a -> [a] -> [a]
    :[Declaration]
    cs')
              ([Declaration]
    cs, [Declaration]
    cs') -> (Declaration
    cDeclaration -> [Declaration] -> [Declaration]
    forall a. a -> [a] -> [a]
    :[Declaration]
    cs, [Declaration]
    cs')
            subClauses [] = ([],[])
            subClauses [Declaration]
    _  = ([Declaration], [Declaration])
    forall a. HasCallStack => a
    __IMPOSSIBLE__
        mkClauses Name
    _ [Declaration]
    _ Catchall
    _ = Nice [Clause]
    forall a. HasCallStack => a
    __IMPOSSIBLE__

        couldBeCallOf :: Maybe Fixity' -> Name -> Pattern -> Bool
        couldBeCallOf :: Maybe Fixity' -> Name -> Pattern -> Bool
    couldBeCallOf Maybe Fixity'
    mFixity Name
    x Pattern
    p =
          let
          pns :: [QName]
    pns        = Pattern -> [QName]
    forall p. CPatternLike p => p -> [QName]
    patternQNames Pattern
    p
          xStrings :: [String]
    xStrings   = Name -> [String]
    nameStringParts Name
    x
          patStrings :: [String]
    patStrings = (Name -> [String]) -> [Name] -> [String]
    forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
    concatMap Name -> [String]
    nameStringParts ([Name] -> [String]) -> [Name] -> [String]
    forall a b. (a -> b) -> a -> b
    $ (QName -> Maybe Name) -> [QName] -> [Name]
    forall a b. (a -> Maybe b) -> [a] -> [b]
    mapMaybe QName -> Maybe Name
    isUnqualified [QName]
    pns
          in
    --          trace ("x = " ++ prettyShow x) $
    --          trace ("pns = " ++ show pns) $
    --          trace ("xStrings = " ++ show xStrings) $
    --          trace ("patStrings = " ++ show patStrings) $
    --          trace ("mFixity = " ++ show mFixity) $
          case ([QName] -> Maybe QName
    forall a. [a] -> Maybe a
    listToMaybe [QName]
    pns, Maybe Fixity'
    mFixity) of
            -- first identifier in the patterns is the fun.symbol?
            (Just QName
    y, Maybe Fixity'
    _) | Name -> Maybe Name
    forall a. a -> Maybe a
    Just Name
    x Maybe Name -> Maybe Name -> Bool
    forall a. Eq a => a -> a -> Bool
    == QName -> Maybe Name
    isUnqualified QName
    y -> Bool
    True -- trace ("couldBe since y = " ++ prettyShow y) $ True
            -- are the parts of x contained in p
            (Maybe QName, Maybe Fixity')
    _ | [String]
    xStrings [String] -> [String] -> Bool
    forall a. Eq a => [a] -> [a] -> Bool
    `List.isSubsequenceOf` [String]
    patStrings -> Bool
    True
            -- looking for a mixfix fun.symb
            (Maybe QName
    _, Just Fixity'
    fix) ->  -- also matches in case of a postfix
               let notStrings :: [String]
    notStrings = Notation -> [String]
    stringParts (Fixity' -> Notation
    theNotation Fixity'
    fix)
               in  -- trace ("notStrings = " ++ show notStrings) $
                   -- trace ("patStrings = " ++ show patStrings) $
                   Bool -> Bool
    not ([String] -> Bool
    forall a. Null a => a -> Bool
    null [String]
    notStrings) Bool -> Bool -> Bool
    && ([String]
    notStrings [String] -> [String] -> Bool
    forall a. Eq a => [a] -> [a] -> Bool
    `List.isSubsequenceOf` [String]
    patStrings)
            -- not a notation, not first id: give up
            (Maybe QName, Maybe Fixity')
    _ -> Bool
    False -- trace ("couldBe not (case default)") $ False

        -- for finding nice clauses for a type sig in mutual blocks
        couldBeNiceFunClauseOf :: Maybe Fixity' -> Name -> NiceDeclaration
                               -> Maybe (MutualChecks, Declaration)
        couldBeNiceFunClauseOf :: Maybe Fixity'
    -> Name -> NiceDeclaration -> Maybe (MutualChecks, Declaration)
    couldBeNiceFunClauseOf Maybe Fixity'
    mf Name
    n (NiceFunClause Range
    _ Access
    _ IsAbstract
    _ TerminationCheck
    tc CoverageCheck
    cc Catchall
    _ Declaration
    d)
          = ([TerminationCheck]
    -> [CoverageCheck] -> [PositivityCheck] -> MutualChecks
    MutualChecks [TerminationCheck
    tc] [CoverageCheck
    cc] [], Declaration
    d) (MutualChecks, Declaration)
    -> Maybe () -> Maybe (MutualChecks, Declaration)
    forall a b. a -> Maybe b -> Maybe a
    forall (f :: * -> *) a b. Functor f => a -> f b -> f a
    <$ Bool -> Maybe ()
    forall b (m :: * -> *). (IsBool b, MonadPlus m) => b -> m ()
    guard (Maybe Fixity' -> Name -> Declaration -> Bool
    couldBeFunClauseOf Maybe Fixity'
    mf Name
    n Declaration
    d)
        couldBeNiceFunClauseOf Maybe Fixity'
    _ Name
    _ NiceDeclaration
    _ = Maybe (MutualChecks, Declaration)
    forall a. Maybe a
    Nothing

        -- for finding clauses for a type sig in mutual blocks
        couldBeFunClauseOf :: Maybe Fixity' -> Name -> Declaration -> Bool
        couldBeFunClauseOf :: Maybe Fixity' -> Name -> Declaration -> Bool
    couldBeFunClauseOf Maybe Fixity'
    mFixity Name
    x (Pragma (CatchallPragma{})) = Bool
    True
        couldBeFunClauseOf Maybe Fixity'
    mFixity Name
    x (FunClause (LHS Pattern
    p [RewriteEqn]
    _ [WithExpr]
    _) RHS
    _ WhereClause
    _ Catchall
    _) =
           Pattern -> Bool
    forall a. HasEllipsis a => a -> Bool
    hasEllipsis Pattern
    p Bool -> Bool -> Bool
    || Maybe Fixity' -> Name -> Pattern -> Bool
    couldBeCallOf Maybe Fixity'
    mFixity Name
    x Pattern
    p
        couldBeFunClauseOf Maybe Fixity'
    _ Name
    _ Declaration
    _ = Bool
    False -- trace ("couldBe not (fun default)") $ False

        -- Turn a new style `interleaved mutual' block into a new style mutual block
        -- by grouping the declarations in blocks.
        mkInterleavedMutual
          :: KwRange               -- Range of the @interleaved mutual@ keywords.
          -> [NiceDeclaration]     -- Declarations inside the block.
          -> Nice NiceDeclaration  -- Returns a 'NiceMutual'.
        mkInterleavedMutual :: KwRange -> [NiceDeclaration] -> Nice NiceDeclaration
    mkInterleavedMutual KwRange
    kwr [NiceDeclaration]
    ds' = do
          (other, (m, checks, _)) <- StateT
      (InterleavedMutual, MutualChecks, Int)
      Nice
      [(Int, NiceDeclaration)]
    -> (InterleavedMutual, MutualChecks, Int)
    -> Nice
         ([(Int, NiceDeclaration)], (InterleavedMutual, MutualChecks, Int))
    forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
    runStateT (KwRange
    -> [NiceDeclaration]
    -> StateT
         (InterleavedMutual, MutualChecks, Int)
         Nice
         [(Int, NiceDeclaration)]
    groupByBlocks KwRange
    kwr [NiceDeclaration]
    ds') (InterleavedMutual
    forall a. Null a => a
    empty, MutualChecks
    forall a. Monoid a => a
    mempty, Int
    0)
          let idecls = [(Int, NiceDeclaration)]
    other [(Int, NiceDeclaration)]
    -> [(Int, NiceDeclaration)] -> [(Int, NiceDeclaration)]
    forall a. [a] -> [a] -> [a]
    ++ ((Name, InterleavedDecl) -> [(Int, NiceDeclaration)])
    -> [(Name, InterleavedDecl)] -> [(Int, NiceDeclaration)]
    forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
    concatMap ((Name -> InterleavedDecl -> [(Int, NiceDeclaration)])
    -> (Name, InterleavedDecl) -> [(Int, NiceDeclaration)]
    forall a b c. (a -> b -> c) -> (a, b) -> c
    uncurry Name -> InterleavedDecl -> [(Int, NiceDeclaration)]
    interleavedDecl) (InterleavedMutual -> [(Name, InterleavedDecl)]
    forall k a. Map k a -> [(k, a)]
    Map.toList InterleavedMutual
    m)
          let decls0 = ((Int, NiceDeclaration) -> NiceDeclaration)
    -> [(Int, NiceDeclaration)] -> [NiceDeclaration]
    forall a b. (a -> b) -> [a] -> [b]
    map (Int, NiceDeclaration) -> NiceDeclaration
    forall a b. (a, b) -> b
    snd ([(Int, NiceDeclaration)] -> [NiceDeclaration])
    -> [(Int, NiceDeclaration)] -> [NiceDeclaration]
    forall a b. (a -> b) -> a -> b
    $ ((Int, NiceDeclaration) -> (Int, NiceDeclaration) -> Ordering)
    -> [(Int, NiceDeclaration)] -> [(Int, NiceDeclaration)]
    forall a. (a -> a -> Ordering) -> [a] -> [a]
    List.sortBy (Int -> Int -> Ordering
    forall a. Ord a => a -> a -> Ordering
    compare (Int -> Int -> Ordering)
    -> ((Int, NiceDeclaration) -> Int)
    -> (Int, NiceDeclaration)
    -> (Int, NiceDeclaration)
    -> Ordering
    forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
    `on` (Int, NiceDeclaration) -> Int
    forall a b. (a, b) -> a
    fst) [(Int, NiceDeclaration)]
    idecls
          ps <- use loneSigs
          checkLoneSigs ps
          let decls = LoneSigs -> [NiceDeclaration] -> [NiceDeclaration]
    replaceSigs LoneSigs
    ps [NiceDeclaration]
    decls0
          -- process the checks
          let r = KwRange -> [NiceDeclaration] -> Range
    forall u t. (HasRange u, HasRange t) => u -> t -> Range
    fuseRange KwRange
    kwr [NiceDeclaration]
    ds'
          tc <- combineTerminationChecks r (mutualTermination checks)
          let cc = [CoverageCheck] -> CoverageCheck
    combineCoverageChecks   (MutualChecks -> [CoverageCheck]
    mutualCoverage MutualChecks
    checks)
          let pc = [PositivityCheck] -> PositivityCheck
    combinePositivityChecks (MutualChecks -> [PositivityCheck]
    mutualPositivity MutualChecks
    checks)
          pure $ NiceMutual kwr tc cc pc decls

          where

            ------------------------------------------------------------------------------
            -- Adding Signatures
            addType :: Name -> (DeclNum -> a) -> MutualChecks
                    -> StateT (Map Name a, MutualChecks, DeclNum) Nice ()
            addType :: forall a.
    Name
    -> (Int -> a)
    -> MutualChecks
    -> StateT (Map Name a, MutualChecks, Int) Nice ()
    addType Name
    n Int -> a
    c MutualChecks
    mc = do
              (m, checks, i) <- StateT
      (Map Name a, MutualChecks, Int)
      Nice
      (Map Name a, MutualChecks, Int)
    forall s (m :: * -> *). MonadState s m => m s
    get
              when (isJust $ Map.lookup n m) $ lift $ declarationException $ DuplicateDefinition n
              put (Map.insert n (c i) m, mc <> checks, i + 1)

            addFunType :: NiceDeclaration
    -> StateT (InterleavedMutual, MutualChecks, Int) Nice ()
    addFunType d :: NiceDeclaration
    d@(FunSig Range
    _ Access
    _ IsAbstract
    _ IsInstance
    _ IsMacro
    _ ArgInfo
    _ TerminationCheck
    tc CoverageCheck
    cc Name
    n Expr
    _) = do
               let checks :: MutualChecks
    checks = [TerminationCheck]
    -> [CoverageCheck] -> [PositivityCheck] -> MutualChecks
    MutualChecks [TerminationCheck
    tc] [CoverageCheck
    cc] []
               Name
    -> (Int -> InterleavedDecl)
    -> MutualChecks
    -> StateT (InterleavedMutual, MutualChecks, Int) Nice ()
    forall a.
    Name
    -> (Int -> a)
    -> MutualChecks
    -> StateT (Map Name a, MutualChecks, Int) Nice ()
    addType Name
    n (\ Int
    i -> Int
    -> NiceDeclaration
    -> Maybe (Int, List1 ([Declaration], [Clause]))
    -> InterleavedDecl
    InterleavedFun Int
    i NiceDeclaration
    d Maybe (Int, List1 ([Declaration], [Clause]))
    forall a. Maybe a
    Nothing) MutualChecks
    checks
            addFunType NiceDeclaration
    _ = StateT (InterleavedMutual, MutualChecks, Int) Nice ()
    forall a. HasCallStack => a
    __IMPOSSIBLE__

            addDataType :: NiceDeclaration
    -> StateT (InterleavedMutual, MutualChecks, Int) Nice ()
    addDataType d :: NiceDeclaration
    d@(NiceDataSig Range
    _ Erased
    _ Access
    _ IsAbstract
    _ PositivityCheck
    pc UniverseCheck
    uc Name
    n [LamBinding]
    _ Expr
    _) = do
              let checks :: MutualChecks
    checks = [TerminationCheck]
    -> [CoverageCheck] -> [PositivityCheck] -> MutualChecks
    MutualChecks [] [] [PositivityCheck
    pc]
              Name
    -> (Int -> InterleavedDecl)
    -> MutualChecks
    -> StateT (InterleavedMutual, MutualChecks, Int) Nice ()
    forall a.
    Name
    -> (Int -> a)
    -> MutualChecks
    -> StateT (Map Name a, MutualChecks, Int) Nice ()
    addType Name
    n (\ Int
    i -> Int
    -> NiceDeclaration
    -> Maybe (Int, List1 [NiceDeclaration])
    -> InterleavedDecl
    InterleavedData Int
    i NiceDeclaration
    d Maybe (Int, List1 [NiceDeclaration])
    forall a. Maybe a
    Nothing) MutualChecks
    checks
            addDataType NiceDeclaration
    _ = StateT (InterleavedMutual, MutualChecks, Int) Nice ()
    forall a. HasCallStack => a
    __IMPOSSIBLE__

            ------------------------------------------------------------------------------
            -- Adding constructors & clauses

            addDataConstructors :: Maybe Range        -- Range of the `data A where` (if any)
                                -> Maybe Name         -- Data type the constructors belong to
                                -> [NiceConstructor]  -- Constructors to add
                                -> StateT (InterleavedMutual, MutualChecks, DeclNum) Nice ()
            -- if we know the type's name, we can go ahead
            addDataConstructors :: Maybe Range
    -> Maybe Name
    -> [NiceDeclaration]
    -> StateT (InterleavedMutual, MutualChecks, Int) Nice ()
    addDataConstructors Maybe Range
    mr (Just Name
    n) [NiceDeclaration]
    ds = do
              (m, checks, i) <- StateT
      (InterleavedMutual, MutualChecks, Int)
      Nice
      (InterleavedMutual, MutualChecks, Int)
    forall s (m :: * -> *). MonadState s m => m s
    get
              case Map.lookup n m of
                Just (InterleavedData Int
    i0 NiceDeclaration
    sig Maybe (Int, List1 [NiceDeclaration])
    cs) -> do
                  Nice () -> StateT (InterleavedMutual, MutualChecks, Int) Nice ()
    forall (m :: * -> *) a.
    Monad m =>
    m a -> StateT (InterleavedMutual, MutualChecks, Int) m a
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (Nice () -> StateT (InterleavedMutual, MutualChecks, Int) Nice ())
    -> Nice () -> StateT (InterleavedMutual, MutualChecks, Int) Nice ()
    forall a b. (a -> b) -> a -> b
    $ Name -> Nice ()
    removeLoneSig Name
    n
                  -- add the constructors to the existing ones (if any)
                  let ((Int, List1 [NiceDeclaration])
    cs', Int
    i') = case Maybe (Int, List1 [NiceDeclaration])
    cs of
                        Maybe (Int, List1 [NiceDeclaration])
    Nothing        -> ((Int
    i , [NiceDeclaration]
    ds [NiceDeclaration] -> [[NiceDeclaration]] -> List1 [NiceDeclaration]
    forall a. a -> [a] -> NonEmpty a
    :| [] ), Int
    i Int -> Int -> Int
    forall a. Num a => a -> a -> a
    + Int
    1)
                        Just (Int
    i1, List1 [NiceDeclaration]
    ds1) -> ((Int
    i1, [NiceDeclaration]
    ds [NiceDeclaration]
    -> List1 [NiceDeclaration] -> List1 [NiceDeclaration]
    forall a. a -> NonEmpty a -> NonEmpty a
    <| List1 [NiceDeclaration]
    ds1), Int
    i)
                  (InterleavedMutual, MutualChecks, Int)
    -> StateT (InterleavedMutual, MutualChecks, Int) Nice ()
    forall s (m :: * -> *). MonadState s m => s -> m ()
    put (Name -> InterleavedDecl -> InterleavedMutual -> InterleavedMutual
    forall k a. Ord k => k -> a -> Map k a -> Map k a
    Map.insert Name
    n (Int
    -> NiceDeclaration
    -> Maybe (Int, List1 [NiceDeclaration])
    -> InterleavedDecl
    InterleavedData Int
    i0 NiceDeclaration
    sig ((Int, List1 [NiceDeclaration])
    -> Maybe (Int, List1 [NiceDeclaration])
    forall a. a -> Maybe a
    Just (Int, List1 [NiceDeclaration])
    cs')) InterleavedMutual
    m, MutualChecks
    checks, Int
    i')
                Maybe InterleavedDecl
    _ -> Nice () -> StateT (InterleavedMutual, MutualChecks, Int) Nice ()
    forall (m :: * -> *) a.
    Monad m =>
    m a -> StateT (InterleavedMutual, MutualChecks, Int) m a
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (Nice () -> StateT (InterleavedMutual, MutualChecks, Int) Nice ())
    -> Nice () -> StateT (InterleavedMutual, MutualChecks, Int) Nice ()
    forall a b. (a -> b) -> a -> b
    $ HasCallStack => DeclarationWarning' -> Nice ()
    DeclarationWarning' -> Nice ()
    declarationWarning (DeclarationWarning' -> Nice ()) -> DeclarationWarning' -> Nice ()
    forall a b. (a -> b) -> a -> b
    $ Name -> DeclarationWarning'
    MissingDataDeclaration Name
    n

            addDataConstructors Maybe Range
    mr Maybe Name
    Nothing [] = () -> StateT (InterleavedMutual, MutualChecks, Int) Nice ()
    forall a. a -> StateT (InterleavedMutual, MutualChecks, Int) Nice a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure ()

            -- Otherwise we try to guess which datasig the constructor is referring to
            addDataConstructors Maybe Range
    mr Maybe Name
    Nothing (NiceDeclaration
    d : [NiceDeclaration]
    ds) = do
              -- get the candidate data types that are in this interleaved mutual block
              (m, _, _) <- StateT
      (InterleavedMutual, MutualChecks, Int)
      Nice
      (InterleavedMutual, MutualChecks, Int)
    forall s (m :: * -> *). MonadState s m => m s
    get
              let sigs = ((Name, InterleavedDecl) -> Maybe Name)
    -> [(Name, InterleavedDecl)] -> [Name]
    forall a b. (a -> Maybe b) -> [a] -> [b]
    mapMaybe (\ (Name
    n, InterleavedDecl
    d) -> Name
    n Name -> Maybe () -> Maybe Name
    forall a b. a -> Maybe b -> Maybe a
    forall (f :: * -> *) a b. Functor f => a -> f b -> f a
    <$ InterleavedDecl -> Maybe ()
    isInterleavedData InterleavedDecl
    d) ([(Name, InterleavedDecl)] -> [Name])
    -> [(Name, InterleavedDecl)] -> [Name]
    forall a b. (a -> b) -> a -> b
    $ InterleavedMutual -> [(Name, InterleavedDecl)]
    forall k a. Map k a -> [(k, a)]
    Map.toList InterleavedMutual
    m
              -- check whether this constructor matches any of them
              case isConstructor sigs d of
                Right Name
    n -> do
                  -- if so grab the whole block that may work and add them
                  let ([NiceDeclaration]
    ds0, [NiceDeclaration]
    ds1) = (NiceDeclaration -> Bool)
    -> [NiceDeclaration] -> ([NiceDeclaration], [NiceDeclaration])
    forall a. (a -> Bool) -> [a] -> ([a], [a])
    span (Either (Name, [Name]) Name -> Bool
    forall a b. Either a b -> Bool
    isRight (Either (Name, [Name]) Name -> Bool)
    -> (NiceDeclaration -> Either (Name, [Name]) Name)
    -> NiceDeclaration
    -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [Name] -> NiceDeclaration -> Either (Name, [Name]) Name
    isConstructor [Name
    n]) [NiceDeclaration]
    ds
                  Maybe Range
    -> Maybe Name
    -> [NiceDeclaration]
    -> StateT (InterleavedMutual, MutualChecks, Int) Nice ()
    addDataConstructors Maybe Range
    forall a. Maybe a
    Nothing (Name -> Maybe Name
    forall a. a -> Maybe a
    Just Name
    n) (NiceDeclaration
    d NiceDeclaration -> [NiceDeclaration] -> [NiceDeclaration]
    forall a. a -> [a] -> [a]
    : [NiceDeclaration]
    ds0)
                  -- and then repeat the process for the rest of the block
                  Maybe Range
    -> Maybe Name
    -> [NiceDeclaration]
    -> StateT (InterleavedMutual, MutualChecks, Int) Nice ()
    addDataConstructors Maybe Range
    forall a. Maybe a
    Nothing Maybe Name
    forall a. Maybe a
    Nothing [NiceDeclaration]
    ds1
                Left (Name
    n, [Name]
    ns) -> Nice () -> StateT (InterleavedMutual, MutualChecks, Int) Nice ()
    forall (m :: * -> *) a.
    Monad m =>
    m a -> StateT (InterleavedMutual, MutualChecks, Int) m a
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (Nice () -> StateT (InterleavedMutual, MutualChecks, Int) Nice ())
    -> Nice () -> StateT (InterleavedMutual, MutualChecks, Int) Nice ()
    forall a b. (a -> b) -> a -> b
    $ DeclarationException' -> Nice ()
    forall a. HasCallStack => DeclarationException' -> Nice a
    declarationException (DeclarationException' -> Nice ())
    -> DeclarationException' -> Nice ()
    forall a b. (a -> b) -> a -> b
    $ Range -> Name -> [Name] -> DeclarationException'
    AmbiguousConstructor (NiceDeclaration -> Range
    forall a. HasRange a => a -> Range
    getRange NiceDeclaration
    d) Name
    n [Name]
    ns

            addFunDef :: NiceDeclaration -> StateT (InterleavedMutual, MutualChecks, DeclNum) Nice ()
            addFunDef :: NiceDeclaration
    -> StateT (InterleavedMutual, MutualChecks, Int) Nice ()
    addFunDef (FunDef Range
    _ [Declaration]
    ds IsAbstract
    _ IsInstance
    _ TerminationCheck
    tc CoverageCheck
    cc Name
    n [Clause]
    cs) = do
              let check :: MutualChecks
    check = [TerminationCheck]
    -> [CoverageCheck] -> [PositivityCheck] -> MutualChecks
    MutualChecks [TerminationCheck
    tc] [CoverageCheck
    cc] []
              (m, checks, i) <- StateT
      (InterleavedMutual, MutualChecks, Int)
      Nice
      (InterleavedMutual, MutualChecks, Int)
    forall s (m :: * -> *). MonadState s m => m s
    get
              case Map.lookup n m of
                Just (InterleavedFun Int
    i0 NiceDeclaration
    sig Maybe (Int, List1 ([Declaration], [Clause]))
    cs0) -> do
                  let ((Int, List1 ([Declaration], [Clause]))
    cs', Int
    i') = case Maybe (Int, List1 ([Declaration], [Clause]))
    cs0 of
                        Maybe (Int, List1 ([Declaration], [Clause]))
    Nothing        -> ((Int
    i,  ([Declaration]
    ds, [Clause]
    cs) ([Declaration], [Clause])
    -> [([Declaration], [Clause])] -> List1 ([Declaration], [Clause])
    forall a. a -> [a] -> NonEmpty a
    :| [] ), Int
    i Int -> Int -> Int
    forall a. Num a => a -> a -> a
    + Int
    1)
                        Just (Int
    i1, List1 ([Declaration], [Clause])
    cs1) -> ((Int
    i1, ([Declaration]
    ds, [Clause]
    cs) ([Declaration], [Clause])
    -> List1 ([Declaration], [Clause])
    -> List1 ([Declaration], [Clause])
    forall a. a -> NonEmpty a -> NonEmpty a
    <| List1 ([Declaration], [Clause])
    cs1), Int
    i)
                  (InterleavedMutual, MutualChecks, Int)
    -> StateT (InterleavedMutual, MutualChecks, Int) Nice ()
    forall s (m :: * -> *). MonadState s m => s -> m ()
    put (Name -> InterleavedDecl -> InterleavedMutual -> InterleavedMutual
    forall k a. Ord k => k -> a -> Map k a -> Map k a
    Map.insert Name
    n (Int
    -> NiceDeclaration
    -> Maybe (Int, List1 ([Declaration], [Clause]))
    -> InterleavedDecl
    InterleavedFun Int
    i0 NiceDeclaration
    sig ((Int, List1 ([Declaration], [Clause]))
    -> Maybe (Int, List1 ([Declaration], [Clause]))
    forall a. a -> Maybe a
    Just (Int, List1 ([Declaration], [Clause]))
    cs')) InterleavedMutual
    m, MutualChecks
    check MutualChecks -> MutualChecks -> MutualChecks
    forall a. Semigroup a => a -> a -> a
    <> MutualChecks
    checks, Int
    i')
                Maybe InterleavedDecl
    _ -> StateT (InterleavedMutual, MutualChecks, Int) Nice ()
    forall a. HasCallStack => a
    __IMPOSSIBLE__ -- A FunDef always come after an existing FunSig!
            addFunDef NiceDeclaration
    _ = StateT (InterleavedMutual, MutualChecks, Int) Nice ()
    forall a. HasCallStack => a
    __IMPOSSIBLE__

            addFunClauses ::
                 KwRange
              -> [NiceDeclaration]
              -> StateT (InterleavedMutual, MutualChecks, DeclNum) Nice [(DeclNum, NiceDeclaration)]
            addFunClauses :: KwRange
    -> [NiceDeclaration]
    -> StateT
         (InterleavedMutual, MutualChecks, Int)
         Nice
         [(Int, NiceDeclaration)]
    addFunClauses KwRange
    r (nd :: NiceDeclaration
    nd@(NiceFunClause Range
    _ Access
    _ IsAbstract
    _ TerminationCheck
    tc CoverageCheck
    cc Catchall
    _ d :: Declaration
    d@(FunClause LHS
    lhs RHS
    _ WhereClause
    _ Catchall
    _)) : [NiceDeclaration]
    ds) = do
              -- get the candidate functions that are in this interleaved mutual block
              (m, checks, i) <- StateT
      (InterleavedMutual, MutualChecks, Int)
      Nice
      (InterleavedMutual, MutualChecks, Int)
    forall s (m :: * -> *). MonadState s m => m s
    get
              let sigs = ((Name, InterleavedDecl) -> Maybe Name)
    -> [(Name, InterleavedDecl)] -> [Name]
    forall a b. (a -> Maybe b) -> [a] -> [b]
    mapMaybe (\ (Name
    n, InterleavedDecl
    d) -> Name
    n Name -> Maybe () -> Maybe Name
    forall a b. a -> Maybe b -> Maybe a
    forall (f :: * -> *) a b. Functor f => a -> f b -> f a
    <$ InterleavedDecl -> Maybe ()
    isInterleavedFun InterleavedDecl
    d) ([(Name, InterleavedDecl)] -> [Name])
    -> [(Name, InterleavedDecl)] -> [Name]
    forall a b. (a -> b) -> a -> b
    $ InterleavedMutual -> [(Name, InterleavedDecl)]
    forall k a. Map k a -> [(k, a)]
    Map.toList InterleavedMutual
    m
              -- find the funsig candidates for the funclause of interest
              case [ (x, fits, rest)
                   | x <- sigs
                   , let (fits, rest) = spanJust (couldBeNiceFunClauseOf (Map.lookup x fixs) x) (nd : ds)
                   , not (null fits)
                   ] of
                -- no candidate: keep the isolated fun clause, we'll complain about it later
                [] -> do
                  let check :: MutualChecks
    check = [TerminationCheck]
    -> [CoverageCheck] -> [PositivityCheck] -> MutualChecks
    MutualChecks [TerminationCheck
    tc] [CoverageCheck
    cc] []
                  (InterleavedMutual, MutualChecks, Int)
    -> StateT (InterleavedMutual, MutualChecks, Int) Nice ()
    forall s (m :: * -> *). MonadState s m => s -> m ()
    put (InterleavedMutual
    m, MutualChecks
    check MutualChecks -> MutualChecks -> MutualChecks
    forall a. Semigroup a => a -> a -> a
    <> MutualChecks
    checks, Int
    i Int -> Int -> Int
    forall a. Num a => a -> a -> a
    + Int
    1)
                  ((Int
    i,NiceDeclaration
    nd) (Int, NiceDeclaration)
    -> [(Int, NiceDeclaration)] -> [(Int, NiceDeclaration)]
    forall a. a -> [a] -> [a]
    :) ([(Int, NiceDeclaration)] -> [(Int, NiceDeclaration)])
    -> StateT
         (InterleavedMutual, MutualChecks, Int)
         Nice
         [(Int, NiceDeclaration)]
    -> StateT
         (InterleavedMutual, MutualChecks, Int)
         Nice
         [(Int, NiceDeclaration)]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> KwRange
    -> [NiceDeclaration]
    -> StateT
         (InterleavedMutual, MutualChecks, Int)
         Nice
         [(Int, NiceDeclaration)]
    groupByBlocks KwRange
    r [NiceDeclaration]
    ds
                -- exactly one candidate: attach the funclause to the definition
                [(Name
    n, Prefix (MutualChecks, Declaration)
    fits0, [NiceDeclaration]
    rest)] -> do
                  let ([MutualChecks]
    checkss, [Declaration]
    fits) = Prefix (MutualChecks, Declaration)
    -> ([MutualChecks], [Declaration])
    forall a b. [(a, b)] -> ([a], [b])
    unzip Prefix (MutualChecks, Declaration)
    fits0
                  ds <- Nice [Declaration]
    -> StateT (InterleavedMutual, MutualChecks, Int) Nice [Declaration]
    forall (m :: * -> *) a.
    Monad m =>
    m a -> StateT (InterleavedMutual, MutualChecks, Int) m a
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (Nice [Declaration]
     -> StateT
          (InterleavedMutual, MutualChecks, Int) Nice [Declaration])
    -> Nice [Declaration]
    -> StateT (InterleavedMutual, MutualChecks, Int) Nice [Declaration]
    forall a b. (a -> b) -> a -> b
    $ [Declaration] -> Nice [Declaration]
    expandEllipsis [Declaration]
    fits
                  cs <- lift $ mkClauses n ds empty
                  case Map.lookup n m of
                    Just (InterleavedFun Int
    i0 NiceDeclaration
    sig Maybe (Int, List1 ([Declaration], [Clause]))
    cs0) -> do
                      let ((Int, List1 ([Declaration], [Clause]))
    cs', Int
    i') = case Maybe (Int, List1 ([Declaration], [Clause]))
    cs0 of
                            Maybe (Int, List1 ([Declaration], [Clause]))
    Nothing        -> ((Int
    i,  ([Declaration]
    fits,[Clause]
    cs) ([Declaration], [Clause])
    -> [([Declaration], [Clause])] -> List1 ([Declaration], [Clause])
    forall a. a -> [a] -> NonEmpty a
    :| [] ), Int
    i Int -> Int -> Int
    forall a. Num a => a -> a -> a
    + Int
    1)
                            Just (Int
    i1, List1 ([Declaration], [Clause])
    cs1) -> ((Int
    i1, ([Declaration]
    fits,[Clause]
    cs) ([Declaration], [Clause])
    -> List1 ([Declaration], [Clause])
    -> List1 ([Declaration], [Clause])
    forall a. a -> NonEmpty a -> NonEmpty a
    <| List1 ([Declaration], [Clause])
    cs1), Int
    i)
                      let checks' :: MutualChecks
    checks' = [MutualChecks] -> MutualChecks
    forall m. Monoid m => [m] -> m
    forall (t :: * -> *) m. (Foldable t, Monoid m) => t m -> m
    Fold.fold [MutualChecks]
    checkss
                      (InterleavedMutual, MutualChecks, Int)
    -> StateT (InterleavedMutual, MutualChecks, Int) Nice ()
    forall s (m :: * -> *). MonadState s m => s -> m ()
    put (Name -> InterleavedDecl -> InterleavedMutual -> InterleavedMutual
    forall k a. Ord k => k -> a -> Map k a -> Map k a
    Map.insert Name
    n (Int
    -> NiceDeclaration
    -> Maybe (Int, List1 ([Declaration], [Clause]))
    -> InterleavedDecl
    InterleavedFun Int
    i0 NiceDeclaration
    sig ((Int, List1 ([Declaration], [Clause]))
    -> Maybe (Int, List1 ([Declaration], [Clause]))
    forall a. a -> Maybe a
    Just (Int, List1 ([Declaration], [Clause]))
    cs')) InterleavedMutual
    m, MutualChecks
    checks' MutualChecks -> MutualChecks -> MutualChecks
    forall a. Semigroup a => a -> a -> a
    <> MutualChecks
    checks, Int
    i')
                    Maybe InterleavedDecl
    _ -> StateT (InterleavedMutual, MutualChecks, Int) Nice ()
    forall a. HasCallStack => a
    __IMPOSSIBLE__
                  groupByBlocks r rest
                -- more than one candidate: fail, complaining about the ambiguity!
                (Name, Prefix (MutualChecks, Declaration), [NiceDeclaration])
    xf:[(Name, Prefix (MutualChecks, Declaration), [NiceDeclaration])]
    xfs -> Nice [(Int, NiceDeclaration)]
    -> StateT
         (InterleavedMutual, MutualChecks, Int)
         Nice
         [(Int, NiceDeclaration)]
    forall (m :: * -> *) a.
    Monad m =>
    m a -> StateT (InterleavedMutual, MutualChecks, Int) m a
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (Nice [(Int, NiceDeclaration)]
     -> StateT
          (InterleavedMutual, MutualChecks, Int)
          Nice
          [(Int, NiceDeclaration)])
    -> Nice [(Int, NiceDeclaration)]
    -> StateT
         (InterleavedMutual, MutualChecks, Int)
         Nice
         [(Int, NiceDeclaration)]
    forall a b. (a -> b) -> a -> b
    $ DeclarationException' -> Nice [(Int, NiceDeclaration)]
    forall a. HasCallStack => DeclarationException' -> Nice a
    declarationException
                               (DeclarationException' -> Nice [(Int, NiceDeclaration)])
    -> DeclarationException' -> Nice [(Int, NiceDeclaration)]
    forall a b. (a -> b) -> a -> b
    $ LHS -> List1 Name -> DeclarationException'
    AmbiguousFunClauses LHS
    lhs
                               (List1 Name -> DeclarationException')
    -> List1 Name -> DeclarationException'
    forall a b. (a -> b) -> a -> b
    $ List1 Name -> List1 Name
    forall a. NonEmpty a -> NonEmpty a
    List1.reverse (List1 Name -> List1 Name) -> List1 Name -> List1 Name
    forall a b. (a -> b) -> a -> b
    $ ((Name, Prefix (MutualChecks, Declaration), [NiceDeclaration])
     -> Name)
    -> NonEmpty
         (Name, Prefix (MutualChecks, Declaration), [NiceDeclaration])
    -> List1 Name
    forall a b. (a -> b) -> NonEmpty a -> NonEmpty b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (\ (Name
    a,Prefix (MutualChecks, Declaration)
    _,[NiceDeclaration]
    _) -> Name
    a) (NonEmpty
       (Name, Prefix (MutualChecks, Declaration), [NiceDeclaration])
     -> List1 Name)
    -> NonEmpty
         (Name, Prefix (MutualChecks, Declaration), [NiceDeclaration])
    -> List1 Name
    forall a b. (a -> b) -> a -> b
    $ (Name, Prefix (MutualChecks, Declaration), [NiceDeclaration])
    xf (Name, Prefix (MutualChecks, Declaration), [NiceDeclaration])
    -> [(Name, Prefix (MutualChecks, Declaration), [NiceDeclaration])]
    -> NonEmpty
         (Name, Prefix (MutualChecks, Declaration), [NiceDeclaration])
    forall a. a -> [a] -> NonEmpty a
    :| [(Name, Prefix (MutualChecks, Declaration), [NiceDeclaration])]
    xfs
            addFunClauses KwRange
    _ [NiceDeclaration]
    _ = StateT
      (InterleavedMutual, MutualChecks, Int)
      Nice
      [(Int, NiceDeclaration)]
    forall a. HasCallStack => a
    __IMPOSSIBLE__

            groupByBlocks ::
                  KwRange
              -> [NiceDeclaration]
              -> StateT (InterleavedMutual, MutualChecks, DeclNum) Nice [(DeclNum, NiceDeclaration)]
            groupByBlocks :: KwRange
    -> [NiceDeclaration]
    -> StateT
         (InterleavedMutual, MutualChecks, Int)
         Nice
         [(Int, NiceDeclaration)]
    groupByBlocks KwRange
    kwr []       = [(Int, NiceDeclaration)]
    -> StateT
         (InterleavedMutual, MutualChecks, Int)
         Nice
         [(Int, NiceDeclaration)]
    forall a. a -> StateT (InterleavedMutual, MutualChecks, Int) Nice a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure []
            groupByBlocks KwRange
    kwr (NiceDeclaration
    d : [NiceDeclaration]
    ds) = do
              -- for most branches we deal with the one declaration and move on
              let oneOff :: StateT
      (InterleavedMutual, MutualChecks, Int)
      Nice
      [(Int, NiceDeclaration)]
    -> StateT
         (InterleavedMutual, MutualChecks, Int)
         Nice
         [(Int, NiceDeclaration)]
    oneOff StateT
      (InterleavedMutual, MutualChecks, Int)
      Nice
      [(Int, NiceDeclaration)]
    act = StateT
      (InterleavedMutual, MutualChecks, Int)
      Nice
      [(Int, NiceDeclaration)]
    act StateT
      (InterleavedMutual, MutualChecks, Int)
      Nice
      [(Int, NiceDeclaration)]
    -> ([(Int, NiceDeclaration)]
        -> StateT
             (InterleavedMutual, MutualChecks, Int)
             Nice
             [(Int, NiceDeclaration)])
    -> StateT
         (InterleavedMutual, MutualChecks, Int)
         Nice
         [(Int, NiceDeclaration)]
    forall a b.
    StateT (InterleavedMutual, MutualChecks, Int) Nice a
    -> (a -> StateT (InterleavedMutual, MutualChecks, Int) Nice b)
    -> StateT (InterleavedMutual, MutualChecks, Int) Nice b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \ [(Int, NiceDeclaration)]
    ns -> ([(Int, NiceDeclaration)]
    ns [(Int, NiceDeclaration)]
    -> [(Int, NiceDeclaration)] -> [(Int, NiceDeclaration)]
    forall a. [a] -> [a] -> [a]
    ++) ([(Int, NiceDeclaration)] -> [(Int, NiceDeclaration)])
    -> StateT
         (InterleavedMutual, MutualChecks, Int)
         Nice
         [(Int, NiceDeclaration)]
    -> StateT
         (InterleavedMutual, MutualChecks, Int)
         Nice
         [(Int, NiceDeclaration)]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> KwRange
    -> [NiceDeclaration]
    -> StateT
         (InterleavedMutual, MutualChecks, Int)
         Nice
         [(Int, NiceDeclaration)]
    groupByBlocks KwRange
    kwr [NiceDeclaration]
    ds
              case NiceDeclaration
    d of
                NiceDataSig{}                -> StateT
      (InterleavedMutual, MutualChecks, Int)
      Nice
      [(Int, NiceDeclaration)]
    -> StateT
         (InterleavedMutual, MutualChecks, Int)
         Nice
         [(Int, NiceDeclaration)]
    oneOff (StateT
       (InterleavedMutual, MutualChecks, Int)
       Nice
       [(Int, NiceDeclaration)]
     -> StateT
          (InterleavedMutual, MutualChecks, Int)
          Nice
          [(Int, NiceDeclaration)])
    -> StateT
         (InterleavedMutual, MutualChecks, Int)
         Nice
         [(Int, NiceDeclaration)]
    -> StateT
         (InterleavedMutual, MutualChecks, Int)
         Nice
         [(Int, NiceDeclaration)]
    forall a b. (a -> b) -> a -> b
    $ [] [(Int, NiceDeclaration)]
    -> StateT (InterleavedMutual, MutualChecks, Int) Nice ()
    -> StateT
         (InterleavedMutual, MutualChecks, Int)
         Nice
         [(Int, NiceDeclaration)]
    forall a b.
    a
    -> StateT (InterleavedMutual, MutualChecks, Int) Nice b
    -> StateT (InterleavedMutual, MutualChecks, Int) Nice a
    forall (f :: * -> *) a b. Functor f => a -> f b -> f a
    <$ NiceDeclaration
    -> StateT (InterleavedMutual, MutualChecks, Int) Nice ()
    addDataType NiceDeclaration
    d
                NiceDataDef Range
    r Origin
    _ IsAbstract
    _ PositivityCheck
    _ UniverseCheck
    _ Name
    n [LamBinding]
    _ [NiceDeclaration]
    ds -> StateT
      (InterleavedMutual, MutualChecks, Int)
      Nice
      [(Int, NiceDeclaration)]
    -> StateT
         (InterleavedMutual, MutualChecks, Int)
         Nice
         [(Int, NiceDeclaration)]
    oneOff (StateT
       (InterleavedMutual, MutualChecks, Int)
       Nice
       [(Int, NiceDeclaration)]
     -> StateT
          (InterleavedMutual, MutualChecks, Int)
          Nice
          [(Int, NiceDeclaration)])
    -> StateT
         (InterleavedMutual, MutualChecks, Int)
         Nice
         [(Int, NiceDeclaration)]
    -> StateT
         (InterleavedMutual, MutualChecks, Int)
         Nice
         [(Int, NiceDeclaration)]
    forall a b. (a -> b) -> a -> b
    $ [] [(Int, NiceDeclaration)]
    -> StateT (InterleavedMutual, MutualChecks, Int) Nice ()
    -> StateT
         (InterleavedMutual, MutualChecks, Int)
         Nice
         [(Int, NiceDeclaration)]
    forall a b.
    a
    -> StateT (InterleavedMutual, MutualChecks, Int) Nice b
    -> StateT (InterleavedMutual, MutualChecks, Int) Nice a
    forall (f :: * -> *) a b. Functor f => a -> f b -> f a
    <$ Maybe Range
    -> Maybe Name
    -> [NiceDeclaration]
    -> StateT (InterleavedMutual, MutualChecks, Int) Nice ()
    addDataConstructors (Range -> Maybe Range
    forall a. a -> Maybe a
    Just Range
    r) (Name -> Maybe Name
    forall a. a -> Maybe a
    Just Name
    n) [NiceDeclaration]
    ds
                NiceLoneConstructor KwRange
    _ [NiceDeclaration]
    ds     -> StateT
      (InterleavedMutual, MutualChecks, Int)
      Nice
      [(Int, NiceDeclaration)]
    -> StateT
         (InterleavedMutual, MutualChecks, Int)
         Nice
         [(Int, NiceDeclaration)]
    oneOff (StateT
       (InterleavedMutual, MutualChecks, Int)
       Nice
       [(Int, NiceDeclaration)]
     -> StateT
          (InterleavedMutual, MutualChecks, Int)
          Nice
          [(Int, NiceDeclaration)])
    -> StateT
         (InterleavedMutual, MutualChecks, Int)
         Nice
         [(Int, NiceDeclaration)]
    -> StateT
         (InterleavedMutual, MutualChecks, Int)
         Nice
         [(Int, NiceDeclaration)]
    forall a b. (a -> b) -> a -> b
    $ [] [(Int, NiceDeclaration)]
    -> StateT (InterleavedMutual, MutualChecks, Int) Nice ()
    -> StateT
         (InterleavedMutual, MutualChecks, Int)
         Nice
         [(Int, NiceDeclaration)]
    forall a b.
    a
    -> StateT (InterleavedMutual, MutualChecks, Int) Nice b
    -> StateT (InterleavedMutual, MutualChecks, Int) Nice a
    forall (f :: * -> *) a b. Functor f => a -> f b -> f a
    <$ Maybe Range
    -> Maybe Name
    -> [NiceDeclaration]
    -> StateT (InterleavedMutual, MutualChecks, Int) Nice ()
    addDataConstructors Maybe Range
    forall a. Maybe a
    Nothing Maybe Name
    forall a. Maybe a
    Nothing [NiceDeclaration]
    ds
                FunSig{}                     -> StateT
      (InterleavedMutual, MutualChecks, Int)
      Nice
      [(Int, NiceDeclaration)]
    -> StateT
         (InterleavedMutual, MutualChecks, Int)
         Nice
         [(Int, NiceDeclaration)]
    oneOff (StateT
       (InterleavedMutual, MutualChecks, Int)
       Nice
       [(Int, NiceDeclaration)]
     -> StateT
          (InterleavedMutual, MutualChecks, Int)
          Nice
          [(Int, NiceDeclaration)])
    -> StateT
         (InterleavedMutual, MutualChecks, Int)
         Nice
         [(Int, NiceDeclaration)]
    -> StateT
         (InterleavedMutual, MutualChecks, Int)
         Nice
         [(Int, NiceDeclaration)]
    forall a b. (a -> b) -> a -> b
    $ [] [(Int, NiceDeclaration)]
    -> StateT (InterleavedMutual, MutualChecks, Int) Nice ()
    -> StateT
         (InterleavedMutual, MutualChecks, Int)
         Nice
         [(Int, NiceDeclaration)]
    forall a b.
    a
    -> StateT (InterleavedMutual, MutualChecks, Int) Nice b
    -> StateT (InterleavedMutual, MutualChecks, Int) Nice a
    forall (f :: * -> *) a b. Functor f => a -> f b -> f a
    <$ NiceDeclaration
    -> StateT (InterleavedMutual, MutualChecks, Int) Nice ()
    addFunType NiceDeclaration
    d
                FunDef Range
    _ [Declaration]
    _ IsAbstract
    _  IsInstance
    _ TerminationCheck
    _ CoverageCheck
    _ Name
    n [Clause]
    cs
                          | Bool -> Bool
    not (Name -> Bool
    forall a. IsNoName a => a -> Bool
    isNoName Name
    n) -> StateT
      (InterleavedMutual, MutualChecks, Int)
      Nice
      [(Int, NiceDeclaration)]
    -> StateT
         (InterleavedMutual, MutualChecks, Int)
         Nice
         [(Int, NiceDeclaration)]
    oneOff (StateT
       (InterleavedMutual, MutualChecks, Int)
       Nice
       [(Int, NiceDeclaration)]
     -> StateT
          (InterleavedMutual, MutualChecks, Int)
          Nice
          [(Int, NiceDeclaration)])
    -> StateT
         (InterleavedMutual, MutualChecks, Int)
         Nice
         [(Int, NiceDeclaration)]
    -> StateT
         (InterleavedMutual, MutualChecks, Int)
         Nice
         [(Int, NiceDeclaration)]
    forall a b. (a -> b) -> a -> b
    $ [] [(Int, NiceDeclaration)]
    -> StateT (InterleavedMutual, MutualChecks, Int) Nice ()
    -> StateT
         (InterleavedMutual, MutualChecks, Int)
         Nice
         [(Int, NiceDeclaration)]
    forall a b.
    a
    -> StateT (InterleavedMutual, MutualChecks, Int) Nice b
    -> StateT (InterleavedMutual, MutualChecks, Int) Nice a
    forall (f :: * -> *) a b. Functor f => a -> f b -> f a
    <$ NiceDeclaration
    -> StateT (InterleavedMutual, MutualChecks, Int) Nice ()
    addFunDef NiceDeclaration
    d
                -- It's a bit different for fun clauses because we may need to grab a lot
                -- of clauses to handle ellipses properly.
                NiceFunClause{}              -> KwRange
    -> [NiceDeclaration]
    -> StateT
         (InterleavedMutual, MutualChecks, Int)
         Nice
         [(Int, NiceDeclaration)]
    addFunClauses KwRange
    kwr (NiceDeclaration
    dNiceDeclaration -> [NiceDeclaration] -> [NiceDeclaration]
    forall a. a -> [a] -> [a]
    :[NiceDeclaration]
    ds)
                -- We do not need to worry about RecSig vs. RecDef: we know there's exactly one
                -- of each for record definitions and leaving them in place should be enough!
                NiceDeclaration
    _ -> StateT
      (InterleavedMutual, MutualChecks, Int)
      Nice
      [(Int, NiceDeclaration)]
    -> StateT
         (InterleavedMutual, MutualChecks, Int)
         Nice
         [(Int, NiceDeclaration)]
    oneOff (StateT
       (InterleavedMutual, MutualChecks, Int)
       Nice
       [(Int, NiceDeclaration)]
     -> StateT
          (InterleavedMutual, MutualChecks, Int)
          Nice
          [(Int, NiceDeclaration)])
    -> StateT
         (InterleavedMutual, MutualChecks, Int)
         Nice
         [(Int, NiceDeclaration)]
    -> StateT
         (InterleavedMutual, MutualChecks, Int)
         Nice
         [(Int, NiceDeclaration)]
    forall a b. (a -> b) -> a -> b
    $ do
                  (m, c, i) <- StateT
      (InterleavedMutual, MutualChecks, Int)
      Nice
      (InterleavedMutual, MutualChecks, Int)
    forall s (m :: * -> *). MonadState s m => m s
    get -- TODO: grab checks from c?
                  put (m, c, i + 1)
                  pure [(i,d)]

        -- Extract the name of the return type (if any) of a potential constructor.
        -- In case of failure return the name of the constructor and the list of candidates
        -- for the return type.
        -- A `constructor' block should only contain NiceConstructors so we crash with
        -- an IMPOSSIBLE otherwise
        isConstructor :: [Name] -> NiceDeclaration -> Either (Name, [Name]) Name
        isConstructor :: [Name] -> NiceDeclaration -> Either (Name, [Name]) Name
    isConstructor [Name]
    ns (Axiom Range
    _ Access
    _ IsAbstract
    _ IsInstance
    _ ArgInfo
    _ Name
    n Expr
    e)
           -- extract the return type & see it as an LHS-style pattern
           | Just Pattern
    p <- Expr -> Pattern
    exprToPatternWithHoles (Expr -> Pattern) -> Maybe Expr -> Maybe Pattern
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Expr -> Maybe Expr
    returnExpr Expr
    e =
             case [ Name
    x | Name
    x <- [Name]
    ns
                      , Maybe Fixity' -> Name -> Pattern -> Bool
    couldBeCallOf (Name -> Fixities -> Maybe Fixity'
    forall k a. Ord k => k -> Map k a -> Maybe a
    Map.lookup Name
    x Fixities
    fixs) Name
    x Pattern
    p
                      ] of
               [Name
    x] -> Name -> Either (Name, [Name]) Name
    forall a b. b -> Either a b
    Right Name
    x
               [Name]
    xs  -> (Name, [Name]) -> Either (Name, [Name]) Name
    forall a b. a -> Either a b
    Left (Name
    n, [Name]
    xs)
           -- which may fail (e.g. if the "return type" is a hole
           | Bool
    otherwise = (Name, [Name]) -> Either (Name, [Name]) Name
    forall a b. a -> Either a b
    Left (Name
    n, [])
        isConstructor [Name]
    _ NiceDeclaration
    _ = Either (Name, [Name]) Name
    forall a. HasCallStack => a
    __IMPOSSIBLE__

        -- Turn an old-style mutual block into a new style mutual block
        -- by pushing the definitions to the end.
        mkOldMutual
          :: KwRange               -- Range of the @mutual@ keyword (if any).
          -> [NiceDeclaration]     -- Declarations inside the block.
          -> Nice NiceDeclaration  -- Returns a 'NiceMutual'.
        mkOldMutual :: KwRange -> [NiceDeclaration] -> Nice NiceDeclaration
    mkOldMutual KwRange
    kwr [NiceDeclaration]
    ds' = do
            -- Postulate the missing definitions
            let ps :: LoneSigs
    ps = [(Range, Name, DataRecOrFun)] -> LoneSigs
    loneSigsFromLoneNames [(Range, Name, DataRecOrFun)]
    loneNames
            LoneSigs -> Nice ()
    checkLoneSigs LoneSigs
    ps
            let ds :: [NiceDeclaration]
    ds = LoneSigs -> [NiceDeclaration] -> [NiceDeclaration]
    replaceSigs LoneSigs
    ps [NiceDeclaration]
    ds'

            -- -- Remove the declarations that aren't allowed in old style mutual blocks
            -- ds <- fmap catMaybes $ forM ds $ \ d -> let success = pure (Just d) in case d of
            --   -- Andreas, 2013-11-23 allow postulates in mutual blocks
            --   Axiom{}          -> success
            --   -- Andreas, 2017-10-09, issue #2576, raise error about missing type signature
            --   -- in ConcreteToAbstract rather than here.
            --   NiceFunClause{}  -> success
            --   -- Andreas, 2018-05-11, issue #3052, allow pat.syn.s in mutual blocks
            --   NicePatternSyn{} -> success
            --   -- Otherwise, only categorized signatures and definitions are allowed:
            --   -- Data, Record, Fun
            --   _ -> if (declKind d /= OtherDecl) then success
            --        else Nothing <$ declarationWarning (NotAllowedInMutual (getRange d) $ declName d)
            -- Sort the declarations in the mutual block.
            -- Declarations of names go to the top.  (Includes module definitions.)
            -- Definitions of names go to the bottom.
            -- Some declarations are forbidden, as their positioning could confuse
            -- the user.
            (top, bottom, invalid) <- [NiceDeclaration]
    -> (NiceDeclaration
        -> Nice (Either3 NiceDeclaration NiceDeclaration NiceDeclaration))
    -> Nice ([NiceDeclaration], [NiceDeclaration], [NiceDeclaration])
    forall (m :: * -> *) a b c d.
    Applicative m =>
    [a] -> (a -> m (Either3 b c d)) -> m ([b], [c], [d])
    forEither3M [NiceDeclaration]
    ds ((NiceDeclaration
      -> Nice (Either3 NiceDeclaration NiceDeclaration NiceDeclaration))
     -> Nice ([NiceDeclaration], [NiceDeclaration], [NiceDeclaration]))
    -> (NiceDeclaration
        -> Nice (Either3 NiceDeclaration NiceDeclaration NiceDeclaration))
    -> Nice ([NiceDeclaration], [NiceDeclaration], [NiceDeclaration])
    forall a b. (a -> b) -> a -> b
    $ \ NiceDeclaration
    d -> do
              let top :: Nice (Either3 NiceDeclaration NiceDeclaration NiceDeclaration)
    top       = Either3 NiceDeclaration NiceDeclaration NiceDeclaration
    -> Nice (Either3 NiceDeclaration NiceDeclaration NiceDeclaration)
    forall a. a -> Nice a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (NiceDeclaration
    -> Either3 NiceDeclaration NiceDeclaration NiceDeclaration
    forall a b c. a -> Either3 a b c
    In1 NiceDeclaration
    d)
                  bottom :: Nice (Either3 NiceDeclaration NiceDeclaration NiceDeclaration)
    bottom    = Either3 NiceDeclaration NiceDeclaration NiceDeclaration
    -> Nice (Either3 NiceDeclaration NiceDeclaration NiceDeclaration)
    forall a. a -> Nice a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (NiceDeclaration
    -> Either3 NiceDeclaration NiceDeclaration NiceDeclaration
    forall a b c. b -> Either3 a b c
    In2 NiceDeclaration
    d)
                  invalid :: String
    -> Nice (Either3 NiceDeclaration NiceDeclaration NiceDeclaration)
    invalid String
    s = NiceDeclaration
    -> Either3 NiceDeclaration NiceDeclaration NiceDeclaration
    forall a b c. c -> Either3 a b c
    In3 NiceDeclaration
    d Either3 NiceDeclaration NiceDeclaration NiceDeclaration
    -> Nice ()
    -> Nice (Either3 NiceDeclaration NiceDeclaration NiceDeclaration)
    forall a b. a -> Nice b -> Nice a
    forall (f :: * -> *) a b. Functor f => a -> f b -> f a
    <$ do HasCallStack => DeclarationWarning' -> Nice ()
    DeclarationWarning' -> Nice ()
    declarationWarning (DeclarationWarning' -> Nice ()) -> DeclarationWarning' -> Nice ()
    forall a b. (a -> b) -> a -> b
    $ Range -> String -> DeclarationWarning'
    NotAllowedInMutual (NiceDeclaration -> Range
    forall a. HasRange a => a -> Range
    getRange NiceDeclaration
    d) String
    s
              case NiceDeclaration
    d of
                -- Andreas, 2013-11-23 allow postulates in mutual blocks
                Axiom{}             -> Nice (Either3 NiceDeclaration NiceDeclaration NiceDeclaration)
    top
                NiceField{}         -> Nice (Either3 NiceDeclaration NiceDeclaration NiceDeclaration)
    top
                PrimitiveFunction{} -> Nice (Either3 NiceDeclaration NiceDeclaration NiceDeclaration)
    top
                -- Andreas, 2019-07-23 issue #3932:
                -- Nested mutual blocks are not supported.
                NiceMutual{}        -> String
    -> Nice (Either3 NiceDeclaration NiceDeclaration NiceDeclaration)
    invalid String
    "mutual blocks"
                -- Andreas, 2018-10-29, issue #3246
                -- We could allow modules (top), but this is potentially confusing.
                NiceModule{}        -> String
    -> Nice (Either3 NiceDeclaration NiceDeclaration NiceDeclaration)
    invalid String
    "Module definitions"
                -- Lone constructors are only allowed in new-style mutual blocks
                NiceLoneConstructor{} -> String
    -> Nice (Either3 NiceDeclaration NiceDeclaration NiceDeclaration)
    invalid String
    "Lone constructors"
                NiceModuleMacro{}   -> Nice (Either3 NiceDeclaration NiceDeclaration NiceDeclaration)
    top
                NiceOpen{}          -> Nice (Either3 NiceDeclaration NiceDeclaration NiceDeclaration)
    top
                NiceImport{}        -> Nice (Either3 NiceDeclaration NiceDeclaration NiceDeclaration)
    top
                NiceRecSig{}        -> Nice (Either3 NiceDeclaration NiceDeclaration NiceDeclaration)
    top
                NiceDataSig{}       -> Nice (Either3 NiceDeclaration NiceDeclaration NiceDeclaration)
    top
                -- Andreas, 2017-10-09, issue #2576, raise error about missing type signature
                -- in ConcreteToAbstract rather than here.
                NiceFunClause{}     -> Nice (Either3 NiceDeclaration NiceDeclaration NiceDeclaration)
    bottom
                FunSig{}            -> Nice (Either3 NiceDeclaration NiceDeclaration NiceDeclaration)
    top
                FunDef{}            -> Nice (Either3 NiceDeclaration NiceDeclaration NiceDeclaration)
    bottom
                NiceDataDef{}       -> Nice (Either3 NiceDeclaration NiceDeclaration NiceDeclaration)
    bottom
                NiceRecDef{}        -> Nice (Either3 NiceDeclaration NiceDeclaration NiceDeclaration)
    bottom
                -- Andreas, 2018-05-11, issue #3051, allow pat.syn.s in mutual blocks
                -- Andreas, 2018-10-29: We shift pattern synonyms to the bottom
                -- since they might refer to constructors defined in a data types
                -- just above them.
                NicePatternSyn{}    -> Nice (Either3 NiceDeclaration NiceDeclaration NiceDeclaration)
    bottom
                NiceGeneralize{}    -> Nice (Either3 NiceDeclaration NiceDeclaration NiceDeclaration)
    top
                NiceUnquoteDecl{}   -> Nice (Either3 NiceDeclaration NiceDeclaration NiceDeclaration)
    top
                NiceUnquoteDef{}    -> Nice (Either3 NiceDeclaration NiceDeclaration NiceDeclaration)
    bottom
                NiceUnquoteData{}   -> Nice (Either3 NiceDeclaration NiceDeclaration NiceDeclaration)
    top

                -- Opaque blocks can not participate in old-style mutual
                -- recursion. If some of the definitions are opaque then
                -- they all need to be.
                NiceOpaque KwRange
    r [QName]
    _ [NiceDeclaration]
    _    ->
                  NiceDeclaration
    -> Either3 NiceDeclaration NiceDeclaration NiceDeclaration
    forall a b c. c -> Either3 a b c
    In3 NiceDeclaration
    d Either3 NiceDeclaration NiceDeclaration NiceDeclaration
    -> Nice (ZonkAny 0)
    -> Nice (Either3 NiceDeclaration NiceDeclaration NiceDeclaration)
    forall a b. a -> Nice b -> Nice a
    forall (f :: * -> *) a b. Functor f => a -> f b -> f a
    <$ do DeclarationException' -> Nice (ZonkAny 0)
    forall a. HasCallStack => DeclarationException' -> Nice a
    declarationException (DeclarationException' -> Nice (ZonkAny 0))
    -> DeclarationException' -> Nice (ZonkAny 0)
    forall a b. (a -> b) -> a -> b
    $ KwRange -> DeclarationException'
    OpaqueInMutual KwRange
    r
                NicePragma Range
    r Pragma
    pragma -> case Pragma
    pragma of

                  OptionsPragma{}           -> Nice (Either3 NiceDeclaration NiceDeclaration NiceDeclaration)
    top     -- error thrown in the type checker

                  -- Some builtins require a definition, and they affect type checking
                  -- Thus, we do not handle BUILTINs in mutual blocks (at least for now).
                  BuiltinPragma{}           -> String
    -> Nice (Either3 NiceDeclaration NiceDeclaration NiceDeclaration)
    invalid String
    "BUILTIN pragmas"

                  -- The REWRITE pragma behaves differently before or after the def.
                  -- and affects type checking.  Thus, we refuse it here.
                  RewritePragma{}           -> String
    -> Nice (Either3 NiceDeclaration NiceDeclaration NiceDeclaration)
    invalid String
    "REWRITE pragmas"

                  -- Compiler pragmas are not needed for type checking, thus,
                  -- can go to the bottom.
                  ForeignPragma{}           -> Nice (Either3 NiceDeclaration NiceDeclaration NiceDeclaration)
    bottom
                  CompilePragma{}           -> Nice (Either3 NiceDeclaration NiceDeclaration NiceDeclaration)
    bottom

                  StaticPragma{}            -> Nice (Either3 NiceDeclaration NiceDeclaration NiceDeclaration)
    bottom
                  InlinePragma{}            -> Nice (Either3 NiceDeclaration NiceDeclaration NiceDeclaration)
    bottom
                  NotProjectionLikePragma{} -> Nice (Either3 NiceDeclaration NiceDeclaration NiceDeclaration)
    bottom

                  OverlapPragma{}           -> Nice (Either3 NiceDeclaration NiceDeclaration NiceDeclaration)
    top

                  ImpossiblePragma{}        -> Nice (Either3 NiceDeclaration NiceDeclaration NiceDeclaration)
    top     -- error thrown in scope checker
                  EtaPragma{}               -> Nice (Either3 NiceDeclaration NiceDeclaration NiceDeclaration)
    bottom  -- needs record definition
                  WarningOnUsage{}          -> Nice (Either3 NiceDeclaration NiceDeclaration NiceDeclaration)
    top
                  WarningOnImport{}         -> Nice (Either3 NiceDeclaration NiceDeclaration NiceDeclaration)
    top
                  InjectivePragma{}         -> Nice (Either3 NiceDeclaration NiceDeclaration NiceDeclaration)
    top     -- only needs name, not definition
                  InjectiveForInferencePragma{} -> Nice (Either3 NiceDeclaration NiceDeclaration NiceDeclaration)
    top
                  DisplayPragma{}           -> Nice (Either3 NiceDeclaration NiceDeclaration NiceDeclaration)
    top     -- only for printing

                  -- The attached pragmas have already been handled at this point.
                  CatchallPragma{}          -> Nice (Either3 NiceDeclaration NiceDeclaration NiceDeclaration)
    forall a. HasCallStack => a
    __IMPOSSIBLE__
                  TerminationCheckPragma{}  -> Nice (Either3 NiceDeclaration NiceDeclaration NiceDeclaration)
    forall a. HasCallStack => a
    __IMPOSSIBLE__
                  NoPositivityCheckPragma{} -> Nice (Either3 NiceDeclaration NiceDeclaration NiceDeclaration)
    forall a. HasCallStack => a
    __IMPOSSIBLE__
                  PolarityPragma{}          -> Nice (Either3 NiceDeclaration NiceDeclaration NiceDeclaration)
    forall a. HasCallStack => a
    __IMPOSSIBLE__
                  NoUniverseCheckPragma{}   -> Nice (Either3 NiceDeclaration NiceDeclaration NiceDeclaration)
    forall a. HasCallStack => a
    __IMPOSSIBLE__
                  NoCoverageCheckPragma{}   -> Nice (Either3 NiceDeclaration NiceDeclaration NiceDeclaration)
    forall a. HasCallStack => a
    __IMPOSSIBLE__

            -- -- Pull type signatures to the top
            -- let (sigs, other) = List.partition isTypeSig ds

            -- -- Push definitions to the bottom
            -- let (other, defs) = flip List.partition ds $ \case
            --       FunDef{}         -> False
            --       NiceDataDef{}    -> False
            --       NiceRecDef{}         -> False
            --       NiceFunClause{}  -> False
            --       NicePatternSyn{} -> False
            --       NiceUnquoteDef{} -> False
            --       _ -> True

            -- Compute termination checking flag for mutual block
            tc0 <- use terminationCheckPragma
            let tcs = (NiceDeclaration -> TerminationCheck)
    -> [NiceDeclaration] -> [TerminationCheck]
    forall a b. (a -> b) -> [a] -> [b]
    map NiceDeclaration -> TerminationCheck
    termCheck [NiceDeclaration]
    ds
            let r   = KwRange -> [NiceDeclaration] -> Range
    forall u t. (HasRange u, HasRange t) => u -> t -> Range
    fuseRange KwRange
    kwr [NiceDeclaration]
    ds'
            tc <- combineTerminationChecks r (tc0:tcs)

            -- Compute coverage checking flag for mutual block
            cc0 <- use coverageCheckPragma
            let ccs = (NiceDeclaration -> CoverageCheck)
    -> [NiceDeclaration] -> [CoverageCheck]
    forall a b. (a -> b) -> [a] -> [b]
    map NiceDeclaration -> CoverageCheck
    covCheck [NiceDeclaration]
    ds
            let cc = [CoverageCheck] -> CoverageCheck
    combineCoverageChecks (CoverageCheck
    cc0CoverageCheck -> [CoverageCheck] -> [CoverageCheck]
    forall a. a -> [a] -> [a]
    :[CoverageCheck]
    ccs)

            -- Compute positivity checking flag for mutual block
            pc0 <- use positivityCheckPragma
            let pcs = (NiceDeclaration -> PositivityCheck)
    -> [NiceDeclaration] -> [PositivityCheck]
    forall a b. (a -> b) -> [a] -> [b]
    map NiceDeclaration -> PositivityCheck
    positivityCheckOldMutual [NiceDeclaration]
    ds
            let pc = [PositivityCheck] -> PositivityCheck
    combinePositivityChecks (PositivityCheck
    pc0PositivityCheck -> [PositivityCheck] -> [PositivityCheck]
    forall a. a -> [a] -> [a]
    :[PositivityCheck]
    pcs)

            return $ NiceMutual kwr tc cc pc $ top ++ bottom

          where
            sigNames :: [(Range, Name, DataRecOrFun)]
    sigNames  = [ (Range
    r, Name
    x, DataRecOrFun
    k) | LoneSigDecl Range
    r DataRecOrFun
    k Name
    x <- (NiceDeclaration -> DeclKind) -> [NiceDeclaration] -> [DeclKind]
    forall a b. (a -> b) -> [a] -> [b]
    map NiceDeclaration -> DeclKind
    declKind [NiceDeclaration]
    ds' ]
            defNames :: [(Name, DataRecOrFun)]
    defNames  = [ (Name
    x, DataRecOrFun
    k) | LoneDefs DataRecOrFun
    k [Name]
    xs <- (NiceDeclaration -> DeclKind) -> [NiceDeclaration] -> [DeclKind]
    forall a b. (a -> b) -> [a] -> [b]
    map NiceDeclaration -> DeclKind
    declKind [NiceDeclaration]
    ds', Name
    x <- [Name]
    xs ]
            -- compute the set difference with equality just on names
            loneNames :: [(Range, Name, DataRecOrFun)]
    loneNames = [ (Range
    r, Name
    x, DataRecOrFun
    k) | (Range
    r, Name
    x, DataRecOrFun
    k) <- [(Range, Name, DataRecOrFun)]
    sigNames, ((Name, DataRecOrFun) -> Bool) -> [(Name, DataRecOrFun)] -> Bool
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
    List.all ((Name
    x Name -> Name -> Bool
    forall a. Eq a => a -> a -> Bool
    /=) (Name -> Bool)
    -> ((Name, DataRecOrFun) -> Name) -> (Name, DataRecOrFun) -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Name, DataRecOrFun) -> Name
    forall a b. (a, b) -> a
    fst) [(Name, DataRecOrFun)]
    defNames ]

            termCheck :: NiceDeclaration -> TerminationCheck
            -- Andreas, 2013-02-28 (issue 804):
            -- do not termination check a mutual block if any of its
            -- inner declarations comes with a {-# NO_TERMINATION_CHECK #-}
            termCheck :: NiceDeclaration -> TerminationCheck
    termCheck (FunSig Range
    _ Access
    _ IsAbstract
    _ IsInstance
    _ IsMacro
    _ ArgInfo
    _ TerminationCheck
    tc CoverageCheck
    _ Name
    _ Expr
    _)      = TerminationCheck
    tc
            termCheck (FunDef Range
    _ [Declaration]
    _ IsAbstract
    _ IsInstance
    _ TerminationCheck
    tc CoverageCheck
    _ Name
    _ [Clause]
    _)          = TerminationCheck
    tc
            -- ASR (28 December 2015): Is this equation necessary?
            termCheck (NiceMutual KwRange
    _ TerminationCheck
    tc CoverageCheck
    _ PositivityCheck
    _ [NiceDeclaration]
    _)            = TerminationCheck
    tc
            termCheck (NiceUnquoteDecl Range
    _ Access
    _ IsAbstract
    _ IsInstance
    _ TerminationCheck
    tc CoverageCheck
    _ [Name]
    _ Expr
    _) = TerminationCheck
    tc
            termCheck (NiceUnquoteDef Range
    _ Access
    _ IsAbstract
    _ TerminationCheck
    tc CoverageCheck
    _ [Name]
    _ Expr
    _)    = TerminationCheck
    tc
            termCheck Axiom{}               = TerminationCheck
    forall m. TerminationCheck m
    TerminationCheck
            termCheck NiceField{}           = TerminationCheck
    forall m. TerminationCheck m
    TerminationCheck
            termCheck PrimitiveFunction{}   = TerminationCheck
    forall m. TerminationCheck m
    TerminationCheck
            termCheck NiceModule{}          = TerminationCheck
    forall m. TerminationCheck m
    TerminationCheck
            termCheck NiceModuleMacro{}     = TerminationCheck
    forall m. TerminationCheck m
    TerminationCheck
            termCheck NiceOpen{}            = TerminationCheck
    forall m. TerminationCheck m
    TerminationCheck
            termCheck NiceImport{}          = TerminationCheck
    forall m. TerminationCheck m
    TerminationCheck
            termCheck NicePragma{}          = TerminationCheck
    forall m. TerminationCheck m
    TerminationCheck
            termCheck NiceRecSig{}          = TerminationCheck
    forall m. TerminationCheck m
    TerminationCheck
            termCheck NiceDataSig{}         = TerminationCheck
    forall m. TerminationCheck m
    TerminationCheck
            termCheck NiceFunClause{}       = TerminationCheck
    forall m. TerminationCheck m
    TerminationCheck
            termCheck NiceDataDef{}         = TerminationCheck
    forall m. TerminationCheck m
    TerminationCheck
            termCheck NiceRecDef{}          = TerminationCheck
    forall m. TerminationCheck m
    TerminationCheck
            termCheck NicePatternSyn{}      = TerminationCheck
    forall m. TerminationCheck m
    TerminationCheck
            termCheck NiceGeneralize{}      = TerminationCheck
    forall m. TerminationCheck m
    TerminationCheck
            termCheck NiceLoneConstructor{} = TerminationCheck
    forall m. TerminationCheck m
    TerminationCheck
            termCheck NiceUnquoteData{}     = TerminationCheck
    forall m. TerminationCheck m
    TerminationCheck
            termCheck NiceOpaque{}          = TerminationCheck
    forall m. TerminationCheck m
    TerminationCheck

            covCheck :: NiceDeclaration -> CoverageCheck
            covCheck :: NiceDeclaration -> CoverageCheck
    covCheck (FunSig Range
    _ Access
    _ IsAbstract
    _ IsInstance
    _ IsMacro
    _ ArgInfo
    _ TerminationCheck
    _ CoverageCheck
    cc Name
    _ Expr
    _)      = CoverageCheck
    cc
            covCheck (FunDef Range
    _ [Declaration]
    _ IsAbstract
    _ IsInstance
    _ TerminationCheck
    _ CoverageCheck
    cc Name
    _ [Clause]
    _)          = CoverageCheck
    cc
            -- ASR (28 December 2015): Is this equation necessary?
            covCheck (NiceMutual KwRange
    _ TerminationCheck
    _ CoverageCheck
    cc PositivityCheck
    _ [NiceDeclaration]
    _)            = CoverageCheck
    cc
            covCheck (NiceUnquoteDecl Range
    _ Access
    _ IsAbstract
    _ IsInstance
    _ TerminationCheck
    _ CoverageCheck
    cc [Name]
    _ Expr
    _) = CoverageCheck
    cc
            covCheck (NiceUnquoteDef Range
    _ Access
    _ IsAbstract
    _ TerminationCheck
    _ CoverageCheck
    cc [Name]
    _ Expr
    _)    = CoverageCheck
    cc
            covCheck Axiom{}               = CoverageCheck
    YesCoverageCheck
            covCheck NiceField{}           = CoverageCheck
    YesCoverageCheck
            covCheck PrimitiveFunction{}   = CoverageCheck
    YesCoverageCheck
            covCheck NiceModule{}          = CoverageCheck
    YesCoverageCheck
            covCheck NiceModuleMacro{}     = CoverageCheck
    YesCoverageCheck
            covCheck NiceOpen{}            = CoverageCheck
    YesCoverageCheck
            covCheck NiceImport{}          = CoverageCheck
    YesCoverageCheck
            covCheck NicePragma{}          = CoverageCheck
    YesCoverageCheck
            covCheck NiceRecSig{}          = CoverageCheck
    YesCoverageCheck
            covCheck NiceDataSig{}         = CoverageCheck
    YesCoverageCheck
            covCheck NiceFunClause{}       = CoverageCheck
    YesCoverageCheck
            covCheck NiceDataDef{}         = CoverageCheck
    YesCoverageCheck
            covCheck NiceRecDef{}          = CoverageCheck
    YesCoverageCheck
            covCheck NicePatternSyn{}      = CoverageCheck
    YesCoverageCheck
            covCheck NiceGeneralize{}      = CoverageCheck
    YesCoverageCheck
            covCheck NiceLoneConstructor{} = CoverageCheck
    YesCoverageCheck
            covCheck NiceUnquoteData{}     = CoverageCheck
    YesCoverageCheck
            covCheck NiceOpaque{}          = CoverageCheck
    YesCoverageCheck

            -- ASR (26 December 2015): Do not positivity check a mutual
            -- block if any of its inner declarations comes with a
            -- NO_POSITIVITY_CHECK pragma. See Issue 1614.
            positivityCheckOldMutual :: NiceDeclaration -> PositivityCheck
            positivityCheckOldMutual :: NiceDeclaration -> PositivityCheck
    positivityCheckOldMutual (NiceDataDef Range
    _ Origin
    _ IsAbstract
    _ PositivityCheck
    pc UniverseCheck
    _ Name
    _ [LamBinding]
    _ [NiceDeclaration]
    _) = PositivityCheck
    pc
            positivityCheckOldMutual (NiceDataSig Range
    _ Erased
    _ Access
    _ IsAbstract
    _ PositivityCheck
    pc UniverseCheck
    _ Name
    _ [LamBinding]
    _ Expr
    _) = PositivityCheck
    pc
            positivityCheckOldMutual (NiceMutual KwRange
    _ TerminationCheck
    _ CoverageCheck
    _ PositivityCheck
    pc [NiceDeclaration]
    _)        = PositivityCheck
    pc
            positivityCheckOldMutual (NiceRecSig Range
    _ Erased
    _ Access
    _ IsAbstract
    _ PositivityCheck
    pc UniverseCheck
    _ Name
    _ [LamBinding]
    _ Expr
    _) = PositivityCheck
    pc
            positivityCheckOldMutual (NiceRecDef Range
    _ Origin
    _ IsAbstract
    _ PositivityCheck
    pc UniverseCheck
    _ Name
    _ [RecordDirective]
    _ [LamBinding]
    _ [Declaration]
    _) = PositivityCheck
    pc
            positivityCheckOldMutual NiceDeclaration
    _                              = PositivityCheck
    YesPositivityCheck

            -- A mutual block cannot have a measure,
            -- but it can skip termination check.

        abstractBlock
          :: KwRange  -- Range of @abstract@ keyword.
          -> [NiceDeclaration]
          -> Nice [NiceDeclaration]
        abstractBlock :: KwRange -> [NiceDeclaration] -> Nice [NiceDeclaration]
    abstractBlock KwRange
    r [NiceDeclaration]
    ds = do
          (ds', anyChange) <- ChangeT Nice [NiceDeclaration] -> Nice ([NiceDeclaration], Bool)
    forall (m :: * -> *) a. Functor m => ChangeT m a -> m (a, Bool)
    runChangeT (ChangeT Nice [NiceDeclaration] -> Nice ([NiceDeclaration], Bool))
    -> ChangeT Nice [NiceDeclaration] -> Nice ([NiceDeclaration], Bool)
    forall a b. (a -> b) -> a -> b
    $ KwRange -> UpdaterT Nice [NiceDeclaration]
    forall a. MakeAbstract a => KwRange -> UpdaterT Nice a
    mkAbstract KwRange
    r [NiceDeclaration]
    ds
          let inherited = KwRange -> Bool
    forall a. Null a => a -> Bool
    null KwRange
    r
          if anyChange then return ds' else do
            -- hack to avoid failing on inherited abstract blocks in where clauses
            unless inherited $ declarationWarning $ UselessAbstract r
            return ds -- no change!

        privateBlock
          :: KwRange  -- Range of @private@ keyword.
          -> Origin   -- Origin of the private block.
          -> [NiceDeclaration]
          -> Nice [NiceDeclaration]
        privateBlock :: KwRange -> Origin -> [NiceDeclaration] -> Nice [NiceDeclaration]
    privateBlock KwRange
    r Origin
    o [NiceDeclaration]
    ds = do
          (ds', anyChange) <- ChangeT Nice [NiceDeclaration] -> Nice ([NiceDeclaration], Bool)
    forall (m :: * -> *) a. Functor m => ChangeT m a -> m (a, Bool)
    runChangeT (ChangeT Nice [NiceDeclaration] -> Nice ([NiceDeclaration], Bool))
    -> ChangeT Nice [NiceDeclaration] -> Nice ([NiceDeclaration], Bool)
    forall a b. (a -> b) -> a -> b
    $ KwRange -> Origin -> UpdaterT Nice [NiceDeclaration]
    forall a. MakePrivate a => KwRange -> Origin -> UpdaterT Nice a
    mkPrivate KwRange
    r Origin
    o [NiceDeclaration]
    ds
          -- Warn if user-written 'private' does not accomplish anything.
          when (o == UserWritten) do
            if anyChange then
              -- Andreas, 2025-03-29, user-written 'private' is useless in anonymous 'where' modules
              -- since Agda automatically inserts a 'private' there.
              whenM ((AnyWhere_ ==) <$> asks checkingWhere) warn
            else warn
          return $ if anyChange then ds' else ds
          where
            warn :: Nice ()
    warn = HasCallStack => DeclarationWarning' -> Nice ()
    DeclarationWarning' -> Nice ()
    declarationWarning (DeclarationWarning' -> Nice ()) -> DeclarationWarning' -> Nice ()
    forall a b. (a -> b) -> a -> b
    $ KwRange -> DeclarationWarning'
    UselessPrivate KwRange
    r

        instanceBlock
          :: KwRange  -- Range of @instance@ keyword.
          -> [NiceDeclaration]
          -> Nice [NiceDeclaration]
        instanceBlock :: KwRange -> [NiceDeclaration] -> Nice [NiceDeclaration]
    instanceBlock KwRange
    r [NiceDeclaration]
    ds = do
          let ([NiceDeclaration]
    ds', Bool
    anyChange) = Change [NiceDeclaration] -> ([NiceDeclaration], Bool)
    forall a. Change a -> (a, Bool)
    runChange (Change [NiceDeclaration] -> ([NiceDeclaration], Bool))
    -> Change [NiceDeclaration] -> ([NiceDeclaration], Bool)
    forall a b. (a -> b) -> a -> b
    $ (NiceDeclaration -> ChangeT Identity NiceDeclaration)
    -> [NiceDeclaration] -> Change [NiceDeclaration]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
    mapM (KwRange -> NiceDeclaration -> ChangeT Identity NiceDeclaration
    mkInstance KwRange
    r) [NiceDeclaration]
    ds
          if Bool
    anyChange then [NiceDeclaration] -> Nice [NiceDeclaration]
    forall a. a -> Nice a
    forall (m :: * -> *) a. Monad m => a -> m a
    return [NiceDeclaration]
    ds' else do
            HasCallStack => DeclarationWarning' -> Nice ()
    DeclarationWarning' -> Nice ()
    declarationWarning (DeclarationWarning' -> Nice ()) -> DeclarationWarning' -> Nice ()
    forall a b. (a -> b) -> a -> b
    $ KwRange -> DeclarationWarning'
    UselessInstance KwRange
    r
            [NiceDeclaration] -> Nice [NiceDeclaration]
    forall a. a -> Nice a
    forall (m :: * -> *) a. Monad m => a -> m a
    return [NiceDeclaration]
    ds -- no change!

        -- Make a declaration eligible for instance search.
        mkInstance
          :: KwRange  -- Range of @instance@ keyword.
          -> Updater NiceDeclaration
        mkInstance :: KwRange -> NiceDeclaration -> ChangeT Identity NiceDeclaration
    mkInstance KwRange
    r0 = \case
            Axiom Range
    r Access
    p IsAbstract
    a IsInstance
    i ArgInfo
    rel Name
    x Expr
    e          -> (\ IsInstance
    i -> Range
    -> Access
    -> IsAbstract
    -> IsInstance
    -> ArgInfo
    -> Name
    -> Expr
    -> NiceDeclaration
    Axiom Range
    r Access
    p IsAbstract
    a IsInstance
    i ArgInfo
    rel Name
    x Expr
    e) (IsInstance -> NiceDeclaration)
    -> ChangeT Identity IsInstance -> ChangeT Identity NiceDeclaration
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> KwRange -> Updater IsInstance
    setInstance KwRange
    r0 IsInstance
    i
            FunSig Range
    r Access
    p IsAbstract
    a IsInstance
    i IsMacro
    m ArgInfo
    rel TerminationCheck
    tc CoverageCheck
    cc Name
    x Expr
    e -> (\ IsInstance
    i -> Range
    -> Access
    -> IsAbstract
    -> IsInstance
    -> IsMacro
    -> ArgInfo
    -> TerminationCheck
    -> CoverageCheck
    -> Name
    -> Expr
    -> NiceDeclaration
    FunSig Range
    r Access
    p IsAbstract
    a IsInstance
    i IsMacro
    m ArgInfo
    rel TerminationCheck
    tc CoverageCheck
    cc Name
    x Expr
    e) (IsInstance -> NiceDeclaration)
    -> ChangeT Identity IsInstance -> ChangeT Identity NiceDeclaration
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> KwRange -> Updater IsInstance
    setInstance KwRange
    r0 IsInstance
    i
            NiceUnquoteDecl Range
    r Access
    p IsAbstract
    a IsInstance
    i TerminationCheck
    tc CoverageCheck
    cc [Name]
    x Expr
    e -> (\ IsInstance
    i -> Range
    -> Access
    -> IsAbstract
    -> IsInstance
    -> TerminationCheck
    -> CoverageCheck
    -> [Name]
    -> Expr
    -> NiceDeclaration
    NiceUnquoteDecl Range
    r Access
    p IsAbstract
    a IsInstance
    i TerminationCheck
    tc CoverageCheck
    cc [Name]
    x Expr
    e) (IsInstance -> NiceDeclaration)
    -> ChangeT Identity IsInstance -> ChangeT Identity NiceDeclaration
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> KwRange -> Updater IsInstance
    setInstance KwRange
    r0 IsInstance
    i
            NiceMutual KwRange
    r TerminationCheck
    tc CoverageCheck
    cc PositivityCheck
    pc [NiceDeclaration]
    ds       -> KwRange
    -> TerminationCheck
    -> CoverageCheck
    -> PositivityCheck
    -> [NiceDeclaration]
    -> NiceDeclaration
    NiceMutual KwRange
    r TerminationCheck
    tc CoverageCheck
    cc PositivityCheck
    pc ([NiceDeclaration] -> NiceDeclaration)
    -> Change [NiceDeclaration] -> ChangeT Identity NiceDeclaration
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (NiceDeclaration -> ChangeT Identity NiceDeclaration)
    -> [NiceDeclaration] -> Change [NiceDeclaration]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
    mapM (KwRange -> NiceDeclaration -> ChangeT Identity NiceDeclaration
    mkInstance KwRange
    r0) [NiceDeclaration]
    ds
            NiceLoneConstructor KwRange
    r [NiceDeclaration]
    ds       -> KwRange -> [NiceDeclaration] -> NiceDeclaration
    NiceLoneConstructor KwRange
    r ([NiceDeclaration] -> NiceDeclaration)
    -> Change [NiceDeclaration] -> ChangeT Identity NiceDeclaration
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (NiceDeclaration -> ChangeT Identity NiceDeclaration)
    -> [NiceDeclaration] -> Change [NiceDeclaration]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
    mapM (KwRange -> NiceDeclaration -> ChangeT Identity NiceDeclaration
    mkInstance KwRange
    r0) [NiceDeclaration]
    ds
            d :: NiceDeclaration
    d@NiceFunClause{}              -> NiceDeclaration -> ChangeT Identity NiceDeclaration
    forall a. a -> ChangeT Identity a
    forall (m :: * -> *) a. Monad m => a -> m a
    return NiceDeclaration
    d
            FunDef Range
    r [Declaration]
    ds IsAbstract
    a IsInstance
    i TerminationCheck
    tc CoverageCheck
    cc Name
    x [Clause]
    cs     -> (\ IsInstance
    i -> Range
    -> [Declaration]
    -> IsAbstract
    -> IsInstance
    -> TerminationCheck
    -> CoverageCheck
    -> Name
    -> [Clause]
    -> NiceDeclaration
    FunDef Range
    r [Declaration]
    ds IsAbstract
    a IsInstance
    i TerminationCheck
    tc CoverageCheck
    cc Name
    x [Clause]
    cs) (IsInstance -> NiceDeclaration)
    -> ChangeT Identity IsInstance -> ChangeT Identity NiceDeclaration
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> KwRange -> Updater IsInstance
    setInstance KwRange
    r0 IsInstance
    i
            NiceOpaque KwRange
    r [QName]
    ns [NiceDeclaration]
    i              -> (\ [NiceDeclaration]
    i -> KwRange -> [QName] -> [NiceDeclaration] -> NiceDeclaration
    NiceOpaque KwRange
    r [QName]
    ns [NiceDeclaration]
    i) ([NiceDeclaration] -> NiceDeclaration)
    -> Change [NiceDeclaration] -> ChangeT Identity NiceDeclaration
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (NiceDeclaration -> ChangeT Identity NiceDeclaration)
    -> [NiceDeclaration] -> Change [NiceDeclaration]
    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) -> [a] -> f [b]
    traverse (KwRange -> NiceDeclaration -> ChangeT Identity NiceDeclaration
    mkInstance KwRange
    r0) [NiceDeclaration]
    i
            d :: NiceDeclaration
    d@NiceField{}                  -> NiceDeclaration -> ChangeT Identity NiceDeclaration
    forall a. a -> ChangeT Identity a
    forall (m :: * -> *) a. Monad m => a -> m a
    return NiceDeclaration
    d  -- Field instance are handled by the parser
            d :: NiceDeclaration
    d@PrimitiveFunction{}          -> NiceDeclaration -> ChangeT Identity NiceDeclaration
    forall a. a -> ChangeT Identity a
    forall (m :: * -> *) a. Monad m => a -> m a
    return NiceDeclaration
    d
            d :: NiceDeclaration
    d@NiceUnquoteDef{}             -> NiceDeclaration -> ChangeT Identity NiceDeclaration
    forall a. a -> ChangeT Identity a
    forall (m :: * -> *) a. Monad m => a -> m a
    return NiceDeclaration
    d
            d :: NiceDeclaration
    d@NiceRecSig{}                 -> NiceDeclaration -> ChangeT Identity NiceDeclaration
    forall a. a -> ChangeT Identity a
    forall (m :: * -> *) a. Monad m => a -> m a
    return NiceDeclaration
    d
            d :: NiceDeclaration
    d@NiceDataSig{}                -> NiceDeclaration -> ChangeT Identity NiceDeclaration
    forall a. a -> ChangeT Identity a
    forall (m :: * -> *) a. Monad m => a -> m a
    return NiceDeclaration
    d
            d :: NiceDeclaration
    d@NiceModuleMacro{}            -> NiceDeclaration -> ChangeT Identity NiceDeclaration
    forall a. a -> ChangeT Identity a
    forall (m :: * -> *) a. Monad m => a -> m a
    return NiceDeclaration
    d
            d :: NiceDeclaration
    d@NiceModule{}                 -> NiceDeclaration -> ChangeT Identity NiceDeclaration
    forall a. a -> ChangeT Identity a
    forall (m :: * -> *) a. Monad m => a -> m a
    return NiceDeclaration
    d
            d :: NiceDeclaration
    d@NicePragma{}                 -> NiceDeclaration -> ChangeT Identity NiceDeclaration
    forall a. a -> ChangeT Identity a
    forall (m :: * -> *) a. Monad m => a -> m a
    return NiceDeclaration
    d
            d :: NiceDeclaration
    d@NiceOpen{}                   -> NiceDeclaration -> ChangeT Identity NiceDeclaration
    forall a. a -> ChangeT Identity a
    forall (m :: * -> *) a. Monad m => a -> m a
    return NiceDeclaration
    d
            d :: NiceDeclaration
    d@NiceImport{}                 -> NiceDeclaration -> ChangeT Identity NiceDeclaration
    forall a. a -> ChangeT Identity a
    forall (m :: * -> *) a. Monad m => a -> m a
    return NiceDeclaration
    d
            d :: NiceDeclaration
    d@NiceDataDef{}                -> NiceDeclaration -> ChangeT Identity NiceDeclaration
    forall a. a -> ChangeT Identity a
    forall (m :: * -> *) a. Monad m => a -> m a
    return NiceDeclaration
    d
            d :: NiceDeclaration
    d@NiceRecDef{}                 -> NiceDeclaration -> ChangeT Identity NiceDeclaration
    forall a. a -> ChangeT Identity a
    forall (m :: * -> *) a. Monad m => a -> m a
    return NiceDeclaration
    d
            d :: NiceDeclaration
    d@NicePatternSyn{}             -> NiceDeclaration -> ChangeT Identity NiceDeclaration
    forall a. a -> ChangeT Identity a
    forall (m :: * -> *) a. Monad m => a -> m a
    return NiceDeclaration
    d
            d :: NiceDeclaration
    d@NiceGeneralize{}             -> NiceDeclaration -> ChangeT Identity NiceDeclaration
    forall a. a -> ChangeT Identity a
    forall (m :: * -> *) a. Monad m => a -> m a
    return NiceDeclaration
    d
            d :: NiceDeclaration
    d@NiceUnquoteData{}            -> NiceDeclaration -> ChangeT Identity NiceDeclaration
    forall a. a -> ChangeT Identity a
    forall (m :: * -> *) a. Monad m => a -> m a
    return NiceDeclaration
    d

        setInstance
          :: KwRange  -- Range of @instance@ keyword.
          -> Updater IsInstance
        setInstance :: KwRange -> Updater IsInstance
    setInstance KwRange
    r0 = \case
          i :: IsInstance
    i@InstanceDef{} -> Updater IsInstance
    forall a. a -> ChangeT Identity a
    forall (m :: * -> *) a. Monad m => a -> m a
    return IsInstance
    i
          IsInstance
    _               -> Updater IsInstance
    forall (m :: * -> *) a. Monad m => UpdaterT m a
    dirty Updater IsInstance -> Updater IsInstance
    forall a b. (a -> b) -> a -> b
    $ KwRange -> IsInstance
    InstanceDef KwRange
    r0

        macroBlock
          :: KwRange  -- Range of @macro@ keyword.
          -> [NiceDeclaration]
          -> Nice [NiceDeclaration]
        macroBlock :: KwRange -> [NiceDeclaration] -> Nice [NiceDeclaration]
    macroBlock KwRange
    r [NiceDeclaration]
    ds = do
          (ds', anyChange) <- ChangeT Nice [NiceDeclaration] -> Nice ([NiceDeclaration], Bool)
    forall (m :: * -> *) a. Functor m => ChangeT m a -> m (a, Bool)
    runChangeT (ChangeT Nice [NiceDeclaration] -> Nice ([NiceDeclaration], Bool))
    -> ChangeT Nice [NiceDeclaration] -> Nice ([NiceDeclaration], Bool)
    forall a b. (a -> b) -> a -> b
    $ UpdaterT Nice [NiceDeclaration]
    forall a. MakeMacro a => UpdaterT Nice a
    mkMacro [NiceDeclaration]
    ds
          if anyChange then return ds' else do
            declarationWarning $ UselessMacro r
            return ds -- no change!

    class MakeMacro a where
      mkMacro :: UpdaterT Nice a

      default mkMacro :: (Traversable f, MakeMacro a', a ~ f a') => UpdaterT Nice a
      mkMacro = (a' -> ChangeT Nice a') -> f a' -> ChangeT Nice (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' -> ChangeT Nice a'
    forall a. MakeMacro a => UpdaterT Nice a
    mkMacro

    instance MakeMacro a => MakeMacro [a]

    instance MakeMacro NiceDeclaration where
      mkMacro :: UpdaterT Nice NiceDeclaration
    mkMacro = \case
        FunSig Range
    r Access
    p IsAbstract
    a IsInstance
    i IsMacro
    _ ArgInfo
    rel TerminationCheck
    tc CoverageCheck
    cc Name
    x Expr
    e -> UpdaterT Nice NiceDeclaration
    forall (m :: * -> *) a. Monad m => UpdaterT m a
    dirty UpdaterT Nice NiceDeclaration -> UpdaterT Nice NiceDeclaration
    forall a b. (a -> b) -> a -> b
    $ Range
    -> Access
    -> IsAbstract
    -> IsInstance
    -> IsMacro
    -> ArgInfo
    -> TerminationCheck
    -> CoverageCheck
    -> Name
    -> Expr
    -> NiceDeclaration
    FunSig Range
    r Access
    p IsAbstract
    a IsInstance
    i IsMacro
    MacroDef ArgInfo
    rel TerminationCheck
    tc CoverageCheck
    cc Name
    x Expr
    e
        d :: NiceDeclaration
    d@FunDef{}                     -> UpdaterT Nice NiceDeclaration
    forall a. a -> ChangeT Nice a
    forall (m :: * -> *) a. Monad m => a -> m a
    return NiceDeclaration
    d
        NiceDeclaration
    d                              -> Nice NiceDeclaration -> ChangeT Nice NiceDeclaration
    forall (m :: * -> *) a. Monad m => m a -> ChangeT m a
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (Nice NiceDeclaration -> ChangeT Nice NiceDeclaration)
    -> Nice NiceDeclaration -> ChangeT Nice NiceDeclaration
    forall a b. (a -> b) -> a -> b
    $ DeclarationException' -> Nice NiceDeclaration
    forall a. HasCallStack => DeclarationException' -> Nice a
    declarationException (DeclarationException' -> Nice NiceDeclaration)
    -> DeclarationException' -> Nice NiceDeclaration
    forall a b. (a -> b) -> a -> b
    $ NiceDeclaration -> DeclarationException'
    BadMacroDef NiceDeclaration
    d

    -- | Make a declaration abstract.
    --
    -- Mark computation as 'dirty' if there was a declaration that could be made abstract.
    -- If no abstraction is taking place, we want to complain about 'UselessAbstract'.
    --
    -- Alternatively, we could only flag 'dirty' if a non-abstract thing was abstracted.
    -- Then, nested @abstract@s would sometimes also be complained about.

    class MakeAbstract a where
      mkAbstract ::
           KwRange
             -- ^ Range of the keyword @abstract@.
        -> UpdaterT Nice a

      default mkAbstract :: (Traversable f, MakeAbstract a', a ~ f a') => KwRange -> UpdaterT Nice a
      mkAbstract = (a' -> ChangeT Nice a') -> UpdaterT Nice a
    (a' -> ChangeT Nice a') -> f a' -> ChangeT Nice (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' -> ChangeT Nice a') -> UpdaterT Nice a)
    -> (KwRange -> a' -> ChangeT Nice a') -> KwRange -> UpdaterT Nice a
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . KwRange -> a' -> ChangeT Nice a'
    forall a. MakeAbstract a => KwRange -> UpdaterT Nice a
    mkAbstract

    instance MakeAbstract a => MakeAbstract [a]

    -- Leads to overlap with 'WhereClause':
    -- instance (Traversable f, MakeAbstract a) => MakeAbstract (f a) where
    --   mkAbstract = traverse mkAbstract

    instance MakeAbstract IsAbstract where
      mkAbstract :: KwRange -> UpdaterT Nice IsAbstract
    mkAbstract KwRange
    _ = \case
        a :: IsAbstract
    a@IsAbstract
    AbstractDef -> UpdaterT Nice IsAbstract
    forall a. a -> ChangeT Nice a
    forall (m :: * -> *) a. Monad m => a -> m a
    return IsAbstract
    a
        IsAbstract
    ConcreteDef -> UpdaterT Nice IsAbstract
    forall (m :: * -> *) a. Monad m => UpdaterT m a
    dirty UpdaterT Nice IsAbstract -> UpdaterT Nice IsAbstract
    forall a b. (a -> b) -> a -> b
    $ IsAbstract
    AbstractDef

    instance MakeAbstract NiceDeclaration where
      mkAbstract :: KwRange -> UpdaterT Nice NiceDeclaration
      mkAbstract :: KwRange -> UpdaterT Nice NiceDeclaration
    mkAbstract KwRange
    kwr = \case
        NiceMutual KwRange
    r TerminationCheck
    termCheck CoverageCheck
    cc PositivityCheck
    pc [NiceDeclaration]
    ds      -> KwRange
    -> TerminationCheck
    -> CoverageCheck
    -> PositivityCheck
    -> [NiceDeclaration]
    -> NiceDeclaration
    NiceMutual KwRange
    r TerminationCheck
    termCheck CoverageCheck
    cc PositivityCheck
    pc ([NiceDeclaration] -> NiceDeclaration)
    -> ChangeT Nice [NiceDeclaration] -> ChangeT Nice NiceDeclaration
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> KwRange -> UpdaterT Nice [NiceDeclaration]
    forall a. MakeAbstract a => KwRange -> UpdaterT Nice a
    mkAbstract KwRange
    kwr [NiceDeclaration]
    ds
        NiceLoneConstructor KwRange
    r [NiceDeclaration]
    ds             -> KwRange -> [NiceDeclaration] -> NiceDeclaration
    NiceLoneConstructor KwRange
    r ([NiceDeclaration] -> NiceDeclaration)
    -> ChangeT Nice [NiceDeclaration] -> ChangeT Nice NiceDeclaration
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> KwRange -> UpdaterT Nice [NiceDeclaration]
    forall a. MakeAbstract a => KwRange -> UpdaterT Nice a
    mkAbstract KwRange
    kwr [NiceDeclaration]
    ds
        FunDef Range
    r [Declaration]
    ds IsAbstract
    a IsInstance
    i TerminationCheck
    tc CoverageCheck
    cc Name
    x [Clause]
    cs           -> (\ IsAbstract
    a -> Range
    -> [Declaration]
    -> IsAbstract
    -> IsInstance
    -> TerminationCheck
    -> CoverageCheck
    -> Name
    -> [Clause]
    -> NiceDeclaration
    FunDef Range
    r [Declaration]
    ds IsAbstract
    a IsInstance
    i TerminationCheck
    tc CoverageCheck
    cc Name
    x) (IsAbstract -> [Clause] -> NiceDeclaration)
    -> ChangeT Nice IsAbstract
    -> ChangeT Nice ([Clause] -> NiceDeclaration)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> KwRange -> UpdaterT Nice IsAbstract
    forall a. MakeAbstract a => KwRange -> UpdaterT Nice a
    mkAbstract KwRange
    kwr IsAbstract
    a ChangeT Nice ([Clause] -> NiceDeclaration)
    -> ChangeT Nice [Clause] -> ChangeT Nice NiceDeclaration
    forall a b.
    ChangeT Nice (a -> b) -> ChangeT Nice a -> ChangeT Nice b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> KwRange -> UpdaterT Nice [Clause]
    forall a. MakeAbstract a => KwRange -> UpdaterT Nice a
    mkAbstract KwRange
    kwr [Clause]
    cs
        NiceDataDef Range
    r Origin
    o IsAbstract
    a PositivityCheck
    pc UniverseCheck
    uc Name
    x [LamBinding]
    ps [NiceDeclaration]
    cs      -> (\ IsAbstract
    a -> Range
    -> Origin
    -> IsAbstract
    -> PositivityCheck
    -> UniverseCheck
    -> Name
    -> [LamBinding]
    -> [NiceDeclaration]
    -> NiceDeclaration
    NiceDataDef Range
    r Origin
    o IsAbstract
    a PositivityCheck
    pc UniverseCheck
    uc Name
    x [LamBinding]
    ps) (IsAbstract -> [NiceDeclaration] -> NiceDeclaration)
    -> ChangeT Nice IsAbstract
    -> ChangeT Nice ([NiceDeclaration] -> NiceDeclaration)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> KwRange -> UpdaterT Nice IsAbstract
    forall a. MakeAbstract a => KwRange -> UpdaterT Nice a
    mkAbstract KwRange
    kwr IsAbstract
    a ChangeT Nice ([NiceDeclaration] -> NiceDeclaration)
    -> ChangeT Nice [NiceDeclaration] -> ChangeT Nice NiceDeclaration
    forall a b.
    ChangeT Nice (a -> b) -> ChangeT Nice a -> ChangeT Nice b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> KwRange -> UpdaterT Nice [NiceDeclaration]
    forall a. MakeAbstract a => KwRange -> UpdaterT Nice a
    mkAbstract KwRange
    kwr [NiceDeclaration]
    cs
        NiceRecDef Range
    r Origin
    o IsAbstract
    a PositivityCheck
    pc UniverseCheck
    uc Name
    x [RecordDirective]
    dir [LamBinding]
    ps [Declaration]
    cs   -> (\ IsAbstract
    a -> Range
    -> Origin
    -> IsAbstract
    -> PositivityCheck
    -> UniverseCheck
    -> Name
    -> [RecordDirective]
    -> [LamBinding]
    -> [Declaration]
    -> NiceDeclaration
    NiceRecDef Range
    r Origin
    o IsAbstract
    a PositivityCheck
    pc UniverseCheck
    uc Name
    x [RecordDirective]
    dir [LamBinding]
    ps [Declaration]
    cs) (IsAbstract -> NiceDeclaration)
    -> ChangeT Nice IsAbstract -> ChangeT Nice NiceDeclaration
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> KwRange -> UpdaterT Nice IsAbstract
    forall a. MakeAbstract a => KwRange -> UpdaterT Nice a
    mkAbstract KwRange
    kwr IsAbstract
    a
        NiceFunClause Range
    r Access
    p IsAbstract
    a TerminationCheck
    tc CoverageCheck
    cc Catchall
    catchall Declaration
    d -> (\ IsAbstract
    a -> Range
    -> Access
    -> IsAbstract
    -> TerminationCheck
    -> CoverageCheck
    -> Catchall
    -> Declaration
    -> NiceDeclaration
    NiceFunClause Range
    r Access
    p IsAbstract
    a TerminationCheck
    tc CoverageCheck
    cc Catchall
    catchall Declaration
    d) (IsAbstract -> NiceDeclaration)
    -> ChangeT Nice IsAbstract -> ChangeT Nice NiceDeclaration
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> KwRange -> UpdaterT Nice IsAbstract
    forall a. MakeAbstract a => KwRange -> UpdaterT Nice a
    mkAbstract KwRange
    kwr IsAbstract
    a
        -- The following declarations have an @InAbstract@ field
        -- but are not really definitions, so we do count them into
        -- the declarations which can be made abstract
        -- (thus, do not notify progress with @dirty@).
        Axiom Range
    r Access
    p IsAbstract
    a IsInstance
    i ArgInfo
    rel Name
    x Expr
    e                -> UpdaterT Nice NiceDeclaration
    forall a. a -> ChangeT Nice a
    forall (m :: * -> *) a. Monad m => a -> m a
    return UpdaterT Nice NiceDeclaration -> UpdaterT Nice NiceDeclaration
    forall a b. (a -> b) -> a -> b
    $ Range
    -> Access
    -> IsAbstract
    -> IsInstance
    -> ArgInfo
    -> Name
    -> Expr
    -> NiceDeclaration
    Axiom             Range
    r Access
    p IsAbstract
    AbstractDef IsInstance
    i ArgInfo
    rel Name
    x Expr
    e
        FunSig Range
    r Access
    p IsAbstract
    a IsInstance
    i IsMacro
    m ArgInfo
    rel TerminationCheck
    tc CoverageCheck
    cc Name
    x Expr
    e       -> UpdaterT Nice NiceDeclaration
    forall a. a -> ChangeT Nice a
    forall (m :: * -> *) a. Monad m => a -> m a
    return UpdaterT Nice NiceDeclaration -> UpdaterT Nice NiceDeclaration
    forall a b. (a -> b) -> a -> b
    $ Range
    -> Access
    -> IsAbstract
    -> IsInstance
    -> IsMacro
    -> ArgInfo
    -> TerminationCheck
    -> CoverageCheck
    -> Name
    -> Expr
    -> NiceDeclaration
    FunSig            Range
    r Access
    p IsAbstract
    AbstractDef IsInstance
    i IsMacro
    m ArgInfo
    rel TerminationCheck
    tc CoverageCheck
    cc Name
    x Expr
    e
        NiceRecSig  Range
    r Erased
    er Access
    p IsAbstract
    a PositivityCheck
    pc UniverseCheck
    uc Name
    x [LamBinding]
    ls Expr
    t    -> UpdaterT Nice NiceDeclaration
    forall a. a -> ChangeT Nice a
    forall (m :: * -> *) a. Monad m => a -> m a
    return UpdaterT Nice NiceDeclaration -> UpdaterT Nice NiceDeclaration
    forall a b. (a -> b) -> a -> b
    $ Range
    -> Erased
    -> Access
    -> IsAbstract
    -> PositivityCheck
    -> UniverseCheck
    -> Name
    -> [LamBinding]
    -> Expr
    -> NiceDeclaration
    NiceRecSig     Range
    r Erased
    er Access
    p IsAbstract
    AbstractDef PositivityCheck
    pc UniverseCheck
    uc Name
    x [LamBinding]
    ls Expr
    t
        NiceDataSig Range
    r Erased
    er Access
    p IsAbstract
    a PositivityCheck
    pc UniverseCheck
    uc Name
    x [LamBinding]
    ls Expr
    t    -> UpdaterT Nice NiceDeclaration
    forall a. a -> ChangeT Nice a
    forall (m :: * -> *) a. Monad m => a -> m a
    return UpdaterT Nice NiceDeclaration -> UpdaterT Nice NiceDeclaration
    forall a b. (a -> b) -> a -> b
    $ Range
    -> Erased
    -> Access
    -> IsAbstract
    -> PositivityCheck
    -> UniverseCheck
    -> Name
    -> [LamBinding]
    -> Expr
    -> NiceDeclaration
    NiceDataSig    Range
    r Erased
    er Access
    p IsAbstract
    AbstractDef PositivityCheck
    pc UniverseCheck
    uc Name
    x [LamBinding]
    ls Expr
    t
        NiceField Range
    r Access
    p IsAbstract
    _ IsInstance
    i TacticAttribute
    tac Name
    x Arg Expr
    e            -> UpdaterT Nice NiceDeclaration
    forall a. a -> ChangeT Nice a
    forall (m :: * -> *) a. Monad m => a -> m a
    return UpdaterT Nice NiceDeclaration -> UpdaterT Nice NiceDeclaration
    forall a b. (a -> b) -> a -> b
    $ Range
    -> Access
    -> IsAbstract
    -> IsInstance
    -> TacticAttribute
    -> Name
    -> Arg Expr
    -> NiceDeclaration
    NiceField         Range
    r Access
    p IsAbstract
    AbstractDef IsInstance
    i TacticAttribute
    tac Name
    x Arg Expr
    e
        PrimitiveFunction Range
    r Access
    p IsAbstract
    _ Name
    x Arg Expr
    e          -> UpdaterT Nice NiceDeclaration
    forall a. a -> ChangeT Nice a
    forall (m :: * -> *) a. Monad m => a -> m a
    return UpdaterT Nice NiceDeclaration -> UpdaterT Nice NiceDeclaration
    forall a b. (a -> b) -> a -> b
    $ Range
    -> Access -> IsAbstract -> Name -> Arg Expr -> NiceDeclaration
    PrimitiveFunction Range
    r Access
    p IsAbstract
    AbstractDef Name
    x Arg Expr
    e
        -- Andreas, 2016-07-17 it does have effect on unquoted defs.
        -- Need to set updater state to dirty!
        NiceUnquoteDecl Range
    r Access
    p IsAbstract
    _ IsInstance
    i TerminationCheck
    tc CoverageCheck
    cc [Name]
    x Expr
    e    -> ChangeT Nice ()
    forall (m :: * -> *). MonadChange m => m ()
    tellDirty ChangeT Nice () -> UpdaterT Nice NiceDeclaration
    forall (f :: * -> *) a b. Functor f => f a -> b -> f b
    $> Range
    -> Access
    -> IsAbstract
    -> IsInstance
    -> TerminationCheck
    -> CoverageCheck
    -> [Name]
    -> Expr
    -> NiceDeclaration
    NiceUnquoteDecl Range
    r Access
    p IsAbstract
    AbstractDef IsInstance
    i TerminationCheck
    tc CoverageCheck
    cc [Name]
    x Expr
    e
        NiceUnquoteDef Range
    r Access
    p IsAbstract
    _ TerminationCheck
    tc CoverageCheck
    cc [Name]
    x Expr
    e       -> ChangeT Nice ()
    forall (m :: * -> *). MonadChange m => m ()
    tellDirty ChangeT Nice () -> UpdaterT Nice NiceDeclaration
    forall (f :: * -> *) a b. Functor f => f a -> b -> f b
    $> Range
    -> Access
    -> IsAbstract
    -> TerminationCheck
    -> CoverageCheck
    -> [Name]
    -> Expr
    -> NiceDeclaration
    NiceUnquoteDef  Range
    r Access
    p IsAbstract
    AbstractDef TerminationCheck
    tc CoverageCheck
    cc [Name]
    x Expr
    e
        NiceUnquoteData Range
    r Access
    p IsAbstract
    _ PositivityCheck
    tc UniverseCheck
    cc Name
    x [Name]
    xs Expr
    e   -> ChangeT Nice ()
    forall (m :: * -> *). MonadChange m => m ()
    tellDirty ChangeT Nice () -> UpdaterT Nice NiceDeclaration
    forall (f :: * -> *) a b. Functor f => f a -> b -> f b
    $> Range
    -> Access
    -> IsAbstract
    -> PositivityCheck
    -> UniverseCheck
    -> Name
    -> [Name]
    -> Expr
    -> NiceDeclaration
    NiceUnquoteData Range
    r Access
    p IsAbstract
    AbstractDef PositivityCheck
    tc UniverseCheck
    cc Name
    x [Name]
    xs Expr
    e
        d :: NiceDeclaration
    d@NiceModule{}                       -> UpdaterT Nice NiceDeclaration
    forall a. a -> ChangeT Nice a
    forall (m :: * -> *) a. Monad m => a -> m a
    return NiceDeclaration
    d
        d :: NiceDeclaration
    d@NiceModuleMacro{}                  -> UpdaterT Nice NiceDeclaration
    forall a. a -> ChangeT Nice a
    forall (m :: * -> *) a. Monad m => a -> m a
    return NiceDeclaration
    d
        d :: NiceDeclaration
    d@NicePragma{}                       -> UpdaterT Nice NiceDeclaration
    forall a. a -> ChangeT Nice a
    forall (m :: * -> *) a. Monad m => a -> m a
    return NiceDeclaration
    d
        d :: NiceDeclaration
    d@NiceOpen{}                         -> NiceDeclaration
    d NiceDeclaration -> ChangeT Nice () -> ChangeT Nice NiceDeclaration
    forall a b. a -> ChangeT Nice b -> ChangeT Nice a
    forall (f :: * -> *) a b. Functor f => a -> f b -> f a
    <$ do
          Bool -> ChangeT Nice () -> ChangeT Nice ()
    forall b (m :: * -> *). (IsBool b, Monad m) => b -> m () -> m ()
    unless (KwRange -> Bool
    forall a. Null a => a -> Bool
    null KwRange
    kwr) (ChangeT Nice () -> ChangeT Nice ())
    -> ChangeT Nice () -> ChangeT Nice ()
    forall a b. (a -> b) -> a -> b
    $
            Nice () -> ChangeT Nice ()
    forall (m :: * -> *) a. Monad m => m a -> ChangeT m a
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (Nice () -> ChangeT Nice ()) -> Nice () -> ChangeT Nice ()
    forall a b. (a -> b) -> a -> b
    $ HasCallStack => DeclarationWarning' -> Nice ()
    DeclarationWarning' -> Nice ()
    declarationWarning (DeclarationWarning' -> Nice ()) -> DeclarationWarning' -> Nice ()
    forall a b. (a -> b) -> a -> b
    $ Range -> KwRange -> OpenOrImport -> DeclarationWarning'
    OpenImportAbstract (NiceDeclaration -> Range
    forall a. HasRange a => a -> Range
    getRange NiceDeclaration
    d) KwRange
    kwr OpenOrImport
    OpenNotImport
        d :: NiceDeclaration
    d@NiceImport{}                       -> NiceDeclaration
    d NiceDeclaration -> ChangeT Nice () -> ChangeT Nice NiceDeclaration
    forall a b. a -> ChangeT Nice b -> ChangeT Nice a
    forall (f :: * -> *) a b. Functor f => a -> f b -> f a
    <$ do
          Bool -> ChangeT Nice () -> ChangeT Nice ()
    forall b (m :: * -> *). (IsBool b, Monad m) => b -> m () -> m ()
    unless (KwRange -> Bool
    forall a. Null a => a -> Bool
    null KwRange
    kwr) (ChangeT Nice () -> ChangeT Nice ())
    -> ChangeT Nice () -> ChangeT Nice ()
    forall a b. (a -> b) -> a -> b
    $
            Nice () -> ChangeT Nice ()
    forall (m :: * -> *) a. Monad m => m a -> ChangeT m a
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (Nice () -> ChangeT Nice ()) -> Nice () -> ChangeT Nice ()
    forall a b. (a -> b) -> a -> b
    $ HasCallStack => DeclarationWarning' -> Nice ()
    DeclarationWarning' -> Nice ()
    declarationWarning (DeclarationWarning' -> Nice ()) -> DeclarationWarning' -> Nice ()
    forall a b. (a -> b) -> a -> b
    $ Range -> KwRange -> OpenOrImport -> DeclarationWarning'
    OpenImportAbstract (NiceDeclaration -> Range
    forall a. HasRange a => a -> Range
    getRange NiceDeclaration
    d) KwRange
    kwr OpenOrImport
    ImportMayOpen
        d :: NiceDeclaration
    d@NicePatternSyn{}                   -> UpdaterT Nice NiceDeclaration
    forall a. a -> ChangeT Nice a
    forall (m :: * -> *) a. Monad m => a -> m a
    return NiceDeclaration
    d
        d :: NiceDeclaration
    d@NiceGeneralize{}                   -> UpdaterT Nice NiceDeclaration
    forall a. a -> ChangeT Nice a
    forall (m :: * -> *) a. Monad m => a -> m a
    return NiceDeclaration
    d
        NiceOpaque KwRange
    r [QName]
    ns [NiceDeclaration]
    ds                   -> KwRange -> [QName] -> [NiceDeclaration] -> NiceDeclaration
    NiceOpaque KwRange
    r [QName]
    ns ([NiceDeclaration] -> NiceDeclaration)
    -> ChangeT Nice [NiceDeclaration] -> ChangeT Nice NiceDeclaration
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> KwRange -> UpdaterT Nice [NiceDeclaration]
    forall a. MakeAbstract a => KwRange -> UpdaterT Nice a
    mkAbstract KwRange
    kwr [NiceDeclaration]
    ds

    instance MakeAbstract Clause where
      mkAbstract :: KwRange -> UpdaterT Nice Clause
    mkAbstract KwRange
    kwr (Clause Name
    x Catchall
    catchall LHS
    lhs RHS
    rhs WhereClause
    wh [Clause]
    with) = do
        Name -> Catchall -> LHS -> RHS -> WhereClause -> [Clause] -> Clause
    Clause Name
    x Catchall
    catchall LHS
    lhs RHS
    rhs (WhereClause -> [Clause] -> Clause)
    -> ChangeT Nice WhereClause -> ChangeT Nice ([Clause] -> Clause)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> KwRange -> UpdaterT Nice WhereClause
    forall a. MakeAbstract a => KwRange -> UpdaterT Nice a
    mkAbstract KwRange
    kwr WhereClause
    wh ChangeT Nice ([Clause] -> Clause)
    -> ChangeT Nice [Clause] -> ChangeT Nice Clause
    forall a b.
    ChangeT Nice (a -> b) -> ChangeT Nice a -> ChangeT Nice b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> KwRange -> UpdaterT Nice [Clause]
    forall a. MakeAbstract a => KwRange -> UpdaterT Nice a
    mkAbstract KwRange
    kwr [Clause]
    with

    -- | Contents of a @where@ clause are abstract if the parent is.
    --
    --   These are inherited 'Abstract' blocks, indicated by an empty range
    --   for the @abstract@ keyword.
    instance MakeAbstract WhereClause where
      mkAbstract :: KwRange -> UpdaterT Nice WhereClause
    mkAbstract KwRange
    _  WhereClause
    NoWhere               = UpdaterT Nice WhereClause
    forall a. a -> ChangeT Nice a
    forall (m :: * -> *) a. Monad m => a -> m a
    return UpdaterT Nice WhereClause -> UpdaterT Nice WhereClause
    forall a b. (a -> b) -> a -> b
    $ WhereClause
    forall decls. WhereClause' decls
    NoWhere
      mkAbstract KwRange
    _ (AnyWhere Range
    r [Declaration]
    ds)        = UpdaterT Nice WhereClause
    forall (m :: * -> *) a. Monad m => UpdaterT m a
    dirty UpdaterT Nice WhereClause -> UpdaterT Nice WhereClause
    forall a b. (a -> b) -> a -> b
    $ Range -> [Declaration] -> WhereClause
    forall decls. Range -> decls -> WhereClause' decls
    AnyWhere Range
    r
                                                      [KwRange -> [Declaration] -> Declaration
    Abstract KwRange
    forall a. Null a => a
    empty [Declaration]
    ds]
      mkAbstract KwRange
    _ (SomeWhere Range
    r Erased
    e Name
    m Access
    a [Declaration]
    ds) = UpdaterT Nice WhereClause
    forall (m :: * -> *) a. Monad m => UpdaterT m a
    dirty UpdaterT Nice WhereClause -> UpdaterT Nice WhereClause
    forall a b. (a -> b) -> a -> b
    $ Range -> Erased -> Name -> Access -> [Declaration] -> WhereClause
    forall decls.
    Range -> Erased -> Name -> Access -> decls -> WhereClause' decls
    SomeWhere Range
    r Erased
    e Name
    m Access
    a
                                                      [KwRange -> [Declaration] -> Declaration
    Abstract KwRange
    forall a. Null a => a
    empty [Declaration]
    ds]

    -- | Make a declaration private.
    --
    -- Andreas, 2012-11-17:
    -- Mark computation as 'dirty' if there was a declaration that could be privatized.
    -- If no privatization is taking place, we want to complain about 'UselessPrivate'.
    --
    -- Alternatively, we could only flag 'dirty' if a non-private thing was privatized.
    -- Then, nested @private@s would sometimes also be complained about.

    class MakePrivate a where
      mkPrivate ::
           KwRange
             -- ^ Range of the @private@ keyword.
        -> Origin
             -- ^ Origin of the @private@ block.
        -> UpdaterT Nice a

      default mkPrivate :: (Traversable f, MakePrivate a', a ~ f a') => KwRange -> Origin -> UpdaterT Nice a
      mkPrivate KwRange
    kwr Origin
    o = (a' -> ChangeT Nice a') -> f a' -> ChangeT Nice (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' -> ChangeT Nice a') -> f a' -> ChangeT Nice (f a'))
    -> (a' -> ChangeT Nice a') -> f a' -> ChangeT Nice (f a')
    forall a b. (a -> b) -> a -> b
    $ KwRange -> Origin -> a' -> ChangeT Nice a'
    forall a. MakePrivate a => KwRange -> Origin -> UpdaterT Nice a
    mkPrivate KwRange
    kwr Origin
    o

    instance MakePrivate a => MakePrivate [a]

    -- Leads to overlap with 'WhereClause':
    -- instance (Traversable f, MakePrivate a) => MakePrivate (f a) where
    --   mkPrivate = traverse mkPrivate

    instance MakePrivate Access where
      mkPrivate :: KwRange -> Origin -> UpdaterT Nice Access
    mkPrivate KwRange
    kwr Origin
    o = \case
        p :: Access
    p@PrivateAccess{} -> UpdaterT Nice Access
    forall a. a -> ChangeT Nice a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Access
    p  -- OR? return $ PrivateAccess o
        Access
    _                 -> UpdaterT Nice Access
    forall (m :: * -> *) a. Monad m => UpdaterT m a
    dirty UpdaterT Nice Access -> UpdaterT Nice Access
    forall a b. (a -> b) -> a -> b
    $ KwRange -> Origin -> Access
    PrivateAccess KwRange
    kwr Origin
    o

    instance MakePrivate NiceDeclaration where
      mkPrivate :: KwRange -> Origin -> UpdaterT Nice NiceDeclaration
    mkPrivate KwRange
    kwr Origin
    o = \case
          Axiom Range
    r Access
    p IsAbstract
    a IsInstance
    i ArgInfo
    rel Name
    x Expr
    e                    -> (\ Access
    p -> Range
    -> Access
    -> IsAbstract
    -> IsInstance
    -> ArgInfo
    -> Name
    -> Expr
    -> NiceDeclaration
    Axiom Range
    r Access
    p IsAbstract
    a IsInstance
    i ArgInfo
    rel Name
    x Expr
    e)                (Access -> NiceDeclaration)
    -> ChangeT Nice Access -> ChangeT Nice NiceDeclaration
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> KwRange -> Origin -> UpdaterT Nice Access
    forall a. MakePrivate a => KwRange -> Origin -> UpdaterT Nice a
    mkPrivate KwRange
    kwr Origin
    o Access
    p
          NiceField Range
    r Access
    p IsAbstract
    a IsInstance
    i TacticAttribute
    tac Name
    x Arg Expr
    e                -> (\ Access
    p -> Range
    -> Access
    -> IsAbstract
    -> IsInstance
    -> TacticAttribute
    -> Name
    -> Arg Expr
    -> NiceDeclaration
    NiceField Range
    r Access
    p IsAbstract
    a IsInstance
    i TacticAttribute
    tac Name
    x Arg Expr
    e)            (Access -> NiceDeclaration)
    -> ChangeT Nice Access -> ChangeT Nice NiceDeclaration
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> KwRange -> Origin -> UpdaterT Nice Access
    forall a. MakePrivate a => KwRange -> Origin -> UpdaterT Nice a
    mkPrivate KwRange
    kwr Origin
    o Access
    p
          PrimitiveFunction Range
    r Access
    p IsAbstract
    a Name
    x Arg Expr
    e              -> (\ Access
    p -> Range
    -> Access -> IsAbstract -> Name -> Arg Expr -> NiceDeclaration
    PrimitiveFunction Range
    r Access
    p IsAbstract
    a Name
    x Arg Expr
    e)          (Access -> NiceDeclaration)
    -> ChangeT Nice Access -> ChangeT Nice NiceDeclaration
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> KwRange -> Origin -> UpdaterT Nice Access
    forall a. MakePrivate a => KwRange -> Origin -> UpdaterT Nice a
    mkPrivate KwRange
    kwr Origin
    o Access
    p
          NiceMutual KwRange
    r TerminationCheck
    tc CoverageCheck
    cc PositivityCheck
    pc [NiceDeclaration]
    ds                 -> (\ [NiceDeclaration]
    ds-> KwRange
    -> TerminationCheck
    -> CoverageCheck
    -> PositivityCheck
    -> [NiceDeclaration]
    -> NiceDeclaration
    NiceMutual KwRange
    r TerminationCheck
    tc CoverageCheck
    cc PositivityCheck
    pc [NiceDeclaration]
    ds)             ([NiceDeclaration] -> NiceDeclaration)
    -> ChangeT Nice [NiceDeclaration] -> ChangeT Nice NiceDeclaration
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> KwRange -> Origin -> UpdaterT Nice [NiceDeclaration]
    forall a. MakePrivate a => KwRange -> Origin -> UpdaterT Nice a
    mkPrivate KwRange
    kwr Origin
    o [NiceDeclaration]
    ds
          NiceLoneConstructor KwRange
    r [NiceDeclaration]
    ds                 -> KwRange -> [NiceDeclaration] -> NiceDeclaration
    NiceLoneConstructor KwRange
    r                         ([NiceDeclaration] -> NiceDeclaration)
    -> ChangeT Nice [NiceDeclaration] -> ChangeT Nice NiceDeclaration
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> KwRange -> Origin -> UpdaterT Nice [NiceDeclaration]
    forall a. MakePrivate a => KwRange -> Origin -> UpdaterT Nice a
    mkPrivate KwRange
    kwr Origin
    o [NiceDeclaration]
    ds
          NiceModule Range
    r Access
    p IsAbstract
    a Erased
    e QName
    x Telescope
    tel [Declaration]
    ds              -> (\ Access
    p -> Range
    -> Access
    -> IsAbstract
    -> Erased
    -> QName
    -> Telescope
    -> [Declaration]
    -> NiceDeclaration
    NiceModule Range
    r Access
    p IsAbstract
    a Erased
    e QName
    x Telescope
    tel [Declaration]
    ds)          (Access -> NiceDeclaration)
    -> ChangeT Nice Access -> ChangeT Nice NiceDeclaration
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> KwRange -> Origin -> UpdaterT Nice Access
    forall a. MakePrivate a => KwRange -> Origin -> UpdaterT Nice a
    mkPrivate KwRange
    kwr Origin
    o Access
    p
          NiceModuleMacro Range
    r Access
    p Erased
    e Name
    x ModuleApplication
    ma OpenShortHand
    op ImportDirective
    is         -> (\ Access
    p -> Range
    -> Access
    -> Erased
    -> Name
    -> ModuleApplication
    -> OpenShortHand
    -> ImportDirective
    -> NiceDeclaration
    NiceModuleMacro Range
    r Access
    p Erased
    e Name
    x ModuleApplication
    ma OpenShortHand
    op ImportDirective
    is)     (Access -> NiceDeclaration)
    -> ChangeT Nice Access -> ChangeT Nice NiceDeclaration
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> KwRange -> Origin -> UpdaterT Nice Access
    forall a. MakePrivate a => KwRange -> Origin -> UpdaterT Nice a
    mkPrivate KwRange
    kwr Origin
    o Access
    p
          FunSig Range
    r Access
    p IsAbstract
    a IsInstance
    i IsMacro
    m ArgInfo
    rel TerminationCheck
    tc CoverageCheck
    cc Name
    x Expr
    e           -> (\ Access
    p -> Range
    -> Access
    -> IsAbstract
    -> IsInstance
    -> IsMacro
    -> ArgInfo
    -> TerminationCheck
    -> CoverageCheck
    -> Name
    -> Expr
    -> NiceDeclaration
    FunSig Range
    r Access
    p IsAbstract
    a IsInstance
    i IsMacro
    m ArgInfo
    rel TerminationCheck
    tc CoverageCheck
    cc Name
    x Expr
    e)       (Access -> NiceDeclaration)
    -> ChangeT Nice Access -> ChangeT Nice NiceDeclaration
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> KwRange -> Origin -> UpdaterT Nice Access
    forall a. MakePrivate a => KwRange -> Origin -> UpdaterT Nice a
    mkPrivate KwRange
    kwr Origin
    o Access
    p
          NiceRecSig Range
    r Erased
    er Access
    p IsAbstract
    a PositivityCheck
    pc UniverseCheck
    uc Name
    x [LamBinding]
    ls Expr
    t         -> (\ Access
    p -> Range
    -> Erased
    -> Access
    -> IsAbstract
    -> PositivityCheck
    -> UniverseCheck
    -> Name
    -> [LamBinding]
    -> Expr
    -> NiceDeclaration
    NiceRecSig Range
    r Erased
    er Access
    p IsAbstract
    a PositivityCheck
    pc UniverseCheck
    uc Name
    x [LamBinding]
    ls Expr
    t)     (Access -> NiceDeclaration)
    -> ChangeT Nice Access -> ChangeT Nice NiceDeclaration
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> KwRange -> Origin -> UpdaterT Nice Access
    forall a. MakePrivate a => KwRange -> Origin -> UpdaterT Nice a
    mkPrivate KwRange
    kwr Origin
    o Access
    p
          NiceDataSig Range
    r Erased
    er Access
    p IsAbstract
    a PositivityCheck
    pc UniverseCheck
    uc Name
    x [LamBinding]
    ls Expr
    t        -> (\ Access
    p -> Range
    -> Erased
    -> Access
    -> IsAbstract
    -> PositivityCheck
    -> UniverseCheck
    -> Name
    -> [LamBinding]
    -> Expr
    -> NiceDeclaration
    NiceDataSig Range
    r Erased
    er Access
    p IsAbstract
    a PositivityCheck
    pc UniverseCheck
    uc Name
    x [LamBinding]
    ls Expr
    t)    (Access -> NiceDeclaration)
    -> ChangeT Nice Access -> ChangeT Nice NiceDeclaration
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> KwRange -> Origin -> UpdaterT Nice Access
    forall a. MakePrivate a => KwRange -> Origin -> UpdaterT Nice a
    mkPrivate KwRange
    kwr Origin
    o Access
    p
          NiceFunClause Range
    r Access
    p IsAbstract
    a TerminationCheck
    tc CoverageCheck
    cc Catchall
    catchall Declaration
    d     -> (\ Access
    p -> Range
    -> Access
    -> IsAbstract
    -> TerminationCheck
    -> CoverageCheck
    -> Catchall
    -> Declaration
    -> NiceDeclaration
    NiceFunClause Range
    r Access
    p IsAbstract
    a TerminationCheck
    tc CoverageCheck
    cc Catchall
    catchall Declaration
    d) (Access -> NiceDeclaration)
    -> ChangeT Nice Access -> ChangeT Nice NiceDeclaration
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> KwRange -> Origin -> UpdaterT Nice Access
    forall a. MakePrivate a => KwRange -> Origin -> UpdaterT Nice a
    mkPrivate KwRange
    kwr Origin
    o Access
    p
          NiceUnquoteDecl Range
    r Access
    p IsAbstract
    a IsInstance
    i TerminationCheck
    tc CoverageCheck
    cc [Name]
    x Expr
    e        -> (\ Access
    p -> Range
    -> Access
    -> IsAbstract
    -> IsInstance
    -> TerminationCheck
    -> CoverageCheck
    -> [Name]
    -> Expr
    -> NiceDeclaration
    NiceUnquoteDecl Range
    r Access
    p IsAbstract
    a IsInstance
    i TerminationCheck
    tc CoverageCheck
    cc [Name]
    x Expr
    e)    (Access -> NiceDeclaration)
    -> ChangeT Nice Access -> ChangeT Nice NiceDeclaration
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> KwRange -> Origin -> UpdaterT Nice Access
    forall a. MakePrivate a => KwRange -> Origin -> UpdaterT Nice a
    mkPrivate KwRange
    kwr Origin
    o Access
    p
          NiceUnquoteDef Range
    r Access
    p IsAbstract
    a TerminationCheck
    tc CoverageCheck
    cc [Name]
    x Expr
    e           -> (\ Access
    p -> Range
    -> Access
    -> IsAbstract
    -> TerminationCheck
    -> CoverageCheck
    -> [Name]
    -> Expr
    -> NiceDeclaration
    NiceUnquoteDef Range
    r Access
    p IsAbstract
    a TerminationCheck
    tc CoverageCheck
    cc [Name]
    x Expr
    e)       (Access -> NiceDeclaration)
    -> ChangeT Nice Access -> ChangeT Nice NiceDeclaration
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> KwRange -> Origin -> UpdaterT Nice Access
    forall a. MakePrivate a => KwRange -> Origin -> UpdaterT Nice a
    mkPrivate KwRange
    kwr Origin
    o Access
    p
          NicePatternSyn Range
    r Access
    p Name
    x [WithHiding Name]
    xs Pattern
    p'               -> (\ Access
    p -> Range
    -> Access
    -> Name
    -> [WithHiding Name]
    -> Pattern
    -> NiceDeclaration
    NicePatternSyn Range
    r Access
    p Name
    x [WithHiding Name]
    xs Pattern
    p')           (Access -> NiceDeclaration)
    -> ChangeT Nice Access -> ChangeT Nice NiceDeclaration
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> KwRange -> Origin -> UpdaterT Nice Access
    forall a. MakePrivate a => KwRange -> Origin -> UpdaterT Nice a
    mkPrivate KwRange
    kwr Origin
    o Access
    p
          NiceGeneralize Range
    r Access
    p ArgInfo
    i TacticAttribute
    tac Name
    x Expr
    t             -> (\ Access
    p -> Range
    -> Access
    -> ArgInfo
    -> TacticAttribute
    -> Name
    -> Expr
    -> NiceDeclaration
    NiceGeneralize Range
    r Access
    p ArgInfo
    i TacticAttribute
    tac Name
    x Expr
    t)         (Access -> NiceDeclaration)
    -> ChangeT Nice Access -> ChangeT Nice NiceDeclaration
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> KwRange -> Origin -> UpdaterT Nice Access
    forall a. MakePrivate a => KwRange -> Origin -> UpdaterT Nice a
    mkPrivate KwRange
    kwr Origin
    o Access
    p
          NiceOpaque KwRange
    r [QName]
    ns [NiceDeclaration]
    ds                       -> (\ [NiceDeclaration]
    p -> KwRange -> [QName] -> [NiceDeclaration] -> NiceDeclaration
    NiceOpaque KwRange
    r [QName]
    ns [NiceDeclaration]
    p)                    ([NiceDeclaration] -> NiceDeclaration)
    -> ChangeT Nice [NiceDeclaration] -> ChangeT Nice NiceDeclaration
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> KwRange -> Origin -> UpdaterT Nice [NiceDeclaration]
    forall a. MakePrivate a => KwRange -> Origin -> UpdaterT Nice a
    mkPrivate KwRange
    kwr Origin
    o [NiceDeclaration]
    ds
          d :: NiceDeclaration
    d@NicePragma{}                           -> UpdaterT Nice NiceDeclaration
    forall a. a -> ChangeT Nice a
    forall (m :: * -> *) a. Monad m => a -> m a
    return NiceDeclaration
    d
          d :: NiceDeclaration
    d@(NiceOpen Range
    r QName
    _x ImportDirective
    dir)                    -> NiceDeclaration
    d NiceDeclaration -> ChangeT Nice () -> ChangeT Nice NiceDeclaration
    forall a b. a -> ChangeT Nice b -> ChangeT Nice a
    forall (f :: * -> *) a b. Functor f => a -> f b -> f a
    <$ do
            Bool -> ChangeT Nice () -> ChangeT Nice ()
    forall b (m :: * -> *). (IsBool b, Monad m) => b -> m () -> m ()
    unless (KwRange -> Bool
    forall a. Null a => a -> Bool
    null KwRange
    kwr) (ChangeT Nice () -> ChangeT Nice ())
    -> ChangeT Nice () -> ChangeT Nice ()
    forall a b. (a -> b) -> a -> b
    $
              Maybe KwRange -> (KwRange -> ChangeT Nice ()) -> ChangeT Nice ()
    forall (m :: * -> *) a. Monad m => Maybe a -> (a -> m ()) -> m ()
    whenJust (ImportDirective -> Maybe KwRange
    forall n m. ImportDirective' n m -> Maybe KwRange
    publicOpen ImportDirective
    dir) \ KwRange
    kwrPublic ->
                Nice () -> ChangeT Nice ()
    forall (m :: * -> *) a. Monad m => m a -> ChangeT m a
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (Nice () -> ChangeT Nice ()) -> Nice () -> ChangeT Nice ()
    forall a b. (a -> b) -> a -> b
    $ HasCallStack => DeclarationWarning' -> Nice ()
    DeclarationWarning' -> Nice ()
    declarationWarning (DeclarationWarning' -> Nice ()) -> DeclarationWarning' -> Nice ()
    forall a b. (a -> b) -> a -> b
    $ Range -> KwRange -> KwRange -> OpenOrImport -> DeclarationWarning'
    OpenImportPrivate Range
    r KwRange
    kwrPublic KwRange
    kwr OpenOrImport
    OpenNotImport
          d :: NiceDeclaration
    d@(NiceImport Range
    r QName
    _x Maybe AsName
    _as OpenShortHand
    _open ImportDirective
    dir)        -> NiceDeclaration
    d NiceDeclaration -> ChangeT Nice () -> ChangeT Nice NiceDeclaration
    forall a b. a -> ChangeT Nice b -> ChangeT Nice a
    forall (f :: * -> *) a b. Functor f => a -> f b -> f a
    <$ do
            Bool -> ChangeT Nice () -> ChangeT Nice ()
    forall b (m :: * -> *). (IsBool b, Monad m) => b -> m () -> m ()
    unless (KwRange -> Bool
    forall a. Null a => a -> Bool
    null KwRange
    kwr) (ChangeT Nice () -> ChangeT Nice ())
    -> ChangeT Nice () -> ChangeT Nice ()
    forall a b. (a -> b) -> a -> b
    $
              Maybe KwRange -> (KwRange -> ChangeT Nice ()) -> ChangeT Nice ()
    forall (m :: * -> *) a. Monad m => Maybe a -> (a -> m ()) -> m ()
    whenJust (ImportDirective -> Maybe KwRange
    forall n m. ImportDirective' n m -> Maybe KwRange
    publicOpen ImportDirective
    dir) \ KwRange
    kwrPublic ->
                Nice () -> ChangeT Nice ()
    forall (m :: * -> *) a. Monad m => m a -> ChangeT m a
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (Nice () -> ChangeT Nice ()) -> Nice () -> ChangeT Nice ()
    forall a b. (a -> b) -> a -> b
    $ HasCallStack => DeclarationWarning' -> Nice ()
    DeclarationWarning' -> Nice ()
    declarationWarning (DeclarationWarning' -> Nice ()) -> DeclarationWarning' -> Nice ()
    forall a b. (a -> b) -> a -> b
    $ Range -> KwRange -> KwRange -> OpenOrImport -> DeclarationWarning'
    OpenImportPrivate Range
    r KwRange
    kwrPublic KwRange
    kwr OpenOrImport
    ImportMayOpen
          -- Andreas, 2016-07-08, issue #2089
          -- we need to propagate 'private' to the named where modules
          FunDef Range
    r [Declaration]
    ds IsAbstract
    a IsInstance
    i TerminationCheck
    tc CoverageCheck
    cc Name
    x [Clause]
    cls              -> Range
    -> [Declaration]
    -> IsAbstract
    -> IsInstance
    -> TerminationCheck
    -> CoverageCheck
    -> Name
    -> [Clause]
    -> NiceDeclaration
    FunDef Range
    r [Declaration]
    ds IsAbstract
    a IsInstance
    i TerminationCheck
    tc CoverageCheck
    cc Name
    x ([Clause] -> NiceDeclaration)
    -> ChangeT Nice [Clause] -> ChangeT Nice NiceDeclaration
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> KwRange -> Origin -> UpdaterT Nice [Clause]
    forall a. MakePrivate a => KwRange -> Origin -> UpdaterT Nice a
    mkPrivate KwRange
    kwr Origin
    o [Clause]
    cls
          d :: NiceDeclaration
    d@NiceDataDef{}                          -> UpdaterT Nice NiceDeclaration
    forall a. a -> ChangeT Nice a
    forall (m :: * -> *) a. Monad m => a -> m a
    return NiceDeclaration
    d
          d :: NiceDeclaration
    d@NiceRecDef{}                           -> UpdaterT Nice NiceDeclaration
    forall a. a -> ChangeT Nice a
    forall (m :: * -> *) a. Monad m => a -> m a
    return NiceDeclaration
    d
          d :: NiceDeclaration
    d@NiceUnquoteData{}                      -> UpdaterT Nice NiceDeclaration
    forall a. a -> ChangeT Nice a
    forall (m :: * -> *) a. Monad m => a -> m a
    return NiceDeclaration
    d

    instance MakePrivate Clause where
      mkPrivate :: KwRange -> Origin -> UpdaterT Nice Clause
    mkPrivate KwRange
    kwr Origin
    o (Clause Name
    x Catchall
    catchall LHS
    lhs RHS
    rhs WhereClause
    wh [Clause]
    with) = do
        Name -> Catchall -> LHS -> RHS -> WhereClause -> [Clause] -> Clause
    Clause Name
    x Catchall
    catchall LHS
    lhs RHS
    rhs (WhereClause -> [Clause] -> Clause)
    -> ChangeT Nice WhereClause -> ChangeT Nice ([Clause] -> Clause)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> KwRange -> Origin -> UpdaterT Nice WhereClause
    forall a. MakePrivate a => KwRange -> Origin -> UpdaterT Nice a
    mkPrivate KwRange
    kwr Origin
    o WhereClause
    wh ChangeT Nice ([Clause] -> Clause)
    -> ChangeT Nice [Clause] -> ChangeT Nice Clause
    forall a b.
    ChangeT Nice (a -> b) -> ChangeT Nice a -> ChangeT Nice b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> KwRange -> Origin -> UpdaterT Nice [Clause]
    forall a. MakePrivate a => KwRange -> Origin -> UpdaterT Nice a
    mkPrivate KwRange
    kwr Origin
    o [Clause]
    with

    instance MakePrivate WhereClause where
      mkPrivate :: KwRange -> Origin -> UpdaterT Nice WhereClause
    mkPrivate KwRange
    kwr Origin
    o = \case
        d :: WhereClause
    d@WhereClause
    NoWhere    -> UpdaterT Nice WhereClause
    forall a. a -> ChangeT Nice a
    forall (m :: * -> *) a. Monad m => a -> m a
    return WhereClause
    d
        -- @where@-declarations are protected behind an anonymous module,
        -- thus, they are effectively private by default.
        d :: WhereClause
    d@AnyWhere{} -> UpdaterT Nice WhereClause
    forall a. a -> ChangeT Nice a
    forall (m :: * -> *) a. Monad m => a -> m a
    return WhereClause
    d
        -- Andreas, 2016-07-08
        -- A named @where@-module is private if the parent function is private.
        -- The contents of this module are not private, unless declared so!
        -- Thus, we do not recurse into the @ds@ (could not anyway).
        SomeWhere Range
    r Erased
    e Name
    m Access
    a [Declaration]
    ds ->
          KwRange -> Origin -> UpdaterT Nice Access
    forall a. MakePrivate a => KwRange -> Origin -> UpdaterT Nice a
    mkPrivate KwRange
    kwr Origin
    o Access
    a ChangeT Nice Access
    -> (Access -> WhereClause) -> ChangeT Nice WhereClause
    forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
    <&> \Access
    a' -> Range -> Erased -> Name -> Access -> [Declaration] -> WhereClause
    forall decls.
    Range -> Erased -> Name -> Access -> decls -> WhereClause' decls
    SomeWhere Range
    r Erased
    e Name
    m Access
    a' [Declaration]
    ds

    -- The following function is (at the time of writing) only used three
    -- times: for building Lets, and for printing error messages.

    -- | (Approximately) convert a 'NiceDeclaration' back to a list of
    -- 'Declaration's.
    notSoNiceDeclarations :: NiceDeclaration -> List1 Declaration
    notSoNiceDeclarations :: NiceDeclaration -> List1 Declaration
    notSoNiceDeclarations = \case
        Axiom Range
    _ Access
    _ IsAbstract
    _ IsInstance
    i ArgInfo
    rel Name
    x Expr
    e            -> IsInstance -> Declaration -> List1 Declaration
    forall {coll}.
    Singleton Declaration coll =>
    IsInstance -> Declaration -> coll
    inst IsInstance
    i (Declaration -> List1 Declaration)
    -> Declaration -> List1 Declaration
    forall a b. (a -> b) -> a -> b
    $ ArgInfo -> TacticAttribute -> Name -> Expr -> Declaration
    TypeSig ArgInfo
    rel TacticAttribute
    forall a. Null a => a
    empty Name
    x Expr
    e
        NiceField Range
    _ Access
    _ IsAbstract
    _ IsInstance
    i TacticAttribute
    tac Name
    x Arg Expr
    argt     -> Declaration -> List1 Declaration
    forall el coll. Singleton el coll => el -> coll
    singleton (Declaration -> List1 Declaration)
    -> Declaration -> List1 Declaration
    forall a b. (a -> b) -> a -> b
    $ IsInstance -> TacticAttribute -> Name -> Arg Expr -> Declaration
    FieldSig IsInstance
    i TacticAttribute
    tac Name
    x Arg Expr
    argt
        PrimitiveFunction Range
    _ Access
    _ IsAbstract
    _ Name
    x Arg Expr
    e      -> Declaration -> List1 Declaration
    forall el coll. Singleton el coll => el -> coll
    singleton (Declaration -> List1 Declaration)
    -> Declaration -> List1 Declaration
    forall a b. (a -> b) -> a -> b
    $ KwRange -> [Declaration] -> Declaration
    Primitive KwRange
    forall a. Null a => a
    empty ([Declaration] -> Declaration) -> [Declaration] -> Declaration
    forall a b. (a -> b) -> a -> b
    $ Declaration -> [Declaration]
    forall el coll. Singleton el coll => el -> coll
    singleton (Declaration -> [Declaration]) -> Declaration -> [Declaration]
    forall a b. (a -> b) -> a -> b
    $ ArgInfo -> TacticAttribute -> Name -> Expr -> Declaration
    TypeSig (Arg Expr -> ArgInfo
    forall e. Arg e -> ArgInfo
    argInfo Arg Expr
    e) TacticAttribute
    forall a. Null a => a
    empty Name
    x (Arg Expr -> Expr
    forall e. Arg e -> e
    unArg Arg Expr
    e)
        NiceMutual KwRange
    r TerminationCheck
    _ CoverageCheck
    _ PositivityCheck
    _ [NiceDeclaration]
    ds            -> Declaration -> List1 Declaration
    forall el coll. Singleton el coll => el -> coll
    singleton (Declaration -> List1 Declaration)
    -> Declaration -> List1 Declaration
    forall a b. (a -> b) -> a -> b
    $ KwRange -> [Declaration] -> Declaration
    Mutual KwRange
    r ([Declaration] -> Declaration) -> [Declaration] -> Declaration
    forall a b. (a -> b) -> a -> b
    $ [List1 Declaration] -> [Declaration]
    forall a. [List1 a] -> [a]
    List1.concat ([List1 Declaration] -> [Declaration])
    -> [List1 Declaration] -> [Declaration]
    forall a b. (a -> b) -> a -> b
    $ (NiceDeclaration -> List1 Declaration)
    -> [NiceDeclaration] -> [List1 Declaration]
    forall a b. (a -> b) -> [a] -> [b]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap NiceDeclaration -> List1 Declaration
    notSoNiceDeclarations [NiceDeclaration]
    ds
        NiceLoneConstructor KwRange
    r [NiceDeclaration]
    ds         -> Declaration -> List1 Declaration
    forall el coll. Singleton el coll => el -> coll
    singleton (Declaration -> List1 Declaration)
    -> Declaration -> List1 Declaration
    forall a b. (a -> b) -> a -> b
    $ KwRange -> [Declaration] -> Declaration
    LoneConstructor KwRange
    r ([Declaration] -> Declaration) -> [Declaration] -> Declaration
    forall a b. (a -> b) -> a -> b
    $ [List1 Declaration] -> [Declaration]
    forall a. [List1 a] -> [a]
    List1.concat ([List1 Declaration] -> [Declaration])
    -> [List1 Declaration] -> [Declaration]
    forall a b. (a -> b) -> a -> b
    $ (NiceDeclaration -> List1 Declaration)
    -> [NiceDeclaration] -> [List1 Declaration]
    forall a b. (a -> b) -> [a] -> [b]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap NiceDeclaration -> List1 Declaration
    notSoNiceDeclarations [NiceDeclaration]
    ds
        NiceModule Range
    r Access
    _ IsAbstract
    _ Erased
    e QName
    x Telescope
    tel [Declaration]
    ds      -> Declaration -> List1 Declaration
    forall el coll. Singleton el coll => el -> coll
    singleton (Declaration -> List1 Declaration)
    -> Declaration -> List1 Declaration
    forall a b. (a -> b) -> a -> b
    $ Range
    -> Erased -> QName -> Telescope -> [Declaration] -> Declaration
    Module Range
    r Erased
    e QName
    x Telescope
    tel [Declaration]
    ds
        NiceModuleMacro Range
    r Access
    _ Erased
    e Name
    x ModuleApplication
    ma OpenShortHand
    o ImportDirective
    dir
                                         -> Declaration -> List1 Declaration
    forall el coll. Singleton el coll => el -> coll
    singleton (Declaration -> List1 Declaration)
    -> Declaration -> List1 Declaration
    forall a b. (a -> b) -> a -> b
    $ Range
    -> Erased
    -> Name
    -> ModuleApplication
    -> OpenShortHand
    -> ImportDirective
    -> Declaration
    ModuleMacro Range
    r Erased
    e Name
    x ModuleApplication
    ma OpenShortHand
    o ImportDirective
    dir
        NiceOpen Range
    r QName
    x ImportDirective
    dir                 -> Declaration -> List1 Declaration
    forall el coll. Singleton el coll => el -> coll
    singleton (Declaration -> List1 Declaration)
    -> Declaration -> List1 Declaration
    forall a b. (a -> b) -> a -> b
    $ Range -> QName -> ImportDirective -> Declaration
    Open Range
    r QName
    x ImportDirective
    dir
        NiceImport Range
    r QName
    x Maybe AsName
    as OpenShortHand
    o ImportDirective
    dir          -> Declaration -> List1 Declaration
    forall el coll. Singleton el coll => el -> coll
    singleton (Declaration -> List1 Declaration)
    -> Declaration -> List1 Declaration
    forall a b. (a -> b) -> a -> b
    $ Range
    -> QName
    -> Maybe AsName
    -> OpenShortHand
    -> ImportDirective
    -> Declaration
    Import Range
    r QName
    x Maybe AsName
    as OpenShortHand
    o ImportDirective
    dir
        NicePragma Range
    _ Pragma
    p                   -> Declaration -> List1 Declaration
    forall el coll. Singleton el coll => el -> coll
    singleton (Declaration -> List1 Declaration)
    -> Declaration -> List1 Declaration
    forall a b. (a -> b) -> a -> b
    $ Pragma -> Declaration
    Pragma Pragma
    p
        NiceRecSig Range
    r Erased
    er Access
    _ IsAbstract
    _ PositivityCheck
    _ UniverseCheck
    _ Name
    x [LamBinding]
    bs Expr
    e   -> Declaration -> List1 Declaration
    forall el coll. Singleton el coll => el -> coll
    singleton (Declaration -> List1 Declaration)
    -> Declaration -> List1 Declaration
    forall a b. (a -> b) -> a -> b
    $ Range -> Erased -> Name -> [LamBinding] -> Expr -> Declaration
    RecordSig Range
    r Erased
    er Name
    x [LamBinding]
    bs Expr
    e
        NiceDataSig Range
    r Erased
    er Access
    _ IsAbstract
    _ PositivityCheck
    _ UniverseCheck
    _ Name
    x [LamBinding]
    bs Expr
    e  -> Declaration -> List1 Declaration
    forall el coll. Singleton el coll => el -> coll
    singleton (Declaration -> List1 Declaration)
    -> Declaration -> List1 Declaration
    forall a b. (a -> b) -> a -> b
    $ Range -> Erased -> Name -> [LamBinding] -> Expr -> Declaration
    DataSig Range
    r Erased
    er Name
    x [LamBinding]
    bs Expr
    e
        NiceFunClause Range
    _ Access
    _ IsAbstract
    _ TerminationCheck
    _ CoverageCheck
    _ Catchall
    _ Declaration
    d      -> Declaration -> List1 Declaration
    forall el coll. Singleton el coll => el -> coll
    singleton (Declaration -> List1 Declaration)
    -> Declaration -> List1 Declaration
    forall a b. (a -> b) -> a -> b
    $ Declaration
    d
        FunSig Range
    _ Access
    _ IsAbstract
    _ IsInstance
    i IsMacro
    _ ArgInfo
    rel TerminationCheck
    _ CoverageCheck
    _ Name
    x Expr
    e     -> IsInstance -> Declaration -> List1 Declaration
    forall {coll}.
    Singleton Declaration coll =>
    IsInstance -> Declaration -> coll
    inst IsInstance
    i (Declaration -> List1 Declaration)
    -> Declaration -> List1 Declaration
    forall a b. (a -> b) -> a -> b
    $ ArgInfo -> TacticAttribute -> Name -> Expr -> Declaration
    TypeSig ArgInfo
    rel TacticAttribute
    forall a. Null a => a
    empty Name
    x Expr
    e
        FunDef Range
    _ [Declaration]
    ds IsAbstract
    _ IsInstance
    _ TerminationCheck
    _ CoverageCheck
    _ Name
    _ [Clause]
    _          -> List1 Declaration -> [Declaration] -> List1 Declaration
    forall a. List1 a -> [a] -> List1 a
    List1.fromListSafe List1 Declaration
    forall a. HasCallStack => a
    __IMPOSSIBLE__ [Declaration]
    ds -- TODO: use List1 in type of FunDef
        NiceDataDef Range
    r Origin
    _ IsAbstract
    _ PositivityCheck
    _ UniverseCheck
    _ Name
    x [LamBinding]
    bs [NiceDeclaration]
    cs    -> Declaration -> List1 Declaration
    forall el coll. Singleton el coll => el -> coll
    singleton (Declaration -> List1 Declaration)
    -> Declaration -> List1 Declaration
    forall a b. (a -> b) -> a -> b
    $ Range -> Name -> [LamBinding] -> [Declaration] -> Declaration
    DataDef Range
    r Name
    x [LamBinding]
    bs ([Declaration] -> Declaration) -> [Declaration] -> Declaration
    forall a b. (a -> b) -> a -> b
    $ [List1 Declaration] -> [Declaration]
    forall a. [List1 a] -> [a]
    List1.concat ([List1 Declaration] -> [Declaration])
    -> [List1 Declaration] -> [Declaration]
    forall a b. (a -> b) -> a -> b
    $ (NiceDeclaration -> List1 Declaration)
    -> [NiceDeclaration] -> [List1 Declaration]
    forall a b. (a -> b) -> [a] -> [b]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap NiceDeclaration -> List1 Declaration
    notSoNiceDeclarations [NiceDeclaration]
    cs
        NiceRecDef Range
    r Origin
    _ IsAbstract
    _ PositivityCheck
    _ UniverseCheck
    _ Name
    x [RecordDirective]
    dir [LamBinding]
    bs [Declaration]
    ds -> Declaration -> List1 Declaration
    forall el coll. Singleton el coll => el -> coll
    singleton (Declaration -> List1 Declaration)
    -> Declaration -> List1 Declaration
    forall a b. (a -> b) -> a -> b
    $ Range
    -> Name
    -> [RecordDirective]
    -> [LamBinding]
    -> [Declaration]
    -> Declaration
    RecordDef Range
    r Name
    x [RecordDirective]
    dir [LamBinding]
    bs [Declaration]
    ds
        NicePatternSyn Range
    r Access
    _ Name
    n [WithHiding Name]
    as Pattern
    p        -> Declaration -> List1 Declaration
    forall el coll. Singleton el coll => el -> coll
    singleton (Declaration -> List1 Declaration)
    -> Declaration -> List1 Declaration
    forall a b. (a -> b) -> a -> b
    $ Range -> Name -> [WithHiding Name] -> Pattern -> Declaration
    PatternSyn Range
    r Name
    n [WithHiding Name]
    as Pattern
    p
        NiceGeneralize Range
    _ Access
    _ ArgInfo
    i TacticAttribute
    tac Name
    n Expr
    e     -> Declaration -> List1 Declaration
    forall el coll. Singleton el coll => el -> coll
    singleton (Declaration -> List1 Declaration)
    -> Declaration -> List1 Declaration
    forall a b. (a -> b) -> a -> b
    $ KwRange -> [Declaration] -> Declaration
    Generalize KwRange
    forall a. Null a => a
    empty ([Declaration] -> Declaration) -> [Declaration] -> Declaration
    forall a b. (a -> b) -> a -> b
    $ Declaration -> [Declaration]
    forall el coll. Singleton el coll => el -> coll
    singleton (Declaration -> [Declaration]) -> Declaration -> [Declaration]
    forall a b. (a -> b) -> a -> b
    $ ArgInfo -> TacticAttribute -> Name -> Expr -> Declaration
    TypeSig ArgInfo
    i TacticAttribute
    tac Name
    n Expr
    e
        NiceUnquoteDecl Range
    r Access
    _ IsAbstract
    _ IsInstance
    i TerminationCheck
    _ CoverageCheck
    _ [Name]
    x Expr
    e  -> IsInstance -> Declaration -> List1 Declaration
    forall {coll}.
    Singleton Declaration coll =>
    IsInstance -> Declaration -> coll
    inst IsInstance
    i (Declaration -> List1 Declaration)
    -> Declaration -> List1 Declaration
    forall a b. (a -> b) -> a -> b
    $ Range -> [Name] -> Expr -> Declaration
    UnquoteDecl Range
    r [Name]
    x Expr
    e
        NiceUnquoteDef Range
    r Access
    _ IsAbstract
    _ TerminationCheck
    _ CoverageCheck
    _ [Name]
    x Expr
    e     -> Declaration -> List1 Declaration
    forall el coll. Singleton el coll => el -> coll
    singleton (Declaration -> List1 Declaration)
    -> Declaration -> List1 Declaration
    forall a b. (a -> b) -> a -> b
    $ Range -> [Name] -> Expr -> Declaration
    UnquoteDef Range
    r [Name]
    x Expr
    e
        NiceUnquoteData Range
    r Access
    _ IsAbstract
    _ PositivityCheck
    _ UniverseCheck
    _ Name
    x [Name]
    xs Expr
    e -> Declaration -> List1 Declaration
    forall el coll. Singleton el coll => el -> coll
    singleton (Declaration -> List1 Declaration)
    -> Declaration -> List1 Declaration
    forall a b. (a -> b) -> a -> b
    $ Range -> Name -> [Name] -> Expr -> Declaration
    UnquoteData Range
    r Name
    x [Name]
    xs Expr
    e
        NiceOpaque KwRange
    r [QName]
    ns [NiceDeclaration]
    ds               -> Declaration -> List1 Declaration
    forall el coll. Singleton el coll => el -> coll
    singleton (Declaration -> List1 Declaration)
    -> Declaration -> List1 Declaration
    forall a b. (a -> b) -> a -> b
    $ KwRange -> [Declaration] -> Declaration
    Opaque KwRange
    r ([Declaration] -> Declaration) -> [Declaration] -> Declaration
    forall a b. (a -> b) -> a -> b
    $ (KwRange -> [QName] -> Declaration
    Unfolding KwRange
    r [QName]
    ns Declaration -> [Declaration] -> [Declaration]
    forall a. a -> [a] -> [a]
    :) ([Declaration] -> [Declaration]) -> [Declaration] -> [Declaration]
    forall a b. (a -> b) -> a -> b
    $ [List1 Declaration] -> [Declaration]
    forall a. [List1 a] -> [a]
    List1.concat ([List1 Declaration] -> [Declaration])
    -> [List1 Declaration] -> [Declaration]
    forall a b. (a -> b) -> a -> b
    $ (NiceDeclaration -> List1 Declaration)
    -> [NiceDeclaration] -> [List1 Declaration]
    forall a b. (a -> b) -> [a] -> [b]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap NiceDeclaration -> List1 Declaration
    notSoNiceDeclarations [NiceDeclaration]
    ds
      where
        inst :: IsInstance -> Declaration -> coll
    inst (InstanceDef KwRange
    r) Declaration
    d = Declaration -> coll
    forall el coll. Singleton el coll => el -> coll
    singleton (Declaration -> coll) -> Declaration -> coll
    forall a b. (a -> b) -> a -> b
    $ KwRange -> [Declaration] -> Declaration
    InstanceB KwRange
    r ([Declaration] -> Declaration) -> [Declaration] -> Declaration
    forall a b. (a -> b) -> a -> b
    $ Declaration -> [Declaration]
    forall el coll. Singleton el coll => el -> coll
    singleton Declaration
    d
        inst IsInstance
    NotInstanceDef  Declaration
    d = Declaration -> coll
    forall el coll. Singleton el coll => el -> coll
    singleton Declaration
    d

    -- | Has the 'NiceDeclaration' a field of type 'IsAbstract'?
    niceHasAbstract :: NiceDeclaration -> Maybe IsAbstract
    niceHasAbstract :: NiceDeclaration -> Maybe IsAbstract
    niceHasAbstract = \case
        Axiom{}                       -> Maybe IsAbstract
    forall a. Maybe a
    Nothing
        NiceField Range
    _ Access
    _ IsAbstract
    a IsInstance
    _ TacticAttribute
    _ Name
    _ Arg Expr
    _       -> IsAbstract -> Maybe IsAbstract
    forall a. a -> Maybe a
    Just IsAbstract
    a
        PrimitiveFunction Range
    _ Access
    _ IsAbstract
    a Name
    _ Arg Expr
    _   -> IsAbstract -> Maybe IsAbstract
    forall a. a -> Maybe a
    Just IsAbstract
    a
        NiceMutual{}                  -> Maybe IsAbstract
    forall a. Maybe a
    Nothing
        NiceLoneConstructor{}         -> Maybe IsAbstract
    forall a. Maybe a
    Nothing
        NiceModule Range
    _ Access
    _ IsAbstract
    a Erased
    _ QName
    _ Telescope
    _ [Declaration]
    _      -> IsAbstract -> Maybe IsAbstract
    forall a. a -> Maybe a
    Just IsAbstract
    a
        NiceModuleMacro{}             -> Maybe IsAbstract
    forall a. Maybe a
    Nothing
        NiceOpen{}                    -> Maybe IsAbstract
    forall a. Maybe a
    Nothing
        NiceImport{}                  -> Maybe IsAbstract
    forall a. Maybe a
    Nothing
        NicePragma{}                  -> Maybe IsAbstract
    forall a. Maybe a
    Nothing
        NiceRecSig{}                  -> Maybe IsAbstract
    forall a. Maybe a
    Nothing
        NiceDataSig{}                 -> Maybe IsAbstract
    forall a. Maybe a
    Nothing
        NiceFunClause Range
    _ Access
    _ IsAbstract
    a TerminationCheck
    _ CoverageCheck
    _ Catchall
    _ Declaration
    _   -> IsAbstract -> Maybe IsAbstract
    forall a. a -> Maybe a
    Just IsAbstract
    a
        FunSig{}                      -> Maybe IsAbstract
    forall a. Maybe a
    Nothing
        FunDef Range
    _ [Declaration]
    _ IsAbstract
    a IsInstance
    _ TerminationCheck
    _ CoverageCheck
    _ Name
    _ [Clause]
    _        -> IsAbstract -> Maybe IsAbstract
    forall a. a -> Maybe a
    Just IsAbstract
    a
        NiceDataDef Range
    _ Origin
    _ IsAbstract
    a PositivityCheck
    _ UniverseCheck
    _ Name
    _ [LamBinding]
    _ [NiceDeclaration]
    _   -> IsAbstract -> Maybe IsAbstract
    forall a. a -> Maybe a
    Just IsAbstract
    a
        NiceRecDef Range
    _ Origin
    _ IsAbstract
    a PositivityCheck
    _ UniverseCheck
    _ Name
    _ [RecordDirective]
    _ [LamBinding]
    _ [Declaration]
    _ -> IsAbstract -> Maybe IsAbstract
    forall a. a -> Maybe a
    Just IsAbstract
    a
        NicePatternSyn{}              -> Maybe IsAbstract
    forall a. Maybe a
    Nothing
        NiceGeneralize{}              -> Maybe IsAbstract
    forall a. Maybe a
    Nothing
        NiceUnquoteDecl Range
    _ Access
    _ IsAbstract
    a IsInstance
    _ TerminationCheck
    _ CoverageCheck
    _ [Name]
    _ Expr
    _ -> IsAbstract -> Maybe IsAbstract
    forall a. a -> Maybe a
    Just IsAbstract
    a
        NiceUnquoteDef Range
    _ Access
    _ IsAbstract
    a TerminationCheck
    _ CoverageCheck
    _ [Name]
    _ Expr
    _    -> IsAbstract -> Maybe IsAbstract
    forall a. a -> Maybe a
    Just IsAbstract
    a
        NiceUnquoteData Range
    _ Access
    _ IsAbstract
    a PositivityCheck
    _ UniverseCheck
    _ Name
    _ [Name]
    _ Expr
    _ -> IsAbstract -> Maybe IsAbstract
    forall a. a -> Maybe a
    Just IsAbstract
    a
        NiceOpaque{}                    -> Maybe IsAbstract
    forall a. Maybe a
    Nothing