    {-# LANGUAGE GADTs              #-}

    -- | 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, runNice
        , niceDeclarations
        , notSoNiceDeclarations
        , niceHasAbstract
        , Measure
        , declarationWarningName
        ) where

    import Prelude hiding (null)

    import Control.Monad         ( forM, guard, unless, void, when )
    import Control.Monad.Except  ( )
    import Control.Monad.State   ( MonadState(..), gets, StateT, runStateT )
    import Control.Monad.Trans   ( lift )

    import Data.Bifunctor
    import Data.Data (Data)
    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.Concrete.Definitions.Errors
    import Agda.Syntax.Concrete.Definitions.Monad
    import Agda.Syntax.Concrete.Definitions.Types

    import Agda.Interaction.Options.Warnings

    import Agda.Utils.AffineHole
    import Agda.Utils.CallStack ( CallStack, HasCallStack, withCallerCallStack )
    import Agda.Utils.Functor
    import Agda.Utils.Lens
    import Agda.Utils.List (isSublistOf, spanJust)
    import Agda.Utils.List1 (List1, pattern (:|), (<|))
    import qualified Agda.Utils.List1 as List1
    import Agda.Utils.Maybe
    import Agda.Utils.Null
    import Agda.Utils.Pretty
    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]
    tcs = [TerminationCheck] -> Nice TerminationCheck
    loop [TerminationCheck]
    tcs where
      loop :: [TerminationCheck] -> Nice TerminationCheck
      loop :: [TerminationCheck] -> Nice TerminationCheck
    loop []         = TerminationCheck -> Nice TerminationCheck
    forall (m :: * -> *) a. Monad m => a -> m a
    return TerminationCheck
    forall m. TerminationCheck m
    TerminationCheck
      loop (TerminationCheck
    tc : [TerminationCheck]
    tcs) = do
        let 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
        TerminationCheck
    tc' <- [TerminationCheck] -> Nice TerminationCheck
    loop [TerminationCheck]
    tcs
        case (TerminationCheck
    tc, TerminationCheck
    tc') of
          (TerminationCheck
    TerminationCheck      , TerminationCheck
    tc'                   ) -> TerminationCheck -> Nice TerminationCheck
    forall (m :: * -> *) a. Monad m => a -> m a
    return TerminationCheck
    tc'
          (TerminationCheck
    tc                    , TerminationCheck
    TerminationCheck      ) -> TerminationCheck -> Nice TerminationCheck
    forall (m :: * -> *) a. Monad m => a -> m a
    return TerminationCheck
    tc
          (TerminationCheck
    NonTerminating        , TerminationCheck
    NonTerminating        ) -> TerminationCheck -> Nice TerminationCheck
    forall (m :: * -> *) a. Monad m => a -> m a
    return TerminationCheck
    forall m. TerminationCheck m
    NonTerminating
          (TerminationCheck
    NoTerminationCheck    , TerminationCheck
    NoTerminationCheck    ) -> TerminationCheck -> Nice TerminationCheck
    forall (m :: * -> *) a. Monad m => a -> m a
    return TerminationCheck
    forall m. TerminationCheck m
    NoTerminationCheck
          (TerminationCheck
    NoTerminationCheck    , TerminationCheck
    Terminating           ) -> TerminationCheck -> Nice TerminationCheck
    forall (m :: * -> *) a. Monad m => a -> m a
    return TerminationCheck
    forall m. TerminationCheck m
    Terminating
          (TerminationCheck
    Terminating           , TerminationCheck
    NoTerminationCheck    ) -> TerminationCheck -> Nice TerminationCheck
    forall (m :: * -> *) a. Monad m => a -> m a
    return TerminationCheck
    forall m. TerminationCheck m
    Terminating
          (TerminationCheck
    Terminating           , TerminationCheck
    Terminating           ) -> TerminationCheck -> Nice TerminationCheck
    forall (m :: * -> *) a. Monad m => a -> m a
    return TerminationCheck
    forall m. TerminationCheck m
    Terminating
          (TerminationMeasure{}  , TerminationMeasure{}  ) -> TerminationCheck -> Nice TerminationCheck
    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

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

    combinePositivityChecks :: [PositivityCheck] -> PositivityCheck
    combinePositivityChecks :: [PositivityCheck] -> PositivityCheck
    combinePositivityChecks = [PositivityCheck] -> PositivityCheck
    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
    /= :: DeclKind -> DeclKind -> Bool
    $c/= :: DeclKind -> DeclKind -> Bool
    == :: DeclKind -> DeclKind -> Bool
    $c== :: 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
    showList :: [DeclKind] -> ShowS
    $cshowList :: [DeclKind] -> ShowS
    show :: DeclKind -> String
    $cshow :: DeclKind -> String
    showsPrec :: Int -> DeclKind -> ShowS
    $cshowsPrec :: Int -> 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 Access
    _ IsAbstract
    _ PositivityCheck
    pc UniverseCheck
    uc Name
    x [LamBinding]
    pars Expr
    _)  = Range -> DataRecOrFun -> Name -> DeclKind
    LoneSigDecl Range
    r (PositivityCheck -> UniverseCheck -> DataRecOrFun
    RecName PositivityCheck
    pc UniverseCheck
    uc) Name
    x
    declKind (NiceDataSig Range
    r Access
    _ IsAbstract
    _ PositivityCheck
    pc UniverseCheck
    uc Name
    x [LamBinding]
    pars 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 (NiceRecDef Range
    _ Origin
    _ IsAbstract
    _ PositivityCheck
    pc UniverseCheck
    uc Name
    x RecordDirectives
    _ [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

    -- | 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 ArgInfo
    argi Name
    x' Expr
    e)
          NiceRecSig Range
    r 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 ArgInfo
    defaultArgInfo Name
    x Expr
    e)
          NiceDataSig Range
    r 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 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.
      NiceEnv
    st <- Nice NiceEnv
    forall s (m :: * -> *). MonadState s m => m s
    get
      NiceEnv -> Nice ()
    forall s (m :: * -> *). MonadState s m => s -> m ()
    put (NiceEnv -> Nice ()) -> NiceEnv -> Nice ()
    forall a b. (a -> b) -> a -> b
    $ NiceEnv
    initNiceEnv { niceWarn :: NiceWarnings
    niceWarn = NiceEnv -> NiceWarnings
    niceWarn NiceEnv
    st }
      [NiceDeclaration]
    nds <- [Declaration] -> Nice [NiceDeclaration]
    nice [Declaration]
    ds

      -- Check that every signature got its definition.
      LoneSigs
    ps <- Lens' LoneSigs NiceEnv -> Nice LoneSigs
    forall o (m :: * -> *) i. MonadState o m => Lens' i o -> m i
    use Lens' LoneSigs NiceEnv
    loneSigs
      LoneSigs -> Nice ()
    checkLoneSigs LoneSigs
    ps
      -- We postulate the missing ones and insert them in place of the corresponding @FunSig@
      let ds :: [NiceDeclaration]
    ds = LoneSigs -> [NiceDeclaration] -> [NiceDeclaration]
    replaceSigs LoneSigs
    ps [NiceDeclaration]
    nds

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

      -- Restore the old state, but keep the warnings.
      NiceWarnings
    warns <- (NiceEnv -> NiceWarnings) -> Nice NiceWarnings
    forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
    gets NiceEnv -> NiceWarnings
    niceWarn
      NiceEnv -> Nice ()
    forall s (m :: * -> *). MonadState s m => s -> m ()
    put (NiceEnv -> Nice ()) -> NiceEnv -> Nice ()
    forall a b. (a -> b) -> a -> b
    $ NiceEnv
    st { niceWarn :: NiceWarnings
    niceWarn = NiceWarnings
    warns }
      [NiceDeclaration] -> Nice [NiceDeclaration]
    forall (m :: * -> *) a. Monad m => a -> m a
    return [NiceDeclaration]
    res

      where

        inferMutualBlocks :: [NiceDeclaration] -> Nice [NiceDeclaration]
        inferMutualBlocks :: [NiceDeclaration] -> Nice [NiceDeclaration]
    inferMutualBlocks [] = [NiceDeclaration] -> Nice [NiceDeclaration]
    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
              Name
    _ <- Range -> Name -> DataRecOrFun -> Nice Name
    addLoneSig Range
    r Name
    x DataRecOrFun
    k
              InferredMutual MutualChecks
    checks [NiceDeclaration]
    nds0 [NiceDeclaration]
    ds1 <- MutualChecks -> [NiceDeclaration] -> Nice InferredMutual
    untilAllDefined (DataRecOrFun -> MutualChecks
    mutualChecks DataRecOrFun
    k) [NiceDeclaration]
    ds
              -- If we still have lone signatures without any accompanying definition,
              -- we postulate the definition and substitute the axiom for the lone signature
              LoneSigs
    ps <- Lens' LoneSigs NiceEnv -> Nice LoneSigs
    forall o (m :: * -> *) i. MonadState o m => Lens' i o -> m i
    use Lens' LoneSigs NiceEnv
    loneSigs
              LoneSigs -> Nice ()
    checkLoneSigs LoneSigs
    ps
              let ds0 :: [NiceDeclaration]
    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
              TerminationCheck
    tc <- Range -> [TerminationCheck] -> Nice TerminationCheck
    combineTerminationChecks (NiceDeclaration -> Range
    forall a. HasRange a => a -> Range
    getRange NiceDeclaration
    d) (MutualChecks -> [TerminationCheck]
    mutualTermination MutualChecks
    checks)
              let cc :: CoverageCheck
    cc = [CoverageCheck] -> CoverageCheck
    combineCoverageChecks              (MutualChecks -> [CoverageCheck]
    mutualCoverage MutualChecks
    checks)
              let pc :: PositivityCheck
    pc = [PositivityCheck] -> PositivityCheck
    combinePositivityChecks            (MutualChecks -> [PositivityCheck]
    mutualPositivity MutualChecks
    checks)
              (Range
    -> TerminationCheck
    -> CoverageCheck
    -> PositivityCheck
    -> [NiceDeclaration]
    -> NiceDeclaration
    NiceMutual ([NiceDeclaration] -> Range
    forall a. HasRange a => a -> Range
    getRange [NiceDeclaration]
    ds0) TerminationCheck
    tc CoverageCheck
    cc PositivityCheck
    pc [NiceDeclaration]
    ds0 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]
    ds1
          where
            untilAllDefined :: MutualChecks -> [NiceDeclaration] -> Nice InferredMutual
            untilAllDefined :: MutualChecks -> [NiceDeclaration] -> Nice InferredMutual
    untilAllDefined MutualChecks
    checks [NiceDeclaration]
    ds = do
              Bool
    done <- Nice Bool
    noLoneSigs
              if Bool
    done then InferredMutual -> Nice InferredMutual
    forall (m :: * -> *) a. Monad m => a -> m a
    return (MutualChecks
    -> [NiceDeclaration] -> [NiceDeclaration] -> InferredMutual
    InferredMutual MutualChecks
    checks [] [NiceDeclaration]
    ds) else
                case [NiceDeclaration]
    ds of
                  []     -> InferredMutual -> Nice InferredMutual
    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 (m :: * -> *) a. Monad m => a -> m a
    return []
        nice [Declaration]
    ds = do
          ([NiceDeclaration]
    xs , [Declaration]
    ys) <- [Declaration] -> Nice ([NiceDeclaration], [Declaration])
    nice1 [Declaration]
    ds
          ([NiceDeclaration]
    xs [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
    <$> [Declaration] -> Nice [NiceDeclaration]
    nice [Declaration]
    ys

        nice1 :: [Declaration] -> Nice ([NiceDeclaration], [Declaration])
        nice1 :: [Declaration] -> Nice ([NiceDeclaration], [Declaration])
    nice1 []     = ([NiceDeclaration], [Declaration])
    -> Nice ([NiceDeclaration], [Declaration])
    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
              TerminationCheck
    termCheck <- Lens' TerminationCheck NiceEnv -> Nice TerminationCheck
    forall o (m :: * -> *) i. MonadState o m => Lens' i o -> m i
    use Lens' TerminationCheck NiceEnv
    terminationCheckPragma
              CoverageCheck
    covCheck  <- Lens' CoverageCheck NiceEnv -> Nice CoverageCheck
    forall o (m :: * -> *) i. MonadState o m => Lens' i o -> m i
    use Lens' CoverageCheck NiceEnv
    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 :: Range
    r = Name -> Range
    forall a. HasRange a => a -> Range
    getRange Name
    x
              -- register x as lone type signature, to recognize clauses later
              Name
    x' <- Range -> Name -> DataRecOrFun -> Nice Name
    addLoneSig Range
    r Name
    x (DataRecOrFun -> Nice Name) -> DataRecOrFun -> Nice Name
    forall a b. (a -> b) -> a -> b
    $ TerminationCheck -> CoverageCheck -> DataRecOrFun
    FunName TerminationCheck
    termCheck CoverageCheck
    covCheck
              ([NiceDeclaration], [Declaration])
    -> Nice ([NiceDeclaration], [Declaration])
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([Range
    -> Access
    -> IsAbstract
    -> IsInstance
    -> IsMacro
    -> ArgInfo
    -> TerminationCheck
    -> CoverageCheck
    -> Name
    -> Expr
    -> NiceDeclaration
    FunSig Range
    r Access
    PublicAccess IsAbstract
    ConcreteDef IsInstance
    NotInstanceDef IsMacro
    NotMacroDef ArgInfo
    info TerminationCheck
    termCheck CoverageCheck
    covCheck Name
    x' Expr
    t] , [Declaration]
    ds)

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

            Generalize Range
    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
    $ Range -> DeclarationWarning'
    EmptyGeneralize Range
    r
            Generalize Range
    r [Declaration]
    sigs -> do
              [NiceDeclaration]
    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
                  NiceDeclaration -> Nice NiceDeclaration
    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__
              ([NiceDeclaration], [Declaration])
    -> Nice ([NiceDeclaration], [Declaration])
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([NiceDeclaration]
    gs, [Declaration]
    ds)

            (FunClause LHS
    lhs RHS
    _ WhereClause
    _ Bool
    _)         -> do
              TerminationCheck
    termCheck <- Lens' TerminationCheck NiceEnv -> Nice TerminationCheck
    forall o (m :: * -> *) i. MonadState o m => Lens' i o -> m i
    use Lens' TerminationCheck NiceEnv
    terminationCheckPragma
              CoverageCheck
    covCheck  <- Lens' CoverageCheck NiceEnv -> Nice CoverageCheck
    forall o (m :: * -> *) i. MonadState o m => Lens' i o -> m i
    use Lens' CoverageCheck NiceEnv
    coverageCheckPragma
              Bool
    catchall  <- Nice Bool
    popCatchallPragma
              [(Name, Name)]
    xs <- LoneSigs -> [(Name, Name)]
    loneFuns (LoneSigs -> [(Name, Name)])
    -> Nice LoneSigs -> Nice [(Name, Name)]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Lens' LoneSigs NiceEnv -> Nice LoneSigs
    forall o (m :: * -> *) i. MonadState o m => Lens' i o -> m i
    use Lens' LoneSigs NiceEnv
    loneSigs
              -- for each type signature 'x' waiting for clauses, we try
              -- if we have some clauses for 'x'
              case [ (Name
    x, (Name
    x', [Declaration]
    fits, [Declaration]
    rest))
                   | (Name
    x, Name
    x') <- [(Name, Name)]
    xs
                   , let ([Declaration]
    fits, [Declaration]
    rest) =
                          -- Anonymous declarations only have 1 clause each!
                          if Name -> Bool
    forall a. IsNoName a => a -> Bool
    isNoName Name
    x then ([Declaration
    d], [Declaration]
    ds)
                          else (Declaration -> Bool)
    -> [Declaration] -> ([Declaration], [Declaration])
    forall a. (a -> Bool) -> [a] -> ([a], [a])
    span (Maybe Fixity' -> Name -> Declaration -> Bool
    couldBeFunClauseOf (Name -> Fixities -> Maybe Fixity'
    forall k a. Ord k => k -> Map k a -> Maybe a
    Map.lookup Name
    x Fixities
    fixs) Name
    x) (Declaration
    d Declaration -> [Declaration] -> [Declaration]
    forall a. a -> [a] -> [a]
    : [Declaration]
    ds)
                   , Bool -> Bool
    not ([Declaration] -> Bool
    forall a. Null a => a -> Bool
    null [Declaration]
    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
                    [NiceDeclaration]
    d  <- ArgInfo
    -> TerminationCheck
    -> CoverageCheck
    -> Name
    -> TacticAttribute
    -> [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 TacticAttribute
    forall a. Maybe a
    Nothing [Declaration
    d] -- fun def without type signature is relevant
                    ([NiceDeclaration], [Declaration])
    -> Nice ([NiceDeclaration], [Declaration])
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([NiceDeclaration]
    d , [Declaration]
    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 (m :: * -> *) a. Monad m => a -> m a
    return ([Range
    -> Access
    -> IsAbstract
    -> TerminationCheck
    -> CoverageCheck
    -> Bool
    -> Declaration
    -> NiceDeclaration
    NiceFunClause (Declaration -> Range
    forall a. HasRange a => a -> Range
    getRange Declaration
    d) Access
    PublicAccess IsAbstract
    ConcreteDef TerminationCheck
    termCheck CoverageCheck
    covCheck Bool
    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
                   [Declaration]
    ds  <- [Declaration] -> Nice [Declaration]
    expandEllipsis [Declaration]
    fits
                   [Clause]
    cs  <- Name -> [Declaration] -> Bool -> Nice [Clause]
    mkClauses Name
    x' [Declaration]
    ds Bool
    False
                   ([NiceDeclaration], [Declaration])
    -> Nice ([NiceDeclaration], [Declaration])
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([Range
    -> [Declaration]
    -> IsAbstract
    -> IsInstance
    -> TerminationCheck
    -> CoverageCheck
    -> Name
    -> [Clause]
    -> NiceDeclaration
    FunDef ([Declaration] -> Range
    forall a. HasRange a => a -> Range
    getRange [Declaration]
    fits) [Declaration]
    fits IsAbstract
    ConcreteDef IsInstance
    NotInstanceDef TerminationCheck
    termCheck CoverageCheck
    covCheck Name
    x' [Clause]
    cs] , [Declaration]
    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 (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 Range
    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
    $ Range -> DeclarationWarning'
    EmptyField Range
    r
            Field Range
    _ [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 Name
    x [LamBinding]
    tel Expr
    t -> do
              PositivityCheck
    pc <- Lens' PositivityCheck NiceEnv -> Nice PositivityCheck
    forall o (m :: * -> *) i. MonadState o m => Lens' i o -> m i
    use Lens' PositivityCheck NiceEnv
    positivityCheckPragma
              UniverseCheck
    uc <- Lens' UniverseCheck NiceEnv -> Nice UniverseCheck
    forall o (m :: * -> *) i. MonadState o m => Lens' i o -> m i
    use Lens' UniverseCheck NiceEnv
    universeCheckPragma
              Name
    _ <- Range -> Name -> DataRecOrFun -> Nice Name
    addLoneSig Range
    r Name
    x (DataRecOrFun -> Nice Name) -> DataRecOrFun -> Nice Name
    forall a b. (a -> b) -> a -> b
    $ PositivityCheck -> UniverseCheck -> DataRecOrFun
    DataName PositivityCheck
    pc UniverseCheck
    uc
              (,[Declaration]
    ds) ([NiceDeclaration] -> ([NiceDeclaration], [Declaration]))
    -> Nice [NiceDeclaration]
    -> Nice ([NiceDeclaration], [Declaration])
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> PositivityCheck
    -> UniverseCheck
    -> (Range
        -> Origin
        -> IsAbstract
        -> PositivityCheck
        -> UniverseCheck
        -> Name
        -> [LamBinding]
        -> [NiceDeclaration]
        -> NiceDeclaration)
    -> (Range
        -> Access
        -> IsAbstract
        -> PositivityCheck
        -> UniverseCheck
        -> Name
        -> [LamBinding]
        -> Expr
        -> NiceDeclaration)
    -> ([Declaration] -> Nice [NiceDeclaration])
    -> Range
    -> Name
    -> Maybe ([LamBinding], Expr)
    -> Maybe ([LamBinding], [Declaration])
    -> Nice [NiceDeclaration]
    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]
    -> [NiceDeclaration]
    -> NiceDeclaration
    NiceDataDef Range
    -> Access
    -> IsAbstract
    -> PositivityCheck
    -> UniverseCheck
    -> Name
    -> [LamBinding]
    -> Expr
    -> NiceDeclaration
    NiceDataSig (KindOfBlock -> [Declaration] -> Nice [NiceDeclaration]
    niceAxioms KindOfBlock
    DataBlock) Range
    r Name
    x (([LamBinding], Expr) -> Maybe ([LamBinding], Expr)
    forall a. a -> Maybe a
    Just ([LamBinding]
    tel, Expr
    t)) Maybe ([LamBinding], [Declaration])
    forall a. Maybe a
    Nothing

            Data Range
    r Name
    x [LamBinding]
    tel Expr
    t [Declaration]
    cs -> do
              PositivityCheck
    pc <- Lens' PositivityCheck NiceEnv -> Nice PositivityCheck
    forall o (m :: * -> *) i. MonadState o m => Lens' i o -> m i
    use Lens' PositivityCheck NiceEnv
    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.
              UniverseCheck
    uc <- Lens' UniverseCheck NiceEnv -> Nice UniverseCheck
    forall o (m :: * -> *) i. MonadState o m => Lens' i o -> m i
    use Lens' UniverseCheck NiceEnv
    universeCheckPragma
              UniverseCheck
    uc <- if UniverseCheck
    uc UniverseCheck -> UniverseCheck -> Bool
    forall a. Eq a => a -> a -> Bool
    == UniverseCheck
    NoUniverseCheck then UniverseCheck -> Nice UniverseCheck
    forall (m :: * -> *) a. Monad m => a -> m a
    return UniverseCheck
    uc else Name -> Nice UniverseCheck
    getUniverseCheckFromSig Name
    x
              TacticAttribute
    mt <- DataRecOrFun -> Name -> TacticAttribute -> Nice TacticAttribute
    defaultTypeSig (PositivityCheck -> UniverseCheck -> DataRecOrFun
    DataName PositivityCheck
    pc UniverseCheck
    uc) Name
    x (Expr -> TacticAttribute
    forall a. a -> Maybe a
    Just Expr
    t)
              (,[Declaration]
    ds) ([NiceDeclaration] -> ([NiceDeclaration], [Declaration]))
    -> Nice [NiceDeclaration]
    -> Nice ([NiceDeclaration], [Declaration])
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> PositivityCheck
    -> UniverseCheck
    -> (Range
        -> Origin
        -> IsAbstract
        -> PositivityCheck
        -> UniverseCheck
        -> Name
        -> [LamBinding]
        -> [NiceDeclaration]
        -> NiceDeclaration)
    -> (Range
        -> Access
        -> IsAbstract
        -> PositivityCheck
        -> UniverseCheck
        -> Name
        -> [LamBinding]
        -> Expr
        -> NiceDeclaration)
    -> ([Declaration] -> Nice [NiceDeclaration])
    -> Range
    -> Name
    -> Maybe ([LamBinding], Expr)
    -> Maybe ([LamBinding], [Declaration])
    -> Nice [NiceDeclaration]
    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]
    -> [NiceDeclaration]
    -> NiceDeclaration
    NiceDataDef Range
    -> Access
    -> IsAbstract
    -> PositivityCheck
    -> UniverseCheck
    -> Name
    -> [LamBinding]
    -> Expr
    -> NiceDeclaration
    NiceDataSig (KindOfBlock -> [Declaration] -> Nice [NiceDeclaration]
    niceAxioms KindOfBlock
    DataBlock) Range
    r Name
    x (([LamBinding]
    tel,) (Expr -> ([LamBinding], Expr))
    -> TacticAttribute -> Maybe ([LamBinding], Expr)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> TacticAttribute
    mt) (([LamBinding], [Declaration])
    -> Maybe ([LamBinding], [Declaration])
    forall a. a -> Maybe a
    Just ([LamBinding]
    tel, [Declaration]
    cs))

            DataDef Range
    r Name
    x [LamBinding]
    tel [Declaration]
    cs -> do
              PositivityCheck
    pc <- Lens' PositivityCheck NiceEnv -> Nice PositivityCheck
    forall o (m :: * -> *) i. MonadState o m => Lens' i o -> m i
    use Lens' PositivityCheck NiceEnv
    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.
              UniverseCheck
    uc <- Lens' UniverseCheck NiceEnv -> Nice UniverseCheck
    forall o (m :: * -> *) i. MonadState o m => Lens' i o -> m i
    use Lens' UniverseCheck NiceEnv
    universeCheckPragma
              UniverseCheck
    uc <- if UniverseCheck
    uc UniverseCheck -> UniverseCheck -> Bool
    forall a. Eq a => a -> a -> Bool
    == UniverseCheck
    NoUniverseCheck then UniverseCheck -> Nice UniverseCheck
    forall (m :: * -> *) a. Monad m => a -> m a
    return UniverseCheck
    uc else Name -> Nice UniverseCheck
    getUniverseCheckFromSig Name
    x
              TacticAttribute
    mt <- DataRecOrFun -> Name -> TacticAttribute -> Nice TacticAttribute
    defaultTypeSig (PositivityCheck -> UniverseCheck -> DataRecOrFun
    DataName PositivityCheck
    pc UniverseCheck
    uc) Name
    x TacticAttribute
    forall a. Maybe a
    Nothing
              (,[Declaration]
    ds) ([NiceDeclaration] -> ([NiceDeclaration], [Declaration]))
    -> Nice [NiceDeclaration]
    -> Nice ([NiceDeclaration], [Declaration])
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> PositivityCheck
    -> UniverseCheck
    -> (Range
        -> Origin
        -> IsAbstract
        -> PositivityCheck
        -> UniverseCheck
        -> Name
        -> [LamBinding]
        -> [NiceDeclaration]
        -> NiceDeclaration)
    -> (Range
        -> Access
        -> IsAbstract
        -> PositivityCheck
        -> UniverseCheck
        -> Name
        -> [LamBinding]
        -> Expr
        -> NiceDeclaration)
    -> ([Declaration] -> Nice [NiceDeclaration])
    -> Range
    -> Name
    -> Maybe ([LamBinding], Expr)
    -> Maybe ([LamBinding], [Declaration])
    -> Nice [NiceDeclaration]
    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]
    -> [NiceDeclaration]
    -> NiceDeclaration
    NiceDataDef Range
    -> Access
    -> IsAbstract
    -> PositivityCheck
    -> UniverseCheck
    -> Name
    -> [LamBinding]
    -> Expr
    -> NiceDeclaration
    NiceDataSig (KindOfBlock -> [Declaration] -> Nice [NiceDeclaration]
    niceAxioms KindOfBlock
    DataBlock) Range
    r Name
    x (([LamBinding]
    tel,) (Expr -> ([LamBinding], Expr))
    -> TacticAttribute -> Maybe ([LamBinding], Expr)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> TacticAttribute
    mt) (([LamBinding], [Declaration])
    -> Maybe ([LamBinding], [Declaration])
    forall a. a -> Maybe a
    Just ([LamBinding]
    tel, [Declaration]
    cs))

            RecordSig Range
    r Name
    x [LamBinding]
    tel Expr
    t         -> do
              PositivityCheck
    pc <- Lens' PositivityCheck NiceEnv -> Nice PositivityCheck
    forall o (m :: * -> *) i. MonadState o m => Lens' i o -> m i
    use Lens' PositivityCheck NiceEnv
    positivityCheckPragma
              UniverseCheck
    uc <- Lens' UniverseCheck NiceEnv -> Nice UniverseCheck
    forall o (m :: * -> *) i. MonadState o m => Lens' i o -> m i
    use Lens' UniverseCheck NiceEnv
    universeCheckPragma
              Name
    _ <- Range -> Name -> DataRecOrFun -> Nice Name
    addLoneSig Range
    r Name
    x (DataRecOrFun -> Nice Name) -> DataRecOrFun -> Nice Name
    forall a b. (a -> b) -> a -> b
    $ PositivityCheck -> UniverseCheck -> DataRecOrFun
    RecName PositivityCheck
    pc UniverseCheck
    uc
              ([NiceDeclaration], [Declaration])
    -> Nice ([NiceDeclaration], [Declaration])
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([Range
    -> Access
    -> IsAbstract
    -> PositivityCheck
    -> UniverseCheck
    -> Name
    -> [LamBinding]
    -> Expr
    -> NiceDeclaration
    NiceRecSig Range
    r Access
    PublicAccess IsAbstract
    ConcreteDef PositivityCheck
    pc UniverseCheck
    uc Name
    x [LamBinding]
    tel Expr
    t] , [Declaration]
    ds)

            Record Range
    r Name
    x RecordDirectives
    dir [LamBinding]
    tel Expr
    t [Declaration]
    cs   -> do
              PositivityCheck
    pc <- Lens' PositivityCheck NiceEnv -> Nice PositivityCheck
    forall o (m :: * -> *) i. MonadState o m => Lens' i o -> m i
    use Lens' PositivityCheck NiceEnv
    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.
              UniverseCheck
    uc <- Lens' UniverseCheck NiceEnv -> Nice UniverseCheck
    forall o (m :: * -> *) i. MonadState o m => Lens' i o -> m i
    use Lens' UniverseCheck NiceEnv
    universeCheckPragma
              UniverseCheck
    uc <- if UniverseCheck
    uc UniverseCheck -> UniverseCheck -> Bool
    forall a. Eq a => a -> a -> Bool
    == UniverseCheck
    NoUniverseCheck then UniverseCheck -> Nice UniverseCheck
    forall (m :: * -> *) a. Monad m => a -> m a
    return UniverseCheck
    uc else Name -> Nice UniverseCheck
    getUniverseCheckFromSig Name
    x
              TacticAttribute
    mt <- DataRecOrFun -> Name -> TacticAttribute -> Nice TacticAttribute
    defaultTypeSig (PositivityCheck -> UniverseCheck -> DataRecOrFun
    RecName PositivityCheck
    pc UniverseCheck
    uc) Name
    x (Expr -> TacticAttribute
    forall a. a -> Maybe a
    Just Expr
    t)
              (,[Declaration]
    ds) ([NiceDeclaration] -> ([NiceDeclaration], [Declaration]))
    -> Nice [NiceDeclaration]
    -> Nice ([NiceDeclaration], [Declaration])
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> PositivityCheck
    -> UniverseCheck
    -> (Range
        -> Origin
        -> IsAbstract
        -> PositivityCheck
        -> UniverseCheck
        -> Name
        -> [LamBinding]
        -> [Declaration]
        -> NiceDeclaration)
    -> (Range
        -> Access
        -> IsAbstract
        -> PositivityCheck
        -> UniverseCheck
        -> Name
        -> [LamBinding]
        -> Expr
        -> NiceDeclaration)
    -> ([Declaration] -> Nice [Declaration])
    -> Range
    -> Name
    -> Maybe ([LamBinding], Expr)
    -> Maybe ([LamBinding], [Declaration])
    -> Nice [NiceDeclaration]
    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
    r Origin
    o IsAbstract
    a PositivityCheck
    pc UniverseCheck
    uc Name
    x [LamBinding]
    tel [Declaration]
    cs -> Range
    -> Origin
    -> IsAbstract
    -> PositivityCheck
    -> UniverseCheck
    -> Name
    -> RecordDirectives
    -> [LamBinding]
    -> [Declaration]
    -> NiceDeclaration
    NiceRecDef Range
    r Origin
    o IsAbstract
    a PositivityCheck
    pc UniverseCheck
    uc Name
    x RecordDirectives
    dir [LamBinding]
    tel [Declaration]
    cs) Range
    -> Access
    -> IsAbstract
    -> PositivityCheck
    -> UniverseCheck
    -> Name
    -> [LamBinding]
    -> Expr
    -> NiceDeclaration
    NiceRecSig
                          [Declaration] -> Nice [Declaration]
    forall (m :: * -> *) a. Monad m => a -> m a
    return Range
    r Name
    x (([LamBinding]
    tel,) (Expr -> ([LamBinding], Expr))
    -> TacticAttribute -> Maybe ([LamBinding], Expr)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> TacticAttribute
    mt) (([LamBinding], [Declaration])
    -> Maybe ([LamBinding], [Declaration])
    forall a. a -> Maybe a
    Just ([LamBinding]
    tel, [Declaration]
    cs))

            RecordDef Range
    r Name
    x RecordDirectives
    dir [LamBinding]
    tel [Declaration]
    cs   -> do
              PositivityCheck
    pc <- Lens' PositivityCheck NiceEnv -> Nice PositivityCheck
    forall o (m :: * -> *) i. MonadState o m => Lens' i o -> m i
    use Lens' PositivityCheck NiceEnv
    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.
              UniverseCheck
    uc <- Lens' UniverseCheck NiceEnv -> Nice UniverseCheck
    forall o (m :: * -> *) i. MonadState o m => Lens' i o -> m i
    use Lens' UniverseCheck NiceEnv
    universeCheckPragma
              UniverseCheck
    uc <- if UniverseCheck
    uc UniverseCheck -> UniverseCheck -> Bool
    forall a. Eq a => a -> a -> Bool
    == UniverseCheck
    NoUniverseCheck then UniverseCheck -> Nice UniverseCheck
    forall (m :: * -> *) a. Monad m => a -> m a
    return UniverseCheck
    uc else Name -> Nice UniverseCheck
    getUniverseCheckFromSig Name
    x
              TacticAttribute
    mt <- DataRecOrFun -> Name -> TacticAttribute -> Nice TacticAttribute
    defaultTypeSig (PositivityCheck -> UniverseCheck -> DataRecOrFun
    RecName PositivityCheck
    pc UniverseCheck
    uc) Name
    x TacticAttribute
    forall a. Maybe a
    Nothing
              (,[Declaration]
    ds) ([NiceDeclaration] -> ([NiceDeclaration], [Declaration]))
    -> Nice [NiceDeclaration]
    -> Nice ([NiceDeclaration], [Declaration])
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> PositivityCheck
    -> UniverseCheck
    -> (Range
        -> Origin
        -> IsAbstract
        -> PositivityCheck
        -> UniverseCheck
        -> Name
        -> [LamBinding]
        -> [Declaration]
        -> NiceDeclaration)
    -> (Range
        -> Access
        -> IsAbstract
        -> PositivityCheck
        -> UniverseCheck
        -> Name
        -> [LamBinding]
        -> Expr
        -> NiceDeclaration)
    -> ([Declaration] -> Nice [Declaration])
    -> Range
    -> Name
    -> Maybe ([LamBinding], Expr)
    -> Maybe ([LamBinding], [Declaration])
    -> Nice [NiceDeclaration]
    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
    r Origin
    o IsAbstract
    a PositivityCheck
    pc UniverseCheck
    uc Name
    x [LamBinding]
    tel [Declaration]
    cs -> Range
    -> Origin
    -> IsAbstract
    -> PositivityCheck
    -> UniverseCheck
    -> Name
    -> RecordDirectives
    -> [LamBinding]
    -> [Declaration]
    -> NiceDeclaration
    NiceRecDef Range
    r Origin
    o IsAbstract
    a PositivityCheck
    pc UniverseCheck
    uc Name
    x RecordDirectives
    dir [LamBinding]
    tel [Declaration]
    cs) Range
    -> Access
    -> IsAbstract
    -> PositivityCheck
    -> UniverseCheck
    -> Name
    -> [LamBinding]
    -> Expr
    -> NiceDeclaration
    NiceRecSig
                          [Declaration] -> Nice [Declaration]
    forall (m :: * -> *) a. Monad m => a -> m a
    return Range
    r Name
    x (([LamBinding]
    tel,) (Expr -> ([LamBinding], Expr))
    -> TacticAttribute -> Maybe ([LamBinding], Expr)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> TacticAttribute
    mt) (([LamBinding], [Declaration])
    -> Maybe ([LamBinding], [Declaration])
    forall a. a -> Maybe a
    Just ([LamBinding]
    tel, [Declaration]
    cs))

            RecordDirective RecordDirective
    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
    $ Range -> DeclarationWarning'
    InvalidRecordDirective (RecordDirective -> Range
    forall a. HasRange a => a -> Range
    getRange RecordDirective
    r)

            Mutual Range
    r [Declaration]
    ds' -> do
              -- The lone signatures encountered so far are not in scope
              -- for the mutual definition
              Nice ()
    forgetLoneSigs
              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
    $ Range -> DeclarationWarning'
    EmptyMutual Range
    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
    <$> (Range -> [NiceDeclaration] -> Nice NiceDeclaration
    mkOldMutual Range
    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 Range
    r [Declaration]
    ds' -> do
              -- The lone signatures encountered so far are not in scope
              -- for the mutual definition
              Nice ()
    forgetLoneSigs
              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
    $ Range -> DeclarationWarning'
    EmptyMutual Range
    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
    <$> (Range -> [NiceDeclaration] -> Nice NiceDeclaration
    mkInterleavedMutual Range
    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 Range
    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
    $ Range -> DeclarationWarning'
    EmptyConstructor Range
    r
            LoneConstructor Range
    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
    . Range -> [NiceDeclaration] -> NiceDeclaration
    NiceLoneConstructor Range
    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 Range
    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
    $ Range -> DeclarationWarning'
    EmptyAbstract Range
    r
            Abstract Range
    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
    <$> (Range -> [NiceDeclaration] -> Nice [NiceDeclaration]
    forall {a}. MakeAbstract a => Range -> [a] -> Nice [a]
    abstractBlock Range
    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 Range
    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
    $ Range -> DeclarationWarning'
    EmptyPrivate Range
    r
            Private Range
    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
    <$> (Range -> Origin -> [NiceDeclaration] -> Nice [NiceDeclaration]
    forall {a}. MakePrivate a => Range -> Origin -> [a] -> Nice [a]
    privateBlock Range
    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 Range
    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
    $ Range -> DeclarationWarning'
    EmptyInstance Range
    r
            InstanceB Range
    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
    <$> (Range -> [NiceDeclaration] -> Nice [NiceDeclaration]
    instanceBlock Range
    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 Range
    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
    $ Range -> DeclarationWarning'
    EmptyMacro Range
    r
            Macro Range
    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
    <$> (Range -> [NiceDeclaration] -> Nice [NiceDeclaration]
    forall {t :: * -> *} {p}.
    Traversable t =>
    p -> t NiceDeclaration -> Nice (t NiceDeclaration)
    macroBlock Range
    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 Range
    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
    $ Range -> DeclarationWarning'
    EmptyPostulate Range
    r
            Postulate Range
    _ [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 Range
    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
    $ Range -> DeclarationWarning'
    EmptyPrimitive Range
    r
            Primitive Range
    _ [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 QName
    x Telescope
    tel [Declaration]
    ds' -> ([NiceDeclaration], [Declaration])
    -> Nice ([NiceDeclaration], [Declaration])
    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
    -> QName
    -> Telescope
    -> [Declaration]
    -> NiceDeclaration
    NiceModule Range
    r Access
    PublicAccess IsAbstract
    ConcreteDef QName
    x Telescope
    tel [Declaration]
    ds'] , [Declaration]
    ds)

            ModuleMacro Range
    r Name
    x ModuleApplication
    modapp OpenShortHand
    op ImportDirective
    is -> ([NiceDeclaration], [Declaration])
    -> Nice ([NiceDeclaration], [Declaration])
    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
    -> Name
    -> ModuleApplication
    -> OpenShortHand
    -> ImportDirective
    -> NiceDeclaration
    NiceModuleMacro Range
    r Access
    PublicAccess 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 (m :: * -> *) a. Monad m => a -> m a
    return ([], [Declaration]
    ds)
            Syntax Name
    _ Notation
    _ -> ([NiceDeclaration], [Declaration])
    -> Nice ([NiceDeclaration], [Declaration])
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([], [Declaration]
    ds)

            PatternSyn Range
    r Name
    n [Arg Name]
    as Pattern
    p -> do
              ([NiceDeclaration], [Declaration])
    -> Nice ([NiceDeclaration], [Declaration])
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([Range -> Access -> Name -> [Arg Name] -> Pattern -> NiceDeclaration
    NicePatternSyn Range
    r Access
    PublicAccess Name
    n [Arg Name]
    as Pattern
    p] , [Declaration]
    ds)
            Open Range
    r QName
    x ImportDirective
    is         -> ([NiceDeclaration], [Declaration])
    -> Nice ([NiceDeclaration], [Declaration])
    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 (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
              TerminationCheck
    tc <- Lens' TerminationCheck NiceEnv -> Nice TerminationCheck
    forall o (m :: * -> *) i. MonadState o m => Lens' i o -> m i
    use Lens' TerminationCheck NiceEnv
    terminationCheckPragma
              CoverageCheck
    cc <- Lens' CoverageCheck NiceEnv -> Nice CoverageCheck
    forall o (m :: * -> *) i. MonadState o m => Lens' i o -> m i
    use Lens' CoverageCheck NiceEnv
    coverageCheckPragma
              ([NiceDeclaration], [Declaration])
    -> Nice ([NiceDeclaration], [Declaration])
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([Range
    -> Access
    -> IsAbstract
    -> IsInstance
    -> TerminationCheck
    -> CoverageCheck
    -> [Name]
    -> Expr
    -> NiceDeclaration
    NiceUnquoteDecl Range
    r Access
    PublicAccess IsAbstract
    ConcreteDef IsInstance
    NotInstanceDef TerminationCheck
    tc CoverageCheck
    cc [Name]
    xs Expr
    e] , [Declaration]
    ds)

            UnquoteDef Range
    r [Name]
    xs Expr
    e -> do
              [Name]
    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' LoneSigs NiceEnv -> Nice LoneSigs
    forall o (m :: * -> *) i. MonadState o m => Lens' i o -> m i
    use Lens' LoneSigs NiceEnv
    loneSigs
              [Name]
    -> (List1 Name -> Nice ([NiceDeclaration], [Declaration]))
    -> Nice ([NiceDeclaration], [Declaration])
    -> Nice ([NiceDeclaration], [Declaration])
    forall a b. [a] -> (List1 a -> b) -> b -> b
    List1.ifNotNull ((Name -> Bool) -> [Name] -> [Name]
    forall a. (a -> Bool) -> [a] -> [a]
    filter (Name -> [Name] -> Bool
    forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
    `notElem` [Name]
    sigs) [Name]
    xs)
                {-then-} (DeclarationException' -> Nice ([NiceDeclaration], [Declaration])
    forall a. HasCallStack => DeclarationException' -> Nice a
    declarationException (DeclarationException' -> Nice ([NiceDeclaration], [Declaration]))
    -> (List1 Name -> DeclarationException')
    -> List1 Name
    -> Nice ([NiceDeclaration], [Declaration])
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . List1 Name -> DeclarationException'
    UnquoteDefRequiresSignature)
                {-else-} (Nice ([NiceDeclaration], [Declaration])
     -> Nice ([NiceDeclaration], [Declaration]))
    -> Nice ([NiceDeclaration], [Declaration])
    -> Nice ([NiceDeclaration], [Declaration])
    forall a b. (a -> b) -> a -> b
    $ 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], [Declaration])
    -> Nice ([NiceDeclaration], [Declaration])
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([Range
    -> Access
    -> IsAbstract
    -> TerminationCheck
    -> CoverageCheck
    -> [Name]
    -> Expr
    -> NiceDeclaration
    NiceUnquoteDef Range
    r Access
    PublicAccess IsAbstract
    ConcreteDef TerminationCheck
    forall m. TerminationCheck m
    TerminationCheck CoverageCheck
    YesCoverageCheck [Name]
    xs Expr
    e] , [Declaration]
    ds)

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

        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
            Bool
    -> Nice ([NiceDeclaration], [Declaration])
    -> Nice ([NiceDeclaration], [Declaration])
    forall a. Bool -> Nice a -> Nice a
    withCatchallPragma Bool
    True (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
          HasCallStack => DeclarationWarning' -> Nice ()
    DeclarationWarning' -> Nice ()
    declarationWarning (DeclarationWarning' -> Nice ()) -> DeclarationWarning' -> Nice ()
    forall a b. (a -> b) -> a -> b
    $ Range -> DeclarationWarning'
    PragmaCompiled (Pragma -> Range
    forall a. HasRange a => a -> Range
    getRange Pragma
    p)
          ([NiceDeclaration], [Declaration])
    -> Nice ([NiceDeclaration], [Declaration])
    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 (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 (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 Pragma
    p [Declaration]
    ds = ([NiceDeclaration], [Declaration])
    -> Nice ([NiceDeclaration], [Declaration])
    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 Range
    _ [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 Range
    _ [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 -> TacticAttribute -> Nice TacticAttribute
    defaultTypeSig DataRecOrFun
    k Name
    x t :: TacticAttribute
    t@Just{} = TacticAttribute -> Nice TacticAttribute
    forall (m :: * -> *) a. Monad m => a -> m a
    return TacticAttribute
    t
        defaultTypeSig DataRecOrFun
    k Name
    x TacticAttribute
    Nothing  = do
          Nice (Maybe DataRecOrFun)
    -> Nice TacticAttribute
    -> (DataRecOrFun -> Nice TacticAttribute)
    -> Nice TacticAttribute
    forall (m :: * -> *) a b.
    Monad m =>
    m (Maybe a) -> m b -> (a -> m b) -> m b
    caseMaybeM (Name -> Nice (Maybe DataRecOrFun)
    getSig Name
    x) (TacticAttribute -> Nice TacticAttribute
    forall (m :: * -> *) a. Monad m => a -> m a
    return TacticAttribute
    forall a. Maybe a
    Nothing) ((DataRecOrFun -> Nice TacticAttribute) -> Nice TacticAttribute)
    -> (DataRecOrFun -> Nice TacticAttribute) -> Nice TacticAttribute
    forall a b. (a -> b) -> a -> b
    $ \ DataRecOrFun
    k' -> do
            Bool -> Nice () -> Nice ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    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
            TacticAttribute
    forall a. Maybe a
    Nothing TacticAttribute -> Nice () -> Nice TacticAttribute
    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
          Maybe ([LamBinding], [decl])
    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 :: Origin
    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
          [NiceDeclaration] -> Nice [NiceDeclaration]
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([NiceDeclaration] -> Nice [NiceDeclaration])
    -> [NiceDeclaration] -> Nice [NiceDeclaration]
    forall a b. (a -> b) -> a -> b
    $ [Maybe NiceDeclaration] -> [NiceDeclaration]
    forall a. [Maybe a] -> [a]
    catMaybes ([Maybe NiceDeclaration] -> [NiceDeclaration])
    -> [Maybe NiceDeclaration] -> [NiceDeclaration]
    forall a b. (a -> b) -> a -> b
    $
            [ Maybe ([LamBinding], Expr)
    mt  Maybe ([LamBinding], Expr)
    -> (([LamBinding], Expr) -> NiceDeclaration)
    -> Maybe NiceDeclaration
    forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
    <&> \ ([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
            , Maybe ([LamBinding], [decl])
    mds Maybe ([LamBinding], [decl])
    -> (([LamBinding], [decl]) -> NiceDeclaration)
    -> Maybe NiceDeclaration
    forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
    <&> \ ([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)
    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 (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 (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 Range
    r [Declaration]
    decls -> do
            Range -> [NiceDeclaration] -> Nice [NiceDeclaration]
    instanceBlock Range
    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
          Pragma p :: Pragma
    p@(RewritePragma Range
    r Range
    _ [QName]
    _) -> do
            [NiceDeclaration] -> Nice [NiceDeclaration]
    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
    -> TacticAttribute
    -> [Declaration]
    -> Nice [NiceDeclaration]
    mkFunDef ArgInfo
    info TerminationCheck
    termCheck CoverageCheck
    covCheck Name
    x TacticAttribute
    mt [Declaration]
    ds0 = do
          [Declaration]
    ds <- [Declaration] -> Nice [Declaration]
    expandEllipsis [Declaration]
    ds0
          [Clause]
    cs <- Name -> [Declaration] -> Bool -> Nice [Clause]
    mkClauses Name
    x [Declaration]
    ds Bool
    False
          [NiceDeclaration] -> Nice [NiceDeclaration]
    forall (m :: * -> *) a. Monad m => a -> m a
    return [ Range
    -> Access
    -> IsAbstract
    -> IsInstance
    -> IsMacro
    -> ArgInfo
    -> TerminationCheck
    -> CoverageCheck
    -> Name
    -> Expr
    -> NiceDeclaration
    FunSig (Name -> Expr -> Range
    forall u t. (HasRange u, HasRange t) => u -> t -> Range
    fuseRange Name
    x Expr
    t) Access
    PublicAccess IsAbstract
    ConcreteDef IsInstance
    NotInstanceDef IsMacro
    NotMacroDef ArgInfo
    info TerminationCheck
    termCheck CoverageCheck
    covCheck Name
    x Expr
    t
                 , Range
    -> [Declaration]
    -> IsAbstract
    -> IsInstance
    -> TerminationCheck
    -> CoverageCheck
    -> Name
    -> [Clause]
    -> NiceDeclaration
    FunDef ([Declaration] -> Range
    forall a. HasRange a => a -> Range
    getRange [Declaration]
    ds0) [Declaration]
    ds0 IsAbstract
    ConcreteDef IsInstance
    NotInstanceDef TerminationCheck
    termCheck CoverageCheck
    covCheck Name
    x [Clause]
    cs ]
            where
              t :: Expr
    t = Expr -> TacticAttribute -> Expr
    forall a. a -> Maybe a -> a
    fromMaybe (Range -> Expr
    underscore (Name -> Range
    forall a. HasRange a => a -> Range
    getRange Name
    x)) TacticAttribute
    mt

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

        expandEllipsis :: [Declaration] -> Nice [Declaration]
        expandEllipsis :: [Declaration] -> Nice [Declaration]
    expandEllipsis [] = [Declaration] -> Nice [Declaration]
    forall (m :: * -> *) a. Monad m => a -> m a
    return []
        expandEllipsis (d :: Declaration
    d@(FunClause lhs :: LHS
    lhs@(LHS Pattern
    p [RewriteEqn]
    _ [WithExpr]
    _) RHS
    _ WhereClause
    _ Bool
    _) : [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 (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 Bool
    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 -> Bool -> Declaration
    FunClause (Pattern -> [RewriteEqn] -> [WithExpr] -> LHS
    LHS Pattern
    p1 [RewriteEqn]
    eqs [WithExpr]
    es) RHS
    rhs WhereClause
    wh Bool
    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] -> Bool -> Nice [Clause]
    mkClauses Name
    _ [] Bool
    _ = [Clause] -> Nice [Clause]
    forall (m :: * -> *) a. Monad m => a -> m a
    return []
        mkClauses Name
    x (Pragma (CatchallPragma Range
    r) : [Declaration]
    cs) Bool
    True  = do
          HasCallStack => DeclarationWarning' -> Nice ()
    DeclarationWarning' -> Nice ()
    declarationWarning (DeclarationWarning' -> Nice ()) -> DeclarationWarning' -> Nice ()
    forall a b. (a -> b) -> a -> b
    $ Range -> DeclarationWarning'
    InvalidCatchallPragma Range
    r
          Name -> [Declaration] -> Bool -> Nice [Clause]
    mkClauses Name
    x [Declaration]
    cs Bool
    True
        mkClauses Name
    x (Pragma (CatchallPragma Range
    r) : [Declaration]
    cs) Bool
    False = do
          Bool -> Nice () -> Nice ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    when ([Declaration] -> Bool
    forall a. Null a => a -> Bool
    null [Declaration]
    cs) (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] -> Bool -> Nice [Clause]
    mkClauses Name
    x [Declaration]
    cs Bool
    True

        mkClauses Name
    x (FunClause LHS
    lhs RHS
    rhs WhereClause
    wh Bool
    ca : [Declaration]
    cs) Bool
    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 -> Bool -> LHS -> RHS -> WhereClause -> [Clause] -> Clause
    Clause Name
    x (Bool
    ca Bool -> Bool -> Bool
    || Bool
    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] -> Bool -> Nice [Clause]
    mkClauses Name
    x [Declaration]
    cs Bool
    False   -- Will result in an error later.

        mkClauses Name
    x (FunClause LHS
    lhs RHS
    rhs WhereClause
    wh Bool
    ca : [Declaration]
    cs) Bool
    catchall = do
          Bool -> Nice () -> Nice ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    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
          [Clause]
    wcs <- Name -> [Declaration] -> Bool -> Nice [Clause]
    mkClauses Name
    x [Declaration]
    withClauses Bool
    False
          (Name -> Bool -> LHS -> RHS -> WhereClause -> [Clause] -> Clause
    Clause Name
    x (Bool
    ca Bool -> Bool -> Bool
    || Bool
    catchall) LHS
    lhs RHS
    rhs WhereClause
    wh [Clause]
    wcs 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] -> Bool -> Nice [Clause]
    mkClauses Name
    x [Declaration]
    cs' Bool
    False
          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 (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
    _ Bool
    _) : [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]
    _ Bool
    _ = 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 :: [Name]
    pns        = Pattern -> [Name]
    patternNames 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]
    pns
          in
    --          trace ("x = " ++ prettyShow x) $
    --          trace ("pns = " ++ show pns) $
    --          trace ("xStrings = " ++ show xStrings) $
    --          trace ("patStrings = " ++ show patStrings) $
    --          trace ("mFixity = " ++ show mFixity) $
          case ([Name] -> Maybe Name
    forall a. [a] -> Maybe a
    listToMaybe [Name]
    pns, Maybe Fixity'
    mFixity) of
            -- first identifier in the patterns is the fun.symbol?
            (Just Name
    y, Maybe Fixity'
    _) | Name
    x Name -> Name -> Bool
    forall a. Eq a => a -> a -> Bool
    == Name
    y -> Bool
    True -- trace ("couldBe since y = " ++ prettyShow y) $ True
            -- are the parts of x contained in p
            (Maybe Name, Maybe Fixity')
    _ | [String]
    xStrings [String] -> [String] -> Bool
    forall a. Eq a => [a] -> [a] -> Bool
    `isSublistOf` [String]
    patStrings -> Bool
    True -- trace ("couldBe since isSublistOf") $ True
            -- looking for a mixfix fun.symb
            (Maybe Name
    _, 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
    `isSublistOf` [String]
    patStrings)
            -- not a notation, not first id: give up
            (Maybe Name, 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 Bool
    _ Declaration
    d)
          = ([TerminationCheck]
    -> [CoverageCheck] -> [PositivityCheck] -> MutualChecks
    MutualChecks [TerminationCheck
    tc] [CoverageCheck
    cc] [], Declaration
    d) (MutualChecks, Declaration)
    -> Maybe () -> Maybe (MutualChecks, Declaration)
    forall (f :: * -> *) a b. Functor f => a -> f b -> f a
    <$ Bool -> Maybe ()
    forall (f :: * -> *). Alternative f => Bool -> f ()
    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
    _ Bool
    _) =
           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
          :: Range                 -- Range of the whole @mutual@ block.
          -> [NiceDeclaration]     -- Declarations inside the block.
          -> Nice NiceDeclaration  -- Returns a 'NiceMutual'.
        mkInterleavedMutual :: Range -> [NiceDeclaration] -> Nice NiceDeclaration
    mkInterleavedMutual Range
    r [NiceDeclaration]
    ds' = do
          ([(Int, NiceDeclaration)]
    other, (InterleavedMutual
    m, MutualChecks
    checks, Int
    _)) <- 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 (Range
    -> [NiceDeclaration]
    -> StateT
         (InterleavedMutual, MutualChecks, Int)
         Nice
         [(Int, NiceDeclaration)]
    groupByBlocks Range
    r [NiceDeclaration]
    ds') (InterleavedMutual
    forall a. Null a => a
    empty, MutualChecks
    forall a. Monoid a => a
    mempty, Int
    0)
          let idecls :: [(Int, NiceDeclaration)]
    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 :: [NiceDeclaration]
    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
          LoneSigs
    ps <- Lens' LoneSigs NiceEnv -> Nice LoneSigs
    forall o (m :: * -> *) i. MonadState o m => Lens' i o -> m i
    use Lens' LoneSigs NiceEnv
    loneSigs
          LoneSigs -> Nice ()
    checkLoneSigs LoneSigs
    ps
          let decls :: [NiceDeclaration]
    decls = LoneSigs -> [NiceDeclaration] -> [NiceDeclaration]
    replaceSigs LoneSigs
    ps [NiceDeclaration]
    decls0
          -- process the checks
          TerminationCheck
    tc <- Range -> [TerminationCheck] -> Nice TerminationCheck
    combineTerminationChecks Range
    r (MutualChecks -> [TerminationCheck]
    mutualTermination MutualChecks
    checks)
          let cc :: CoverageCheck
    cc = [CoverageCheck] -> CoverageCheck
    combineCoverageChecks   (MutualChecks -> [CoverageCheck]
    mutualCoverage MutualChecks
    checks)
          let pc :: PositivityCheck
    pc = [PositivityCheck] -> PositivityCheck
    combinePositivityChecks (MutualChecks -> [PositivityCheck]
    mutualPositivity MutualChecks
    checks)
          NiceDeclaration -> Nice NiceDeclaration
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (NiceDeclaration -> Nice NiceDeclaration)
    -> NiceDeclaration -> Nice NiceDeclaration
    forall a b. (a -> b) -> a -> b
    $ Range
    -> TerminationCheck
    -> CoverageCheck
    -> PositivityCheck
    -> [NiceDeclaration]
    -> NiceDeclaration
    NiceMutual Range
    r TerminationCheck
    tc CoverageCheck
    cc PositivityCheck
    pc [NiceDeclaration]
    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
              (Map Name a
    m, MutualChecks
    checks, Int
    i) <- StateT
      (Map Name a, MutualChecks, Int)
      Nice
      (Map Name a, MutualChecks, Int)
    forall s (m :: * -> *). MonadState s m => m s
    get
              Bool
    -> StateT (Map Name a, MutualChecks, Int) Nice ()
    -> StateT (Map Name a, MutualChecks, Int) Nice ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    when (Maybe a -> Bool
    forall a. Maybe a -> Bool
    isJust (Maybe a -> Bool) -> Maybe a -> Bool
    forall a b. (a -> b) -> a -> b
    $ Name -> Map Name a -> Maybe a
    forall k a. Ord k => k -> Map k a -> Maybe a
    Map.lookup Name
    n Map Name a
    m) (StateT (Map Name a, MutualChecks, Int) Nice ()
     -> StateT (Map Name a, MutualChecks, Int) Nice ())
    -> StateT (Map Name a, MutualChecks, Int) Nice ()
    -> StateT (Map Name a, MutualChecks, Int) Nice ()
    forall a b. (a -> b) -> a -> b
    $ Nice () -> StateT (Map Name a, MutualChecks, Int) Nice ()
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (Nice () -> StateT (Map Name a, MutualChecks, Int) Nice ())
    -> Nice () -> StateT (Map Name a, 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
    $ Name -> DeclarationException'
    DuplicateDefinition Name
    n
              (Map Name a, MutualChecks, Int)
    -> StateT (Map Name a, MutualChecks, Int) Nice ()
    forall s (m :: * -> *). MonadState s m => s -> m ()
    put (Name -> a -> Map Name a -> Map Name a
    forall k a. Ord k => k -> a -> Map k a -> Map k a
    Map.insert Name
    n (Int -> a
    c Int
    i) Map Name a
    m, MutualChecks
    mc MutualChecks -> MutualChecks -> MutualChecks
    forall a. Semigroup a => a -> a -> a
    <> MutualChecks
    checks, Int
    iInt -> Int -> Int
    forall a. Num a => a -> a -> a
    +Int
    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
    _ 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
              (InterleavedMutual
    m, MutualChecks
    checks, Int
    i) <- StateT
      (InterleavedMutual, MutualChecks, Int)
      Nice
      (InterleavedMutual, MutualChecks, Int)
    forall s (m :: * -> *). MonadState s m => m s
    get
              case Name -> InterleavedMutual -> Maybe InterleavedDecl
    forall k a. Ord k => k -> Map k a -> Maybe a
    Map.lookup Name
    n InterleavedMutual
    m of
                Just (InterleavedData Int
    i0 NiceDeclaration
    sig Maybe (Int, List1 [NiceDeclaration])
    cs) -> do
                  Nice () -> StateT (InterleavedMutual, MutualChecks, Int) Nice ()
    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
    iInt -> 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 (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, Range)] -> DeclarationWarning'
    MissingDeclarations ([(Name, Range)] -> DeclarationWarning')
    -> [(Name, Range)] -> DeclarationWarning'
    forall a b. (a -> b) -> a -> b
    $ case Maybe Range
    mr of
                       Just Range
    r -> [(Name
    n, Range
    r)]
                       Maybe Range
    Nothing -> ((NiceDeclaration -> [(Name, Range)])
     -> [NiceDeclaration] -> [(Name, Range)])
    -> [NiceDeclaration]
    -> (NiceDeclaration -> [(Name, Range)])
    -> [(Name, Range)]
    forall a b c. (a -> b -> c) -> b -> a -> c
    flip (NiceDeclaration -> [(Name, Range)])
    -> [NiceDeclaration] -> [(Name, Range)]
    forall (t :: * -> *) m a.
    (Foldable t, Monoid m) =>
    (a -> m) -> t a -> m
    foldMap [NiceDeclaration]
    ds ((NiceDeclaration -> [(Name, Range)]) -> [(Name, Range)])
    -> (NiceDeclaration -> [(Name, Range)]) -> [(Name, Range)]
    forall a b. (a -> b) -> a -> b
    $ \case
                         Axiom Range
    r Access
    _ IsAbstract
    _ IsInstance
    _ ArgInfo
    _ Name
    n Expr
    _ -> [(Name
    n, Range
    r)]
                         NiceDeclaration
    _ -> [(Name, Range)]
    forall a. HasCallStack => a
    __IMPOSSIBLE__

            addDataConstructors Maybe Range
    mr Maybe Name
    Nothing [] = () -> StateT (InterleavedMutual, MutualChecks, Int) Nice ()
    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
              (InterleavedMutual
    m, MutualChecks
    _, Int
    _) <- StateT
      (InterleavedMutual, MutualChecks, Int)
      Nice
      (InterleavedMutual, MutualChecks, Int)
    forall s (m :: * -> *). MonadState s m => m s
    get
              let sigs :: [Name]
    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 (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 [Name] -> NiceDeclaration -> Either (Name, [Name]) Name
    isConstructor [Name]
    sigs NiceDeclaration
    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 (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] []
              (InterleavedMutual
    m, MutualChecks
    checks, Int
    i) <- StateT
      (InterleavedMutual, MutualChecks, Int)
      Nice
      (InterleavedMutual, MutualChecks, Int)
    forall s (m :: * -> *). MonadState s m => m s
    get
              case Name -> InterleavedMutual -> Maybe InterleavedDecl
    forall k a. Ord k => k -> Map k a -> Maybe a
    Map.lookup Name
    n InterleavedMutual
    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
    iInt -> 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 :: Range -> [NiceDeclaration]
                          -> StateT (InterleavedMutual, MutualChecks, DeclNum) Nice [(DeclNum, NiceDeclaration)]
            addFunClauses :: Range
    -> [NiceDeclaration]
    -> StateT
         (InterleavedMutual, MutualChecks, Int)
         Nice
         [(Int, NiceDeclaration)]
    addFunClauses Range
    r (nd :: NiceDeclaration
    nd@(NiceFunClause Range
    _ Access
    _ IsAbstract
    _ TerminationCheck
    tc CoverageCheck
    cc Bool
    _ d :: Declaration
    d@(FunClause LHS
    lhs RHS
    _ WhereClause
    _ Bool
    _)) : [NiceDeclaration]
    ds) = do
              -- get the candidate functions that are in this interleaved mutual block
              (InterleavedMutual
    m, MutualChecks
    checks, Int
    i) <- StateT
      (InterleavedMutual, MutualChecks, Int)
      Nice
      (InterleavedMutual, MutualChecks, Int)
    forall s (m :: * -> *). MonadState s m => m s
    get
              let sigs :: [Name]
    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 (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 [ (Name
    x, Prefix (MutualChecks, Declaration)
    fits, [NiceDeclaration]
    rest)
                   | Name
    x <- [Name]
    sigs
                   , let (Prefix (MutualChecks, Declaration)
    fits, [NiceDeclaration]
    rest) = (NiceDeclaration -> Maybe (MutualChecks, Declaration))
    -> [NiceDeclaration]
    -> (Prefix (MutualChecks, Declaration), [NiceDeclaration])
    forall a b. (a -> Maybe b) -> [a] -> (Prefix b, [a])
    spanJust (Maybe Fixity'
    -> Name -> NiceDeclaration -> Maybe (MutualChecks, Declaration)
    couldBeNiceFunClauseOf (Name -> Fixities -> Maybe Fixity'
    forall k a. Ord k => k -> Map k a -> Maybe a
    Map.lookup Name
    x Fixities
    fixs) Name
    x) (NiceDeclaration
    nd NiceDeclaration -> [NiceDeclaration] -> [NiceDeclaration]
    forall a. a -> [a] -> [a]
    : [NiceDeclaration]
    ds)
                   , Bool -> Bool
    not (Prefix (MutualChecks, Declaration) -> Bool
    forall a. Null a => a -> Bool
    null Prefix (MutualChecks, Declaration)
    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
    iInt -> 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
    <$> Range
    -> [NiceDeclaration]
    -> StateT
         (InterleavedMutual, MutualChecks, Int)
         Nice
         [(Int, NiceDeclaration)]
    groupByBlocks Range
    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
                  [Declaration]
    ds <- Nice [Declaration]
    -> StateT (InterleavedMutual, MutualChecks, Int) Nice [Declaration]
    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
                  [Clause]
    cs <- Nice [Clause]
    -> StateT (InterleavedMutual, MutualChecks, Int) Nice [Clause]
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (Nice [Clause]
     -> StateT (InterleavedMutual, MutualChecks, Int) Nice [Clause])
    -> Nice [Clause]
    -> StateT (InterleavedMutual, MutualChecks, Int) Nice [Clause]
    forall a b. (a -> b) -> a -> b
    $ Name -> [Declaration] -> Bool -> Nice [Clause]
    mkClauses Name
    n [Declaration]
    ds Bool
    False
                  case Name -> InterleavedMutual -> Maybe InterleavedDecl
    forall k a. Ord k => k -> Map k a -> Maybe a
    Map.lookup Name
    n InterleavedMutual
    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
    iInt -> 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 (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__
                  Range
    -> [NiceDeclaration]
    -> StateT
         (InterleavedMutual, MutualChecks, Int)
         Nice
         [(Int, NiceDeclaration)]
    groupByBlocks Range
    r [NiceDeclaration]
    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 (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 (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 Range
    _ [NiceDeclaration]
    _ = StateT
      (InterleavedMutual, MutualChecks, Int)
      Nice
      [(Int, NiceDeclaration)]
    forall a. HasCallStack => a
    __IMPOSSIBLE__

            groupByBlocks :: Range -> [NiceDeclaration]
                          -> StateT (InterleavedMutual, MutualChecks, DeclNum) Nice [(DeclNum, NiceDeclaration)]
            groupByBlocks :: Range
    -> [NiceDeclaration]
    -> StateT
         (InterleavedMutual, MutualChecks, Int)
         Nice
         [(Int, NiceDeclaration)]
    groupByBlocks Range
    r []       = [(Int, NiceDeclaration)]
    -> StateT
         (InterleavedMutual, MutualChecks, Int)
         Nice
         [(Int, NiceDeclaration)]
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure []
            groupByBlocks Range
    r (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 (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
    <$> Range
    -> [NiceDeclaration]
    -> StateT
         (InterleavedMutual, MutualChecks, Int)
         Nice
         [(Int, NiceDeclaration)]
    groupByBlocks Range
    r [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 (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 (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 Range
    r [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 (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 (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 (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{}              -> Range
    -> [NiceDeclaration]
    -> StateT
         (InterleavedMutual, MutualChecks, Int)
         Nice
         [(Int, NiceDeclaration)]
    addFunClauses Range
    r (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
                  (InterleavedMutual
    m, MutualChecks
    c, Int
    i) <- StateT
      (InterleavedMutual, MutualChecks, Int)
      Nice
      (InterleavedMutual, MutualChecks, Int)
    forall s (m :: * -> *). MonadState s m => m s
    get -- TODO: grab checks from c?
                  (InterleavedMutual, MutualChecks, Int)
    -> StateT (InterleavedMutual, MutualChecks, Int) Nice ()
    forall s (m :: * -> *). MonadState s m => s -> m ()
    put (InterleavedMutual
    m, MutualChecks
    c, Int
    iInt -> Int -> Int
    forall a. Num a => a -> a -> a
    +Int
    1)
                  [(Int, NiceDeclaration)]
    -> StateT
         (InterleavedMutual, MutualChecks, Int)
         Nice
         [(Int, NiceDeclaration)]
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure [(Int
    i,NiceDeclaration
    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) -> TacticAttribute -> Maybe Pattern
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Expr -> TacticAttribute
    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
          :: Range                 -- Range of the whole @mutual@ block.
          -> [NiceDeclaration]     -- Declarations inside the block.
          -> Nice NiceDeclaration  -- Returns a 'NiceMutual'.
        mkOldMutual :: Range -> [NiceDeclaration] -> Nice NiceDeclaration
    mkOldMutual Range
    r [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.
            ([NiceDeclaration]
    top, [NiceDeclaration]
    bottom, [NiceDeclaration]
    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 (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 (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 (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
                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

                  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
                  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
            TerminationCheck
    tc0 <- Lens' TerminationCheck NiceEnv -> Nice TerminationCheck
    forall o (m :: * -> *) i. MonadState o m => Lens' i o -> m i
    use Lens' TerminationCheck NiceEnv
    terminationCheckPragma
            let tcs :: [TerminationCheck]
    tcs = (NiceDeclaration -> TerminationCheck)
    -> [NiceDeclaration] -> [TerminationCheck]
    forall a b. (a -> b) -> [a] -> [b]
    map NiceDeclaration -> TerminationCheck
    termCheck [NiceDeclaration]
    ds
            TerminationCheck
    tc <- Range -> [TerminationCheck] -> Nice TerminationCheck
    combineTerminationChecks Range
    r (TerminationCheck
    tc0TerminationCheck -> [TerminationCheck] -> [TerminationCheck]
    forall a. a -> [a] -> [a]
    :[TerminationCheck]
    tcs)

            -- Compute coverage checking flag for mutual block
            CoverageCheck
    cc0 <- Lens' CoverageCheck NiceEnv -> Nice CoverageCheck
    forall o (m :: * -> *) i. MonadState o m => Lens' i o -> m i
    use Lens' CoverageCheck NiceEnv
    coverageCheckPragma
            let ccs :: [CoverageCheck]
    ccs = (NiceDeclaration -> CoverageCheck)
    -> [NiceDeclaration] -> [CoverageCheck]
    forall a b. (a -> b) -> [a] -> [b]
    map NiceDeclaration -> CoverageCheck
    covCheck [NiceDeclaration]
    ds
            let cc :: CoverageCheck
    cc = [CoverageCheck] -> CoverageCheck
    combineCoverageChecks (CoverageCheck
    cc0CoverageCheck -> [CoverageCheck] -> [CoverageCheck]
    forall a. a -> [a] -> [a]
    :[CoverageCheck]
    ccs)

            -- Compute positivity checking flag for mutual block
            PositivityCheck
    pc0 <- Lens' PositivityCheck NiceEnv -> Nice PositivityCheck
    forall o (m :: * -> *) i. MonadState o m => Lens' i o -> m i
    use Lens' PositivityCheck NiceEnv
    positivityCheckPragma
            let pcs :: [PositivityCheck]
    pcs = (NiceDeclaration -> PositivityCheck)
    -> [NiceDeclaration] -> [PositivityCheck]
    forall a b. (a -> b) -> [a] -> [b]
    map NiceDeclaration -> PositivityCheck
    positivityCheckOldMutual [NiceDeclaration]
    ds
            let pc :: PositivityCheck
    pc = [PositivityCheck] -> PositivityCheck
    combinePositivityChecks (PositivityCheck
    pc0PositivityCheck -> [PositivityCheck] -> [PositivityCheck]
    forall a. a -> [a] -> [a]
    :[PositivityCheck]
    pcs)

            NiceDeclaration -> Nice NiceDeclaration
    forall (m :: * -> *) a. Monad m => a -> m a
    return (NiceDeclaration -> Nice NiceDeclaration)
    -> NiceDeclaration -> Nice NiceDeclaration
    forall a b. (a -> b) -> a -> b
    $ Range
    -> TerminationCheck
    -> CoverageCheck
    -> PositivityCheck
    -> [NiceDeclaration]
    -> NiceDeclaration
    NiceMutual Range
    r TerminationCheck
    tc CoverageCheck
    cc PositivityCheck
    pc ([NiceDeclaration] -> NiceDeclaration)
    -> [NiceDeclaration] -> NiceDeclaration
    forall a b. (a -> b) -> a -> b
    $ [NiceDeclaration]
    top [NiceDeclaration] -> [NiceDeclaration] -> [NiceDeclaration]
    forall a. [a] -> [a] -> [a]
    ++ [NiceDeclaration]
    bottom
            -- return $ NiceMutual r tc pc $ other ++ defs
            -- return $ NiceMutual r tc pc $ sigs ++ other
          where

            -- isTypeSig Axiom{}                     = True
            -- isTypeSig d | LoneSig{} <- declKind d = True
            -- isTypeSig _                           = False

            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 Range
    _ 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

            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 Range
    _ 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

            -- 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
    _ Access
    _ IsAbstract
    _ PositivityCheck
    pc UniverseCheck
    _ Name
    _ [LamBinding]
    _ Expr
    _) = PositivityCheck
    pc
            positivityCheckOldMutual (NiceMutual Range
    _ TerminationCheck
    _ CoverageCheck
    _ PositivityCheck
    pc [NiceDeclaration]
    _)        = PositivityCheck
    pc
            positivityCheckOldMutual (NiceRecSig Range
    _ Access
    _ IsAbstract
    _ PositivityCheck
    pc UniverseCheck
    _ Name
    _ [LamBinding]
    _ Expr
    _)  = PositivityCheck
    pc
            positivityCheckOldMutual (NiceRecDef Range
    _ Origin
    _ IsAbstract
    _ PositivityCheck
    pc UniverseCheck
    _ Name
    _ RecordDirectives
    _ [LamBinding]
    _ [Declaration]
    _) = PositivityCheck
    pc
            positivityCheckOldMutual NiceDeclaration
    _                              = PositivityCheck
    YesPositivityCheck

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

        abstractBlock :: Range -> [a] -> Nice [a]
    abstractBlock Range
    _ [] = [a] -> Nice [a]
    forall (m :: * -> *) a. Monad m => a -> m a
    return []
        abstractBlock Range
    r [a]
    ds = do
          ([a]
    ds', Bool
    anyChange) <- ChangeT Nice [a] -> Nice ([a], Bool)
    forall (m :: * -> *) a. Functor m => ChangeT m a -> m (a, Bool)
    runChangeT (ChangeT Nice [a] -> Nice ([a], Bool))
    -> ChangeT Nice [a] -> Nice ([a], Bool)
    forall a b. (a -> b) -> a -> b
    $ UpdaterT Nice [a]
    forall a. MakeAbstract a => UpdaterT Nice a
    mkAbstract [a]
    ds
          let inherited :: Bool
    inherited = Range
    r Range -> Range -> Bool
    forall a. Eq a => a -> a -> Bool
    == Range
    forall a. Range' a
    noRange
          if Bool
    anyChange then [a] -> Nice [a]
    forall (m :: * -> *) a. Monad m => a -> m a
    return [a]
    ds' else do
            -- hack to avoid failing on inherited abstract blocks in where clauses
            Bool -> Nice () -> Nice ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    unless Bool
    inherited (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'
    UselessAbstract Range
    r
            [a] -> Nice [a]
    forall (m :: * -> *) a. Monad m => a -> m a
    return [a]
    ds -- no change!

        privateBlock :: Range -> Origin -> [a] -> Nice [a]
    privateBlock Range
    _ Origin
    _ [] = [a] -> Nice [a]
    forall (m :: * -> *) a. Monad m => a -> m a
    return []
        privateBlock Range
    r Origin
    o [a]
    ds = do
          ([a]
    ds', Bool
    anyChange) <- ChangeT Nice [a] -> Nice ([a], Bool)
    forall (m :: * -> *) a. Functor m => ChangeT m a -> m (a, Bool)
    runChangeT (ChangeT Nice [a] -> Nice ([a], Bool))
    -> ChangeT Nice [a] -> Nice ([a], Bool)
    forall a b. (a -> b) -> a -> b
    $ Origin -> UpdaterT Nice [a]
    forall a. MakePrivate a => Origin -> UpdaterT Nice a
    mkPrivate Origin
    o [a]
    ds
          if Bool
    anyChange then [a] -> Nice [a]
    forall (m :: * -> *) a. Monad m => a -> m a
    return [a]
    ds' else do
            Bool -> Nice () -> Nice ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    when (Origin
    o Origin -> Origin -> Bool
    forall a. Eq a => a -> a -> Bool
    == Origin
    UserWritten) (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'
    UselessPrivate Range
    r
            [a] -> Nice [a]
    forall (m :: * -> *) a. Monad m => a -> m a
    return [a]
    ds -- no change!

        instanceBlock
          :: Range  -- Range of @instance@ keyword.
          -> [NiceDeclaration]
          -> Nice [NiceDeclaration]
        instanceBlock :: Range -> [NiceDeclaration] -> Nice [NiceDeclaration]
    instanceBlock Range
    _ [] = [NiceDeclaration] -> Nice [NiceDeclaration]
    forall (m :: * -> *) a. Monad m => a -> m a
    return []
        instanceBlock Range
    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)
    mapM (Range -> NiceDeclaration -> ChangeT Identity NiceDeclaration
    mkInstance Range
    r) [NiceDeclaration]
    ds
          if Bool
    anyChange then [NiceDeclaration] -> Nice [NiceDeclaration]
    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
    $ Range -> DeclarationWarning'
    UselessInstance Range
    r
            [NiceDeclaration] -> Nice [NiceDeclaration]
    forall (m :: * -> *) a. Monad m => a -> m a
    return [NiceDeclaration]
    ds -- no change!

        -- Make a declaration eligible for instance search.
        mkInstance
          :: Range  -- Range of @instance@ keyword.
          -> Updater NiceDeclaration
        mkInstance :: Range -> NiceDeclaration -> ChangeT Identity NiceDeclaration
    mkInstance Range
    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
    <$> Range -> Updater IsInstance
    setInstance Range
    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
    <$> Range -> Updater IsInstance
    setInstance Range
    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
    <$> Range -> Updater IsInstance
    setInstance Range
    r0 IsInstance
    i
            NiceMutual Range
    r TerminationCheck
    tc CoverageCheck
    cc PositivityCheck
    pc [NiceDeclaration]
    ds       -> Range
    -> TerminationCheck
    -> CoverageCheck
    -> PositivityCheck
    -> [NiceDeclaration]
    -> NiceDeclaration
    NiceMutual Range
    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)
    mapM (Range -> NiceDeclaration -> ChangeT Identity NiceDeclaration
    mkInstance Range
    r0) [NiceDeclaration]
    ds
            NiceLoneConstructor Range
    r [NiceDeclaration]
    ds       -> Range -> [NiceDeclaration] -> NiceDeclaration
    NiceLoneConstructor Range
    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)
    mapM (Range -> NiceDeclaration -> ChangeT Identity NiceDeclaration
    mkInstance Range
    r0) [NiceDeclaration]
    ds
            d :: NiceDeclaration
    d@NiceFunClause{}              -> NiceDeclaration -> ChangeT Identity NiceDeclaration
    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
    <$> Range -> Updater IsInstance
    setInstance Range
    r0 IsInstance
    i
            d :: NiceDeclaration
    d@NiceField{}                  -> NiceDeclaration -> ChangeT Identity NiceDeclaration
    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 (m :: * -> *) a. Monad m => a -> m a
    return NiceDeclaration
    d
            d :: NiceDeclaration
    d@NiceUnquoteDef{}             -> NiceDeclaration -> ChangeT Identity NiceDeclaration
    forall (m :: * -> *) a. Monad m => a -> m a
    return NiceDeclaration
    d
            d :: NiceDeclaration
    d@NiceRecSig{}                 -> NiceDeclaration -> ChangeT Identity NiceDeclaration
    forall (m :: * -> *) a. Monad m => a -> m a
    return NiceDeclaration
    d
            d :: NiceDeclaration
    d@NiceDataSig{}                -> NiceDeclaration -> ChangeT Identity NiceDeclaration
    forall (m :: * -> *) a. Monad m => a -> m a
    return NiceDeclaration
    d
            d :: NiceDeclaration
    d@NiceModuleMacro{}            -> NiceDeclaration -> ChangeT Identity NiceDeclaration
    forall (m :: * -> *) a. Monad m => a -> m a
    return NiceDeclaration
    d
            d :: NiceDeclaration
    d@NiceModule{}                 -> NiceDeclaration -> ChangeT Identity NiceDeclaration
    forall (m :: * -> *) a. Monad m => a -> m a
    return NiceDeclaration
    d
            d :: NiceDeclaration
    d@NicePragma{}                 -> NiceDeclaration -> ChangeT Identity NiceDeclaration
    forall (m :: * -> *) a. Monad m => a -> m a
    return NiceDeclaration
    d
            d :: NiceDeclaration
    d@NiceOpen{}                   -> NiceDeclaration -> ChangeT Identity NiceDeclaration
    forall (m :: * -> *) a. Monad m => a -> m a
    return NiceDeclaration
    d
            d :: NiceDeclaration
    d@NiceImport{}                 -> NiceDeclaration -> ChangeT Identity NiceDeclaration
    forall (m :: * -> *) a. Monad m => a -> m a
    return NiceDeclaration
    d
            d :: NiceDeclaration
    d@NiceDataDef{}                -> NiceDeclaration -> ChangeT Identity NiceDeclaration
    forall (m :: * -> *) a. Monad m => a -> m a
    return NiceDeclaration
    d
            d :: NiceDeclaration
    d@NiceRecDef{}                 -> NiceDeclaration -> ChangeT Identity NiceDeclaration
    forall (m :: * -> *) a. Monad m => a -> m a
    return NiceDeclaration
    d
            d :: NiceDeclaration
    d@NicePatternSyn{}             -> NiceDeclaration -> ChangeT Identity NiceDeclaration
    forall (m :: * -> *) a. Monad m => a -> m a
    return NiceDeclaration
    d
            d :: NiceDeclaration
    d@NiceGeneralize{}             -> NiceDeclaration -> ChangeT Identity NiceDeclaration
    forall (m :: * -> *) a. Monad m => a -> m a
    return NiceDeclaration
    d

        setInstance
          :: Range  -- Range of @instance@ keyword.
          -> Updater IsInstance
        setInstance :: Range -> Updater IsInstance
    setInstance Range
    r0 = \case
          i :: IsInstance
    i@InstanceDef{} -> Updater IsInstance
    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
    $ Range -> IsInstance
    InstanceDef Range
    r0

        macroBlock :: p -> t NiceDeclaration -> Nice (t NiceDeclaration)
    macroBlock p
    r t NiceDeclaration
    ds = (NiceDeclaration -> Nice NiceDeclaration)
    -> t NiceDeclaration -> Nice (t NiceDeclaration)
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    mapM NiceDeclaration -> Nice NiceDeclaration
    mkMacro t NiceDeclaration
    ds

        mkMacro :: NiceDeclaration -> Nice NiceDeclaration
        mkMacro :: NiceDeclaration -> Nice NiceDeclaration
    mkMacro = \case
            FunSig Range
    r Access
    p IsAbstract
    a IsInstance
    i IsMacro
    _ ArgInfo
    rel TerminationCheck
    tc CoverageCheck
    cc Name
    x Expr
    e -> NiceDeclaration -> Nice NiceDeclaration
    forall (m :: * -> *) a. Monad m => a -> m a
    return (NiceDeclaration -> Nice NiceDeclaration)
    -> NiceDeclaration -> 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{}                     -> NiceDeclaration -> Nice NiceDeclaration
    forall (m :: * -> *) a. Monad m => a -> m a
    return NiceDeclaration
    d
            NiceDeclaration
    d                              -> DeclarationException' -> Nice NiceDeclaration
    forall a. HasCallStack => DeclarationException' -> Nice a
    declarationException (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 :: UpdaterT Nice a

      default mkAbstract :: (Traversable f, MakeAbstract a', a ~ f a') => UpdaterT Nice a
      mkAbstract = (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)
    traverse a' -> ChangeT Nice a'
    forall a. MakeAbstract a => 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 :: UpdaterT Nice IsAbstract
    mkAbstract = \case
        a :: IsAbstract
    a@IsAbstract
    AbstractDef -> UpdaterT Nice IsAbstract
    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 :: UpdaterT Nice NiceDeclaration
    mkAbstract = \case
          NiceMutual Range
    r TerminationCheck
    termCheck CoverageCheck
    cc PositivityCheck
    pc [NiceDeclaration]
    ds  -> Range
    -> TerminationCheck
    -> CoverageCheck
    -> PositivityCheck
    -> [NiceDeclaration]
    -> NiceDeclaration
    NiceMutual Range
    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
    <$> UpdaterT Nice [NiceDeclaration]
    forall a. MakeAbstract a => UpdaterT Nice a
    mkAbstract [NiceDeclaration]
    ds
          NiceLoneConstructor Range
    r [NiceDeclaration]
    ds         -> Range -> [NiceDeclaration] -> NiceDeclaration
    NiceLoneConstructor Range
    r ([NiceDeclaration] -> NiceDeclaration)
    -> ChangeT Nice [NiceDeclaration] -> ChangeT Nice NiceDeclaration
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> UpdaterT Nice [NiceDeclaration]
    forall a. MakeAbstract a => UpdaterT Nice a
    mkAbstract [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
    <$> UpdaterT Nice IsAbstract
    forall a. MakeAbstract a => UpdaterT Nice a
    mkAbstract IsAbstract
    a ChangeT Nice ([Clause] -> NiceDeclaration)
    -> ChangeT Nice [Clause] -> ChangeT Nice NiceDeclaration
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> UpdaterT Nice [Clause]
    forall a. MakeAbstract a => UpdaterT Nice a
    mkAbstract [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
    <$> UpdaterT Nice IsAbstract
    forall a. MakeAbstract a => UpdaterT Nice a
    mkAbstract IsAbstract
    a ChangeT Nice ([NiceDeclaration] -> NiceDeclaration)
    -> ChangeT Nice [NiceDeclaration] -> ChangeT Nice NiceDeclaration
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> UpdaterT Nice [NiceDeclaration]
    forall a. MakeAbstract a => UpdaterT Nice a
    mkAbstract [NiceDeclaration]
    cs
          NiceRecDef Range
    r Origin
    o IsAbstract
    a PositivityCheck
    pc UniverseCheck
    uc Name
    x RecordDirectives
    dir [LamBinding]
    ps [Declaration]
    cs -> (\ IsAbstract
    a -> Range
    -> Origin
    -> IsAbstract
    -> PositivityCheck
    -> UniverseCheck
    -> Name
    -> RecordDirectives
    -> [LamBinding]
    -> [Declaration]
    -> NiceDeclaration
    NiceRecDef Range
    r Origin
    o IsAbstract
    a PositivityCheck
    pc UniverseCheck
    uc Name
    x RecordDirectives
    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
    <$> UpdaterT Nice IsAbstract
    forall a. MakeAbstract a => UpdaterT Nice a
    mkAbstract IsAbstract
    a
          NiceFunClause Range
    r Access
    p IsAbstract
    a TerminationCheck
    tc CoverageCheck
    cc Bool
    catchall Declaration
    d  -> (\ IsAbstract
    a -> Range
    -> Access
    -> IsAbstract
    -> TerminationCheck
    -> CoverageCheck
    -> Bool
    -> Declaration
    -> NiceDeclaration
    NiceFunClause Range
    r Access
    p IsAbstract
    a TerminationCheck
    tc CoverageCheck
    cc Bool
    catchall Declaration
    d) (IsAbstract -> NiceDeclaration)
    -> ChangeT Nice IsAbstract -> ChangeT Nice NiceDeclaration
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> UpdaterT Nice IsAbstract
    forall a. MakeAbstract a => UpdaterT Nice a
    mkAbstract 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 (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 (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 Access
    p IsAbstract
    a PositivityCheck
    pc UniverseCheck
    uc Name
    x [LamBinding]
    ls Expr
    t  -> UpdaterT Nice NiceDeclaration
    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
    -> PositivityCheck
    -> UniverseCheck
    -> Name
    -> [LamBinding]
    -> Expr
    -> NiceDeclaration
    NiceRecSig        Range
    r Access
    p IsAbstract
    AbstractDef PositivityCheck
    pc UniverseCheck
    uc Name
    x [LamBinding]
    ls Expr
    t
          NiceDataSig Range
    r Access
    p IsAbstract
    a PositivityCheck
    pc UniverseCheck
    uc Name
    x [LamBinding]
    ls Expr
    t -> UpdaterT Nice NiceDeclaration
    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
    -> PositivityCheck
    -> UniverseCheck
    -> Name
    -> [LamBinding]
    -> Expr
    -> NiceDeclaration
    NiceDataSig       Range
    r 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 (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 (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
          d :: NiceDeclaration
    d@NiceModule{}                 -> UpdaterT Nice NiceDeclaration
    forall (m :: * -> *) a. Monad m => a -> m a
    return NiceDeclaration
    d
          d :: NiceDeclaration
    d@NiceModuleMacro{}            -> UpdaterT Nice NiceDeclaration
    forall (m :: * -> *) a. Monad m => a -> m a
    return NiceDeclaration
    d
          d :: NiceDeclaration
    d@NicePragma{}                 -> UpdaterT Nice NiceDeclaration
    forall (m :: * -> *) a. Monad m => a -> m a
    return NiceDeclaration
    d
          d :: NiceDeclaration
    d@(NiceOpen Range
    _ QName
    _ ImportDirective
    directives)              -> do
            Maybe Range -> (Range -> ChangeT Nice ()) -> ChangeT Nice ()
    forall (m :: * -> *) a. Monad m => Maybe a -> (a -> m ()) -> m ()
    whenJust (ImportDirective -> Maybe Range
    forall n m. ImportDirective' n m -> Maybe Range
    publicOpen ImportDirective
    directives) ((Range -> ChangeT Nice ()) -> ChangeT Nice ())
    -> (Range -> ChangeT Nice ()) -> ChangeT Nice ()
    forall a b. (a -> b) -> a -> b
    $ Nice () -> ChangeT Nice ()
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (Nice () -> ChangeT Nice ())
    -> (Range -> Nice ()) -> Range -> ChangeT Nice ()
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . HasCallStack => DeclarationWarning' -> Nice ()
    DeclarationWarning' -> Nice ()
    declarationWarning (DeclarationWarning' -> Nice ())
    -> (Range -> DeclarationWarning') -> Range -> Nice ()
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Range -> DeclarationWarning'
    OpenPublicAbstract
            UpdaterT Nice NiceDeclaration
    forall (m :: * -> *) a. Monad m => a -> m a
    return NiceDeclaration
    d
          d :: NiceDeclaration
    d@NiceImport{}                 -> UpdaterT Nice NiceDeclaration
    forall (m :: * -> *) a. Monad m => a -> m a
    return NiceDeclaration
    d
          d :: NiceDeclaration
    d@NicePatternSyn{}             -> UpdaterT Nice NiceDeclaration
    forall (m :: * -> *) a. Monad m => a -> m a
    return NiceDeclaration
    d
          d :: NiceDeclaration
    d@NiceGeneralize{}             -> UpdaterT Nice NiceDeclaration
    forall (m :: * -> *) a. Monad m => a -> m a
    return NiceDeclaration
    d

    instance MakeAbstract Clause where
      mkAbstract :: UpdaterT Nice Clause
    mkAbstract (Clause Name
    x Bool
    catchall LHS
    lhs RHS
    rhs WhereClause
    wh [Clause]
    with) = do
        Name -> Bool -> LHS -> RHS -> WhereClause -> [Clause] -> Clause
    Clause Name
    x Bool
    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
    <$> UpdaterT Nice WhereClause
    forall a. MakeAbstract a => UpdaterT Nice a
    mkAbstract WhereClause
    wh ChangeT Nice ([Clause] -> Clause)
    -> ChangeT Nice [Clause] -> ChangeT Nice Clause
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> UpdaterT Nice [Clause]
    forall a. MakeAbstract a => UpdaterT Nice a
    mkAbstract [Clause]
    with

    -- | Contents of a @where@ clause are abstract if the parent is.
    instance MakeAbstract WhereClause where
      mkAbstract :: UpdaterT Nice WhereClause
    mkAbstract  WhereClause
    NoWhere             = UpdaterT Nice WhereClause
    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 (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 [Range -> [Declaration] -> Declaration
    Abstract Range
    forall a. Range' a
    noRange [Declaration]
    ds]
      mkAbstract (SomeWhere Range
    r 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 -> Name -> Access -> [Declaration] -> WhereClause
    forall decls.
    Range -> Name -> Access -> decls -> WhereClause' decls
    SomeWhere Range
    r Name
    m Access
    a [Range -> [Declaration] -> Declaration
    Abstract Range
    forall a. Range' a
    noRange [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 :: Origin -> UpdaterT Nice a

      default mkPrivate :: (Traversable f, MakePrivate a', a ~ f a') => Origin -> UpdaterT Nice a
      mkPrivate 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)
    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
    $ Origin -> a' -> ChangeT Nice a'
    forall a. MakePrivate a => Origin -> UpdaterT Nice a
    mkPrivate 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 :: Origin -> UpdaterT Nice Access
    mkPrivate Origin
    o = \case
        p :: Access
    p@PrivateAccess{} -> UpdaterT Nice Access
    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
    $ Origin -> Access
    PrivateAccess Origin
    o

    instance MakePrivate NiceDeclaration where
      mkPrivate :: Origin -> UpdaterT Nice NiceDeclaration
    mkPrivate 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
    <$> Origin -> UpdaterT Nice Access
    forall a. MakePrivate a => Origin -> UpdaterT Nice a
    mkPrivate 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
    <$> Origin -> UpdaterT Nice Access
    forall a. MakePrivate a => Origin -> UpdaterT Nice a
    mkPrivate 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
    <$> Origin -> UpdaterT Nice Access
    forall a. MakePrivate a => Origin -> UpdaterT Nice a
    mkPrivate Origin
    o Access
    p
          NiceMutual Range
    r TerminationCheck
    tc CoverageCheck
    cc PositivityCheck
    pc [NiceDeclaration]
    ds                 -> (\ [NiceDeclaration]
    ds-> Range
    -> TerminationCheck
    -> CoverageCheck
    -> PositivityCheck
    -> [NiceDeclaration]
    -> NiceDeclaration
    NiceMutual Range
    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
    <$> Origin -> UpdaterT Nice [NiceDeclaration]
    forall a. MakePrivate a => Origin -> UpdaterT Nice a
    mkPrivate Origin
    o [NiceDeclaration]
    ds
          NiceLoneConstructor Range
    r [NiceDeclaration]
    ds                 -> Range -> [NiceDeclaration] -> NiceDeclaration
    NiceLoneConstructor Range
    r                         ([NiceDeclaration] -> NiceDeclaration)
    -> ChangeT Nice [NiceDeclaration] -> ChangeT Nice NiceDeclaration
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Origin -> UpdaterT Nice [NiceDeclaration]
    forall a. MakePrivate a => Origin -> UpdaterT Nice a
    mkPrivate Origin
    o [NiceDeclaration]
    ds
          NiceModule Range
    r Access
    p IsAbstract
    a QName
    x Telescope
    tel [Declaration]
    ds                -> (\ Access
    p -> Range
    -> Access
    -> IsAbstract
    -> QName
    -> Telescope
    -> [Declaration]
    -> NiceDeclaration
    NiceModule Range
    r Access
    p IsAbstract
    a 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
    <$> Origin -> UpdaterT Nice Access
    forall a. MakePrivate a => Origin -> UpdaterT Nice a
    mkPrivate Origin
    o Access
    p
          NiceModuleMacro Range
    r Access
    p Name
    x ModuleApplication
    ma OpenShortHand
    op ImportDirective
    is           -> (\ Access
    p -> Range
    -> Access
    -> Name
    -> ModuleApplication
    -> OpenShortHand
    -> ImportDirective
    -> NiceDeclaration
    NiceModuleMacro Range
    r Access
    p 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
    <$> Origin -> UpdaterT Nice Access
    forall a. MakePrivate a => Origin -> UpdaterT Nice a
    mkPrivate 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
    <$> Origin -> UpdaterT Nice Access
    forall a. MakePrivate a => Origin -> UpdaterT Nice a
    mkPrivate Origin
    o Access
    p
          NiceRecSig Range
    r Access
    p IsAbstract
    a PositivityCheck
    pc UniverseCheck
    uc Name
    x [LamBinding]
    ls Expr
    t            -> (\ Access
    p -> Range
    -> Access
    -> IsAbstract
    -> PositivityCheck
    -> UniverseCheck
    -> Name
    -> [LamBinding]
    -> Expr
    -> NiceDeclaration
    NiceRecSig Range
    r 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
    <$> Origin -> UpdaterT Nice Access
    forall a. MakePrivate a => Origin -> UpdaterT Nice a
    mkPrivate Origin
    o Access
    p
          NiceDataSig Range
    r Access
    p IsAbstract
    a PositivityCheck
    pc UniverseCheck
    uc Name
    x [LamBinding]
    ls Expr
    t           -> (\ Access
    p -> Range
    -> Access
    -> IsAbstract
    -> PositivityCheck
    -> UniverseCheck
    -> Name
    -> [LamBinding]
    -> Expr
    -> NiceDeclaration
    NiceDataSig Range
    r 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
    <$> Origin -> UpdaterT Nice Access
    forall a. MakePrivate a => Origin -> UpdaterT Nice a
    mkPrivate Origin
    o Access
    p
          NiceFunClause Range
    r Access
    p IsAbstract
    a TerminationCheck
    tc CoverageCheck
    cc Bool
    catchall Declaration
    d     -> (\ Access
    p -> Range
    -> Access
    -> IsAbstract
    -> TerminationCheck
    -> CoverageCheck
    -> Bool
    -> Declaration
    -> NiceDeclaration
    NiceFunClause Range
    r Access
    p IsAbstract
    a TerminationCheck
    tc CoverageCheck
    cc Bool
    catchall Declaration
    d) (Access -> NiceDeclaration)
    -> ChangeT Nice Access -> ChangeT Nice NiceDeclaration
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Origin -> UpdaterT Nice Access
    forall a. MakePrivate a => Origin -> UpdaterT Nice a
    mkPrivate 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
    <$> Origin -> UpdaterT Nice Access
    forall a. MakePrivate a => Origin -> UpdaterT Nice a
    mkPrivate 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
    <$> Origin -> UpdaterT Nice Access
    forall a. MakePrivate a => Origin -> UpdaterT Nice a
    mkPrivate Origin
    o Access
    p
          NicePatternSyn Range
    r Access
    p Name
    x [Arg Name]
    xs Pattern
    p'               -> (\ Access
    p -> Range -> Access -> Name -> [Arg Name] -> Pattern -> NiceDeclaration
    NicePatternSyn Range
    r Access
    p Name
    x [Arg Name]
    xs Pattern
    p')           (Access -> NiceDeclaration)
    -> ChangeT Nice Access -> ChangeT Nice NiceDeclaration
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Origin -> UpdaterT Nice Access
    forall a. MakePrivate a => Origin -> UpdaterT Nice a
    mkPrivate 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
    <$> Origin -> UpdaterT Nice Access
    forall a. MakePrivate a => Origin -> UpdaterT Nice a
    mkPrivate Origin
    o Access
    p
          d :: NiceDeclaration
    d@NicePragma{}                           -> UpdaterT Nice NiceDeclaration
    forall (m :: * -> *) a. Monad m => a -> m a
    return NiceDeclaration
    d
          d :: NiceDeclaration
    d@(NiceOpen Range
    _ QName
    _ ImportDirective
    directives)              -> do
            Maybe Range -> (Range -> ChangeT Nice ()) -> ChangeT Nice ()
    forall (m :: * -> *) a. Monad m => Maybe a -> (a -> m ()) -> m ()
    whenJust (ImportDirective -> Maybe Range
    forall n m. ImportDirective' n m -> Maybe Range
    publicOpen ImportDirective
    directives) ((Range -> ChangeT Nice ()) -> ChangeT Nice ())
    -> (Range -> ChangeT Nice ()) -> ChangeT Nice ()
    forall a b. (a -> b) -> a -> b
    $ Nice () -> ChangeT Nice ()
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (Nice () -> ChangeT Nice ())
    -> (Range -> Nice ()) -> Range -> ChangeT Nice ()
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . HasCallStack => DeclarationWarning' -> Nice ()
    DeclarationWarning' -> Nice ()
    declarationWarning (DeclarationWarning' -> Nice ())
    -> (Range -> DeclarationWarning') -> Range -> Nice ()
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Range -> DeclarationWarning'
    OpenPublicPrivate
            UpdaterT Nice NiceDeclaration
    forall (m :: * -> *) a. Monad m => a -> m a
    return NiceDeclaration
    d
          d :: NiceDeclaration
    d@NiceImport{}                           -> UpdaterT Nice NiceDeclaration
    forall (m :: * -> *) a. Monad m => a -> m a
    return NiceDeclaration
    d
          -- 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
    <$> Origin -> UpdaterT Nice [Clause]
    forall a. MakePrivate a => Origin -> UpdaterT Nice a
    mkPrivate Origin
    o [Clause]
    cls
          d :: NiceDeclaration
    d@NiceDataDef{}                          -> UpdaterT Nice NiceDeclaration
    forall (m :: * -> *) a. Monad m => a -> m a
    return NiceDeclaration
    d
          d :: NiceDeclaration
    d@NiceRecDef{}                           -> UpdaterT Nice NiceDeclaration
    forall (m :: * -> *) a. Monad m => a -> m a
    return NiceDeclaration
    d

    instance MakePrivate Clause where
      mkPrivate :: Origin -> UpdaterT Nice Clause
    mkPrivate Origin
    o (Clause Name
    x Bool
    catchall LHS
    lhs RHS
    rhs WhereClause
    wh [Clause]
    with) = do
        Name -> Bool -> LHS -> RHS -> WhereClause -> [Clause] -> Clause
    Clause Name
    x Bool
    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
    <$> Origin -> UpdaterT Nice WhereClause
    forall a. MakePrivate a => Origin -> UpdaterT Nice a
    mkPrivate Origin
    o WhereClause
    wh ChangeT Nice ([Clause] -> Clause)
    -> ChangeT Nice [Clause] -> ChangeT Nice Clause
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> Origin -> UpdaterT Nice [Clause]
    forall a. MakePrivate a => Origin -> UpdaterT Nice a
    mkPrivate Origin
    o [Clause]
    with

    instance MakePrivate WhereClause where
      mkPrivate :: Origin -> UpdaterT Nice WhereClause
    mkPrivate Origin
    o = \case
        d :: WhereClause
    d@WhereClause
    NoWhere    -> UpdaterT Nice WhereClause
    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 (m :: * -> *) a. Monad m => a -> m a
    return WhereClause
    d
        -- Andreas, 2016-07-08
        -- A @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 Name
    m Access
    a [Declaration]
    ds -> Origin -> UpdaterT Nice Access
    forall a. MakePrivate a => Origin -> UpdaterT Nice a
    mkPrivate Origin
    o Access
    a ChangeT Nice Access
    -> (Access -> WhereClause) -> ChangeT Nice WhereClause
    forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
    <&> \ Access
    a' -> Range -> Name -> Access -> [Declaration] -> WhereClause
    forall decls.
    Range -> Name -> Access -> decls -> WhereClause' decls
    SomeWhere Range
    r 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 -> [Declaration]
    notSoNiceDeclarations :: NiceDeclaration -> [Declaration]
    notSoNiceDeclarations = \case
        Axiom Range
    _ Access
    _ IsAbstract
    _ IsInstance
    i ArgInfo
    rel Name
    x Expr
    e          -> IsInstance -> [Declaration] -> [Declaration]
    inst IsInstance
    i [ArgInfo -> TacticAttribute -> Name -> Expr -> Declaration
    TypeSig ArgInfo
    rel TacticAttribute
    forall a. Maybe a
    Nothing Name
    x Expr
    e]
        NiceField Range
    _ Access
    _ IsAbstract
    _ IsInstance
    i TacticAttribute
    tac Name
    x Arg Expr
    argt   -> [IsInstance -> TacticAttribute -> Name -> Arg Expr -> Declaration
    FieldSig IsInstance
    i TacticAttribute
    tac Name
    x Arg Expr
    argt]
        PrimitiveFunction Range
    r Access
    _ IsAbstract
    _ Name
    x Arg Expr
    e    -> [Range -> [Declaration] -> Declaration
    Primitive Range
    r [ArgInfo -> TacticAttribute -> Name -> Expr -> Declaration
    TypeSig (Arg Expr -> ArgInfo
    forall e. Arg e -> ArgInfo
    argInfo Arg Expr
    e) TacticAttribute
    forall a. Maybe a
    Nothing Name
    x (Arg Expr -> Expr
    forall e. Arg e -> e
    unArg Arg Expr
    e)]]
        NiceMutual Range
    r TerminationCheck
    _ CoverageCheck
    _ PositivityCheck
    _ [NiceDeclaration]
    ds          -> [Range -> [Declaration] -> Declaration
    Mutual Range
    r ([Declaration] -> Declaration) -> [Declaration] -> Declaration
    forall a b. (a -> b) -> a -> b
    $ (NiceDeclaration -> [Declaration])
    -> [NiceDeclaration] -> [Declaration]
    forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
    concatMap NiceDeclaration -> [Declaration]
    notSoNiceDeclarations [NiceDeclaration]
    ds]
        NiceLoneConstructor Range
    r [NiceDeclaration]
    ds       -> [Range -> [Declaration] -> Declaration
    LoneConstructor Range
    r ([Declaration] -> Declaration) -> [Declaration] -> Declaration
    forall a b. (a -> b) -> a -> b
    $ (NiceDeclaration -> [Declaration])
    -> [NiceDeclaration] -> [Declaration]
    forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
    concatMap NiceDeclaration -> [Declaration]
    notSoNiceDeclarations [NiceDeclaration]
    ds]
        NiceModule Range
    r Access
    _ IsAbstract
    _ QName
    x Telescope
    tel [Declaration]
    ds      -> [Range -> QName -> Telescope -> [Declaration] -> Declaration
    Module Range
    r QName
    x Telescope
    tel [Declaration]
    ds]
        NiceModuleMacro Range
    r Access
    _ Name
    x ModuleApplication
    ma OpenShortHand
    o ImportDirective
    dir -> [Range
    -> Name
    -> ModuleApplication
    -> OpenShortHand
    -> ImportDirective
    -> Declaration
    ModuleMacro Range
    r Name
    x ModuleApplication
    ma OpenShortHand
    o ImportDirective
    dir]
        NiceOpen Range
    r QName
    x ImportDirective
    dir               -> [Range -> QName -> ImportDirective -> Declaration
    Open Range
    r QName
    x ImportDirective
    dir]
        NiceImport Range
    r QName
    x Maybe AsName
    as OpenShortHand
    o ImportDirective
    dir        -> [Range
    -> QName
    -> Maybe AsName
    -> OpenShortHand
    -> ImportDirective
    -> Declaration
    Import Range
    r QName
    x Maybe AsName
    as OpenShortHand
    o ImportDirective
    dir]
        NicePragma Range
    _ Pragma
    p                 -> [Pragma -> Declaration
    Pragma Pragma
    p]
        NiceRecSig Range
    r Access
    _ IsAbstract
    _ PositivityCheck
    _ UniverseCheck
    _ Name
    x [LamBinding]
    bs Expr
    e    -> [Range -> Name -> [LamBinding] -> Expr -> Declaration
    RecordSig Range
    r Name
    x [LamBinding]
    bs Expr
    e]
        NiceDataSig Range
    r Access
    _ IsAbstract
    _ PositivityCheck
    _ UniverseCheck
    _ Name
    x [LamBinding]
    bs Expr
    e   -> [Range -> Name -> [LamBinding] -> Expr -> Declaration
    DataSig Range
    r Name
    x [LamBinding]
    bs Expr
    e]
        NiceFunClause Range
    _ Access
    _ IsAbstract
    _ TerminationCheck
    _ CoverageCheck
    _ Bool
    _ Declaration
    d    -> [Declaration
    d]
        FunSig Range
    _ Access
    _ IsAbstract
    _ IsInstance
    i IsMacro
    _ ArgInfo
    rel TerminationCheck
    _ CoverageCheck
    _ Name
    x Expr
    e   -> IsInstance -> [Declaration] -> [Declaration]
    inst IsInstance
    i [ArgInfo -> TacticAttribute -> Name -> Expr -> Declaration
    TypeSig ArgInfo
    rel TacticAttribute
    forall a. Maybe a
    Nothing Name
    x Expr
    e]
        FunDef Range
    _ [Declaration]
    ds IsAbstract
    _ IsInstance
    _ TerminationCheck
    _ CoverageCheck
    _ Name
    _ [Clause]
    _        -> [Declaration]
    ds
        NiceDataDef Range
    r Origin
    _ IsAbstract
    _ PositivityCheck
    _ UniverseCheck
    _ Name
    x [LamBinding]
    bs [NiceDeclaration]
    cs  -> [Range -> Name -> [LamBinding] -> [Declaration] -> Declaration
    DataDef Range
    r Name
    x [LamBinding]
    bs ([Declaration] -> Declaration) -> [Declaration] -> Declaration
    forall a b. (a -> b) -> a -> b
    $ (NiceDeclaration -> [Declaration])
    -> [NiceDeclaration] -> [Declaration]
    forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
    concatMap NiceDeclaration -> [Declaration]
    notSoNiceDeclarations [NiceDeclaration]
    cs]
        NiceRecDef Range
    r Origin
    _ IsAbstract
    _ PositivityCheck
    _ UniverseCheck
    _ Name
    x RecordDirectives
    dir [LamBinding]
    bs [Declaration]
    ds -> [Range
    -> Name
    -> RecordDirectives
    -> [LamBinding]
    -> [Declaration]
    -> Declaration
    RecordDef Range
    r Name
    x RecordDirectives
    dir [LamBinding]
    bs [Declaration]
    ds]
        NicePatternSyn Range
    r Access
    _ Name
    n [Arg Name]
    as Pattern
    p      -> [Range -> Name -> [Arg Name] -> Pattern -> Declaration
    PatternSyn Range
    r Name
    n [Arg Name]
    as Pattern
    p]
        NiceGeneralize Range
    r Access
    _ ArgInfo
    i TacticAttribute
    tac Name
    n Expr
    e   -> [Range -> [Declaration] -> Declaration
    Generalize Range
    r [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] -> [Declaration]
    inst IsInstance
    i [Range -> [Name] -> Expr -> Declaration
    UnquoteDecl Range
    r [Name]
    x Expr
    e]
        NiceUnquoteDef Range
    r Access
    _ IsAbstract
    _ TerminationCheck
    _ CoverageCheck
    _ [Name]
    x Expr
    e    -> [Range -> [Name] -> Expr -> Declaration
    UnquoteDef Range
    r [Name]
    x Expr
    e]
      where
        inst :: IsInstance -> [Declaration] -> [Declaration]
    inst (InstanceDef Range
    r) [Declaration]
    ds = [Range -> [Declaration] -> Declaration
    InstanceB Range
    r [Declaration]
    ds]
        inst IsInstance
    NotInstanceDef  [Declaration]
    ds = [Declaration]
    ds

    -- | 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 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
    _ Bool
    _ 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
    _ RecordDirectives
    _ [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