    {-# OPTIONS_GHC -Wunused-imports #-}

    module Agda.Syntax.Concrete.Definitions.Monad where

    import Prelude hiding ( null )

    import Control.Monad        ()
    import Control.Monad.Except ( MonadError(..), ExceptT, runExceptT )
    import Control.Monad.Reader ( MonadReader, ReaderT, runReaderT )
    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 ( WhereClause_ )
    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 qualified Agda.Utils.List1 as List1
    import Agda.Utils.Null (Null(..))

    import Agda.Utils.Impossible

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

    newtype Nice a = Nice { forall a.
    Nice a
    -> ReaderT
         NiceEnv (ExceptT DeclarationException (State NiceState)) a
    unNice :: ReaderT NiceEnv (ExceptT DeclarationException (State NiceState)) 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
    $cfmap :: forall a b. (a -> b) -> Nice a -> Nice b
    fmap :: forall a b. (a -> b) -> Nice a -> Nice b
    $c<$ :: forall a b. a -> Nice b -> Nice a
    <$ :: forall a b. a -> Nice b -> Nice a
    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
    $cpure :: forall a. a -> Nice a
    pure :: forall a. a -> Nice a
    $c<*> :: forall a b. Nice (a -> b) -> Nice a -> Nice b
    <*> :: forall a b. Nice (a -> b) -> Nice a -> Nice b
    $cliftA2 :: forall a b c. (a -> b -> c) -> Nice a -> Nice b -> Nice c
    liftA2 :: forall a b c. (a -> b -> c) -> Nice a -> Nice b -> Nice c
    $c*> :: forall a b. Nice a -> Nice b -> Nice b
    *> :: forall a b. Nice a -> Nice b -> Nice b
    $c<* :: forall a b. Nice a -> Nice b -> Nice a
    <* :: forall a b. Nice a -> Nice b -> 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
    $c>>= :: forall a b. Nice a -> (a -> Nice b) -> Nice b
    >>= :: forall a b. Nice a -> (a -> Nice b) -> Nice b
    $c>> :: forall a b. Nice a -> Nice b -> Nice b
    >> :: forall a b. Nice a -> Nice b -> Nice b
    $creturn :: forall a. a -> Nice a
    return :: forall a. a -> Nice a
    Monad
               , MonadReader NiceEnv, MonadState NiceState, MonadError DeclarationException
               )

    -- | Run a Nicifier computation, return result and warnings
    --   (in chronological order).
    runNice :: NiceEnv -> Nice a -> (Either DeclarationException a, NiceWarnings)
    runNice :: forall a.
    NiceEnv -> Nice a -> (Either DeclarationException a, NiceWarnings)
    runNice NiceEnv
    env Nice a
    m = (NiceState -> NiceWarnings)
    -> (Either DeclarationException a, NiceState)
    -> (Either DeclarationException a, NiceWarnings)
    forall b c a. (b -> c) -> (a, b) -> (a, c)
    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)
    -> (NiceState -> NiceWarnings) -> NiceState -> NiceWarnings
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . NiceState -> NiceWarnings
    niceWarn) ((Either DeclarationException a, NiceState)
     -> (Either DeclarationException a, NiceWarnings))
    -> (Either DeclarationException a, NiceState)
    -> (Either DeclarationException a, NiceWarnings)
    forall a b. (a -> b) -> a -> b
    $
      ExceptT DeclarationException (State NiceState) a
    -> StateT NiceState Identity (Either DeclarationException a)
    forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
    runExceptT (Nice a
    -> ReaderT
         NiceEnv (ExceptT DeclarationException (State NiceState)) a
    forall a.
    Nice a
    -> ReaderT
         NiceEnv (ExceptT DeclarationException (State NiceState)) a
    unNice Nice a
    m ReaderT NiceEnv (ExceptT DeclarationException (State NiceState)) a
    -> NiceEnv -> ExceptT DeclarationException (State NiceState) a
    forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
    `runReaderT` NiceEnv
    env) StateT NiceState Identity (Either DeclarationException a)
    -> NiceState -> (Either DeclarationException a, NiceState)
    forall s a. State s a -> s -> (a, s)
    `runState` NiceState
    initNiceState

    instance Null a => Null (Nice a) where
      empty :: Nice a
    empty = a -> Nice a
    forall a. a -> Nice a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure a
    forall a. Null a => a
    empty
      null :: Nice a -> Bool
    null Nice a
    _ = Bool
    forall a. HasCallStack => a
    __IMPOSSIBLE__

    -- | Nicifier parameters.

    data NiceEnv = NiceEnv
      { NiceEnv -> Bool
    safeButNotBuiltin :: Bool
           -- ^ We are in a module declared @--safe@ which is not a builtin module.
      , NiceEnv -> WhereClause_
    checkingWhere     :: WhereClause_
           -- ^ Are we checking a @where@ module?
      }

    -- | Nicifier state.

    data NiceState = NiceState
      { NiceState -> LoneSigs
    _loneSigs :: LoneSigs
        -- ^ Lone type signatures that wait for their definition.
      , NiceState -> TerminationCheck
    _termChk  :: TerminationCheck
        -- ^ Termination checking pragma waiting for a definition.
      , NiceState -> PositivityCheck
    _posChk   :: PositivityCheck
        -- ^ Positivity checking pragma waiting for a definition.
      , NiceState -> UniverseCheck
    _uniChk   :: UniverseCheck
        -- ^ Universe checking pragma waiting for a data/rec signature or definition.
      , NiceState -> Catchall
    _catchall :: Catchall
        -- ^ Catchall pragma waiting for a function clause.
      , NiceState -> CoverageCheck
    _covChk  :: CoverageCheck
        -- ^ Coverage pragma waiting for a definition.
      , NiceState -> NiceWarnings
    niceWarn :: NiceWarnings
        -- ^ Stack of warnings. Head is last warning.
      , NiceState -> 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
      }
      deriving Int -> LoneSig -> ShowS
    [LoneSig] -> ShowS
    LoneSig -> String
    (Int -> LoneSig -> ShowS)
    -> (LoneSig -> String) -> ([LoneSig] -> ShowS) -> Show LoneSig
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    $cshowsPrec :: Int -> LoneSig -> ShowS
    showsPrec :: Int -> LoneSig -> ShowS
    $cshow :: LoneSig -> String
    show :: LoneSig -> String
    $cshowList :: [LoneSig] -> ShowS
    showList :: [LoneSig] -> ShowS
    Show

    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.

    initNiceState :: NiceState
    initNiceState :: NiceState
    initNiceState = NiceState
      { _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
    forall a. Null a => a
    empty
      , _covChk :: CoverageCheck
    _covChk   = CoverageCheck
    YesCoverageCheck
      , niceWarn :: NiceWarnings
    niceWarn  = []
      , _nameId :: NameId
    _nameId   = Word64 -> ModuleNameHash -> NameId
    NameId Word64
    1 ModuleNameHash
    noModuleNameHash
      }

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

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

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

    -- | Lens for field '_loneSigs'.

    loneSigs :: Lens' NiceState LoneSigs
    loneSigs :: Lens' NiceState LoneSigs
    loneSigs LoneSigs -> f LoneSigs
    f NiceState
    e = LoneSigs -> f LoneSigs
    f (NiceState -> LoneSigs
    _loneSigs NiceState
    e) f LoneSigs -> (LoneSigs -> NiceState) -> f NiceState
    forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
    <&> \ LoneSigs
    s -> NiceState
    e { _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.
      x' <- case Name
    x of
        Name{}     -> Name -> Nice Name
    forall a. a -> Nice a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Name
    x
        NoName Range
    r NameId
    _ -> Range -> NameId -> Name
    NoName Range
    r (NameId -> Name) -> Nice NameId -> Nice Name
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Nice NameId
    nextNameId
      loneSigs %== \ 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 a. a -> Nice a
    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 Bool -> Bool
    not (Bool -> Bool) -> Bool -> Bool
    forall a b. (a -> b) -> a -> b
    $ Name -> Bool
    forall a. IsNoName a => a -> Bool
    isNoName Name
    x then Name -> DeclarationException'
    DuplicateDefinition Name
    x else Range -> DeclarationException'
    DuplicateAnonDeclaration Range
    r
      return x'

    -- | Remove a lone signature from the state.

    removeLoneSig :: Name -> Nice ()
    removeLoneSig :: Name -> Nice ()
    removeLoneSig Name
    x = (LoneSigs -> f LoneSigs) -> NiceState -> f NiceState
    Lens' NiceState LoneSigs
    loneSigs Lens' NiceState LoneSigs -> (LoneSigs -> LoneSigs) -> Nice ()
    forall o (m :: * -> *) i.
    MonadState o m =>
    Lens' o i -> (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 a b. (a -> b) -> Maybe a -> Maybe b
    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' NiceState LoneSigs -> Nice LoneSigs
    forall o (m :: * -> *) i. MonadState o m => Lens' o i -> m i
    use (LoneSigs -> f LoneSigs) -> NiceState -> f NiceState
    Lens' NiceState LoneSigs
    loneSigs

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

    noLoneSigs :: Nice Bool
    noLoneSigs :: Nice Bool
    noLoneSigs = LoneSigs -> Bool
    forall a. Null a => a -> Bool
    null (LoneSigs -> Bool) -> Nice LoneSigs -> Nice Bool
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Lens' NiceState LoneSigs -> Nice LoneSigs
    forall o (m :: * -> *) i. MonadState o m => Lens' o i -> m i
    use (LoneSigs -> f LoneSigs) -> NiceState -> f NiceState
    Lens' NiceState LoneSigs
    loneSigs

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

    -- | Ensure that all forward declarations have been given a definition.
    checkLoneSigs :: LoneSigs -> Nice ()
    checkLoneSigs :: LoneSigs -> Nice ()
    checkLoneSigs LoneSigs
    xs = do
      Nice ()
    forgetLoneSigs
      [LoneSig] -> (List1 LoneSig -> Nice ()) -> Nice ()
    forall (m :: * -> *) a.
    Applicative m =>
    [a] -> (List1 a -> m ()) -> m ()
    List1.unlessNull (LoneSigs -> [LoneSig]
    forall k a. Map k a -> [a]
    Map.elems LoneSigs
    xs) \ List1 LoneSig
    ss -> HasCallStack => DeclarationWarning' -> Nice ()
    DeclarationWarning' -> Nice ()
    declarationWarning (DeclarationWarning' -> Nice ()) -> DeclarationWarning' -> Nice ()
    forall a b. (a -> b) -> a -> b
    $ List1 (Name, Range) -> DeclarationWarning'
    MissingDefinitions (List1 (Name, Range) -> DeclarationWarning')
    -> List1 (Name, Range) -> DeclarationWarning'
    forall a b. (a -> b) -> a -> b
    $
        (LoneSig -> (Name, Range)) -> List1 LoneSig -> List1 (Name, Range)
    forall a b. (a -> b) -> NonEmpty a -> NonEmpty b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (\LoneSig
    s -> (LoneSig -> Name
    loneSigName LoneSig
    s , LoneSig -> Range
    loneSigRange LoneSig
    s)) List1 LoneSig
    ss

    -- | Ensure that all forward declarations have been given a definition,
    -- raising an error indicating *why* they would have had to have been
    -- defined.
    breakImplicitMutualBlock :: KwRange -> String -> Nice ()
    breakImplicitMutualBlock :: KwRange -> String -> Nice ()
    breakImplicitMutualBlock KwRange
    r String
    why = do
      m <- Lens' NiceState LoneSigs -> Nice LoneSigs
    forall o (m :: * -> *) i. MonadState o m => Lens' o i -> m i
    use (LoneSigs -> f LoneSigs) -> NiceState -> f NiceState
    Lens' NiceState LoneSigs
    loneSigs
      List1.unlessNull (Map.elems m) $ \ List1 LoneSig
    xs ->
        DeclarationException' -> Nice ()
    forall a. HasCallStack => DeclarationException' -> Nice a
    declarationException (DeclarationException' -> Nice ())
    -> DeclarationException' -> Nice ()
    forall a b. (a -> b) -> a -> b
    $ KwRange -> String -> List1 Name -> DeclarationException'
    DisallowedInterleavedMutual KwRange
    r String
    why (List1 Name -> DeclarationException')
    -> List1 Name -> DeclarationException'
    forall a b. (a -> b) -> a -> b
    $
          -- Andreas, 2023-09-07: We discard the 'loneSigRange's because the 'Name' already has a range.
          (LoneSig -> Name) -> List1 LoneSig -> List1 Name
    forall a b. (a -> b) -> NonEmpty a -> NonEmpty b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap LoneSig -> Name
    loneSigName List1 LoneSig
    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 b c a. (b -> c) -> (a, b) -> (a, c)
    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) -> Bool) -> [(Name, LoneSig)] -> [(Name, LoneSig)]
    forall a. (a -> Bool) -> [a] -> [a]
    filter (DataRecOrFun -> Bool
    isFunName (DataRecOrFun -> Bool)
    -> ((Name, LoneSig) -> DataRecOrFun) -> (Name, LoneSig) -> Bool
    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' NiceState TerminationCheck
    terminationCheckPragma :: Lens' NiceState TerminationCheck
    terminationCheckPragma TerminationCheck -> f TerminationCheck
    f NiceState
    e = TerminationCheck -> f TerminationCheck
    f (NiceState -> TerminationCheck
    _termChk NiceState
    e) f TerminationCheck
    -> (TerminationCheck -> NiceState) -> f NiceState
    forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
    <&> \ TerminationCheck
    s -> NiceState
    e { _termChk = s }

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

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

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

    -- | Lens for field '_posChk'.

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

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

    -- | Lens for field '_uniChk'.

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

    withUniverseCheckPragma :: UniverseCheck -> Nice a -> Nice a
    withUniverseCheckPragma :: forall a. UniverseCheck -> Nice a -> Nice a
    withUniverseCheckPragma UniverseCheck
    uc Nice a
    f = do
      uc_old <- Lens' NiceState UniverseCheck -> Nice UniverseCheck
    forall o (m :: * -> *) i. MonadState o m => Lens' o i -> m i
    use (UniverseCheck -> f UniverseCheck) -> NiceState -> f NiceState
    Lens' NiceState UniverseCheck
    universeCheckPragma
      universeCheckPragma .= uc
      result <- f
      universeCheckPragma .= uc_old
      return 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' NiceState Catchall
    catchallPragma :: Lens' NiceState Catchall
    catchallPragma Catchall -> f Catchall
    f NiceState
    e = Catchall -> f Catchall
    f (NiceState -> Catchall
    _catchall NiceState
    e) f Catchall -> (Catchall -> NiceState) -> f NiceState
    forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
    <&> \ Catchall
    s -> NiceState
    e { _catchall = s }

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

    popCatchallPragma :: Nice Catchall
    popCatchallPragma :: Nice Catchall
    popCatchallPragma = do
      ca <- Lens' NiceState Catchall -> Nice Catchall
    forall o (m :: * -> *) i. MonadState o m => Lens' o i -> m i
    use (Catchall -> f Catchall) -> NiceState -> f NiceState
    Lens' NiceState Catchall
    catchallPragma
      catchallPragma .= empty
      return ca

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

    -- | Add a new warning.
    niceWarning :: DeclarationWarning -> Nice ()
    niceWarning :: DeclarationWarning -> Nice ()
    niceWarning DeclarationWarning
    w = (NiceState -> NiceState) -> Nice ()
    forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
    modify ((NiceState -> NiceState) -> Nice ())
    -> (NiceState -> NiceState) -> Nice ()
    forall a b. (a -> b) -> a -> b
    $ \ NiceState
    st -> NiceState
    st { niceWarn = w : niceWarn 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 a. 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'