    module Agda.Syntax.Concrete.Definitions.Monad where

    import Control.Monad        ( unless )
    import Control.Monad.Except ( MonadError(..), ExceptT, runExceptT )
    import Control.Monad.State  ( MonadState(..), modify, State, runState )

    import Data.Bifunctor (second)
    import Data.Map (Map)
    import qualified Data.Map as Map

    import Agda.Syntax.Position
    import Agda.Syntax.Common hiding (TerminationCheck())
    import Agda.Syntax.Concrete.Name
    import Agda.Syntax.Concrete.Definitions.Types
    import Agda.Syntax.Concrete.Definitions.Errors

    import Agda.Utils.CallStack ( CallStack, HasCallStack, withCallerCallStack )
    import Agda.Utils.Lens

    import Agda.Utils.Impossible

    -- | Nicifier monad.
    --   Preserve the state when throwing an exception.

    newtype Nice a = Nice { forall a. Nice a -> ExceptT DeclarationException (State NiceEnv) a
    unNice :: ExceptT DeclarationException (State NiceEnv) a }
      deriving ( (forall a b. (a -> b) -> Nice a -> Nice b)
    -> (forall a b. a -> Nice b -> Nice a) -> Functor Nice
    forall a b. a -> Nice b -> Nice a
    forall a b. (a -> b) -> Nice a -> Nice b
    forall (f :: * -> *).
    (forall a b. (a -> b) -> f a -> f b)
    -> (forall a b. a -> f b -> f a) -> Functor f
    <$ :: forall a b. a -> Nice b -> Nice a
    $c<$ :: forall a b. a -> Nice b -> Nice a
    fmap :: forall a b. (a -> b) -> Nice a -> Nice b
    $cfmap :: forall a b. (a -> b) -> Nice a -> Nice b
    Functor, Functor Nice
    Functor Nice
    -> (forall a. a -> Nice a)
    -> (forall a b. Nice (a -> b) -> Nice a -> Nice b)
    -> (forall a b c. (a -> b -> c) -> Nice a -> Nice b -> Nice c)
    -> (forall a b. Nice a -> Nice b -> Nice b)
    -> (forall a b. Nice a -> Nice b -> Nice a)
    -> Applicative Nice
    forall a. a -> Nice a
    forall a b. Nice a -> Nice b -> Nice a
    forall a b. Nice a -> Nice b -> Nice b
    forall a b. Nice (a -> b) -> Nice a -> Nice b
    forall a b c. (a -> b -> c) -> Nice a -> Nice b -> Nice c
    forall (f :: * -> *).
    Functor f
    -> (forall a. a -> f a)
    -> (forall a b. f (a -> b) -> f a -> f b)
    -> (forall a b c. (a -> b -> c) -> f a -> f b -> f c)
    -> (forall a b. f a -> f b -> f b)
    -> (forall a b. f a -> f b -> f a)
    -> Applicative f
    <* :: forall a b. Nice a -> Nice b -> Nice a
    $c<* :: forall a b. Nice a -> Nice b -> Nice a
    *> :: forall a b. Nice a -> Nice b -> Nice b
    $c*> :: forall a b. Nice a -> Nice b -> Nice b
    liftA2 :: forall a b c. (a -> b -> c) -> Nice a -> Nice b -> Nice c
    $cliftA2 :: forall a b c. (a -> b -> c) -> Nice a -> Nice b -> Nice c
    <*> :: forall a b. Nice (a -> b) -> Nice a -> Nice b
    $c<*> :: forall a b. Nice (a -> b) -> Nice a -> Nice b
    pure :: forall a. a -> Nice a
    $cpure :: forall a. a -> Nice a
    Applicative, Applicative Nice
    Applicative Nice
    -> (forall a b. Nice a -> (a -> Nice b) -> Nice b)
    -> (forall a b. Nice a -> Nice b -> Nice b)
    -> (forall a. a -> Nice a)
    -> Monad Nice
    forall a. a -> Nice a
    forall a b. Nice a -> Nice b -> Nice b
    forall a b. Nice a -> (a -> Nice b) -> Nice b
    forall (m :: * -> *).
    Applicative m
    -> (forall a b. m a -> (a -> m b) -> m b)
    -> (forall a b. m a -> m b -> m b)
    -> (forall a. a -> m a)
    -> Monad m
    return :: forall a. a -> Nice a
    $creturn :: forall a. a -> Nice a
    >> :: forall a b. Nice a -> Nice b -> Nice b
    $c>> :: forall a b. Nice a -> Nice b -> Nice b
    >>= :: forall a b. Nice a -> (a -> Nice b) -> Nice b
    $c>>= :: forall a b. Nice a -> (a -> Nice b) -> Nice b
    Monad
               , MonadState NiceEnv, MonadError DeclarationException
               )

    -- | Run a Nicifier computation, return result and warnings
    --   (in chronological order).
    runNice :: Nice a -> (Either DeclarationException a, NiceWarnings)
    runNice :: forall a. Nice a -> (Either DeclarationException a, NiceWarnings)
    runNice Nice a
    m = (NiceEnv -> NiceWarnings)
    -> (Either DeclarationException a, NiceEnv)
    -> (Either DeclarationException a, NiceWarnings)
    forall (p :: * -> * -> *) b c a.
    Bifunctor p =>
    (b -> c) -> p a b -> p a c
    second (NiceWarnings -> NiceWarnings
    forall a. [a] -> [a]
    reverse (NiceWarnings -> NiceWarnings)
    -> (NiceEnv -> NiceWarnings) -> NiceEnv -> NiceWarnings
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . NiceEnv -> NiceWarnings
    niceWarn) ((Either DeclarationException a, NiceEnv)
     -> (Either DeclarationException a, NiceWarnings))
    -> (Either DeclarationException a, NiceEnv)
    -> (Either DeclarationException a, NiceWarnings)
    forall a b. (a -> b) -> a -> b
    $
      ExceptT DeclarationException (State NiceEnv) a
    -> State NiceEnv (Either DeclarationException a)
    forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
    runExceptT (Nice a -> ExceptT DeclarationException (State NiceEnv) a
    forall a. Nice a -> ExceptT DeclarationException (State NiceEnv) a
    unNice Nice a
    m) State NiceEnv (Either DeclarationException a)
    -> NiceEnv -> (Either DeclarationException a, NiceEnv)
    forall s a. State s a -> s -> (a, s)
    `runState` NiceEnv
    initNiceEnv

    -- | Nicifier state.

    data NiceEnv = NiceEnv
      { NiceEnv -> LoneSigs
    _loneSigs :: LoneSigs
        -- ^ Lone type signatures that wait for their definition.
      , NiceEnv -> TerminationCheck
    _termChk  :: TerminationCheck
        -- ^ Termination checking pragma waiting for a definition.
      , NiceEnv -> PositivityCheck
    _posChk   :: PositivityCheck
        -- ^ Positivity checking pragma waiting for a definition.
      , NiceEnv -> UniverseCheck
    _uniChk   :: UniverseCheck
        -- ^ Universe checking pragma waiting for a data/rec signature or definition.
      , NiceEnv -> Catchall
    _catchall :: Catchall
        -- ^ Catchall pragma waiting for a function clause.
      , NiceEnv -> CoverageCheck
    _covChk  :: CoverageCheck
        -- ^ Coverage pragma waiting for a definition.
      , NiceEnv -> NiceWarnings
    niceWarn :: NiceWarnings
        -- ^ Stack of warnings. Head is last warning.
      , NiceEnv -> NameId
    _nameId  :: NameId
        -- ^ We distinguish different 'NoName's (anonymous definitions) by a unique 'NameId'.
      }

    data LoneSig = LoneSig
      { LoneSig -> Range
    loneSigRange :: Range
      , LoneSig -> Name
    loneSigName  :: Name
          -- ^ If 'isNoName', this name can have a different 'NameId'
          --   than the key of 'LoneSigs' pointing to it.
      , LoneSig -> DataRecOrFun
    loneSigKind  :: DataRecOrFun
      }

    type LoneSigs     = Map Name LoneSig
         -- ^ We retain the 'Name' also in the codomain since
         --   'Name' as a key is up to @Eq Name@ which ignores the range.
         --   However, without range names are not unique in case the
         --   user gives a second definition of the same name.
         --   This causes then problems in 'replaceSigs' which might
         --   replace the wrong signature.
         --
         --   Another reason is that we want to distinguish different
         --   occurrences of 'NoName' in a mutual block (issue #4157).
         --   The 'NoName' in the codomain will have a unique 'NameId'.

    type NiceWarnings = [DeclarationWarning]
         -- ^ Stack of warnings. Head is last warning.

    -- | Initial nicifier state.

    initNiceEnv :: NiceEnv
    initNiceEnv :: NiceEnv
    initNiceEnv = NiceEnv :: LoneSigs
    -> TerminationCheck
    -> PositivityCheck
    -> UniverseCheck
    -> Catchall
    -> CoverageCheck
    -> NiceWarnings
    -> NameId
    -> NiceEnv
    NiceEnv
      { _loneSigs :: LoneSigs
    _loneSigs = LoneSigs
    forall k a. Map k a
    Map.empty
      , _termChk :: TerminationCheck
    _termChk  = TerminationCheck
    forall m. TerminationCheck m
    TerminationCheck
      , _posChk :: PositivityCheck
    _posChk   = PositivityCheck
    YesPositivityCheck
      , _uniChk :: UniverseCheck
    _uniChk   = UniverseCheck
    YesUniverseCheck
      , _catchall :: Catchall
    _catchall = Catchall
    False
      , _covChk :: CoverageCheck
    _covChk   = CoverageCheck
    YesCoverageCheck
      , niceWarn :: NiceWarnings
    niceWarn  = []
      , _nameId :: NameId
    _nameId   = Word64 -> ModuleNameHash -> NameId
    NameId Word64
    1 ModuleNameHash
    noModuleNameHash
      }

    lensNameId :: Lens' NameId NiceEnv
    lensNameId :: Lens' NameId NiceEnv
    lensNameId NameId -> f NameId
    f NiceEnv
    e = NameId -> f NameId
    f (NiceEnv -> NameId
    _nameId NiceEnv
    e) f NameId -> (NameId -> NiceEnv) -> f NiceEnv
    forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
    <&> \ NameId
    i -> NiceEnv
    e { _nameId :: NameId
    _nameId = NameId
    i }

    nextNameId :: Nice NameId
    nextNameId :: Nice NameId
    nextNameId = do
      NameId
    i <- Lens' NameId NiceEnv -> Nice NameId
    forall o (m :: * -> *) i. MonadState o m => Lens' i o -> m i
    use Lens' NameId NiceEnv
    lensNameId
      Lens' NameId NiceEnv
    lensNameId Lens' NameId NiceEnv -> (NameId -> NameId) -> Nice ()
    forall o (m :: * -> *) i.
    MonadState o m =>
    Lens' i o -> (i -> i) -> m ()
    %= NameId -> NameId
    forall a. Enum a => a -> a
    succ
      NameId -> Nice NameId
    forall (m :: * -> *) a. Monad m => a -> m a
    return NameId
    i

    -- * Handling the lone signatures, stored to infer mutual blocks.

    -- | Lens for field '_loneSigs'.

    loneSigs :: Lens' LoneSigs NiceEnv
    loneSigs :: Lens' LoneSigs NiceEnv
    loneSigs LoneSigs -> f LoneSigs
    f NiceEnv
    e = LoneSigs -> f LoneSigs
    f (NiceEnv -> LoneSigs
    _loneSigs NiceEnv
    e) f LoneSigs -> (LoneSigs -> NiceEnv) -> f NiceEnv
    forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
    <&> \ LoneSigs
    s -> NiceEnv
    e { _loneSigs :: LoneSigs
    _loneSigs = LoneSigs
    s }

    -- | Adding a lone signature to the state.
    --   Return the name (which is made unique if 'isNoName').

    addLoneSig :: Range -> Name -> DataRecOrFun -> Nice Name
    addLoneSig :: Range -> Name -> DataRecOrFun -> Nice Name
    addLoneSig Range
    r Name
    x DataRecOrFun
    k = do
      -- Andreas, 2020-05-19, issue #4157, make '_' unique.
      Name
    x' <- if Catchall -> Catchall
    not (Catchall -> Catchall) -> Catchall -> Catchall
    forall a b. (a -> b) -> a -> b
    $ Name -> Catchall
    forall a. IsNoName a => a -> Catchall
    isNoName Name
    x then Name -> Nice Name
    forall (m :: * -> *) a. Monad m => a -> m a
    return Name
    x else do
        NameId
    i <- Nice NameId
    nextNameId
        Name -> Nice Name
    forall (m :: * -> *) a. Monad m => a -> m a
    return Name
    x{ nameId :: NameId
    nameId = NameId
    i }
      Lens' LoneSigs NiceEnv
    loneSigs Lens' LoneSigs NiceEnv -> (LoneSigs -> Nice LoneSigs) -> Nice ()
    forall o (m :: * -> *) i.
    MonadState o m =>
    Lens' i o -> (i -> m i) -> m ()
    %== \ LoneSigs
    s -> do
        let (Maybe LoneSig
    mr, LoneSigs
    s') = (Name -> LoneSig -> LoneSig -> LoneSig)
    -> Name -> LoneSig -> LoneSigs -> (Maybe LoneSig, LoneSigs)
    forall k a.
    Ord k =>
    (k -> a -> a -> a) -> k -> a -> Map k a -> (Maybe a, Map k a)
    Map.insertLookupWithKey (\ Name
    _k LoneSig
    new LoneSig
    _old -> LoneSig
    new) Name
    x (Range -> Name -> DataRecOrFun -> LoneSig
    LoneSig Range
    r Name
    x' DataRecOrFun
    k) LoneSigs
    s
        case Maybe LoneSig
    mr of
          Maybe LoneSig
    Nothing -> LoneSigs -> Nice LoneSigs
    forall (m :: * -> *) a. Monad m => a -> m a
    return LoneSigs
    s'
          Just{}  -> DeclarationException' -> Nice LoneSigs
    forall a. HasCallStack => DeclarationException' -> Nice a
    declarationException (DeclarationException' -> Nice LoneSigs)
    -> DeclarationException' -> Nice LoneSigs
    forall a b. (a -> b) -> a -> b
    $
            if Catchall -> Catchall
    not (Catchall -> Catchall) -> Catchall -> Catchall
    forall a b. (a -> b) -> a -> b
    $ Name -> Catchall
    forall a. IsNoName a => a -> Catchall
    isNoName Name
    x then Name -> DeclarationException'
    DuplicateDefinition Name
    x else Range -> DeclarationException'
    DuplicateAnonDeclaration Range
    r
      Name -> Nice Name
    forall (m :: * -> *) a. Monad m => a -> m a
    return Name
    x'

    -- | Remove a lone signature from the state.

    removeLoneSig :: Name -> Nice ()
    removeLoneSig :: Name -> Nice ()
    removeLoneSig Name
    x = Lens' LoneSigs NiceEnv
    loneSigs Lens' LoneSigs NiceEnv -> (LoneSigs -> LoneSigs) -> Nice ()
    forall o (m :: * -> *) i.
    MonadState o m =>
    Lens' i o -> (i -> i) -> m ()
    %= Name -> LoneSigs -> LoneSigs
    forall k a. Ord k => k -> Map k a -> Map k a
    Map.delete Name
    x

    -- | Search for forward type signature.

    getSig :: Name -> Nice (Maybe DataRecOrFun)
    getSig :: Name -> Nice (Maybe DataRecOrFun)
    getSig Name
    x = (LoneSig -> DataRecOrFun) -> Maybe LoneSig -> Maybe DataRecOrFun
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap LoneSig -> DataRecOrFun
    loneSigKind (Maybe LoneSig -> Maybe DataRecOrFun)
    -> (LoneSigs -> Maybe LoneSig) -> LoneSigs -> Maybe DataRecOrFun
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Name -> LoneSigs -> Maybe LoneSig
    forall k a. Ord k => k -> Map k a -> Maybe a
    Map.lookup Name
    x (LoneSigs -> Maybe DataRecOrFun)
    -> Nice LoneSigs -> Nice (Maybe DataRecOrFun)
    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

    -- | Check that no lone signatures are left in the state.

    noLoneSigs :: Nice Bool
    noLoneSigs :: Nice Catchall
    noLoneSigs = LoneSigs -> Catchall
    forall (t :: * -> *) a. Foldable t => t a -> Catchall
    null (LoneSigs -> Catchall) -> Nice LoneSigs -> Nice Catchall
    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

    -- | Ensure that all forward declarations have been given a definition.

    forgetLoneSigs :: Nice ()
    forgetLoneSigs :: Nice ()
    forgetLoneSigs = Lens' LoneSigs NiceEnv
    loneSigs Lens' LoneSigs NiceEnv -> LoneSigs -> Nice ()
    forall o (m :: * -> *) i. MonadState o m => Lens' i o -> i -> m ()
    .= LoneSigs
    forall k a. Map k a
    Map.empty

    checkLoneSigs :: LoneSigs -> Nice ()
    checkLoneSigs :: LoneSigs -> Nice ()
    checkLoneSigs LoneSigs
    xs = do
      Nice ()
    forgetLoneSigs
      Catchall -> Nice () -> Nice ()
    forall (f :: * -> *). Applicative f => Catchall -> f () -> f ()
    unless (LoneSigs -> Catchall
    forall k a. Map k a -> Catchall
    Map.null LoneSigs
    xs) (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
    $ [(Name, Range)] -> DeclarationWarning'
    MissingDefinitions ([(Name, Range)] -> DeclarationWarning')
    -> [(Name, Range)] -> DeclarationWarning'
    forall a b. (a -> b) -> a -> b
    $
        (LoneSig -> (Name, Range)) -> [LoneSig] -> [(Name, Range)]
    forall a b. (a -> b) -> [a] -> [b]
    map (\LoneSig
    s -> (LoneSig -> Name
    loneSigName LoneSig
    s , LoneSig -> Range
    loneSigRange LoneSig
    s)) ([LoneSig] -> [(Name, Range)]) -> [LoneSig] -> [(Name, Range)]
    forall a b. (a -> b) -> a -> b
    $ LoneSigs -> [LoneSig]
    forall k a. Map k a -> [a]
    Map.elems LoneSigs
    xs

    -- | Get names of lone function signatures, plus their unique names.

    loneFuns :: LoneSigs -> [(Name,Name)]
    loneFuns :: LoneSigs -> [(Name, Name)]
    loneFuns = ((Name, LoneSig) -> (Name, Name))
    -> [(Name, LoneSig)] -> [(Name, Name)]
    forall a b. (a -> b) -> [a] -> [b]
    map ((LoneSig -> Name) -> (Name, LoneSig) -> (Name, Name)
    forall (p :: * -> * -> *) b c a.
    Bifunctor p =>
    (b -> c) -> p a b -> p a c
    second LoneSig -> Name
    loneSigName) ([(Name, LoneSig)] -> [(Name, Name)])
    -> (LoneSigs -> [(Name, LoneSig)]) -> LoneSigs -> [(Name, Name)]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ((Name, LoneSig) -> Catchall)
    -> [(Name, LoneSig)] -> [(Name, LoneSig)]
    forall a. (a -> Catchall) -> [a] -> [a]
    filter (DataRecOrFun -> Catchall
    isFunName (DataRecOrFun -> Catchall)
    -> ((Name, LoneSig) -> DataRecOrFun) -> (Name, LoneSig) -> Catchall
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . LoneSig -> DataRecOrFun
    loneSigKind (LoneSig -> DataRecOrFun)
    -> ((Name, LoneSig) -> LoneSig) -> (Name, LoneSig) -> DataRecOrFun
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Name, LoneSig) -> LoneSig
    forall a b. (a, b) -> b
    snd) ([(Name, LoneSig)] -> [(Name, LoneSig)])
    -> (LoneSigs -> [(Name, LoneSig)]) -> LoneSigs -> [(Name, LoneSig)]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . LoneSigs -> [(Name, LoneSig)]
    forall k a. Map k a -> [(k, a)]
    Map.toList

    -- | Create a 'LoneSigs' map from an association list.

    loneSigsFromLoneNames :: [(Range, Name, DataRecOrFun)] -> LoneSigs
    loneSigsFromLoneNames :: [(Range, Name, DataRecOrFun)] -> LoneSigs
    loneSigsFromLoneNames = (LoneSig -> LoneSig -> LoneSig) -> [(Name, LoneSig)] -> LoneSigs
    forall k a. Ord k => (a -> a -> a) -> [(k, a)] -> Map k a
    Map.fromListWith LoneSig -> LoneSig -> LoneSig
    forall a. HasCallStack => a
    __IMPOSSIBLE__ ([(Name, LoneSig)] -> LoneSigs)
    -> ([(Range, Name, DataRecOrFun)] -> [(Name, LoneSig)])
    -> [(Range, Name, DataRecOrFun)]
    -> LoneSigs
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ((Range, Name, DataRecOrFun) -> (Name, LoneSig))
    -> [(Range, Name, DataRecOrFun)] -> [(Name, LoneSig)]
    forall a b. (a -> b) -> [a] -> [b]
    map (\(Range
    r,Name
    x,DataRecOrFun
    k) -> (Name
    x, Range -> Name -> DataRecOrFun -> LoneSig
    LoneSig Range
    r Name
    x DataRecOrFun
    k))

    -- | Lens for field '_termChk'.

    terminationCheckPragma :: Lens' TerminationCheck NiceEnv
    terminationCheckPragma :: Lens' TerminationCheck NiceEnv
    terminationCheckPragma TerminationCheck -> f TerminationCheck
    f NiceEnv
    e = TerminationCheck -> f TerminationCheck
    f (NiceEnv -> TerminationCheck
    _termChk NiceEnv
    e) f TerminationCheck -> (TerminationCheck -> NiceEnv) -> f NiceEnv
    forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
    <&> \ TerminationCheck
    s -> NiceEnv
    e { _termChk :: TerminationCheck
    _termChk = TerminationCheck
    s }

    withTerminationCheckPragma :: TerminationCheck -> Nice a -> Nice a
    withTerminationCheckPragma :: forall a. TerminationCheck -> Nice a -> Nice a
    withTerminationCheckPragma TerminationCheck
    tc Nice a
    f = do
      TerminationCheck
    tc_old <- Lens' TerminationCheck NiceEnv -> Nice TerminationCheck
    forall o (m :: * -> *) i. MonadState o m => Lens' i o -> m i
    use Lens' TerminationCheck NiceEnv
    terminationCheckPragma
      Lens' TerminationCheck NiceEnv
    terminationCheckPragma Lens' TerminationCheck NiceEnv -> TerminationCheck -> Nice ()
    forall o (m :: * -> *) i. MonadState o m => Lens' i o -> i -> m ()
    .= TerminationCheck
    tc
      a
    result <- Nice a
    f
      Lens' TerminationCheck NiceEnv
    terminationCheckPragma Lens' TerminationCheck NiceEnv -> TerminationCheck -> Nice ()
    forall o (m :: * -> *) i. MonadState o m => Lens' i o -> i -> m ()
    .= TerminationCheck
    tc_old
      a -> Nice a
    forall (m :: * -> *) a. Monad m => a -> m a
    return a
    result

    coverageCheckPragma :: Lens' CoverageCheck NiceEnv
    coverageCheckPragma :: Lens' CoverageCheck NiceEnv
    coverageCheckPragma CoverageCheck -> f CoverageCheck
    f NiceEnv
    e = CoverageCheck -> f CoverageCheck
    f (NiceEnv -> CoverageCheck
    _covChk NiceEnv
    e) f CoverageCheck -> (CoverageCheck -> NiceEnv) -> f NiceEnv
    forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
    <&> \ CoverageCheck
    s -> NiceEnv
    e { _covChk :: CoverageCheck
    _covChk = CoverageCheck
    s }

    withCoverageCheckPragma :: CoverageCheck -> Nice a -> Nice a
    withCoverageCheckPragma :: forall a. CoverageCheck -> Nice a -> Nice a
    withCoverageCheckPragma CoverageCheck
    tc Nice a
    f = do
      CoverageCheck
    tc_old <- Lens' CoverageCheck NiceEnv -> Nice CoverageCheck
    forall o (m :: * -> *) i. MonadState o m => Lens' i o -> m i
    use Lens' CoverageCheck NiceEnv
    coverageCheckPragma
      Lens' CoverageCheck NiceEnv
    coverageCheckPragma Lens' CoverageCheck NiceEnv -> CoverageCheck -> Nice ()
    forall o (m :: * -> *) i. MonadState o m => Lens' i o -> i -> m ()
    .= CoverageCheck
    tc
      a
    result <- Nice a
    f
      Lens' CoverageCheck NiceEnv
    coverageCheckPragma Lens' CoverageCheck NiceEnv -> CoverageCheck -> Nice ()
    forall o (m :: * -> *) i. MonadState o m => Lens' i o -> i -> m ()
    .= CoverageCheck
    tc_old
      a -> Nice a
    forall (m :: * -> *) a. Monad m => a -> m a
    return a
    result

    -- | Lens for field '_posChk'.

    positivityCheckPragma :: Lens' PositivityCheck NiceEnv
    positivityCheckPragma :: Lens' PositivityCheck NiceEnv
    positivityCheckPragma PositivityCheck -> f PositivityCheck
    f NiceEnv
    e = PositivityCheck -> f PositivityCheck
    f (NiceEnv -> PositivityCheck
    _posChk NiceEnv
    e) f PositivityCheck -> (PositivityCheck -> NiceEnv) -> f NiceEnv
    forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
    <&> \ PositivityCheck
    s -> NiceEnv
    e { _posChk :: PositivityCheck
    _posChk = PositivityCheck
    s }

    withPositivityCheckPragma :: PositivityCheck -> Nice a -> Nice a
    withPositivityCheckPragma :: forall a. PositivityCheck -> Nice a -> Nice a
    withPositivityCheckPragma PositivityCheck
    pc Nice a
    f = do
      PositivityCheck
    pc_old <- Lens' PositivityCheck NiceEnv -> Nice PositivityCheck
    forall o (m :: * -> *) i. MonadState o m => Lens' i o -> m i
    use Lens' PositivityCheck NiceEnv
    positivityCheckPragma
      Lens' PositivityCheck NiceEnv
    positivityCheckPragma Lens' PositivityCheck NiceEnv -> PositivityCheck -> Nice ()
    forall o (m :: * -> *) i. MonadState o m => Lens' i o -> i -> m ()
    .= PositivityCheck
    pc
      a
    result <- Nice a
    f
      Lens' PositivityCheck NiceEnv
    positivityCheckPragma Lens' PositivityCheck NiceEnv -> PositivityCheck -> Nice ()
    forall o (m :: * -> *) i. MonadState o m => Lens' i o -> i -> m ()
    .= PositivityCheck
    pc_old
      a -> Nice a
    forall (m :: * -> *) a. Monad m => a -> m a
    return a
    result

    -- | Lens for field '_uniChk'.

    universeCheckPragma :: Lens' UniverseCheck NiceEnv
    universeCheckPragma :: Lens' UniverseCheck NiceEnv
    universeCheckPragma UniverseCheck -> f UniverseCheck
    f NiceEnv
    e = UniverseCheck -> f UniverseCheck
    f (NiceEnv -> UniverseCheck
    _uniChk NiceEnv
    e) f UniverseCheck -> (UniverseCheck -> NiceEnv) -> f NiceEnv
    forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
    <&> \ UniverseCheck
    s -> NiceEnv
    e { _uniChk :: UniverseCheck
    _uniChk = UniverseCheck
    s }

    withUniverseCheckPragma :: UniverseCheck -> Nice a -> Nice a
    withUniverseCheckPragma :: forall a. UniverseCheck -> Nice a -> Nice a
    withUniverseCheckPragma UniverseCheck
    uc Nice a
    f = do
      UniverseCheck
    uc_old <- Lens' UniverseCheck NiceEnv -> Nice UniverseCheck
    forall o (m :: * -> *) i. MonadState o m => Lens' i o -> m i
    use Lens' UniverseCheck NiceEnv
    universeCheckPragma
      Lens' UniverseCheck NiceEnv
    universeCheckPragma Lens' UniverseCheck NiceEnv -> UniverseCheck -> Nice ()
    forall o (m :: * -> *) i. MonadState o m => Lens' i o -> i -> m ()
    .= UniverseCheck
    uc
      a
    result <- Nice a
    f
      Lens' UniverseCheck NiceEnv
    universeCheckPragma Lens' UniverseCheck NiceEnv -> UniverseCheck -> Nice ()
    forall o (m :: * -> *) i. MonadState o m => Lens' i o -> i -> m ()
    .= UniverseCheck
    uc_old
      a -> Nice a
    forall (m :: * -> *) a. Monad m => a -> m a
    return a
    result

    -- | Get universe check pragma from a data/rec signature.
    --   Defaults to 'YesUniverseCheck'.

    getUniverseCheckFromSig :: Name -> Nice UniverseCheck
    getUniverseCheckFromSig :: Name -> Nice UniverseCheck
    getUniverseCheckFromSig Name
    x = UniverseCheck
    -> (DataRecOrFun -> UniverseCheck)
    -> Maybe DataRecOrFun
    -> UniverseCheck
    forall b a. b -> (a -> b) -> Maybe a -> b
    maybe UniverseCheck
    YesUniverseCheck DataRecOrFun -> UniverseCheck
    universeCheck (Maybe DataRecOrFun -> UniverseCheck)
    -> Nice (Maybe DataRecOrFun) -> Nice UniverseCheck
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Name -> Nice (Maybe DataRecOrFun)
    getSig Name
    x

    -- | Lens for field '_catchall'.

    catchallPragma :: Lens' Catchall NiceEnv
    catchallPragma :: Lens' Catchall NiceEnv
    catchallPragma Catchall -> f Catchall
    f NiceEnv
    e = Catchall -> f Catchall
    f (NiceEnv -> Catchall
    _catchall NiceEnv
    e) f Catchall -> (Catchall -> NiceEnv) -> f NiceEnv
    forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
    <&> \ Catchall
    s -> NiceEnv
    e { _catchall :: Catchall
    _catchall = Catchall
    s }

    -- | Get current catchall pragma, and reset it for the next clause.

    popCatchallPragma :: Nice Catchall
    popCatchallPragma :: Nice Catchall
    popCatchallPragma = do
      Catchall
    ca <- Lens' Catchall NiceEnv -> Nice Catchall
    forall o (m :: * -> *) i. MonadState o m => Lens' i o -> m i
    use Lens' Catchall NiceEnv
    catchallPragma
      Lens' Catchall NiceEnv
    catchallPragma Lens' Catchall NiceEnv -> Catchall -> Nice ()
    forall o (m :: * -> *) i. MonadState o m => Lens' i o -> i -> m ()
    .= Catchall
    False
      Catchall -> Nice Catchall
    forall (m :: * -> *) a. Monad m => a -> m a
    return Catchall
    ca

    withCatchallPragma :: Catchall -> Nice a -> Nice a
    withCatchallPragma :: forall a. Catchall -> Nice a -> Nice a
    withCatchallPragma Catchall
    ca Nice a
    f = do
      Catchall
    ca_old <- Lens' Catchall NiceEnv -> Nice Catchall
    forall o (m :: * -> *) i. MonadState o m => Lens' i o -> m i
    use Lens' Catchall NiceEnv
    catchallPragma
      Lens' Catchall NiceEnv
    catchallPragma Lens' Catchall NiceEnv -> Catchall -> Nice ()
    forall o (m :: * -> *) i. MonadState o m => Lens' i o -> i -> m ()
    .= Catchall
    ca
      a
    result <- Nice a
    f
      Lens' Catchall NiceEnv
    catchallPragma Lens' Catchall NiceEnv -> Catchall -> Nice ()
    forall o (m :: * -> *) i. MonadState o m => Lens' i o -> i -> m ()
    .= Catchall
    ca_old
      a -> Nice a
    forall (m :: * -> *) a. Monad m => a -> m a
    return a
    result

    -- | Add a new warning.
    niceWarning :: DeclarationWarning -> Nice ()
    niceWarning :: DeclarationWarning -> Nice ()
    niceWarning DeclarationWarning
    w = (NiceEnv -> NiceEnv) -> Nice ()
    forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
    modify ((NiceEnv -> NiceEnv) -> Nice ())
    -> (NiceEnv -> NiceEnv) -> Nice ()
    forall a b. (a -> b) -> a -> b
    $ \ NiceEnv
    st -> NiceEnv
    st { niceWarn :: NiceWarnings
    niceWarn = DeclarationWarning
    w DeclarationWarning -> NiceWarnings -> NiceWarnings
    forall a. a -> [a] -> [a]
    : NiceEnv -> NiceWarnings
    niceWarn NiceEnv
    st }

    declarationException :: HasCallStack => DeclarationException' -> Nice a
    declarationException :: forall a. HasCallStack => DeclarationException' -> Nice a
    declarationException DeclarationException'
    e = (CallStack -> Nice a) -> Nice a
    forall b. HasCallStack => (CallStack -> b) -> b
    withCallerCallStack ((CallStack -> Nice a) -> Nice a)
    -> (CallStack -> Nice a) -> Nice a
    forall a b. (a -> b) -> a -> b
    $ DeclarationException -> Nice a
    forall e (m :: * -> *) a. MonadError e m => e -> m a
    throwError (DeclarationException -> Nice a)
    -> (CallStack -> DeclarationException) -> CallStack -> Nice a
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (CallStack -> DeclarationException' -> DeclarationException)
    -> DeclarationException' -> CallStack -> DeclarationException
    forall a b c. (a -> b -> c) -> b -> a -> c
    flip CallStack -> DeclarationException' -> DeclarationException
    DeclarationException DeclarationException'
    e

    declarationWarning' :: DeclarationWarning' -> CallStack -> Nice ()
    declarationWarning' :: DeclarationWarning' -> CallStack -> Nice ()
    declarationWarning' DeclarationWarning'
    w CallStack
    loc = DeclarationWarning -> Nice ()
    niceWarning (DeclarationWarning -> Nice ()) -> DeclarationWarning -> Nice ()
    forall a b. (a -> b) -> a -> b
    $ CallStack -> DeclarationWarning' -> DeclarationWarning
    DeclarationWarning CallStack
    loc DeclarationWarning'
    w

    declarationWarning :: HasCallStack => DeclarationWarning' -> Nice ()
    declarationWarning :: HasCallStack => DeclarationWarning' -> Nice ()
    declarationWarning = (CallStack -> Nice ()) -> Nice ()
    forall b. HasCallStack => (CallStack -> b) -> b
    withCallerCallStack ((CallStack -> Nice ()) -> Nice ())
    -> (DeclarationWarning' -> CallStack -> Nice ())
    -> DeclarationWarning'
    -> Nice ()
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . DeclarationWarning' -> CallStack -> Nice ()
    declarationWarning'