    {-# OPTIONS_GHC -Wunused-imports #-}

    {-# LANGUAGE NondecreasingIndentation #-}

    module Agda.TypeChecking.Rules.Decl where

    import Prelude hiding ( null )

    import Control.Monad.Writer (tell)

    import Data.Either (partitionEithers)
    import qualified Data.Foldable as Fold
    import qualified Data.Map.Strict as MapS
    import Data.Maybe
    import qualified Data.Set as Set
    import Data.Set (Set)

    import Agda.Interaction.Highlighting.Generate
    import Agda.Interaction.Options

    import qualified Agda.Syntax.Abstract as A
    import Agda.Syntax.Abstract.Views (deepUnscopeDecl, deepUnscopeDecls)
    import Agda.Syntax.Internal
    import qualified Agda.Syntax.Info as Info
    import Agda.Syntax.Position
    import Agda.Syntax.Common
    import Agda.Syntax.Common.Pretty (prettyShow)
    import Agda.Syntax.Concrete (pattern NoWhere_)
    import Agda.Syntax.Literal
    import Agda.Syntax.Scope.Base ( KindOfName(..) )

    import Agda.TypeChecking.Monad
    import Agda.TypeChecking.Monad.Benchmark (MonadBench, Phase)
    import qualified Agda.TypeChecking.Monad.Benchmark as Bench

    import Agda.TypeChecking.Constraints
    import Agda.TypeChecking.Conversion
    import Agda.TypeChecking.IApplyConfluence
    import Agda.TypeChecking.Generalize
    import Agda.TypeChecking.Injectivity
    import Agda.TypeChecking.InstanceArguments
    import Agda.TypeChecking.Level.Solve
    import Agda.TypeChecking.Positivity
    import Agda.TypeChecking.Positivity.Occurrence
    import Agda.TypeChecking.Polarity
    import Agda.TypeChecking.Pretty
    import Agda.TypeChecking.Primitive
    import Agda.TypeChecking.ProjectionLike
    import Agda.TypeChecking.Unquote
    import Agda.TypeChecking.Records
    import Agda.TypeChecking.RecordPatterns
    import Agda.TypeChecking.Reduce
    import Agda.TypeChecking.Rewriting
    import Agda.TypeChecking.SizedTypes.Solve
    import Agda.TypeChecking.Substitute
    import Agda.TypeChecking.Telescope
    import Agda.TypeChecking.Warnings

    import Agda.TypeChecking.Rules.Application
    import Agda.TypeChecking.Rules.Term
    import Agda.TypeChecking.Rules.Data    ( checkDataDef )
    import Agda.TypeChecking.Rules.Record  ( checkRecDef )
    import Agda.TypeChecking.Rules.Def     ( checkFunDef, newSection, useTerPragma )
    import Agda.TypeChecking.Rules.Builtin
    import Agda.TypeChecking.Rules.Display ( checkDisplayPragma )

    import Agda.Termination.TermCheck

    import Agda.Utils.Function ( applyUnless, applyWhen )
    import Agda.Utils.Functor
    import Agda.Utils.Lens
    import Agda.Utils.List1 ( pattern (:|) )
    import qualified Agda.Utils.List1 as List1
    import Agda.Utils.Maybe
    import Agda.Utils.Monad
    import Agda.Utils.Null
    import Agda.Utils.Size
    import Agda.Utils.Update
    import qualified Agda.Syntax.Common.Pretty as P
    import qualified Agda.Utils.SmallSet as SmallSet

    import Agda.Utils.Impossible

    -- | Cached checkDecl
    checkDeclCached :: A.Declaration -> TCM ()
    checkDeclCached :: Declaration -> TCM ()
    checkDeclCached d :: Declaration
    d@A.ScopedDecl{} = Declaration -> TCM ()
    checkDecl Declaration
    d
    checkDeclCached
      d :: Declaration
    d@(A.Section Range
    _ Erased
    erased ModuleName
    mname (A.GeneralizeTel Map QName Name
    _ Telescope
    tbinds) [Declaration]
    _) = do
      e <- TCMT IO (Maybe (TypeCheckAction, PostScopeState))
    forall (m :: * -> *).
    (MonadDebug m, MonadTCState m, ReadTCState m) =>
    m (Maybe (TypeCheckAction, PostScopeState))
    readFromCachedLog  -- Can ignore the set of generalizable vars (they occur in the telescope)
      reportSLn "cache.decl" 10 $ "checkDeclCached: " ++ show (isJust e)
      case e of
        Just (EnterSection Erased
    erased' ModuleName
    mname' Telescope
    tbinds', PostScopeState
    _)
          | Erased
    erased Erased -> Erased -> Bool
    forall a. Eq a => a -> a -> Bool
    == Erased
    erased' Bool -> Bool -> Bool
    && ModuleName
    mname ModuleName -> ModuleName -> Bool
    forall a. Eq a => a -> a -> Bool
    == ModuleName
    mname' Bool -> Bool -> Bool
    && Telescope
    tbinds Telescope -> Telescope -> Bool
    forall a. Eq a => a -> a -> Bool
    == Telescope
    tbinds' ->
            () -> TCM ()
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
        Maybe (TypeCheckAction, PostScopeState)
    _ -> TCM ()
    forall (m :: * -> *). (MonadDebug m, MonadTCState m) => m ()
    cleanCachedLog
      writeToCurrentLog $ EnterSection erased mname tbinds
      checkDecl d
      readFromCachedLog >>= \case
        Just (LeaveSection ModuleName
    mname', PostScopeState
    _) | ModuleName
    mname ModuleName -> ModuleName -> Bool
    forall a. Eq a => a -> a -> Bool
    == ModuleName
    mname' -> () -> TCM ()
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
        Maybe (TypeCheckAction, PostScopeState)
    _ -> TCM ()
    forall (m :: * -> *). (MonadDebug m, MonadTCState m) => m ()
    cleanCachedLog
      writeToCurrentLog $ LeaveSection mname

    checkDeclCached Declaration
    d = do
        e <- TCMT IO (Maybe (TypeCheckAction, PostScopeState))
    forall (m :: * -> *).
    (MonadDebug m, MonadTCState m, ReadTCState m) =>
    m (Maybe (TypeCheckAction, PostScopeState))
    readFromCachedLog

        reportSLn "cache.decl" 10 $ "checkDeclCached: " ++ show (isJust e)

        case e of
          (Just (Decl Declaration
    d',PostScopeState
    s)) | Declaration -> Declaration -> Bool
    compareDecl Declaration
    d Declaration
    d' -> do
            PostScopeState -> TCM ()
    forall (m :: * -> *).
    (MonadDebug m, MonadTCState m) =>
    PostScopeState -> m ()
    restorePostScopeState PostScopeState
    s
            [Char] -> Int -> [Char] -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> [Char] -> m ()
    reportSLn [Char]
    "cache.decl" Int
    50 ([Char] -> TCM ()) -> [Char] -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ [Char]
    "range: " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ Range -> [Char]
    forall a. Pretty a => a -> [Char]
    prettyShow (Declaration -> Range
    forall a. HasRange a => a -> Range
    getRange Declaration
    d)
            Range -> TCM ()
    printSyntaxInfo (Declaration -> Range
    forall a. HasRange a => a -> Range
    getRange Declaration
    d)
          Maybe (TypeCheckAction, PostScopeState)
    _ -> do
            TCM ()
    forall (m :: * -> *). (MonadDebug m, MonadTCState m) => m ()
    cleanCachedLog
            Declaration -> TCM ()
    checkDeclWrap Declaration
    d
        writeToCurrentLog $ Decl d
     where
       compareDecl :: Declaration -> Declaration -> Bool
    compareDecl A.Section{} A.Section{} = Bool
    forall a. HasCallStack => a
    __IMPOSSIBLE__
       compareDecl A.ScopedDecl{} A.ScopedDecl{} = Bool
    forall a. HasCallStack => a
    __IMPOSSIBLE__
       compareDecl Declaration
    x Declaration
    y = Declaration
    x Declaration -> Declaration -> Bool
    forall a. Eq a => a -> a -> Bool
    == Declaration
    y
       -- changes to CS inside a RecDef or Mutual ought not happen,
       -- but they do happen, so we discard them.
       ignoreChanges :: m a -> m a
    ignoreChanges m a
    m = m a -> m a
    forall (m :: * -> *) a.
    (MonadTCState m, ReadTCState m) =>
    m a -> m a
    localCache (m a -> m a) -> m a -> m a
    forall a b. (a -> b) -> a -> b
    $ do
         m ()
    forall (m :: * -> *). (MonadDebug m, MonadTCState m) => m ()
    cleanCachedLog
         m a
    m
       checkDeclWrap :: Declaration -> TCM ()
    checkDeclWrap d :: Declaration
    d@A.RecDef{} = TCM () -> TCM ()
    forall {m :: * -> *} {a}.
    (MonadTCState m, ReadTCState m, MonadDebug m) =>
    m a -> m a
    ignoreChanges (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ Declaration -> TCM ()
    checkDecl Declaration
    d
       checkDeclWrap d :: Declaration
    d@A.Mutual{} = TCM () -> TCM ()
    forall {m :: * -> *} {a}.
    (MonadTCState m, ReadTCState m, MonadDebug m) =>
    m a -> m a
    ignoreChanges (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ Declaration -> TCM ()
    checkDecl Declaration
    d
       checkDeclWrap Declaration
    d            = Declaration -> TCM ()
    checkDecl Declaration
    d

    -- | Type check a sequence of declarations.
    checkDecls :: [A.Declaration] -> TCM ()
    checkDecls :: [Declaration] -> TCM ()
    checkDecls [Declaration]
    ds = do
      [Char] -> Int -> [Char] -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> [Char] -> m ()
    reportSLn [Char]
    "tc.decl" Int
    45 ([Char] -> TCM ()) -> [Char] -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ [Char]
    "Checking " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ Int -> [Char]
    forall a. Show a => a -> [Char]
    show ([Declaration] -> Int
    forall a. [a] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length [Declaration]
    ds) [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    " declarations..."
      (Declaration -> TCM ()) -> [Declaration] -> TCM ()
    forall (t :: * -> *) (m :: * -> *) a b.
    (Foldable t, Monad m) =>
    (a -> m b) -> t a -> m ()
    mapM_ Declaration -> TCM ()
    checkDecl [Declaration]
    ds

    -- | Type check a single declaration.

    checkDecl :: A.Declaration -> TCM ()
    checkDecl :: Declaration -> TCM ()
    checkDecl Declaration
    d = Declaration -> TCM () -> TCM ()
    forall (m :: * -> *) x a.
    (MonadTrace m, HasRange x) =>
    x -> m a -> m a
    setCurrentRange Declaration
    d (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ do
        [Char] -> Int -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "tc.decl" Int
    10 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Doc
    "checking declaration"
        Declaration -> TCM ()
    debugPrintDecl Declaration
    d
        [Char] -> Int -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "tc.decl" Int
    90 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ ([Char] -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => [Char] -> m Doc
    text ([Char] -> TCMT IO Doc)
    -> ([Declaration] -> [Char]) -> [Declaration] -> TCMT IO Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [Declaration] -> [Char]
    forall a. Show a => a -> [Char]
    show) (Declaration -> [Declaration]
    deepUnscopeDecl Declaration
    d)
        [Char] -> Int -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "tc.decl" Int
    10 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ Declaration -> TCMT IO Doc
    forall a (m :: * -> *).
    (ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
    a -> m Doc
    prettyA Declaration
    d  -- Might loop, see e.g. Issue 1597

        let -- What kind of final checks/computations should be performed
            -- if we're not inside a mutual block?
            none :: f a -> f (Maybe a)
    none        f a
    m = f a
    m f a -> Maybe a -> f (Maybe a)
    forall (f :: * -> *) a b. Functor f => f a -> b -> f b
    $>  Maybe a
    forall a. Maybe a
    Nothing           -- skip all checks
            meta :: f a -> f (Maybe (m ()))
    meta        f a
    m = f a
    m f a -> Maybe (m ()) -> f (Maybe (m ()))
    forall (f :: * -> *) a b. Functor f => f a -> b -> f b
    $>  m () -> Maybe (m ())
    forall a. a -> Maybe a
    Just (() -> m ()
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ())  -- do the usual checks
            mutual :: MutualInfo
    -> [Declaration]
    -> TCMT IO (MutualId, Set QName)
    -> TCMT IO (Maybe (TCM ()))
    mutual MutualInfo
    i [Declaration]
    ds TCMT IO (MutualId, Set QName)
    m = TCMT IO (MutualId, Set QName)
    m TCMT IO (MutualId, Set QName)
    -> ((MutualId, Set QName) -> Maybe (TCM ()))
    -> TCMT IO (Maybe (TCM ()))
    forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
    <&> TCM () -> Maybe (TCM ())
    forall a. a -> Maybe a
    Just (TCM () -> Maybe (TCM ()))
    -> ((MutualId, Set QName) -> TCM ())
    -> (MutualId, Set QName)
    -> Maybe (TCM ())
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (MutualId -> Set QName -> TCM ())
    -> (MutualId, Set QName) -> TCM ()
    forall a b c. (a -> b -> c) -> (a, b) -> c
    uncurry (MutualInfo
    -> Declaration -> [Declaration] -> MutualId -> Set QName -> TCM ()
    mutualChecks MutualInfo
    i Declaration
    d [Declaration]
    ds)
            impossible :: f a -> f b
    impossible  f a
    m = f a
    m f a -> b -> f b
    forall (f :: * -> *) a b. Functor f => f a -> b -> f b
    $>  b
    forall a. HasCallStack => a
    __IMPOSSIBLE__
                            -- We're definitely inside a mutual block.

        (finalChecks, metas) <- TCMT IO (Maybe (TCM ()))
    -> TCMT IO (Maybe (TCM ()), LocalMetaStores)
    forall (m :: * -> *) a.
    ReadTCState m =>
    m a -> m (a, LocalMetaStores)
    metasCreatedBy (TCMT IO (Maybe (TCM ()))
     -> TCMT IO (Maybe (TCM ()), LocalMetaStores))
    -> TCMT IO (Maybe (TCM ()))
    -> TCMT IO (Maybe (TCM ()), LocalMetaStores)
    forall a b. (a -> b) -> a -> b
    $ case Declaration
    d of
          A.Axiom{}                -> TCM () -> TCMT IO (Maybe (TCM ()))
    forall {m :: * -> *} {f :: * -> *} {a}.
    (Monad m, Functor f) =>
    f a -> f (Maybe (m ()))
    meta (TCM () -> TCMT IO (Maybe (TCM ())))
    -> TCM () -> TCMT IO (Maybe (TCM ()))
    forall a b. (a -> b) -> a -> b
    $ Declaration -> TCM ()
    checkTypeSignature Declaration
    d
          A.Generalize Set QName
    s DefInfo
    i ArgInfo
    info QName
    x Expr
    e -> TCM () -> TCMT IO (Maybe (TCM ()))
    forall {m :: * -> *} {f :: * -> *} {a}.
    (Monad m, Functor f) =>
    f a -> f (Maybe (m ()))
    meta (TCM () -> TCMT IO (Maybe (TCM ())))
    -> TCM () -> TCMT IO (Maybe (TCM ()))
    forall a b. (a -> b) -> a -> b
    $ TCM () -> TCM ()
    forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
    inConcreteMode (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ Set QName -> DefInfo -> ArgInfo -> QName -> Expr -> TCM ()
    checkGeneralize Set QName
    s DefInfo
    i ArgInfo
    info QName
    x Expr
    e
          A.Field{}                -> TypeError -> TCMT IO (Maybe (TCM ()))
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    TypeError -> m a
    typeError TypeError
    FieldOutsideRecord
          A.Primitive DefInfo
    i QName
    x Arg Expr
    e        -> TCM () -> TCMT IO (Maybe (TCM ()))
    forall {m :: * -> *} {f :: * -> *} {a}.
    (Monad m, Functor f) =>
    f a -> f (Maybe (m ()))
    meta (TCM () -> TCMT IO (Maybe (TCM ())))
    -> TCM () -> TCMT IO (Maybe (TCM ()))
    forall a b. (a -> b) -> a -> b
    $ DefInfo -> QName -> Arg Expr -> TCM ()
    checkPrimitive DefInfo
    i QName
    x Arg Expr
    e
          A.Mutual MutualInfo
    i [Declaration]
    ds            -> MutualInfo
    -> [Declaration]
    -> TCMT IO (MutualId, Set QName)
    -> TCMT IO (Maybe (TCM ()))
    mutual MutualInfo
    i [Declaration]
    ds (TCMT IO (MutualId, Set QName) -> TCMT IO (Maybe (TCM ())))
    -> TCMT IO (MutualId, Set QName) -> TCMT IO (Maybe (TCM ()))
    forall a b. (a -> b) -> a -> b
    $ MutualInfo -> [Declaration] -> TCMT IO (MutualId, Set QName)
    checkMutual MutualInfo
    i [Declaration]
    ds
          A.Section Range
    _r Erased
    er ModuleName
    x GeneralizeTelescope
    tel [Declaration]
    ds -> TCM () -> TCMT IO (Maybe (TCM ()))
    forall {m :: * -> *} {f :: * -> *} {a}.
    (Monad m, Functor f) =>
    f a -> f (Maybe (m ()))
    meta (TCM () -> TCMT IO (Maybe (TCM ())))
    -> TCM () -> TCMT IO (Maybe (TCM ()))
    forall a b. (a -> b) -> a -> b
    $ Erased
    -> ModuleName -> GeneralizeTelescope -> [Declaration] -> TCM ()
    checkSection Erased
    er ModuleName
    x GeneralizeTelescope
    tel [Declaration]
    ds
          A.Apply ModuleInfo
    i Erased
    er ModuleName
    x ModuleApplication
    mapp ScopeCopyInfo
    ci ImportDirective
    d -> TCM () -> TCMT IO (Maybe (TCM ()))
    forall {m :: * -> *} {f :: * -> *} {a}.
    (Monad m, Functor f) =>
    f a -> f (Maybe (m ()))
    meta (TCM () -> TCMT IO (Maybe (TCM ())))
    -> TCM () -> TCMT IO (Maybe (TCM ()))
    forall a b. (a -> b) -> a -> b
    $ ModuleInfo
    -> Erased
    -> ModuleName
    -> ModuleApplication
    -> ScopeCopyInfo
    -> ImportDirective
    -> TCM ()
    checkSectionApplication ModuleInfo
    i Erased
    er ModuleName
    x ModuleApplication
    mapp ScopeCopyInfo
    ci ImportDirective
    d
          A.Import ModuleInfo
    _ ModuleName
    _ ImportDirective
    dir         -> TCM () -> TCMT IO (Maybe (TCM ()))
    forall {f :: * -> *} {a} {a}. Functor f => f a -> f (Maybe a)
    none (TCM () -> TCMT IO (Maybe (TCM ())))
    -> TCM () -> TCMT IO (Maybe (TCM ()))
    forall a b. (a -> b) -> a -> b
    $ ImportDirective -> TCM ()
    checkImportDirective ImportDirective
    dir
          A.Pragma Range
    i Pragma
    p             -> TCM () -> TCMT IO (Maybe (TCM ()))
    forall {f :: * -> *} {a} {a}. Functor f => f a -> f (Maybe a)
    none (TCM () -> TCMT IO (Maybe (TCM ())))
    -> TCM () -> TCMT IO (Maybe (TCM ()))
    forall a b. (a -> b) -> a -> b
    $ Range -> Pragma -> TCM ()
    checkPragma Range
    i Pragma
    p
          A.ScopedDecl ScopeInfo
    scope [Declaration]
    ds    -> TCM () -> TCMT IO (Maybe (TCM ()))
    forall {f :: * -> *} {a} {a}. Functor f => f a -> f (Maybe a)
    none (TCM () -> TCMT IO (Maybe (TCM ())))
    -> TCM () -> TCMT IO (Maybe (TCM ()))
    forall a b. (a -> b) -> a -> b
    $ ScopeInfo -> TCM ()
    setScope ScopeInfo
    scope TCM () -> TCM () -> TCM ()
    forall a b. TCMT IO a -> TCMT IO b -> TCMT IO b
    forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
    >> (Declaration -> TCM ()) -> [Declaration] -> TCM ()
    forall (t :: * -> *) (m :: * -> *) a b.
    (Foldable t, Monad m) =>
    (a -> m b) -> t a -> m ()
    mapM_ Declaration -> TCM ()
    checkDeclCached [Declaration]
    ds
          A.FunDef DefInfo
    i QName
    x [Clause]
    cs          -> TCM () -> TCMT IO (Maybe (TCM ()))
    forall {f :: * -> *} {a} {b}. Functor f => f a -> f b
    impossible (TCM () -> TCMT IO (Maybe (TCM ())))
    -> TCM () -> TCMT IO (Maybe (TCM ()))
    forall a b. (a -> b) -> a -> b
    $ QName -> DefInfo -> TCM () -> TCM ()
    forall (m :: * -> *) i a.
    (MonadTCEnv m, MonadPretty m, MonadDebug m, MonadBench m,
     BenchPhase m ~ Phase, AnyIsAbstract i, AllAreOpaque i) =>
    QName -> i -> m a -> m a
    check QName
    x DefInfo
    i (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ DefInfo -> QName -> [Clause] -> TCM ()
    checkFunDef DefInfo
    i QName
    x [Clause]
    cs
          A.DataDef DefInfo
    i QName
    x UniverseCheck
    uc DataDefParams
    ps [Declaration]
    cs   -> TCM () -> TCMT IO (Maybe (TCM ()))
    forall {f :: * -> *} {a} {b}. Functor f => f a -> f b
    impossible (TCM () -> TCMT IO (Maybe (TCM ())))
    -> TCM () -> TCMT IO (Maybe (TCM ()))
    forall a b. (a -> b) -> a -> b
    $ QName -> DefInfo -> TCM () -> TCM ()
    forall (m :: * -> *) i a.
    (MonadTCEnv m, MonadPretty m, MonadDebug m, MonadBench m,
     BenchPhase m ~ Phase, AnyIsAbstract i, AllAreOpaque i) =>
    QName -> i -> m a -> m a
    check QName
    x DefInfo
    i (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ DefInfo
    -> QName
    -> UniverseCheck
    -> DataDefParams
    -> [Declaration]
    -> TCM ()
    checkDataDef DefInfo
    i QName
    x UniverseCheck
    uc DataDefParams
    ps [Declaration]
    cs
          A.RecDef DefInfo
    i QName
    x UniverseCheck
    uc RecordDirectives
    dir DataDefParams
    ps Expr
    tel [Declaration]
    cs -> TCMT IO (MutualId, Set QName) -> TCMT IO (Maybe (TCM ()))
    forall {f :: * -> *} {a} {b}. Functor f => f a -> f b
    impossible (TCMT IO (MutualId, Set QName) -> TCMT IO (Maybe (TCM ())))
    -> TCMT IO (MutualId, Set QName) -> TCMT IO (Maybe (TCM ()))
    forall a b. (a -> b) -> a -> b
    $ QName
    -> DefInfo
    -> TCMT IO (MutualId, Set QName)
    -> TCMT IO (MutualId, Set QName)
    forall (m :: * -> *) i a.
    (MonadTCEnv m, MonadPretty m, MonadDebug m, MonadBench m,
     BenchPhase m ~ Phase, AnyIsAbstract i, AllAreOpaque i) =>
    QName -> i -> m a -> m a
    check QName
    x DefInfo
    i (TCMT IO (MutualId, Set QName) -> TCMT IO (MutualId, Set QName))
    -> TCMT IO (MutualId, Set QName) -> TCMT IO (MutualId, Set QName)
    forall a b. (a -> b) -> a -> b
    $ do
                                        DefInfo
    -> QName
    -> UniverseCheck
    -> RecordDirectives
    -> DataDefParams
    -> Expr
    -> [Declaration]
    -> TCM ()
    checkRecDef DefInfo
    i QName
    x UniverseCheck
    uc RecordDirectives
    dir DataDefParams
    ps Expr
    tel [Declaration]
    cs
                                        blockId <- Definition -> MutualId
    defMutual (Definition -> MutualId) -> TCMT IO Definition -> TCMT IO MutualId
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> QName -> TCMT IO Definition
    forall (m :: * -> *). HasConstInfo m => QName -> m Definition
    getConstInfo QName
    x

                                        -- Andreas, 2016-10-01 testing whether
                                        -- envMutualBlock is set correctly.
                                        -- Apparently not.
                                        verboseS "tc.decl.mutual" 70 $ do
                                          current <- asksTC envMutualBlock
                                          unless (Just blockId == current) $ do
                                            reportS "" 0
                                              [ "mutual block id discrepancy for " ++ prettyShow x
                                              , "  current    mut. bl. = " ++ show current
                                              , "  calculated mut. bl. = " ++ show blockId
                                              ]

                                        return (blockId, Set.singleton x)
          A.DataSig DefInfo
    i Erased
    er QName
    x GeneralizeTelescope
    ps Expr
    t    -> TCM () -> TCMT IO (Maybe (TCM ()))
    forall {f :: * -> *} {a} {b}. Functor f => f a -> f b
    impossible (TCM () -> TCMT IO (Maybe (TCM ())))
    -> TCM () -> TCMT IO (Maybe (TCM ()))
    forall a b. (a -> b) -> a -> b
    $ KindOfName
    -> DefInfo
    -> Erased
    -> QName
    -> GeneralizeTelescope
    -> Expr
    -> TCM ()
    checkSig KindOfName
    DataName DefInfo
    i Erased
    er QName
    x GeneralizeTelescope
    ps Expr
    t
          A.RecSig DefInfo
    i Erased
    er QName
    x GeneralizeTelescope
    ps Expr
    t     -> TCM () -> TCMT IO (Maybe (TCM ()))
    forall {f :: * -> *} {a} {a}. Functor f => f a -> f (Maybe a)
    none (TCM () -> TCMT IO (Maybe (TCM ())))
    -> TCM () -> TCMT IO (Maybe (TCM ()))
    forall a b. (a -> b) -> a -> b
    $ KindOfName
    -> DefInfo
    -> Erased
    -> QName
    -> GeneralizeTelescope
    -> Expr
    -> TCM ()
    checkSig KindOfName
    RecName DefInfo
    i Erased
    er QName
    x GeneralizeTelescope
    ps Expr
    t
                                      -- A record signature is always followed by a
                                      -- record definition. Metas should not be
                                      -- frozen until after the definition has been
                                      -- checked. NOTE: Metas are not frozen
                                      -- immediately after the last field. Perhaps
                                      -- they should be (unless we're in a mutual
                                      -- block).
          A.Open ModuleInfo
    _ ModuleName
    _ ImportDirective
    dir           -> TCM () -> TCMT IO (Maybe (TCM ()))
    forall {f :: * -> *} {a} {a}. Functor f => f a -> f (Maybe a)
    none (TCM () -> TCMT IO (Maybe (TCM ())))
    -> TCM () -> TCMT IO (Maybe (TCM ()))
    forall a b. (a -> b) -> a -> b
    $ ImportDirective -> TCM ()
    checkImportDirective ImportDirective
    dir
          A.UnfoldingDecl{}        -> TCM () -> TCMT IO (Maybe (TCM ()))
    forall {f :: * -> *} {a} {a}. Functor f => f a -> f (Maybe a)
    none (TCM () -> TCMT IO (Maybe (TCM ())))
    -> TCM () -> TCMT IO (Maybe (TCM ()))
    forall a b. (a -> b) -> a -> b
    $ () -> TCM ()
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
          A.PatternSynDef{}        -> TCM () -> TCMT IO (Maybe (TCM ()))
    forall {f :: * -> *} {a} {a}. Functor f => f a -> f (Maybe a)
    none (TCM () -> TCMT IO (Maybe (TCM ())))
    -> TCM () -> TCMT IO (Maybe (TCM ()))
    forall a b. (a -> b) -> a -> b
    $ () -> TCM ()
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
                                      -- Open and PatternSynDef are just artifacts
                                      -- from the concrete syntax, retained for
                                      -- highlighting purposes.
          -- Andreas, 2019-08-19, issue #4010, observe @abstract@ also for unquoting.
          -- TODO: is it possible that some of the unquoted declarations/definitions
          -- are abstract and some are not?  Then allowing all to look into abstract things,
          -- as we do here, will leak information about the implementation of abstract things.
          -- TODO: Benchmarking for unquote.
          A.UnquoteDecl MutualInfo
    mi [DefInfo]
    is [QName]
    xs Expr
    e -> [DefInfo] -> TCMT IO (Maybe (TCM ())) -> TCMT IO (Maybe (TCM ()))
    forall (m :: * -> *) i a.
    (MonadTCEnv m, AnyIsAbstract i, AllAreOpaque i) =>
    i -> m a -> m a
    checkMaybeAbstractly [DefInfo]
    is (TCMT IO (Maybe (TCM ())) -> TCMT IO (Maybe (TCM ())))
    -> TCMT IO (Maybe (TCM ())) -> TCMT IO (Maybe (TCM ()))
    forall a b. (a -> b) -> a -> b
    $ MutualInfo
    -> [DefInfo] -> [QName] -> Expr -> TCMT IO (Maybe (TCM ()))
    checkUnquoteDecl MutualInfo
    mi [DefInfo]
    is [QName]
    xs Expr
    e
          A.UnquoteDef [DefInfo]
    is [QName]
    xs Expr
    e     -> TCM () -> TCMT IO (Maybe (TCM ()))
    forall {f :: * -> *} {a} {b}. Functor f => f a -> f b
    impossible (TCM () -> TCMT IO (Maybe (TCM ())))
    -> TCM () -> TCMT IO (Maybe (TCM ()))
    forall a b. (a -> b) -> a -> b
    $ [DefInfo] -> TCM () -> TCM ()
    forall (m :: * -> *) i a.
    (MonadTCEnv m, AnyIsAbstract i, AllAreOpaque i) =>
    i -> m a -> m a
    checkMaybeAbstractly [DefInfo]
    is (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ [DefInfo] -> [QName] -> Expr -> TCM ()
    checkUnquoteDef [DefInfo]
    is [QName]
    xs Expr
    e
          A.UnquoteData [DefInfo]
    is QName
    x UniverseCheck
    uc [DefInfo]
    js [QName]
    cs Expr
    e -> [DefInfo] -> TCMT IO (Maybe (TCM ())) -> TCMT IO (Maybe (TCM ()))
    forall (m :: * -> *) i a.
    (MonadTCEnv m, AnyIsAbstract i, AllAreOpaque i) =>
    i -> m a -> m a
    checkMaybeAbstractly ([DefInfo]
    is [DefInfo] -> [DefInfo] -> [DefInfo]
    forall a. [a] -> [a] -> [a]
    ++ [DefInfo]
    js) (TCMT IO (Maybe (TCM ())) -> TCMT IO (Maybe (TCM ())))
    -> TCMT IO (Maybe (TCM ())) -> TCMT IO (Maybe (TCM ()))
    forall a b. (a -> b) -> a -> b
    $ do
            [Char] -> Int -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "tc.unquote.data" Int
    20 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Doc
    "Checking unquoteDecl data" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> QName -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => QName -> m Doc
    prettyTCM QName
    x
            Maybe (TCM ())
    forall a. Maybe a
    Nothing Maybe (TCM ()) -> TCMT IO [QName] -> TCMT IO (Maybe (TCM ()))
    forall a b. a -> TCMT IO b -> TCMT IO a
    forall (f :: * -> *) a b. Functor f => a -> f b -> f a
    <$ [QName] -> Expr -> TCMT IO [QName]
    unquoteTop (QName
    xQName -> [QName] -> [QName]
    forall a. a -> [a] -> [a]
    :[QName]
    cs) Expr
    e

        whenNothingM (asksTC envMutualBlock) $ do

          -- Syntax highlighting.
          highlight_ DontHightlightModuleContents d

          -- Defaulting of levels (only when --cumulativity)
          whenM (optCumulativity <$> pragmaOptions) $
            defaultLevelsToZero (openMetas metas)

          -- Post-typing checks.
          whenJust finalChecks \TCM ()
    theMutualChecks -> do
            [Char] -> Int -> [Char] -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> [Char] -> m ()
    reportSLn [Char]
    "tc.decl" Int
    20 ([Char] -> TCM ()) -> [Char] -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ [Char]
    "Attempting to solve constraints before freezing."
            Lens' TCState Bool -> (Bool -> Bool) -> TCM () -> TCM ()
    forall a b. Lens' TCState a -> (a -> a) -> TCMT IO b -> TCMT IO b
    forall (m :: * -> *) a b.
    ReadTCState m =>
    Lens' TCState a -> (a -> a) -> m b -> m b
    locallyTCState (Bool -> f Bool) -> TCState -> f TCState
    Lens' TCState Bool
    stInstanceHack (Bool -> Bool -> Bool
    forall a b. a -> b -> a
    const Bool
    True) (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $
              TCM ()
    wakeupConstraints_   -- solve emptiness and instance constraints

            checkingWhere <- (TCEnv -> WhereClause_) -> TCMT IO WhereClause_
    forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
    asksTC TCEnv -> WhereClause_
    envCheckingWhere
            solveSizeConstraints $ if checkingWhere /= NoWhere_ then DontDefaultToInfty else DefaultToInfty
            wakeupConstraints_   -- Size solver might have unblocked some constraints

            case d of
              A.Generalize{} -> () -> TCM ()
    forall a. a -> TCMT IO a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure ()
              Declaration
    _ -> do
                [Char] -> Int -> [Char] -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> [Char] -> m ()
    reportSLn [Char]
    "tc.decl" Int
    20 ([Char] -> TCM ()) -> [Char] -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ [Char]
    "Freezing all open metas."
                TCMT IO (Set MetaId) -> TCM ()
    forall (f :: * -> *) a. Functor f => f a -> f ()
    void (TCMT IO (Set MetaId) -> TCM ()) -> TCMT IO (Set MetaId) -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ LocalMetaStore -> TCMT IO (Set MetaId)
    forall (m :: * -> *).
    (MonadTCState m, ReadTCState m) =>
    LocalMetaStore -> m (Set MetaId)
    freezeMetas (LocalMetaStores -> LocalMetaStore
    openMetas LocalMetaStores
    metas)

            theMutualChecks

        where

        -- Switch maybe to abstract mode, benchmark, and debug print bracket.
        check :: forall m i a
              . ( MonadTCEnv m, MonadPretty m, MonadDebug m
                , MonadBench m, Bench.BenchPhase m ~ Phase
                , AnyIsAbstract i
                , AllAreOpaque i
                )
              => QName -> i -> m a -> m a
        check :: forall (m :: * -> *) i a.
    (MonadTCEnv m, MonadPretty m, MonadDebug m, MonadBench m,
     BenchPhase m ~ Phase, AnyIsAbstract i, AllAreOpaque i) =>
    QName -> i -> m a -> m a
    check QName
    x i
    i m a
    m = Account (BenchPhase m) -> m a -> m a
    forall (m :: * -> *) c.
    MonadBench m =>
    Account (BenchPhase m) -> m c -> m c
    Bench.billTo [QName -> Phase
    Bench.Definition QName
    x] (m a -> m a) -> m a -> m a
    forall a b. (a -> b) -> a -> b
    $ do
          [Char] -> Int -> TCMT IO Doc -> m ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "tc.decl" Int
    5 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
    forall a b. (a -> b) -> a -> b
    $ (TCMT IO Doc
    "Checking" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> QName -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => QName -> m Doc
    prettyTCM QName
    x) TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall a. Semigroup a => a -> a -> a
    <> TCMT IO Doc
    "."
          [Char] -> Int -> [Char] -> m ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> [Char] -> m ()
    reportSLn [Char]
    "tc.decl.abstract" Int
    25 ([Char] -> m ()) -> [Char] -> m ()
    forall a b. (a -> b) -> a -> b
    $ IsAbstract -> [Char]
    forall a. Show a => a -> [Char]
    show (IsAbstract -> [Char]) -> IsAbstract -> [Char]
    forall a b. (a -> b) -> a -> b
    $ i -> IsAbstract
    forall a. AnyIsAbstract a => a -> IsAbstract
    anyIsAbstract i
    i
          r <- i -> m a -> m a
    forall (m :: * -> *) i a.
    (MonadTCEnv m, AnyIsAbstract i, AllAreOpaque i) =>
    i -> m a -> m a
    checkMaybeAbstractly i
    i m a
    m
          reportSDoc "tc.decl" 5 $ ("Checked" <+> prettyTCM x) <> "."
          return r

        -- Switch to AbstractMode if any of the i is AbstractDef.
        checkMaybeAbstractly :: forall m i a . ( MonadTCEnv m, AnyIsAbstract i, AllAreOpaque i )
                             => i -> m a -> m a
        checkMaybeAbstractly :: forall (m :: * -> *) i a.
    (MonadTCEnv m, AnyIsAbstract i, AllAreOpaque i) =>
    i -> m a -> m a
    checkMaybeAbstractly i
    abs m a
    cont = do
          let
            k1 :: m a -> m a
    k1 = (TCEnv -> TCEnv) -> m a -> m a
    forall a. (TCEnv -> TCEnv) -> m a -> m a
    forall (m :: * -> *) a.
    MonadTCEnv m =>
    (TCEnv -> TCEnv) -> m a -> m a
    localTC (Lens' TCEnv IsAbstract -> LensSet TCEnv IsAbstract
    forall o i. Lens' o i -> LensSet o i
    set (IsAbstract -> f IsAbstract) -> TCEnv -> f TCEnv
    forall a. LensIsAbstract a => Lens' a IsAbstract
    Lens' TCEnv IsAbstract
    lensIsAbstract (i -> IsAbstract
    forall a. AnyIsAbstract a => a -> IsAbstract
    anyIsAbstract i
    abs))
          k2 <- case i -> JointOpacity
    forall a. AllAreOpaque a => a -> JointOpacity
    jointOpacity i
    abs of
            UniqueOpaque OpaqueId
    i     -> (m a -> m a) -> m (m a -> m a)
    forall a. a -> m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure ((m a -> m a) -> m (m a -> m a)) -> (m a -> m a) -> m (m a -> m a)
    forall a b. (a -> b) -> a -> b
    $ (TCEnv -> TCEnv) -> m a -> m a
    forall a. (TCEnv -> TCEnv) -> m a -> m a
    forall (m :: * -> *) a.
    MonadTCEnv m =>
    (TCEnv -> TCEnv) -> m a -> m a
    localTC ((TCEnv -> TCEnv) -> m a -> m a) -> (TCEnv -> TCEnv) -> m a -> m a
    forall a b. (a -> b) -> a -> b
    $ \TCEnv
    env -> TCEnv
    env { envCurrentOpaqueId = Just i }
            JointOpacity
    NoOpaque           -> (m a -> m a) -> m (m a -> m a)
    forall a. a -> m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure m a -> m a
    forall a. a -> a
    id
            DifferentOpaque HashSet OpaqueId
    hs -> m (m a -> m a)
    forall a. HasCallStack => a
    __IMPOSSIBLE__
          k1 (k2 cont)

    -- Some checks that should be run at the end of a mutual block. The
    -- set names contains the names defined in the mutual block.
    mutualChecks :: Info.MutualInfo -> A.Declaration -> [A.Declaration] -> MutualId -> Set QName -> TCM ()
    mutualChecks :: MutualInfo
    -> Declaration -> [Declaration] -> MutualId -> Set QName -> TCM ()
    mutualChecks MutualInfo
    mi Declaration
    d [Declaration]
    ds MutualId
    mid Set QName
    names = do
      -- Andreas, 2014-04-11: instantiate metas in definition types
      let nameList :: [QName]
    nameList = Set QName -> [QName]
    forall a. Set a -> [a]
    Set.toList Set QName
    names
      (QName -> TCM ()) -> [QName] -> TCM ()
    forall (t :: * -> *) (m :: * -> *) a b.
    (Foldable t, Monad m) =>
    (a -> m b) -> t a -> m ()
    mapM_ QName -> TCM ()
    instantiateDefinitionType [QName]
    nameList
      -- Andreas, 2017-03-23: check positivity before termination.
      -- This allows us to reuse the information about SCCs
      -- to skip termination of non-recursive functions.
      (AllowedReductions -> AllowedReductions) -> TCM () -> TCM ()
    forall (m :: * -> *) a.
    MonadTCEnv m =>
    (AllowedReductions -> AllowedReductions) -> m a -> m a
    modifyAllowedReductions (AllowedReduction -> AllowedReductions -> AllowedReductions
    forall a. SmallSetElement a => a -> SmallSet a -> SmallSet a
    SmallSet.delete AllowedReduction
    UnconfirmedReductions) (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $
        MutualInfo -> Set QName -> TCM ()
    checkPositivity_ MutualInfo
    mi Set QName
    names
      -- Andreas, 2013-02-27: check termination before injectivity,
      -- to avoid making the injectivity checker loop.
      (TCEnv -> TCEnv) -> TCM () -> TCM ()
    forall a. (TCEnv -> TCEnv) -> TCMT IO a -> TCMT IO a
    forall (m :: * -> *) a.
    MonadTCEnv m =>
    (TCEnv -> TCEnv) -> m a -> m a
    localTC (\ TCEnv
    e -> TCEnv
    e { envMutualBlock = Just mid }) (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $
        Declaration -> TCM ()
    checkTermination_ Declaration
    d
      [QName] -> TCM ()
    revisitRecordPatternTranslation [QName]
    nameList -- Andreas, 2016-11-19 issue #2308

      (QName -> TCM ()) -> [QName] -> TCM ()
    forall (t :: * -> *) (m :: * -> *) a b.
    (Foldable t, Monad m) =>
    (a -> m b) -> t a -> m ()
    mapM_ QName -> TCM ()
    checkIApplyConfluence_ [QName]
    nameList

      -- Andreas, 2015-03-26 Issue 1470:
      -- Restricting coinduction to recursive does not solve the
      -- actual problem, and prevents interesting sound applications
      -- of sized types.
      -- checkCoinductiveRecords  ds

      -- Andreas, 2019-07-11: The following remarks about injectivity
      -- and polarity seem outdated, since the UnusedArg Relevance has
      -- been removed.
      -- -- Andreas, 2012-09-11:  Injectivity check stores clauses
      -- -- whose 'Relevance' is affected by polarity computation,
      -- -- so do it here (again).
      -- -- Andreas, 2015-07-01:  In particular, 'UnusedArg's of local functions
      -- -- are only recognized after the polarity computation.
      -- -- See Issue 1366 for an example where injectivity of a local function
      -- -- is used to solve metas.  It fails if we do injectivity analysis
      -- -- before polarity only.
      -- However, we need to repeat injectivity checking after termination checking,
      -- since more reductions are available after termination checking, thus,
      -- more instances of injectivity can be recognized.
      Set QName -> TCM ()
    checkInjectivity_        Set QName
    names
      Set QName -> TCM ()
    checkProjectionLikeness_ Set QName
    names

    -- | Check if there is a inferred eta record type in the mutual block.
    --   If yes, repeat the record pattern translation for all function definitions
    --   in the block.
    --   This is necessary since the original record pattern translation will
    --   have skipped record patterns of the new record types (as eta was off for them).
    --   See issue #2308 (and #2197).
    revisitRecordPatternTranslation :: [QName] -> TCM ()
    revisitRecordPatternTranslation :: [QName] -> TCM ()
    revisitRecordPatternTranslation [QName]
    qs = do
      -- rs: inferred eta record types of this mutual block
      -- qccs: compiled clauses of definitions
      (rs, qccs) <- [Either QName (QName, CompiledClauses)]
    -> ([QName], [(QName, CompiledClauses)])
    forall a b. [Either a b] -> ([a], [b])
    partitionEithers ([Either QName (QName, CompiledClauses)]
     -> ([QName], [(QName, CompiledClauses)]))
    -> ([Maybe (Either QName (QName, CompiledClauses))]
        -> [Either QName (QName, CompiledClauses)])
    -> [Maybe (Either QName (QName, CompiledClauses))]
    -> ([QName], [(QName, CompiledClauses)])
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [Maybe (Either QName (QName, CompiledClauses))]
    -> [Either QName (QName, CompiledClauses)]
    forall a. [Maybe a] -> [a]
    catMaybes ([Maybe (Either QName (QName, CompiledClauses))]
     -> ([QName], [(QName, CompiledClauses)]))
    -> TCMT IO [Maybe (Either QName (QName, CompiledClauses))]
    -> TCMT IO ([QName], [(QName, CompiledClauses)])
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (QName -> TCMT IO (Maybe (Either QName (QName, CompiledClauses))))
    -> [QName]
    -> TCMT IO [Maybe (Either QName (QName, CompiledClauses))]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
    mapM QName -> TCMT IO (Maybe (Either QName (QName, CompiledClauses)))
    forall {m :: * -> *}.
    HasConstInfo m =>
    QName -> m (Maybe (Either QName (QName, CompiledClauses)))
    classify [QName]
    qs
      unless (null rs) $ forM_ qccs $ \(QName
    q,CompiledClauses
    cc) -> do
        (cc, recordExpressionBecameCopatternLHS) <- ChangeT (TCMT IO) CompiledClauses
    -> TCMT IO (CompiledClauses, Bool)
    forall (m :: * -> *) a. Functor m => ChangeT m a -> m (a, Bool)
    runChangeT (ChangeT (TCMT IO) CompiledClauses
     -> TCMT IO (CompiledClauses, Bool))
    -> ChangeT (TCMT IO) CompiledClauses
    -> TCMT IO (CompiledClauses, Bool)
    forall a b. (a -> b) -> a -> b
    $ QName -> CompiledClauses -> ChangeT (TCMT IO) CompiledClauses
    forall (m :: * -> *).
    (HasConstInfo m, MonadChange m) =>
    QName -> CompiledClauses -> m CompiledClauses
    translateCompiledClauses QName
    q CompiledClauses
    cc
        modifySignature $ updateDefinition q
          $ updateTheDef (updateCompiledClauses $ const $ Just cc)
          . updateDefCopatternLHS (|| recordExpressionBecameCopatternLHS)
      where
      -- Walk through the definitions and return the set of inferred eta record types
      -- and the set of function definitions in the mutual block
      classify :: QName -> m (Maybe (Either QName (QName, CompiledClauses)))
    classify QName
    q = QName
    -> (Definition
        -> m (Maybe (Either QName (QName, CompiledClauses))))
    -> m (Maybe (Either QName (QName, CompiledClauses)))
    forall (m :: * -> *) a.
    (MonadTCEnv m, HasConstInfo m) =>
    QName -> (Definition -> m a) -> m a
    inConcreteOrAbstractMode QName
    q ((Definition -> m (Maybe (Either QName (QName, CompiledClauses))))
     -> m (Maybe (Either QName (QName, CompiledClauses))))
    -> (Definition
        -> m (Maybe (Either QName (QName, CompiledClauses))))
    -> m (Maybe (Either QName (QName, CompiledClauses)))
    forall a b. (a -> b) -> a -> b
    $ \ Definition
    def -> do
        case Definition -> Defn
    theDef Definition
    def of
          Record{ recEtaEquality' :: Defn -> EtaEquality
    recEtaEquality' = Inferred HasEta' PatternOrCopattern
    YesEta } -> Maybe (Either QName (QName, CompiledClauses))
    -> m (Maybe (Either QName (QName, CompiledClauses)))
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Maybe (Either QName (QName, CompiledClauses))
     -> m (Maybe (Either QName (QName, CompiledClauses))))
    -> Maybe (Either QName (QName, CompiledClauses))
    -> m (Maybe (Either QName (QName, CompiledClauses)))
    forall a b. (a -> b) -> a -> b
    $ Either QName (QName, CompiledClauses)
    -> Maybe (Either QName (QName, CompiledClauses))
    forall a. a -> Maybe a
    Just (Either QName (QName, CompiledClauses)
     -> Maybe (Either QName (QName, CompiledClauses)))
    -> Either QName (QName, CompiledClauses)
    -> Maybe (Either QName (QName, CompiledClauses))
    forall a b. (a -> b) -> a -> b
    $ QName -> Either QName (QName, CompiledClauses)
    forall a b. a -> Either a b
    Left QName
    q
          Function
            { funProjection :: Defn -> Either ProjectionLikenessMissing Projection
    funProjection = Left ProjectionLikenessMissing
    MaybeProjection
                -- Andreas, 2017-08-10, issue #2664:
                -- Do not record pattern translate record projection definitions!
            , funCompiled :: Defn -> Maybe CompiledClauses
    funCompiled   = Just CompiledClauses
    cc
            } -> Maybe (Either QName (QName, CompiledClauses))
    -> m (Maybe (Either QName (QName, CompiledClauses)))
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Maybe (Either QName (QName, CompiledClauses))
     -> m (Maybe (Either QName (QName, CompiledClauses))))
    -> Maybe (Either QName (QName, CompiledClauses))
    -> m (Maybe (Either QName (QName, CompiledClauses)))
    forall a b. (a -> b) -> a -> b
    $ Either QName (QName, CompiledClauses)
    -> Maybe (Either QName (QName, CompiledClauses))
    forall a. a -> Maybe a
    Just (Either QName (QName, CompiledClauses)
     -> Maybe (Either QName (QName, CompiledClauses)))
    -> Either QName (QName, CompiledClauses)
    -> Maybe (Either QName (QName, CompiledClauses))
    forall a b. (a -> b) -> a -> b
    $ (QName, CompiledClauses) -> Either QName (QName, CompiledClauses)
    forall a b. b -> Either a b
    Right (QName
    q, CompiledClauses
    cc)
          Defn
    _ -> Maybe (Either QName (QName, CompiledClauses))
    -> m (Maybe (Either QName (QName, CompiledClauses)))
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Maybe (Either QName (QName, CompiledClauses))
    forall a. Maybe a
    Nothing

    type FinalChecks = Maybe (TCM ())

    checkUnquoteDecl :: Info.MutualInfo -> [A.DefInfo] -> [QName] -> A.Expr -> TCM FinalChecks
    checkUnquoteDecl :: MutualInfo
    -> [DefInfo] -> [QName] -> Expr -> TCMT IO (Maybe (TCM ()))
    checkUnquoteDecl MutualInfo
    mi [DefInfo]
    is [QName]
    xs Expr
    e = do
      [Char] -> Int -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "tc.unquote.decl" Int
    20 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Doc
    "Checking unquoteDecl" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> [TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    sep ((QName -> TCMT IO Doc) -> [QName] -> [TCMT IO Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map QName -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => QName -> m Doc
    prettyTCM [QName]
    xs)
      Maybe (TCM ())
    forall a. Maybe a
    Nothing Maybe (TCM ()) -> TCMT IO [QName] -> TCMT IO (Maybe (TCM ()))
    forall a b. a -> TCMT IO b -> TCMT IO a
    forall (f :: * -> *) a b. Functor f => a -> f b -> f a
    <$ [QName] -> Expr -> TCMT IO [QName]
    unquoteTop [QName]
    xs Expr
    e

    checkUnquoteDef :: [A.DefInfo] -> [QName] -> A.Expr -> TCM ()
    checkUnquoteDef :: [DefInfo] -> [QName] -> Expr -> TCM ()
    checkUnquoteDef [DefInfo]
    _ [QName]
    xs Expr
    e = do
      [Char] -> Int -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "tc.unquote.decl" Int
    20 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Doc
    "Checking unquoteDef" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> [TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    sep ((QName -> TCMT IO Doc) -> [QName] -> [TCMT IO Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map QName -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => QName -> m Doc
    prettyTCM [QName]
    xs)
      () () -> TCMT IO [QName] -> TCM ()
    forall a b. a -> TCMT IO b -> TCMT IO a
    forall (f :: * -> *) a b. Functor f => a -> f b -> f a
    <$ [QName] -> Expr -> TCMT IO [QName]
    unquoteTop [QName]
    xs Expr
    e

    -- | Run a reflected TCM computatation expected to define a given list of
    --   names.
    unquoteTop :: [QName] -> A.Expr -> TCM [QName]
    unquoteTop :: [QName] -> Expr -> TCMT IO [QName]
    unquoteTop [QName]
    xs Expr
    e = do
      tcm   <- TCMT IO Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primAgdaTCM
      unit  <- primUnit
      lzero <- primLevelZero
      let vArg = a -> Arg a
    forall a. a -> Arg a
    defaultArg
          hArg = Hiding -> Arg a -> Arg a
    forall a. LensHiding a => Hiding -> a -> a
    setHiding Hiding
    Hidden (Arg a -> Arg a) -> (a -> Arg a) -> a -> Arg a
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . a -> Arg a
    forall a. a -> Arg a
    vArg
      m    <- applyQuantityToJudgement zeroQuantity $
                checkExpr e $ El (mkType 0) $ apply tcm [hArg lzero, vArg unit]
      res  <- runUnquoteM $ tell xs >> evalTCM m
      case res of
        Left UnquoteError
    err      -> TypeError -> TCMT IO [QName]
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    TypeError -> m a
    typeError (TypeError -> TCMT IO [QName]) -> TypeError -> TCMT IO [QName]
    forall a b. (a -> b) -> a -> b
    $ UnquoteError -> TypeError
    UnquoteFailed UnquoteError
    err
        Right (Term
    _, [QName]
    xs) -> [QName] -> TCMT IO [QName]
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return [QName]
    xs

    -- | Instantiate all metas in 'Definition' associated to 'QName'.
    --   Makes sense after freezing metas. Some checks, like free variable
    --   analysis, are not in 'TCM', so they will be more precise (see issue 1099)
    --   after meta instantiation.
    --   Precondition: name has been added to signature already.
    instantiateDefinitionType :: QName -> TCM ()
    instantiateDefinitionType :: QName -> TCM ()
    instantiateDefinitionType QName
    q = do
      [Char] -> Int -> [Char] -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> [Char] -> m ()
    reportSLn [Char]
    "tc.decl.inst" Int
    20 ([Char] -> TCM ()) -> [Char] -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ [Char]
    "instantiating type of " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ QName -> [Char]
    forall a. Pretty a => a -> [Char]
    prettyShow QName
    q
      t  <- Definition -> Type
    defType (Definition -> Type)
    -> (Signature -> Definition) -> Signature -> Type
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Definition -> Maybe Definition -> Definition
    forall a. a -> Maybe a -> a
    fromMaybe Definition
    forall a. HasCallStack => a
    __IMPOSSIBLE__ (Maybe Definition -> Definition)
    -> (Signature -> Maybe Definition) -> Signature -> Definition
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . QName -> Signature -> Maybe Definition
    lookupDefinition QName
    q (Signature -> Type) -> TCMT IO Signature -> TCMT IO Type
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> TCMT IO Signature
    forall (m :: * -> *). ReadTCState m => m Signature
    getSignature
      t' <- instantiateFull t
      modifySignature $ updateDefinition q $ updateDefType $ const t'
      reportSDoc "tc.decl.inst" 30 $ vcat
        [ "  t  = " <+> prettyTCM t
        , "  t' = " <+> prettyTCM t'
        ]

    -- Andreas, 2014-04-11
    -- UNUSED, costs a couple of sec on the std-lib
    -- -- | Instantiate all metas in 'Definition' associated to 'QName'.
    -- --   Makes sense after freezing metas.
    -- --   Some checks, like free variable analysis, are not in 'TCM',
    -- --   so they will be more precise (see issue 1099) after meta instantiation.
    -- --
    -- --   Precondition: name has been added to signature already.
    -- instantiateDefinition :: QName -> TCM ()
    -- instantiateDefinition q = do
    --   reportSLn "tc.decl.inst" 20 $ "instantiating " ++ prettyShow q
    --   sig <- getSignature
    --   let def = fromMaybe __IMPOSSIBLE__ $ lookupDefinition q sig
    --   def <- instantiateFull def
    --   modifySignature $ updateDefinition q $ const def

    data HighlightModuleContents = DontHightlightModuleContents | DoHighlightModuleContents
      deriving (HighlightModuleContents -> HighlightModuleContents -> Bool
    (HighlightModuleContents -> HighlightModuleContents -> Bool)
    -> (HighlightModuleContents -> HighlightModuleContents -> Bool)
    -> Eq HighlightModuleContents
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    $c== :: HighlightModuleContents -> HighlightModuleContents -> Bool
    == :: HighlightModuleContents -> HighlightModuleContents -> Bool
    $c/= :: HighlightModuleContents -> HighlightModuleContents -> Bool
    /= :: HighlightModuleContents -> HighlightModuleContents -> Bool
    Eq)

    -- | Highlight a declaration. Called after checking a mutual block (to ensure
    --   we have the right definitions for all names). For modules inside mutual
    --   blocks we haven't highlighted their contents, but for modules not in a
    --   mutual block we have. Hence the flag.
    highlight_ :: HighlightModuleContents -> A.Declaration -> TCM ()
    highlight_ :: HighlightModuleContents -> Declaration -> TCM ()
    highlight_ HighlightModuleContents
    hlmod Declaration
    d = do
      [Char] -> Int -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "tc.decl" Int
    45 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    forall a b. (a -> b) -> a -> b
    $
        [Char] -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => [Char] -> m Doc
    text [Char]
    "Highlighting a declaration with the following spine:"
          TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    $$
        [Char] -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => [Char] -> m Doc
    text (DeclarationSpine -> [Char]
    forall a. Show a => a -> [Char]
    show (DeclarationSpine -> [Char]) -> DeclarationSpine -> [Char]
    forall a b. (a -> b) -> a -> b
    $ Declaration -> DeclarationSpine
    A.declarationSpine Declaration
    d)
      let highlight :: Declaration -> TCM ()
    highlight Declaration
    d = Declaration -> Level -> Bool -> TCM ()
    generateAndPrintSyntaxInfo Declaration
    d Level
    Full Bool
    True
      Account (BenchPhase (TCMT IO)) -> TCM () -> TCM ()
    forall (m :: * -> *) c.
    MonadBench m =>
    Account (BenchPhase m) -> m c -> m c
    Bench.billTo [BenchPhase (TCMT IO)
    Phase
    Bench.Highlighting] (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ case Declaration
    d of
        A.Axiom{}                -> Declaration -> TCM ()
    highlight Declaration
    d
        A.Field{}                -> TCM ()
    forall a. HasCallStack => a
    __IMPOSSIBLE__
        A.Primitive{}            -> Declaration -> TCM ()
    highlight Declaration
    d
        A.Mutual MutualInfo
    i [Declaration]
    ds            -> (Declaration -> TCM ()) -> [Declaration] -> TCM ()
    forall (t :: * -> *) (m :: * -> *) a b.
    (Foldable t, Monad m) =>
    (a -> m b) -> t a -> m ()
    mapM_ (HighlightModuleContents -> Declaration -> TCM ()
    highlight_ HighlightModuleContents
    DoHighlightModuleContents) ([Declaration] -> TCM ()) -> [Declaration] -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ [Declaration] -> [Declaration]
    deepUnscopeDecls [Declaration]
    ds
        A.Apply{}                -> Declaration -> TCM ()
    highlight Declaration
    d
        A.Import{}               -> Declaration -> TCM ()
    highlight Declaration
    d
        A.Pragma{}               -> Declaration -> TCM ()
    highlight Declaration
    d
        A.ScopedDecl{}           -> () -> TCM ()
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
        A.FunDef{}               -> Declaration -> TCM ()
    highlight Declaration
    d
        A.DataDef{}              -> Declaration -> TCM ()
    highlight Declaration
    d
        A.DataSig{}              -> Declaration -> TCM ()
    highlight Declaration
    d
        A.Open{}                 -> Declaration -> TCM ()
    highlight Declaration
    d
        A.PatternSynDef{}        -> Declaration -> TCM ()
    highlight Declaration
    d
        A.UnfoldingDecl{}        -> Declaration -> TCM ()
    highlight Declaration
    d
        A.Generalize{}           -> Declaration -> TCM ()
    highlight Declaration
    d
        A.UnquoteDecl{}          -> Declaration -> TCM ()
    highlight Declaration
    d
        A.UnquoteDef{}           -> Declaration -> TCM ()
    highlight Declaration
    d
        A.UnquoteData{}          -> Declaration -> TCM ()
    highlight Declaration
    d
        A.Section Range
    i Erased
    er ModuleName
    x GeneralizeTelescope
    tel [Declaration]
    ds  -> do
          Declaration -> TCM ()
    highlight (Range
    -> Erased
    -> ModuleName
    -> GeneralizeTelescope
    -> [Declaration]
    -> Declaration
    A.Section Range
    i Erased
    er ModuleName
    x GeneralizeTelescope
    tel [])
          Bool -> TCM () -> TCM ()
    forall b (m :: * -> *). (IsBool b, Monad m) => b -> m () -> m ()
    when (HighlightModuleContents
    hlmod HighlightModuleContents -> HighlightModuleContents -> Bool
    forall a. Eq a => a -> a -> Bool
    == HighlightModuleContents
    DoHighlightModuleContents) (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ (Declaration -> TCM ()) -> [Declaration] -> TCM ()
    forall (t :: * -> *) (m :: * -> *) a b.
    (Foldable t, Monad m) =>
    (a -> m b) -> t a -> m ()
    mapM_ (HighlightModuleContents -> Declaration -> TCM ()
    highlight_ HighlightModuleContents
    hlmod) ([Declaration] -> [Declaration]
    deepUnscopeDecls [Declaration]
    ds)
        A.RecSig{}               -> Declaration -> TCM ()
    highlight Declaration
    d
        A.RecDef DefInfo
    i QName
    x UniverseCheck
    uc RecordDirectives
    dir DataDefParams
    ps Expr
    tel [Declaration]
    cs ->
          Declaration -> TCM ()
    highlight (DefInfo
    -> QName
    -> UniverseCheck
    -> RecordDirectives
    -> DataDefParams
    -> Expr
    -> [Declaration]
    -> Declaration
    A.RecDef DefInfo
    i QName
    x UniverseCheck
    uc RecordDirectives
    dir DataDefParams
    ps Expr
    dummy [Declaration]
    cs)
          -- The telescope has already been highlighted.
          where
          -- Andreas, 2016-01-22, issue 1790
          -- The expression denoting the record constructor type
          -- is replace by a dummy expression in order to /not/
          -- generate highlighting from it.
          -- Simply because all the highlighting info is wrong
          -- in the record constructor type:
          -- i) fields become bound variables,
          -- ii) declarations become let-bound variables.
          -- We do not need that crap.
          dummy :: Expr
    dummy = ExprInfo -> Literal -> Expr
    A.Lit ExprInfo
    forall a. Null a => a
    empty (Literal -> Expr) -> Literal -> Expr
    forall a b. (a -> b) -> a -> b
    $ Text -> Literal
    LitString (Text -> Literal) -> Text -> Literal
    forall a b. (a -> b) -> a -> b
    $
            Text
    "do not highlight construct(ed/or) type"

    -- | Termination check a declaration.
    checkTermination_ :: A.Declaration -> TCM ()
    checkTermination_ :: Declaration -> TCM ()
    checkTermination_ Declaration
    d = Account (BenchPhase (TCMT IO)) -> TCM () -> TCM ()
    forall (m :: * -> *) c.
    MonadBench m =>
    Account (BenchPhase m) -> m c -> m c
    Bench.billTo [BenchPhase (TCMT IO)
    Phase
    Bench.Termination] (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ do
      [Char] -> Int -> [Char] -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> [Char] -> m ()
    reportSLn [Char]
    "tc.decl" Int
    20 ([Char] -> TCM ()) -> [Char] -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ [Char]
    "checkDecl: checking termination..."
      -- If there are some termination errors, we throw a warning.
      -- The termination checker already marked non-terminating functions as such.
      TCMT IO [TerminationError]
    -> (List1 TerminationError -> TCM ()) -> TCM ()
    forall (m :: * -> *) a.
    Monad m =>
    m [a] -> (List1 a -> m ()) -> m ()
    List1.unlessNullM (Declaration -> TCMT IO [TerminationError]
    termDecl Declaration
    d) \ List1 TerminationError
    termErrs -> do
        Warning -> TCM ()
    forall (m :: * -> *).
    (HasCallStack, MonadWarning m) =>
    Warning -> m ()
    warning (Warning -> TCM ()) -> Warning -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ List1 TerminationError -> Warning
    TerminationIssue List1 TerminationError
    termErrs

    -- | Check a set of mutual names for positivity.
    checkPositivity_ :: Info.MutualInfo -> Set QName -> TCM ()
    checkPositivity_ :: MutualInfo -> Set QName -> TCM ()
    checkPositivity_ MutualInfo
    mi Set QName
    names = Account (BenchPhase (TCMT IO)) -> TCM () -> TCM ()
    forall (m :: * -> *) c.
    MonadBench m =>
    Account (BenchPhase m) -> m c -> m c
    Bench.billTo [BenchPhase (TCMT IO)
    Phase
    Bench.Positivity] (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ do
      -- Positivity checking.
      [Char] -> Int -> [Char] -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> [Char] -> m ()
    reportSLn [Char]
    "tc.decl" Int
    20 ([Char] -> TCM ()) -> [Char] -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ [Char]
    "checkDecl: checking positivity..."
      MutualInfo -> Set QName -> TCM ()
    checkStrictlyPositive MutualInfo
    mi Set QName
    names

      -- Andreas, 2012-02-13: Polarity computation uses information from the
      -- positivity check, so it needs happen after the positivity check.
      [QName] -> TCM ()
    forall (m :: * -> *).
    (HasOptions m, HasConstInfo m, HasBuiltins m, MonadTCEnv m,
     MonadTCState m, MonadReduce m, MonadAddContext m, MonadTCError m,
     MonadDebug m, MonadPretty m) =>
    [QName] -> m ()
    computePolarity ([QName] -> TCM ()) -> [QName] -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ Set QName -> [QName]
    forall a. Set a -> [a]
    Set.toList Set QName
    names

    -- | Check a set of mutual names for constructor-headedness.
    checkInjectivity_ :: Set QName -> TCM ()
    checkInjectivity_ :: Set QName -> TCM ()
    checkInjectivity_ Set QName
    names = Account (BenchPhase (TCMT IO)) -> TCM () -> TCM ()
    forall (m :: * -> *) c.
    MonadBench m =>
    Account (BenchPhase m) -> m c -> m c
    Bench.billTo [BenchPhase (TCMT IO)
    Phase
    Bench.Injectivity] (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ do
      [Char] -> Int -> [Char] -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> [Char] -> m ()
    reportSLn [Char]
    "tc.decl" Int
    20 ([Char] -> TCM ()) -> [Char] -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ [Char]
    "checkDecl: checking injectivity..."
      -- Andreas, 2015-07-01, see Issue1366b:
      -- Injectivity check needs also to be run for abstract definitions.
      -- Fold.forM_ names $ \ q -> ignoreAbstractMode $ do -- NOT NECESSARY after all
      Set QName -> (QName -> TCM ()) -> TCM ()
    forall (t :: * -> *) (m :: * -> *) a b.
    (Foldable t, Monad m) =>
    t a -> (a -> m b) -> m ()
    Fold.forM_ Set QName
    names ((QName -> TCM ()) -> TCM ()) -> (QName -> TCM ()) -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ \ QName
    q -> QName -> (Definition -> TCM ()) -> TCM ()
    forall (m :: * -> *) a.
    (MonadTCEnv m, HasConstInfo m) =>
    QName -> (Definition -> m a) -> m a
    inConcreteOrAbstractMode QName
    q ((Definition -> TCM ()) -> TCM ())
    -> (Definition -> TCM ()) -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ \ Definition
    def -> do
        -- For abstract q, we should be inAbstractMode,
        -- otherwise getConstInfo returns Axiom.
        --
        -- Andreas, 2015-07-01:
        -- Quite surprisingly, inAbstractMode does not allow us to look
        -- at a local definition (@where@ block) of an abstract definition.
        -- This is because the local definition is defined in a strict submodule.
        -- We can only see through abstract definitions in the current module
        -- or super modules inAbstractMode.
        -- I changed that in Monad.Signature.treatAbstractly', so we can see
        -- our own local definitions.
        case Definition -> Defn
    theDef Definition
    def of
          d :: Defn
    d@Function{ funClauses :: Defn -> [Clause]
    funClauses = [Clause]
    cs, funTerminates :: Defn -> Maybe Bool
    funTerminates = Maybe Bool
    term, funProjection :: Defn -> Either ProjectionLikenessMissing Projection
    funProjection = Either ProjectionLikenessMissing Projection
    mproj }
            | Maybe Bool
    term Maybe Bool -> Maybe Bool -> Bool
    forall a. Eq a => a -> a -> Bool
    /= Bool -> Maybe Bool
    forall a. a -> Maybe a
    Just Bool
    True -> do
                -- Not terminating, thus, running the injectivity check could get us into a loop.
                [Char] -> Int -> [Char] -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> [Char] -> m ()
    reportSLn [Char]
    "tc.inj.check" Int
    35 ([Char] -> TCM ()) -> [Char] -> TCM ()
    forall a b. (a -> b) -> a -> b
    $
                  QName -> [Char]
    forall a. Pretty a => a -> [Char]
    prettyShow QName
    q [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    " is not verified as terminating, thus, not considered for injectivity"
            | Defn -> Bool
    isProperProjection Defn
    d -> do
                [Char] -> Int -> [Char] -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> [Char] -> m ()
    reportSLn [Char]
    "tc.inj.check" Int
    40 ([Char] -> TCM ()) -> [Char] -> TCM ()
    forall a b. (a -> b) -> a -> b
    $
                  QName -> [Char]
    forall a. Pretty a => a -> [Char]
    prettyShow QName
    q [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    " is a projection, thus, not considered for injectivity"
            | Bool
    otherwise -> do

                inv <- QName -> [Clause] -> TCM FunctionInverse
    checkInjectivity QName
    q [Clause]
    cs
                modifySignature $ updateDefinition q $ updateTheDef $ const $
                  d { funInv = inv }

          Defn
    _ -> do
            abstr <- (TCEnv -> AbstractMode) -> TCMT IO AbstractMode
    forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
    asksTC TCEnv -> AbstractMode
    envAbstractMode
            reportSLn "tc.inj.check" 40 $
              "we are in " ++ show abstr ++ " and " ++
                 prettyShow q ++ " is abstract or not a function, thus, not considered for injectivity"

    -- | Check a set of mutual names for projection likeness.
    --
    --   Only a single, non-abstract function can be projection-like.
    --   Making an abstract function projection-like would break the
    --   invariant that the type of the principle argument of a projection-like
    --   function is always inferable.

    checkProjectionLikeness_ :: Set QName -> TCM ()
    checkProjectionLikeness_ :: Set QName -> TCM ()
    checkProjectionLikeness_ Set QName
    names = Account (BenchPhase (TCMT IO)) -> TCM () -> TCM ()
    forall (m :: * -> *) c.
    MonadBench m =>
    Account (BenchPhase m) -> m c -> m c
    Bench.billTo [BenchPhase (TCMT IO)
    Phase
    Bench.ProjectionLikeness] (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ do
          -- Non-mutual definitions can be considered for
          -- projection likeness
          let ds :: [QName]
    ds = Set QName -> [QName]
    forall a. Set a -> [a]
    Set.toList Set QName
    names
          [Char] -> Int -> [Char] -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> [Char] -> m ()
    reportSLn [Char]
    "tc.proj.like" Int
    20 ([Char] -> TCM ()) -> [Char] -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ [Char]
    "checkDecl: checking projection-likeness of " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ [QName] -> [Char]
    forall a. Pretty a => a -> [Char]
    prettyShow [QName]
    ds
          case [QName]
    ds of
            [QName
    d] -> do
              def <- QName -> TCMT IO Definition
    forall (m :: * -> *). HasConstInfo m => QName -> m Definition
    getConstInfo QName
    d
              -- For abstract identifiers, getConstInfo returns Axiom.
              -- Thus, abstract definitions are not considered for projection-likeness.
              case theDef def of
                Function{} -> QName -> TCM ()
    makeProjection (Definition -> QName
    defName Definition
    def)
                Defn
    _          -> [Char] -> Int -> [Char] -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> [Char] -> m ()
    reportSLn [Char]
    "tc.proj.like" Int
    25 ([Char] -> TCM ()) -> [Char] -> TCM ()
    forall a b. (a -> b) -> a -> b
    $
                  QName -> [Char]
    forall a. Pretty a => a -> [Char]
    prettyShow QName
    d [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    " is abstract or not a function, thus, not considered for projection-likeness"
            [QName]
    _ -> [Char] -> Int -> [Char] -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> [Char] -> m ()
    reportSLn [Char]
    "tc.proj.like" Int
    25 ([Char] -> TCM ()) -> [Char] -> TCM ()
    forall a b. (a -> b) -> a -> b
    $
                   [Char]
    "mutual definitions are not considered for projection-likeness"

    -- | Freeze metas created by given computation if in abstract mode.
    whenAbstractFreezeMetasAfter :: A.DefInfo -> TCM a -> TCM a
    whenAbstractFreezeMetasAfter :: forall a. DefInfo -> TCM a -> TCM a
    whenAbstractFreezeMetasAfter Info.DefInfo{Access
    defAccess :: Access
    defAccess :: forall t. DefInfo' t -> Access
    defAccess, IsAbstract
    defAbstract :: IsAbstract
    defAbstract :: forall t. DefInfo' t -> IsAbstract
    defAbstract, IsOpaque
    defOpaque :: IsOpaque
    defOpaque :: forall t. DefInfo' t -> IsOpaque
    defOpaque} TCM a
    m = do
      if (IsAbstract
    defAbstract IsAbstract -> IsAbstract -> Bool
    forall a. Eq a => a -> a -> Bool
    == IsAbstract
    ConcreteDef Bool -> Bool -> Bool
    && IsOpaque
    defOpaque IsOpaque -> IsOpaque -> Bool
    forall a. Eq a => a -> a -> Bool
    == IsOpaque
    TransparentDef) then TCM a
    m else do
        (a, ms) <- TCM a -> TCMT IO (a, LocalMetaStores)
    forall (m :: * -> *) a.
    ReadTCState m =>
    m a -> m (a, LocalMetaStores)
    metasCreatedBy TCM a
    m

        reportSLn "tc.decl" 20 $ "Attempting to solve constraints before freezing."
        locallyTCState stInstanceHack (const True) $
          wakeupConstraints_   -- solve emptiness and instance constraints
        xs <- freezeMetas (openMetas ms)

        reportSDoc "tc.decl.ax" 20 $ vcat
          [ "Abstract type signature produced new open metas: " <+>
            sep (map prettyTCM $ MapS.keys (openMetas ms))
          , "We froze the following ones of these:            " <+>
            sep (map prettyTCM $ Set.toList xs)
          ]
        return a

    checkGeneralize :: Set QName -> A.DefInfo -> ArgInfo -> QName -> A.Expr -> TCM ()
    checkGeneralize :: Set QName -> DefInfo -> ArgInfo -> QName -> Expr -> TCM ()
    checkGeneralize Set QName
    s DefInfo
    i ArgInfo
    info QName
    x Expr
    e = do

        [Char] -> Int -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "tc.decl.gen" Int
    20 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ [TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    sep
          [ TCMT IO Doc
    "checking type signature of generalizable variable" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> QName -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => QName -> m Doc
    prettyTCM QName
    x TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> TCMT IO Doc
    ":"
          , Int -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
    nest Int
    2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ Expr -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => Expr -> m Doc
    prettyTCM Expr
    e
          ]

        -- Check the signature and collect the created metas.
        (telNames, tGen) <-
          Set QName -> TCMT IO Type -> TCM ([Maybe QName], Type)
    generalizeType Set QName
    s (TCMT IO Type -> TCM ([Maybe QName], Type))
    -> TCMT IO Type -> TCM ([Maybe QName], Type)
    forall a b. (a -> b) -> a -> b
    $ Lens' TCEnv DoGeneralize
    -> (DoGeneralize -> DoGeneralize) -> TCMT IO Type -> TCMT IO Type
    forall (m :: * -> *) a b.
    MonadTCEnv m =>
    Lens' TCEnv a -> (a -> a) -> m b -> m b
    locallyTC (DoGeneralize -> f DoGeneralize) -> TCEnv -> f TCEnv
    Lens' TCEnv DoGeneralize
    eGeneralizeMetas (DoGeneralize -> DoGeneralize -> DoGeneralize
    forall a b. a -> b -> a
    const DoGeneralize
    YesGeneralizeMeta) (TCMT IO Type -> TCMT IO Type) -> TCMT IO Type -> TCMT IO Type
    forall a b. (a -> b) -> a -> b
    $
            TCMT IO Type -> TCMT IO Type
    forall (m :: * -> *) a.
    (MonadTCEnv m, HasOptions m, MonadDebug m) =>
    m a -> m a
    workOnTypes (TCMT IO Type -> TCMT IO Type) -> TCMT IO Type -> TCMT IO Type
    forall a b. (a -> b) -> a -> b
    $ Expr -> TCMT IO Type
    isType_ Expr
    e
        let n = [Maybe QName] -> Int
    forall a. [a] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length [Maybe QName]
    telNames

        reportSDoc "tc.decl.gen" 10 $ sep
          [ "checked type signature of generalizable variable" <+> prettyTCM x <+> ":"
          , nest 2 $ prettyTCM tGen
          ]

        lang <- getLanguage
        addConstant x $ defaultDefn info x tGen lang $
          GeneralizableVar $ SomeGeneralizableArgs n

    -- | Type check an axiom.
    checkAxiom :: KindOfName -> A.DefInfo -> ArgInfo ->
                  Maybe PragmaPolarities -> QName -> A.Expr -> TCM ()
    checkAxiom :: KindOfName
    -> DefInfo
    -> ArgInfo
    -> Maybe PragmaPolarities
    -> QName
    -> Expr
    -> TCM ()
    checkAxiom = Maybe GeneralizeTelescope
    -> KindOfName
    -> DefInfo
    -> ArgInfo
    -> Maybe PragmaPolarities
    -> QName
    -> Expr
    -> TCM ()
    checkAxiom' Maybe GeneralizeTelescope
    forall a. Maybe a
    Nothing

    -- | Data and record type signatures need to remember the generalized
    --   parameters for when checking the corresponding definition, so for these we
    --   pass in the parameter telescope separately.
    checkAxiom' :: Maybe A.GeneralizeTelescope -> KindOfName -> A.DefInfo -> ArgInfo ->
                   Maybe PragmaPolarities -> QName -> A.Expr -> TCM ()
    checkAxiom' :: Maybe GeneralizeTelescope
    -> KindOfName
    -> DefInfo
    -> ArgInfo
    -> Maybe PragmaPolarities
    -> QName
    -> Expr
    -> TCM ()
    checkAxiom' Maybe GeneralizeTelescope
    gentel KindOfName
    kind DefInfo
    i ArgInfo
    info0 Maybe PragmaPolarities
    mp QName
    x Expr
    e = DefInfo -> TCM () -> TCM ()
    forall a. DefInfo -> TCM a -> TCM a
    whenAbstractFreezeMetasAfter DefInfo
    i (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ TCM () -> TCM ()
    forall (m :: * -> *) a.
    (PureTCM m, MonadMetaSolver m) =>
    m a -> m a
    defaultOpenLevelsToZero (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ do
      -- Andreas, 2016-07-19 issues #418 #2102:
      -- We freeze metas in type signatures of abstract definitions, to prevent
      -- leakage of implementation details.

      -- If the axiom is erased, then hard compile-time mode is entered.
      ArgInfo -> TCM () -> TCM ()
    forall q a. LensQuantity q => q -> TCM a -> TCM a
    setHardCompileTimeModeIfErased' ArgInfo
    info0 (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ do

      -- Andreas, 2012-04-18  if we are in irrelevant context, axioms are irrelevant
      -- even if not declared as such (Issue 610).
      rel <- Relevance -> Relevance -> Relevance
    forall a. Ord a => a -> a -> a
    max (ArgInfo -> Relevance
    forall a. LensRelevance a => a -> Relevance
    getRelevance ArgInfo
    info0) (Relevance -> Relevance) -> TCMT IO Relevance -> TCMT IO Relevance
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Lens' TCEnv Relevance -> TCMT IO Relevance
    forall (m :: * -> *) a. MonadTCEnv m => Lens' TCEnv a -> m a
    viewTC (Relevance -> f Relevance) -> TCEnv -> f TCEnv
    Lens' TCEnv Relevance
    eRelevance

      -- Andrea, 2019-07-16 Cohesion is purely based on left-division, it
      -- does not take envModality into account.
      let c = ArgInfo -> Cohesion
    forall a. LensCohesion a => a -> Cohesion
    getCohesion ArgInfo
    info0
      let p = ArgInfo -> PolarityModality
    forall a. LensModalPolarity a => a -> PolarityModality
    getModalPolarity ArgInfo
    info0
      let mod  = Relevance -> Quantity -> Cohesion -> PolarityModality -> Modality
    Modality Relevance
    rel (ArgInfo -> Quantity
    forall a. LensQuantity a => a -> Quantity
    getQuantity ArgInfo
    info0) Cohesion
    c PolarityModality
    p
      let info = Modality -> ArgInfo -> ArgInfo
    forall a. LensModality a => Modality -> a -> a
    setModality Modality
    mod ArgInfo
    info0

      -- For now, top-level polarity annotations are forbidden
      when (p /= defaultPolarity) $ warning $ TopLevelPolarity x p

      polarityEnabled <- optPolarity <$> pragmaOptions

      applyWhen polarityEnabled (applyPolarityToContext p) $ applyCohesionToContext c $ do

      reportSDoc "tc.decl.ax" 20 $ sep
        [ text $ "checking type signature"
        , nest 2 $ (prettyTCM mod <> prettyTCM x) <+> ":" <+> prettyTCM e
        , nest 2 $ caseMaybe gentel "(no gentel)" $ \ GeneralizeTelescope
    _ -> TCMT IO Doc
    "(has gentel)"
        ]

      (genParams, npars, t) <- workOnTypes $ case gentel of
            Maybe GeneralizeTelescope
    Nothing     -> ([], Int
    0,) (Type -> ([Maybe Name], Int, Type))
    -> TCMT IO Type -> TCMT IO ([Maybe Name], Int, Type)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Expr -> TCMT IO Type
    isType_ Expr
    e
            Just GeneralizeTelescope
    gentel ->
              Maybe ModuleName
    -> GeneralizeTelescope
    -> ([Maybe Name]
        -> Tele (Dom Type) -> TCMT IO ([Maybe Name], Int, Type))
    -> TCMT IO ([Maybe Name], Int, Type)
    forall a.
    Maybe ModuleName
    -> GeneralizeTelescope
    -> ([Maybe Name] -> Tele (Dom Type) -> TCM a)
    -> TCM a
    checkGeneralizeTelescope Maybe ModuleName
    forall a. Maybe a
    Nothing GeneralizeTelescope
    gentel (([Maybe Name]
      -> Tele (Dom Type) -> TCMT IO ([Maybe Name], Int, Type))
     -> TCMT IO ([Maybe Name], Int, Type))
    -> ([Maybe Name]
        -> Tele (Dom Type) -> TCMT IO ([Maybe Name], Int, Type))
    -> TCMT IO ([Maybe Name], Int, Type)
    forall a b. (a -> b) -> a -> b
    $ \ [Maybe Name]
    genParams Tele (Dom Type)
    ptel -> do
                t <- TCMT IO Type -> TCMT IO Type
    forall (m :: * -> *) a.
    (MonadTCEnv m, HasOptions m, MonadDebug m) =>
    m a -> m a
    workOnTypes (TCMT IO Type -> TCMT IO Type) -> TCMT IO Type -> TCMT IO Type
    forall a b. (a -> b) -> a -> b
    $ Expr -> TCMT IO Type
    isType_ Expr
    e
                return (genParams, size ptel, abstract ptel t)

      reportSDoc "tc.decl.ax" 10 $ sep
        [ text $ "checked type signature"
        , nest 2 $ (prettyTCM mod <> prettyTCM x) <+> ":" <+> prettyTCM t
        , nest 2 $ "of sort " <+> prettyTCM (getSort t)
        ]

      unless (null genParams) $
        reportSLn "tc.decl.ax" 40 $ "  generalized params: " ++ show genParams

      -- Jesper, 2018-06-05: should be done AFTER generalizing
      --whenM (optDoubleCheck <$> pragmaOptions) $ workOnTypes $ do
      --  checkInternal (unEl t) (sort $ getSort t)

      -- Andreas, 2015-03-17 Issue 1428: Do not postulate sizes in parametrized
      -- modules!
      when (kind == AxiomName) $ do
        whenM ((== SizeUniv) <$> do reduce $ getSort t) $ do
          whenM ((> 0) <$> getContextSize) $ typeError PostulatedSizeInModule

      -- get explicitely specified occurences (by looking at polarity annotations, if enabled)
      eoccs <-
        if polarityEnabled
          then do
            args <- telToList . theTel <$> telView t
            return $ fmap (modalPolarityToOccurrence . modPolarityAnn . getModalPolarity) args
          else return []

      -- Lucas, 2022-11-30: If this is a datatype, forbid polarity annotations for indices
      when (kind == DataName && any (/= Mixed) (drop npars eoccs)) $
        typeError DatatypeIndexPolarity

      occs <- case mp of
        Maybe PragmaPolarities
    Nothing -> [Occurrence] -> TCMT IO [Occurrence]
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return [Occurrence]
    eoccs
        Just PragmaPolarities
    occs1 -> do
          -- If any polarity retrieved from the type is not Mixed, it means an explicit
          -- annotation was given, so we throw an error because the pragma shouldn't be used
          Bool -> TCM () -> TCM ()
    forall b (m :: * -> *). (IsBool b, Monad m) => b -> m () -> m ()
    when ((Occurrence -> Bool) -> [Occurrence] -> Bool
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
    any (Occurrence -> Occurrence -> Bool
    forall a. Eq a => a -> a -> Bool
    /= Occurrence
    Mixed) [Occurrence]
    eoccs) (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ TypeError -> TCM ()
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    TypeError -> m a
    typeError (QName -> TypeError
    ExplicitPolarityVsPragma QName
    x)

          -- Ensure that polarity pragmas do not contain too many occurrences.
          let occs :: [Item PragmaPolarities]
    occs = PragmaPolarities -> [Item PragmaPolarities]
    forall l. IsList l => l -> [Item l]
    List1.toList PragmaPolarities
    occs1
          let m :: Int
    m = [Ranged Occurrence] -> Int
    forall a. [a] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length [Item PragmaPolarities]
    [Ranged Occurrence]
    occs
          TelV tel _core <- Int -> Type -> TCMT IO (TelV Type)
    forall (m :: * -> *).
    (MonadReduce m, MonadAddContext m) =>
    Int -> Type -> m (TelV Type)
    telViewUpTo Int
    m Type
    t
          let n = Tele (Dom Type) -> Int
    forall a. Sized a => a -> Int
    size Tele (Dom Type)
    tel
          when (n < m) do
            -- Andreas, 2025-05-03, #7851
            -- ifBlocked _core  then the warning might be spurious.
            -- However, postponing this check seems like an overkill.
            warning $ TooManyPolarities x $
              List1.fromListSafe __IMPOSSIBLE__ $ drop n occs

          return $ map rangedThing occs

      -- Set blocking tag to MissingClauses if we still expect clauses
      let blk = case KindOfName
    kind of
            KindOfName
    FunName   -> NotBlocked' Term -> () -> Blocked' Term ()
    forall t a. NotBlocked' t -> a -> Blocked' t a
    NotBlocked (QName -> NotBlocked' Term
    forall t. QName -> NotBlocked' t
    MissingClauses QName
    x) ()
            KindOfName
    MacroName -> NotBlocked' Term -> () -> Blocked' Term ()
    forall t a. NotBlocked' t -> a -> Blocked' t a
    NotBlocked (QName -> NotBlocked' Term
    forall t. QName -> NotBlocked' t
    MissingClauses QName
    x) ()
            KindOfName
    _         -> NotBlocked' Term -> () -> Blocked' Term ()
    forall t a. NotBlocked' t -> a -> Blocked' t a
    NotBlocked NotBlocked' Term
    forall t. NotBlocked' t
    ReallyNotBlocked ()

      -- Not safe. See Issue 330
      -- t <- addForcingAnnotations t

      lang <- getLanguage
      funD <- emptyFunctionData

      let defn = ArgInfo -> QName -> Type -> Language -> Defn -> Definition
    defaultDefn ArgInfo
    info QName
    x Type
    t Language
    lang (Defn -> Definition) -> Defn -> Definition
    forall a b. (a -> b) -> a -> b
    $
            case KindOfName
    kind of   -- #4833: set abstract already here so it can be inherited by with functions
              KindOfName
    FunName   -> Defn
    fun
              KindOfName
    MacroName -> Lens' Defn Bool -> LensSet Defn Bool
    forall o i. Lens' o i -> LensSet o i
    set (Bool -> f Bool) -> Defn -> f Defn
    Lens' Defn Bool
    funMacro Bool
    True Defn
    fun
              KindOfName
    DataName  -> Int -> Defn
    DataOrRecSig Int
    npars
              KindOfName
    RecName   -> Int -> Defn
    DataOrRecSig Int
    npars
              KindOfName
    AxiomName -> Defn
    defaultAxiom     -- Old comment: NB: used also for data and record type sigs
              KindOfName
    _         -> Defn
    forall a. HasCallStack => a
    __IMPOSSIBLE__
            where
              fun :: Defn
    fun = FunctionData -> Defn
    FunctionDefn (FunctionData -> Defn) -> FunctionData -> Defn
    forall a b. (a -> b) -> a -> b
    $ Lens' FunctionData IsAbstract -> LensSet FunctionData IsAbstract
    forall o i. Lens' o i -> LensSet o i
    set (IsAbstract -> f IsAbstract) -> FunctionData -> f FunctionData
    Lens' FunctionData IsAbstract
    funAbstr_ (DefInfo -> IsAbstract
    forall t. DefInfo' t -> IsAbstract
    Info.defAbstract DefInfo
    i) FunctionData
    funD{ _funOpaque = Info.defOpaque i }

      let pols = (Occurrence -> Polarity) -> [Occurrence] -> [Polarity]
    forall a b. (a -> b) -> [a] -> [b]
    map Occurrence -> Polarity
    polFromOcc [Occurrence]
    occs

      addConstant x =<< do
        useTerPragma $ defn
            { defArgOccurrences    = occs
            , defPolarity          = pols
            , defGeneralizedParams = genParams
            , defBlocked           = blk
            }

      reportSLn "tc.polarity" 10 $
        "Setting occurrences and polarity for " ++ prettyShow x ++ ":\n  " ++
        prettyShow occs ++ "\n  " ++ prettyShow pols

      -- Add the definition to the instance table, if needed
      case Info.defInstance i of
        InstanceDef KwRange
    _r -> QName -> TCM () -> TCM ()
    forall (m :: * -> *) x a.
    (MonadTrace m, HasRange x) =>
    x -> m a -> m a
    setCurrentRange QName
    x (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ QName -> Type -> TCM ()
    addTypedInstance QName
    x Type
    t
          -- Put highlighting on name only; including the instance keyword,
          -- like @(getRange (r,x))@, does not produce good results.
        IsInstance
    NotInstanceDef -> () -> TCM ()
    forall a. a -> TCMT IO a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure ()

      traceCall (IsType_ e) $ do -- need Range for error message
        -- Andreas, 2016-06-21, issue #2054
        -- Do not default size metas to ∞ in local type signatures
        checkingWhere <- asksTC envCheckingWhere
        solveSizeConstraints $ if checkingWhere /= NoWhere_ then DontDefaultToInfty else DefaultToInfty

    -- | Type check a primitive function declaration.
    checkPrimitive :: A.DefInfo -> QName -> Arg A.Expr -> TCM ()
    checkPrimitive :: DefInfo -> QName -> Arg Expr -> TCM ()
    checkPrimitive DefInfo
    i QName
    x (Arg ArgInfo
    info Expr
    e) =
        Call -> TCM () -> TCM ()
    forall a. Call -> TCMT IO a -> TCMT IO a
    forall (m :: * -> *) a. MonadTrace m => Call -> m a -> m a
    traceCall (Range -> QName -> Expr -> Call
    CheckPrimitive (DefInfo -> Range
    forall a. HasRange a => a -> Range
    getRange DefInfo
    i) QName
    x Expr
    e) (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ do
        (name, PrimImpl t' pf) <- QName -> TCM (PrimitiveId, PrimitiveImpl)
    lookupPrimitiveFunctionQ QName
    x
        -- Certain "primitive" functions are BUILTIN rather than
        -- primitive.
        let builtinPrimitives =
              [ PrimitiveId
    PrimNatPlus
              , PrimitiveId
    PrimNatMinus
              , PrimitiveId
    PrimNatTimes
              , PrimitiveId
    PrimNatDivSucAux
              , PrimitiveId
    PrimNatModSucAux
              , PrimitiveId
    PrimNatEquality
              , PrimitiveId
    PrimNatLess
              , PrimitiveId
    PrimLevelZero
              , PrimitiveId
    PrimLevelSuc
              , PrimitiveId
    PrimLevelMax
              ]
        when (name `elem` builtinPrimitives) $ do
          reportSDoc "tc.prim" 20 $ pretty name <+> "is a BUILTIN, not a primitive!"
          typeError $ NoSuchPrimitiveFunction (getBuiltinId name)
        t <- isType_ e
        noConstraints $ equalType t t'
        let s  = Name -> [Char]
    forall a. Pretty a => a -> [Char]
    prettyShow (Name -> [Char]) -> Name -> [Char]
    forall a b. (a -> b) -> a -> b
    $ QName -> Name
    qnameName QName
    x
        -- Checking the ArgInfo. Currently all primitive definitions require default
        -- ArgInfos, and likely very few will have different ArgInfos in the
        -- future. Thus, rather than, the arguably nicer solution of adding an
        -- ArgInfo to PrimImpl we simply check the few special primitives here.
        let expectedInfo =
              -- Currently no special primitives
              -- case name of _ ->
                            ArgInfo
    defaultArgInfo
        unless (info == expectedInfo) $
          typeError $ WrongArgInfoForPrimitive name info expectedInfo
        bindPrimitive name pf
        lang <- getLanguage
        addConstant x
          (defaultDefn info x t lang Primitive
            { primAbstr    = Info.defAbstract i
            , primOpaque   = TransparentDef
            , primName     = name
            , primClauses  = []
            , primInv      = NotInjective
            , primCompiled = Nothing })
          { defArgOccurrences = primFunArgOccurrences pf }

    -- | Check a pragma.
    checkPragma :: Range -> A.Pragma -> TCM ()
    checkPragma :: Range -> Pragma -> TCM ()
    checkPragma Range
    r Pragma
    p = do
        let uselessPragma :: Doc -> TCM ()
    uselessPragma = Warning -> TCM ()
    forall (m :: * -> *).
    (HasCallStack, MonadWarning m) =>
    Warning -> m ()
    warning (Warning -> TCM ()) -> (Doc -> Warning) -> Doc -> TCM ()
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Range -> Doc -> Warning
    UselessPragma Range
    r
        Call -> TCM () -> TCM ()
    forall a. Call -> TCMT IO a -> TCMT IO a
    forall (m :: * -> *) a. MonadTrace m => Call -> m a -> m a
    traceCall (Range -> Pragma -> Call
    CheckPragma Range
    r Pragma
    p) (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ case Pragma
    p of
            A.BuiltinPragma RString
    rb ResolvedName
    x
              | (BuiltinId -> Bool) -> Maybe BuiltinId -> Bool
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
    any BuiltinId -> Bool
    isUntypedBuiltin Maybe BuiltinId
    b -> () -> TCM ()
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
              | Just BuiltinId
    b' <- Maybe BuiltinId
    b -> BuiltinId -> ResolvedName -> TCM ()
    bindBuiltin BuiltinId
    b' ResolvedName
    x
              | Bool
    otherwise -> TypeError -> TCM ()
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    TypeError -> m a
    typeError (TypeError -> TCM ()) -> TypeError -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ [Char] -> TypeError
    NoSuchBuiltinName [Char]
    ident
              where
                ident :: [Char]
    ident = RString -> [Char]
    forall a. Ranged a -> a
    rangedThing RString
    rb
                b :: Maybe BuiltinId
    b = [Char] -> Maybe BuiltinId
    builtinById [Char]
    ident
            A.BuiltinNoDefPragma RString
    rb KindOfName
    _kind QName
    x
              | Just BuiltinId
    b' <- [Char] -> Maybe BuiltinId
    builtinById [Char]
    b -> BuiltinId -> QName -> TCM ()
    bindBuiltinNoDef BuiltinId
    b' QName
    x
              | Bool
    otherwise -> TypeError -> TCM ()
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    TypeError -> m a
    typeError (TypeError -> TCM ()) -> TypeError -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ [Char] -> TypeError
    NoSuchBuiltinName [Char]
    b
              where b :: [Char]
    b = RString -> [Char]
    forall a. Ranged a -> a
    rangedThing RString
    rb
            A.RewritePragma Range
    _ [QName]
    qs -> [QName] -> TCM ()
    addRewriteRules [QName]
    qs
            A.CompilePragma Ranged Text
    b QName
    x [Char]
    s -> do
              -- Check that x resides in the same module (or a child) as the pragma.
              x' <- Definition -> QName
    defName (Definition -> QName) -> TCMT IO Definition -> TCMT IO QName
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> QName -> TCMT IO Definition
    forall (m :: * -> *). HasConstInfo m => QName -> m Definition
    getConstInfo QName
    x  -- Get the canonical name of x.
              ifM ((x' `isInModule`) <$> currentModule)
                {- then -} (addPragma (rangedThing b) x s)
                {- else -} $ uselessPragma
                  "COMPILE pragmas must appear in the same module as their corresponding definitions,"

            A.StaticPragma QName
    x -> do
              def <- TCMT IO Definition -> TCMT IO Definition
    forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
    ignoreAbstractMode (TCMT IO Definition -> TCMT IO Definition)
    -> TCMT IO Definition -> TCMT IO Definition
    forall a b. (a -> b) -> a -> b
    $ QName -> TCMT IO Definition
    forall (m :: * -> *). HasConstInfo m => QName -> m Definition
    getConstInfo QName
    x
              case theDef def of
                Function{} -> QName -> TCM ()
    markStatic QName
    x
                Defn
    _          -> Doc -> TCM ()
    uselessPragma Doc
    "STATIC directive only applies to functions"
            A.InjectivePragma QName
    x -> QName -> TCM ()
    markInjective QName
    x
            A.InjectiveForInferencePragma QName
    x -> do
              def <- TCMT IO Definition -> TCMT IO Definition
    forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
    ignoreAbstractMode (TCMT IO Definition -> TCMT IO Definition)
    -> TCMT IO Definition -> TCMT IO Definition
    forall a b. (a -> b) -> a -> b
    $ QName -> TCMT IO Definition
    forall (m :: * -> *). HasConstInfo m => QName -> m Definition
    getConstInfo QName
    x
              case theDef def of
                Function{} -> QName -> TCM ()
    markFirstOrder QName
    x
                Defn
    _ -> Doc -> TCM ()
    uselessPragma Doc
    "INJECTIVE_FOR_INFERENCE directive only applies to functions"
            A.NotProjectionLikePragma QName
    qn -> do
              def <- TCMT IO Definition -> TCMT IO Definition
    forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
    ignoreAbstractMode (TCMT IO Definition -> TCMT IO Definition)
    -> TCMT IO Definition -> TCMT IO Definition
    forall a b. (a -> b) -> a -> b
    $ QName -> TCMT IO Definition
    forall (m :: * -> *). HasConstInfo m => QName -> m Definition
    getConstInfo QName
    qn
              case theDef def of
                it :: Defn
    it@Function{} ->
                  QName -> (Definition -> Definition) -> TCM ()
    forall (m :: * -> *).
    MonadTCState m =>
    QName -> (Definition -> Definition) -> m ()
    modifyGlobalDefinition QName
    qn ((Definition -> Definition) -> TCM ())
    -> (Definition -> Definition) -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ \Definition
    def -> Definition
    def { theDef = it { funProjection = Left NeverProjection } }
                Defn
    _ -> Doc -> TCM ()
    uselessPragma Doc
    "NOT_PROJECTION_LIKE directive only applies to functions"
            A.InlinePragma Bool
    b QName
    x -> do
              def <- TCMT IO Definition -> TCMT IO Definition
    forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
    ignoreAbstractMode (TCMT IO Definition -> TCMT IO Definition)
    -> TCMT IO Definition -> TCMT IO Definition
    forall a b. (a -> b) -> a -> b
    $ QName -> TCMT IO Definition
    forall (m :: * -> *). HasConstInfo m => QName -> m Definition
    getConstInfo QName
    x
              case theDef def of
                Function{} -> Bool -> QName -> TCM ()
    markInline Bool
    b QName
    x
                d :: Defn
    d@Constructor{ ConHead
    conSrcCon :: ConHead
    conSrcCon :: Defn -> ConHead
    conSrcCon } | ConHead -> Bool
    forall a. CopatternMatchingAllowed a => a -> Bool
    copatternMatchingAllowed ConHead
    conSrcCon
                  -> QName -> (Definition -> Definition) -> TCM ()
    forall (m :: * -> *).
    MonadTCState m =>
    QName -> (Definition -> Definition) -> m ()
    modifyGlobalDefinition QName
    x ((Definition -> Definition) -> TCM ())
    -> (Definition -> Definition) -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ Lens' Definition Defn -> LensSet Definition Defn
    forall o i. Lens' o i -> LensSet o i
    set (Defn -> f Defn) -> Definition -> f Definition
    Lens' Definition Defn
    lensTheDef Defn
    d{ conInline = b }
                Defn
    _ -> Doc -> TCM ()
    uselessPragma (Doc -> TCM ()) -> Doc -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ [Char] -> Doc
    forall a. [Char] -> Doc a
    P.text ([Char] -> Doc) -> [Char] -> Doc
    forall a b. (a -> b) -> a -> b
    $ Bool -> ([Char] -> [Char]) -> [Char] -> [Char]
    forall b a. IsBool b => b -> (a -> a) -> a -> a
    applyUnless Bool
    b ([Char]
    "NO" [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++) [Char]
    "INLINE directive only works on functions or constructors of records that allow copattern matching"
            A.OptionsPragma{} -> Doc -> TCM ()
    uselessPragma (Doc -> TCM ()) -> Doc -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ Doc
    "OPTIONS pragma only allowed at beginning of file, before top module declaration"
            A.DisplayPragma QName
    f [NamedArg Pattern]
    ps Expr
    e -> QName -> [NamedArg Pattern] -> Expr -> TCM ()
    checkDisplayPragma QName
    f [NamedArg Pattern]
    ps Expr
    e

            A.OverlapPragma QName
    q OverlapMode
    new -> do
              TCMT IO Bool -> TCM () -> TCM () -> TCM ()
    forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
    ifNotM ((QName
    q QName -> ModuleName -> Bool
    `isInModule`) (ModuleName -> Bool) -> TCMT IO ModuleName -> TCMT IO Bool
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> TCMT IO ModuleName
    forall (m :: * -> *). MonadTCEnv m => m ModuleName
    currentModule)
                (Doc -> TCM ()
    uselessPragma (Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< [TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    fsep (
                  [Char] -> [TCMT IO Doc]
    forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
    pwords [Char]
    "This" [TCMT IO Doc] -> [TCMT IO Doc] -> [TCMT IO Doc]
    forall a. [a] -> [a] -> [a]
    ++ [OverlapMode -> TCMT IO Doc
    forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
    pretty OverlapMode
    new] [TCMT IO Doc] -> [TCMT IO Doc] -> [TCMT IO Doc]
    forall a. [a] -> [a] -> [a]
    ++
                  [Char] -> [TCMT IO Doc]
    forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
    pwords [Char]
    "pragma must appear in the same module as the definition of" [TCMT IO Doc] -> [TCMT IO Doc] -> [TCMT IO Doc]
    forall a. [a] -> [a] -> [a]
    ++
                  [QName -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => QName -> m Doc
    prettyTCM QName
    q]))

                {- else -} do

              def <- QName -> TCMT IO Definition
    forall (m :: * -> *). HasConstInfo m => QName -> m Definition
    getConstInfo QName
    q
              case defInstance def of
                Just i :: InstanceInfo
    i@InstanceInfo{ instanceOverlap :: InstanceInfo -> OverlapMode
    instanceOverlap = OverlapMode
    DefaultOverlap } ->
                  QName -> (Definition -> Definition) -> TCM ()
    forall (m :: * -> *).
    MonadTCState m =>
    QName -> (Definition -> Definition) -> m ()
    modifyGlobalDefinition QName
    q \Definition
    x -> Definition
    x { defInstance = Just i{ instanceOverlap = new } }
                Just InstanceInfo{ instanceOverlap :: InstanceInfo -> OverlapMode
    instanceOverlap = OverlapMode
    old } -> TypeError -> TCM ()
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    TypeError -> m a
    typeError (TypeError -> TCM ()) -> TypeError -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ QName -> OverlapMode -> OverlapMode -> TypeError
    DuplicateOverlapPragma QName
    q OverlapMode
    old OverlapMode
    new
                Maybe InstanceInfo
    Nothing -> Doc -> TCM ()
    uselessPragma (Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< OverlapMode -> TCMT IO Doc
    forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
    pretty OverlapMode
    new TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> TCMT IO Doc
    "pragma can only be applied to instances"

            A.EtaPragma QName
    q -> QName -> TCMT IO (Maybe RecordData)
    forall (m :: * -> *).
    HasConstInfo m =>
    QName -> m (Maybe RecordData)
    isRecord QName
    q TCMT IO (Maybe RecordData)
    -> (Maybe RecordData -> TCM ()) -> TCM ()
    forall a b. TCMT IO a -> (a -> TCMT IO b) -> TCMT IO b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \case
                Maybe RecordData
    Nothing -> TCM ()
    noRecord
                Just RecordData{ _recInduction :: RecordData -> Maybe Induction
    _recInduction = Maybe Induction
    ind, _recEtaEquality' :: RecordData -> EtaEquality
    _recEtaEquality' = EtaEquality
    eta }
                  | Maybe Induction
    ind Maybe Induction -> Maybe Induction -> Bool
    forall a. Eq a => a -> a -> Bool
    /= Induction -> Maybe Induction
    forall a. a -> Maybe a
    Just Induction
    CoInductive  -> TCM ()
    noRecord
                  | Specified NoEta{} <- EtaEquality
    eta -> Doc -> TCM ()
    uselessPragma Doc
    "ETA pragma conflicts with no-eta-equality declaration"
                  | Bool
    otherwise -> QName -> (EtaEquality -> EtaEquality) -> TCM ()
    forall (m :: * -> *).
    MonadTCState m =>
    QName -> (EtaEquality -> EtaEquality) -> m ()
    modifyRecEta QName
    q ((EtaEquality -> EtaEquality) -> TCM ())
    -> (EtaEquality -> EtaEquality) -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ EtaEquality -> EtaEquality -> EtaEquality
    forall a b. a -> b -> a
    const (EtaEquality -> EtaEquality -> EtaEquality)
    -> EtaEquality -> EtaEquality -> EtaEquality
    forall a b. (a -> b) -> a -> b
    $ HasEta' PatternOrCopattern -> EtaEquality
    Specified HasEta' PatternOrCopattern
    forall a. HasEta' a
    YesEta
              where
                noRecord :: TCM ()
    noRecord = Doc -> TCM ()
    uselessPragma Doc
    "ETA pragma is only applicable to coinductive records"

    -- | Type check a bunch of mutual inductive recursive definitions.
    --
    -- All definitions which have so far been assigned to the given mutual
    -- block are returned.
    checkMutual :: Info.MutualInfo -> [A.Declaration] -> TCM (MutualId, Set QName)
    checkMutual :: MutualInfo -> [Declaration] -> TCMT IO (MutualId, Set QName)
    checkMutual MutualInfo
    i [Declaration]
    ds = (MutualId -> TCMT IO (MutualId, Set QName))
    -> TCMT IO (MutualId, Set QName)
    forall a. (MutualId -> TCM a) -> TCM a
    inMutualBlock ((MutualId -> TCMT IO (MutualId, Set QName))
     -> TCMT IO (MutualId, Set QName))
    -> (MutualId -> TCMT IO (MutualId, Set QName))
    -> TCMT IO (MutualId, Set QName)
    forall a b. (a -> b) -> a -> b
    $ \ MutualId
    blockId -> TCMT IO (MutualId, Set QName) -> TCMT IO (MutualId, Set QName)
    forall (m :: * -> *) a.
    (PureTCM m, MonadMetaSolver m) =>
    m a -> m a
    defaultOpenLevelsToZero (TCMT IO (MutualId, Set QName) -> TCMT IO (MutualId, Set QName))
    -> TCMT IO (MutualId, Set QName) -> TCMT IO (MutualId, Set QName)
    forall a b. (a -> b) -> a -> b
    $ do

      [Char] -> Int -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "tc.decl.mutual" Int
    20 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ [TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    vcat ([TCMT IO Doc] -> TCMT IO Doc) -> [TCMT IO Doc] -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $
          ((TCMT IO Doc
    "Checking mutual block" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> [Char] -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => [Char] -> m Doc
    text (MutualId -> [Char]
    forall a. Show a => a -> [Char]
    show MutualId
    blockId)) TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall a. Semigroup a => a -> a -> a
    <> TCMT IO Doc
    ":") TCMT IO Doc -> [TCMT IO Doc] -> [TCMT IO Doc]
    forall a. a -> [a] -> [a]
    :
          (Declaration -> TCMT IO Doc) -> [Declaration] -> [TCMT IO Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map (Int -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
    nest Int
    2 (TCMT IO Doc -> TCMT IO Doc)
    -> (Declaration -> TCMT IO Doc) -> Declaration -> TCMT IO Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Declaration -> TCMT IO Doc
    forall a (m :: * -> *).
    (ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
    a -> m Doc
    prettyA) [Declaration]
    ds

      MutualId -> MutualInfo -> TCM ()
    insertMutualBlockInfo MutualId
    blockId MutualInfo
    i
      (TCEnv -> TCEnv) -> TCM () -> TCM ()
    forall a. (TCEnv -> TCEnv) -> TCMT IO a -> TCMT IO a
    forall (m :: * -> *) a.
    MonadTCEnv m =>
    (TCEnv -> TCEnv) -> m a -> m a
    localTC ( Lens' TCEnv (TerminationCheck ())
    -> LensSet TCEnv (TerminationCheck ())
    forall o i. Lens' o i -> LensSet o i
    set (TerminationCheck () -> f (TerminationCheck ()))
    -> TCEnv -> f TCEnv
    Lens' TCEnv (TerminationCheck ())
    eTerminationCheck (() () -> TerminationCheck Name -> TerminationCheck ()
    forall a b. a -> TerminationCheck b -> TerminationCheck a
    forall (f :: * -> *) a b. Functor f => a -> f b -> f a
    <$ MutualInfo -> TerminationCheck Name
    Info.mutualTerminationCheck MutualInfo
    i)
              (TCEnv -> TCEnv) -> (TCEnv -> TCEnv) -> TCEnv -> TCEnv
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Lens' TCEnv CoverageCheck -> LensSet TCEnv CoverageCheck
    forall o i. Lens' o i -> LensSet o i
    set (CoverageCheck -> f CoverageCheck) -> TCEnv -> f TCEnv
    Lens' TCEnv CoverageCheck
    eCoverageCheck (MutualInfo -> CoverageCheck
    Info.mutualCoverageCheck MutualInfo
    i)) (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $
        (Declaration -> TCM ()) -> [Declaration] -> TCM ()
    forall (t :: * -> *) (m :: * -> *) a b.
    (Foldable t, Monad m) =>
    (a -> m b) -> t a -> m ()
    mapM_ Declaration -> TCM ()
    checkDecl [Declaration]
    ds

      (MutualId
    blockId, ) (Set QName -> (MutualId, Set QName))
    -> (MutualBlock -> Set QName)
    -> MutualBlock
    -> (MutualId, Set QName)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . MutualBlock -> Set QName
    mutualNames (MutualBlock -> (MutualId, Set QName))
    -> TCMT IO MutualBlock -> TCMT IO (MutualId, Set QName)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> MutualId -> TCMT IO MutualBlock
    forall (tcm :: * -> *).
    ReadTCState tcm =>
    MutualId -> tcm MutualBlock
    lookupMutualBlock MutualId
    blockId

        -- check record or data type signature
    checkSig ::
      KindOfName -> A.DefInfo -> Erased -> QName -> A.GeneralizeTelescope ->
      A.Expr -> TCM ()
    checkSig :: KindOfName
    -> DefInfo
    -> Erased
    -> QName
    -> GeneralizeTelescope
    -> Expr
    -> TCM ()
    checkSig KindOfName
    kind DefInfo
    i Erased
    erased QName
    x GeneralizeTelescope
    gtel Expr
    t =
      Maybe GeneralizeTelescope -> Declaration -> TCM ()
    checkTypeSignature' (GeneralizeTelescope -> Maybe GeneralizeTelescope
    forall a. a -> Maybe a
    Just GeneralizeTelescope
    gtel) (Declaration -> TCM ()) -> Declaration -> TCM ()
    forall a b. (a -> b) -> a -> b
    $
      KindOfName
    -> DefInfo
    -> ArgInfo
    -> Maybe PragmaPolarities
    -> QName
    -> Expr
    -> Declaration
    A.Axiom KindOfName
    kind DefInfo
    i (Quantity -> ArgInfo -> ArgInfo
    forall a. LensQuantity a => Quantity -> a -> a
    setQuantity (Erased -> Quantity
    asQuantity Erased
    erased) ArgInfo
    defaultArgInfo)
        Maybe PragmaPolarities
    forall a. Maybe a
    Nothing QName
    x Expr
    t

    -- | Type check the type signature of an inductive or recursive definition.
    checkTypeSignature :: A.TypeSignature -> TCM ()
    checkTypeSignature :: Declaration -> TCM ()
    checkTypeSignature = Maybe GeneralizeTelescope -> Declaration -> TCM ()
    checkTypeSignature' Maybe GeneralizeTelescope
    forall a. Maybe a
    Nothing

    checkTypeSignature' :: Maybe A.GeneralizeTelescope -> A.TypeSignature -> TCM ()
    checkTypeSignature' :: Maybe GeneralizeTelescope -> Declaration -> TCM ()
    checkTypeSignature' Maybe GeneralizeTelescope
    gtel (A.ScopedDecl ScopeInfo
    scope [Declaration]
    ds) = do
      ScopeInfo -> TCM ()
    setScope ScopeInfo
    scope
      (Declaration -> TCM ()) -> [Declaration] -> TCM ()
    forall (t :: * -> *) (m :: * -> *) a b.
    (Foldable t, Monad m) =>
    (a -> m b) -> t a -> m ()
    mapM_ (Maybe GeneralizeTelescope -> Declaration -> TCM ()
    checkTypeSignature' Maybe GeneralizeTelescope
    gtel) [Declaration]
    ds
    checkTypeSignature' Maybe GeneralizeTelescope
    gtel (A.Axiom KindOfName
    funSig DefInfo
    i ArgInfo
    info Maybe PragmaPolarities
    mp QName
    x Expr
    e) =
      Account (BenchPhase (TCMT IO)) -> TCM () -> TCM ()
    forall (m :: * -> *) c.
    MonadBench m =>
    Account (BenchPhase m) -> m c -> m c
    Bench.billTo [QName -> Phase
    Bench.Definition QName
    x] (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $
      Account (BenchPhase (TCMT IO)) -> TCM () -> TCM ()
    forall (m :: * -> *) c.
    MonadBench m =>
    Account (BenchPhase m) -> m c -> m c
    Bench.billTo [BenchPhase (TCMT IO)
    Phase
    Bench.Typing, BenchPhase (TCMT IO)
    Phase
    Bench.TypeSig] (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $
        let abstr :: TCM () -> TCM ()
    abstr = case DefInfo -> Access
    forall t. DefInfo' t -> Access
    Info.defAccess DefInfo
    i of
              PrivateAccess{}
                | DefInfo -> IsAbstract
    forall t. DefInfo' t -> IsAbstract
    Info.defAbstract DefInfo
    i IsAbstract -> IsAbstract -> Bool
    forall a. Eq a => a -> a -> Bool
    == IsAbstract
    AbstractDef -> TCM () -> TCM ()
    forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
    inConcreteMode
                  -- Issue #2321, only go to AbstractMode for abstract definitions
                  -- Issue #418, #3744, in fact don't go to AbstractMode at all
                | Bool
    otherwise -> TCM () -> TCM ()
    forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
    inConcreteMode
              Access
    PublicAccess  -> TCM () -> TCM ()
    forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
    inConcreteMode
        in TCM () -> TCM ()
    abstr (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ Maybe GeneralizeTelescope
    -> KindOfName
    -> DefInfo
    -> ArgInfo
    -> Maybe PragmaPolarities
    -> QName
    -> Expr
    -> TCM ()
    checkAxiom' Maybe GeneralizeTelescope
    gtel KindOfName
    funSig DefInfo
    i ArgInfo
    info Maybe PragmaPolarities
    mp QName
    x Expr
    e
    checkTypeSignature' Maybe GeneralizeTelescope
    _ Declaration
    _ =
      TCM ()
    forall a. HasCallStack => a
    __IMPOSSIBLE__   -- type signatures are always axioms

    -- | Type check a module.

    checkSection ::
      Erased -> ModuleName -> A.GeneralizeTelescope -> [A.Declaration] ->
      TCM ()
    checkSection :: Erased
    -> ModuleName -> GeneralizeTelescope -> [Declaration] -> TCM ()
    checkSection Erased
    e ModuleName
    x GeneralizeTelescope
    tel [Declaration]
    ds =
      Erased -> ModuleName -> GeneralizeTelescope -> TCM () -> TCM ()
    forall a.
    Erased -> ModuleName -> GeneralizeTelescope -> TCM a -> TCM a
    newSection Erased
    e ModuleName
    x GeneralizeTelescope
    tel (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ (Declaration -> TCM ()) -> [Declaration] -> TCM ()
    forall (t :: * -> *) (m :: * -> *) a b.
    (Foldable t, Monad m) =>
    (a -> m b) -> t a -> m ()
    mapM_ Declaration -> TCM ()
    checkDeclCached [Declaration]
    ds

    -- | Helper for 'checkSectionApplication'.
    --
    --   Matches the arguments of the module application with the
    --   module parameters.
    --
    --   Returns the remaining module parameters as an open telescope.
    --   Warning: the returned telescope is /not/ the final result,
    --   an actual instantiation of the parameters does not occur.
    checkModuleArity ::
         ModuleName           -- ^ Name of applied module.
      -> Telescope            -- ^ The module parameters.
      -> [NamedArg A.Expr]    -- ^ The arguments this module is applied to.
      -> TCM Telescope        -- ^ The remaining module parameters (has free de Bruijn indices!).
    checkModuleArity :: ModuleName
    -> Tele (Dom Type) -> [NamedArg Expr] -> TCM (Tele (Dom Type))
    checkModuleArity ModuleName
    m Tele (Dom Type)
    tel = \case
      []   -> Tele (Dom Type) -> TCM (Tele (Dom Type))
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Tele (Dom Type)
    tel
      NamedArg Expr
    a:[NamedArg Expr]
    as -> Tele (Dom Type)
    -> NamedArg Expr -> [NamedArg Expr] -> TCM (Tele (Dom Type))
    check1 Tele (Dom Type)
    tel NamedArg Expr
    a [NamedArg Expr]
    as
        where
        bad :: TCM (Tele (Dom Type))
    bad = TypeError -> TCM (Tele (Dom Type))
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    TypeError -> m a
    typeError (TypeError -> TCM (Tele (Dom Type)))
    -> TypeError -> TCM (Tele (Dom Type))
    forall a b. (a -> b) -> a -> b
    $ ModuleName
    -> Tele (Dom Type)
    -> Either (List1 (NamedArg Expr)) [Arg Term]
    -> TypeError
    ModuleArityMismatch ModuleName
    m Tele (Dom Type)
    tel (List1 (NamedArg Expr) -> Either (List1 (NamedArg Expr)) [Arg Term]
    forall a b. a -> Either a b
    Left (NamedArg Expr
    a NamedArg Expr -> [NamedArg Expr] -> List1 (NamedArg Expr)
    forall a. a -> [a] -> NonEmpty a
    :| [NamedArg Expr]
    as))

        check :: Telescope -> [NamedArg A.Expr] -> TCM Telescope
        check :: Tele (Dom Type) -> [NamedArg Expr] -> TCM (Tele (Dom Type))
    check Tele (Dom Type)
    tel []             = Tele (Dom Type) -> TCM (Tele (Dom Type))
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Tele (Dom Type)
    tel
        check Tele (Dom Type)
    tel (NamedArg Expr
    a : [NamedArg Expr]
    as)       = Tele (Dom Type)
    -> NamedArg Expr -> [NamedArg Expr] -> TCM (Tele (Dom Type))
    check1 Tele (Dom Type)
    tel NamedArg Expr
    a [NamedArg Expr]
    as

        check1 :: Telescope -> NamedArg A.Expr -> [NamedArg A.Expr] -> TCM Telescope
        check1 :: Tele (Dom Type)
    -> NamedArg Expr -> [NamedArg Expr] -> TCM (Tele (Dom Type))
    check1 Tele (Dom Type)
    EmptyTel NamedArg Expr
    _ [NamedArg Expr]
    _ = TCM (Tele (Dom Type))
    bad
        check1 (ExtendTel dom :: Dom Type
    dom@Dom{domInfo :: forall t e. Dom' t e -> ArgInfo
    domInfo = ArgInfo
    info} Abs (Tele (Dom Type))
    btel) arg0 :: NamedArg Expr
    arg0@(Arg ArgInfo
    info' Named_ Expr
    arg) [NamedArg Expr]
    args = do
          let name :: Maybe [Char]
    name = Named_ Expr -> Maybe [Char]
    forall a. (LensNamed a, NameOf a ~ NamedName) => a -> Maybe [Char]
    bareNameOf Named_ Expr
    arg
              my :: Maybe [Char]
    my   = Dom Type -> Maybe [Char]
    forall a. (LensNamed a, NameOf a ~ NamedName) => a -> Maybe [Char]
    bareNameOf Dom Type
    dom
              tel :: Tele (Dom Type)
    tel  = Abs (Tele (Dom Type)) -> Tele (Dom Type)
    forall a. Subst a => Abs a -> a
    absBody Abs (Tele (Dom Type))
    btel
          case (ArgInfo -> Hiding
    argInfoHiding ArgInfo
    info, ArgInfo -> Hiding
    argInfoHiding ArgInfo
    info', Maybe [Char]
    name) of
            (Instance{}, Hiding
    NotHidden, Maybe [Char]
    _)        -> Tele (Dom Type)
    -> NamedArg Expr -> [NamedArg Expr] -> TCM (Tele (Dom Type))
    check1 Tele (Dom Type)
    tel NamedArg Expr
    arg0 [NamedArg Expr]
    args
            (Instance{}, Hiding
    Hidden, Maybe [Char]
    _)           -> Tele (Dom Type)
    -> NamedArg Expr -> [NamedArg Expr] -> TCM (Tele (Dom Type))
    check1 Tele (Dom Type)
    tel NamedArg Expr
    arg0 [NamedArg Expr]
    args
            (Instance{}, Instance{}, Maybe [Char]
    Nothing) -> Tele (Dom Type) -> [NamedArg Expr] -> TCM (Tele (Dom Type))
    check  Tele (Dom Type)
    tel [NamedArg Expr]
    args
            (Instance{}, Instance{}, Just [Char]
    x)
              | [Char] -> Maybe [Char]
    forall a. a -> Maybe a
    Just [Char]
    x Maybe [Char] -> Maybe [Char] -> Bool
    forall a. Eq a => a -> a -> Bool
    == Maybe [Char]
    my                  -> Tele (Dom Type) -> [NamedArg Expr] -> TCM (Tele (Dom Type))
    check  Tele (Dom Type)
    tel [NamedArg Expr]
    args
              | Bool
    otherwise                     -> Tele (Dom Type)
    -> NamedArg Expr -> [NamedArg Expr] -> TCM (Tele (Dom Type))
    check1 Tele (Dom Type)
    tel NamedArg Expr
    arg0 [NamedArg Expr]
    args
            (Hiding
    Hidden, Hiding
    NotHidden, Maybe [Char]
    _)            -> Tele (Dom Type)
    -> NamedArg Expr -> [NamedArg Expr] -> TCM (Tele (Dom Type))
    check1 Tele (Dom Type)
    tel NamedArg Expr
    arg0 [NamedArg Expr]
    args
            (Hiding
    Hidden, Instance{}, Maybe [Char]
    _)           -> Tele (Dom Type)
    -> NamedArg Expr -> [NamedArg Expr] -> TCM (Tele (Dom Type))
    check1 Tele (Dom Type)
    tel NamedArg Expr
    arg0 [NamedArg Expr]
    args
            (Hiding
    Hidden, Hiding
    Hidden, Maybe [Char]
    Nothing)         -> Tele (Dom Type) -> [NamedArg Expr] -> TCM (Tele (Dom Type))
    check  Tele (Dom Type)
    tel [NamedArg Expr]
    args
            (Hiding
    Hidden, Hiding
    Hidden, Just [Char]
    x)
              | [Char] -> Maybe [Char]
    forall a. a -> Maybe a
    Just [Char]
    x Maybe [Char] -> Maybe [Char] -> Bool
    forall a. Eq a => a -> a -> Bool
    == Maybe [Char]
    my                  -> Tele (Dom Type) -> [NamedArg Expr] -> TCM (Tele (Dom Type))
    check  Tele (Dom Type)
    tel [NamedArg Expr]
    args
              | Bool
    otherwise                     -> Tele (Dom Type)
    -> NamedArg Expr -> [NamedArg Expr] -> TCM (Tele (Dom Type))
    check1 Tele (Dom Type)
    tel NamedArg Expr
    arg0 [NamedArg Expr]
    args
            (Hiding
    NotHidden, Hiding
    NotHidden, Maybe [Char]
    _)         -> Tele (Dom Type) -> [NamedArg Expr] -> TCM (Tele (Dom Type))
    check  Tele (Dom Type)
    tel [NamedArg Expr]
    args
            (Hiding
    NotHidden, Hiding
    Hidden, Maybe [Char]
    _)            -> TCM (Tele (Dom Type))
    bad
            (Hiding
    NotHidden, Instance{}, Maybe [Char]
    _)        -> TCM (Tele (Dom Type))
    bad

    -- | Check an application of a section.
    checkSectionApplication
      :: Info.ModuleInfo
      -> Erased              -- ^ Should \"everything\" be treated as
                             --   erased?
      -> ModuleName          -- ^ Name @m1@ of module defined by the module macro.
      -> A.ModuleApplication -- ^ The module macro @λ tel → m2 args@.
      -> A.ScopeCopyInfo     -- ^ Imported names and modules
      -> A.ImportDirective
      -> TCM ()
    checkSectionApplication :: ModuleInfo
    -> Erased
    -> ModuleName
    -> ModuleApplication
    -> ScopeCopyInfo
    -> ImportDirective
    -> TCM ()
    checkSectionApplication ModuleInfo
    i Erased
    er ModuleName
    m1 ModuleApplication
    modapp ScopeCopyInfo
    copyInfo ImportDirective
    dir =
      Call -> TCM () -> TCM ()
    forall a. Call -> TCMT IO a -> TCMT IO a
    forall (m :: * -> *) a. MonadTrace m => Call -> m a -> m a
    traceCall (Range -> Erased -> ModuleName -> ModuleApplication -> Call
    CheckSectionApplication (ModuleInfo -> Range
    forall a. HasRange a => a -> Range
    getRange ModuleInfo
    i) Erased
    er ModuleName
    m1 ModuleApplication
    modapp) (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ do
      ImportDirective -> TCM ()
    checkImportDirective ImportDirective
    dir
      -- A (non-erased) section application is type-checked in a
      -- non-erased context (#5410), except if hard compile-time mode is
      -- enabled (#4743).
      TCM () -> TCM ()
    forall a. TCM a -> TCM a
    setRunTimeModeUnlessInHardCompileTimeMode (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $
        ModuleInfo
    -> Erased
    -> ModuleName
    -> ModuleApplication
    -> ScopeCopyInfo
    -> TCM ()
    checkSectionApplication' ModuleInfo
    i Erased
    er ModuleName
    m1 ModuleApplication
    modapp ScopeCopyInfo
    copyInfo

    -- | Check an application of a section. (Do not invoke this procedure
    -- directly, use 'checkSectionApplication'.)
    checkSectionApplication'
      :: Info.ModuleInfo
      -> Erased
      -> ModuleName          -- ^ Name @m1@ of module defined by the module macro.
      -> A.ModuleApplication -- ^ The module macro @λ tel → m2 args@.
      -> A.ScopeCopyInfo     -- ^ Imported names and modules
      -> TCM ()
    checkSectionApplication' :: ModuleInfo
    -> Erased
    -> ModuleName
    -> ModuleApplication
    -> ScopeCopyInfo
    -> TCM ()
    checkSectionApplication'
      ModuleInfo
    i Erased
    er ModuleName
    m1 (A.SectionApp Telescope
    ptel ModuleName
    m2 [NamedArg Expr]
    args) ScopeCopyInfo
    copyInfo = do
      -- If the section application is erased, then hard compile-time mode
      -- is entered.
      Erased -> TCM ()
    warnForPlentyInHardCompileTimeMode Erased
    er
      Erased -> TCM () -> TCM ()
    forall a. Erased -> TCM a -> TCM a
    setHardCompileTimeModeIfErased Erased
    er (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ do
      -- Module applications can appear in lets, in which case we treat
      -- lambda-bound variables as additional parameters to the module.
      extraParams <- do
        mfv <- TCMT IO Int
    getCurrentModuleFreeVars
        fv  <- getContextSize
        return (fv - mfv)
      when (extraParams > 0) $ reportSLn "tc.mod.apply" 30 $ "Extra parameters to " ++ prettyShow m1 ++ ": " ++ show extraParams
      -- Type-check the LHS (ptel) of the module macro.
      checkTelescope ptel $ \ Tele (Dom Type)
    ptel -> do
        -- We are now in the context @ptel@.
        -- Get the correct parameter telescope of @m2@. This is the fully lifted
        -- telescope obtained by `lookupSection` instantiated with the module
        -- parameters of `m2` currently in scope. For instance
        -- ```
        --  module _ (A : Set) where
        --    module M (B : Set) where ...
        --    module M' = M B
        -- ```
        -- In the application `M' = M B`, `tel = (A B : Set)` and
        -- `moduleParamsToApply M = [A]`, so the resulting parameter telescope is
        -- `tel' = (B : Set)`.
        tel <- ModuleName -> TCM (Tele (Dom Type))
    forall (m :: * -> *).
    (Functor m, ReadTCState m) =>
    ModuleName -> m (Tele (Dom Type))
    lookupSection ModuleName
    m2
        vs  <- moduleParamsToApply m2
        let tel'  = Tele (Dom Type) -> [Arg Term] -> Tele (Dom Type)
    forall t. Apply t => t -> [Arg Term] -> t
    apply Tele (Dom Type)
    tel [Arg Term]
    vs
        -- Compute the remaining parameter telescope after stripping of
        -- the initial parameters that are determined by the @args@.
        -- Warning: @etaTel@ is not well-formed in @ptel@, since
        -- the actual application has not happened.
        etaTel <- checkModuleArity m2 tel' args
        -- Take the module parameters that will be instantiated by @args@.
        let tel'' = [Dom ([Char], Type)] -> Tele (Dom Type)
    telFromList ([Dom ([Char], Type)] -> Tele (Dom Type))
    -> [Dom ([Char], Type)] -> Tele (Dom Type)
    forall a b. (a -> b) -> a -> b
    $ Int -> [Dom ([Char], Type)] -> [Dom ([Char], Type)]
    forall a. Int -> [a] -> [a]
    take (Tele (Dom Type) -> Int
    forall a. Sized a => a -> Int
    size Tele (Dom Type)
    tel' Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - Tele (Dom Type) -> Int
    forall a. Sized a => a -> Int
    size Tele (Dom Type)
    etaTel) ([Dom ([Char], Type)] -> [Dom ([Char], Type)])
    -> [Dom ([Char], Type)] -> [Dom ([Char], Type)]
    forall a b. (a -> b) -> a -> b
    $ Tele (Dom Type) -> [Dom ([Char], Type)]
    forall t. Tele (Dom t) -> [Dom ([Char], t)]
    telToList Tele (Dom Type)
    tel'
        reportSDoc "tc.mod.apply" 15 $
            "applying section" <+> prettyTCM m2
        reportSDoc "tc.mod.apply" 15 $
            nest 2 $ "args =" <+> sep (map prettyA args)
        reportSDoc "tc.mod.apply" 15 $
            nest 2 $ "ptel =" <+> escapeContext impossible (size ptel) (prettyTCM ptel)
        reportSDoc "tc.mod.apply" 15 $
            nest 2 $ "tel  =" <+> prettyTCM tel
        reportSDoc "tc.mod.apply" 15 $
            nest 2 $ "tel' =" <+> prettyTCM tel'
        reportSDoc "tc.mod.apply" 15 $
            nest 2 $ "tel''=" <+> prettyTCM tel''
        reportSDoc "tc.mod.apply" 15 $
            nest 2 $ "eta  =" <+> escapeContext impossible (size ptel) (addContext tel'' $ prettyTCM etaTel)

        -- Now, type check arguments.
        -- Andreas, 2024-12-06: We fake a head A.Expr for the application.
        let
          hd = QName -> Expr
    A.Def (QName -> Expr) -> QName -> Expr
    forall a b. (a -> b) -> a -> b
    $ ModuleName -> QName
    mnameToQName ModuleName
    m2
          -- Amy, 2025-04-16, issue #7799: for parity with checking
          -- declaration right-hand-sides we have to check section
          -- applications with the 'instance hack' enabled.
          k = Lens' TCState Bool -> (Bool -> Bool) -> TCMT IO b -> TCMT IO b
    forall a b. Lens' TCState a -> (a -> a) -> TCMT IO b -> TCMT IO b
    forall (m :: * -> *) a b.
    ReadTCState m =>
    Lens' TCState a -> (a -> a) -> m b -> m b
    locallyTCState (Bool -> f Bool) -> TCState -> f TCState
    Lens' TCState Bool
    stInstanceHack (Bool -> Bool -> Bool
    forall a b. a -> b -> a
    const Bool
    True) (TCMT IO b -> TCMT IO b)
    -> (TCMT IO b -> TCMT IO b) -> TCMT IO b -> TCMT IO b
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . TCMT IO b -> TCMT IO b
    forall (m :: * -> *) a.
    (MonadConstraint m, MonadWarning m, MonadError TCErr m,
     MonadFresh ProblemId m) =>
    m a -> m a
    noConstraints

        ts <- k (checkArguments_ CmpEq DontExpandLast hd args tel') >>= \case
          (Elims
    ts', Tele (Dom Type)
    etaTel') | (Tele (Dom Type) -> Int
    forall a. Sized a => a -> Int
    size Tele (Dom Type)
    etaTel Int -> Int -> Bool
    forall a. Eq a => a -> a -> Bool
    == Tele (Dom Type) -> Int
    forall a. Sized a => a -> Int
    size Tele (Dom Type)
    etaTel')
                         , Just [Arg Term]
    ts <- Elims -> Maybe [Arg Term]
    forall a. [Elim' a] -> Maybe [Arg a]
    allApplyElims Elims
    ts' -> [Arg Term] -> TCMT IO [Arg Term]
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return [Arg Term]
    ts
          (Elims, Tele (Dom Type))
    _ -> TCMT IO [Arg Term]
    forall a. HasCallStack => a
    __IMPOSSIBLE__
        -- Perform the application of the module parameters.
        let aTel = Tele (Dom Type)
    tel' Tele (Dom Type) -> [Arg Term] -> Tele (Dom Type)
    forall t. Apply t => t -> [Arg Term] -> t
    `apply` [Arg Term]
    ts
        reportSDoc "tc.mod.apply" 15 $ vcat
          [ nest 2 $ "aTel =" <+> prettyTCM aTel
          ]
        -- Andreas, 2014-04-06, Issue 1094:
        -- Add the section with well-formed telescope.
        addContext (KeepNames aTel) $ do
          reportSDoc "tc.mod.apply" 80 $
            "addSection" <+> prettyTCM m1 <+> (getContextTelescope >>= \ Tele (Dom Type)
    tel -> TCMT IO Doc -> TCMT IO Doc
    forall (tcm :: * -> *) a.
    (MonadTCEnv tcm, ReadTCState tcm) =>
    tcm a -> tcm a
    inTopContext (Tele (Dom Type) -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => Tele (Dom Type) -> m Doc
    prettyTCM Tele (Dom Type)
    tel))
          addSection m1

        reportSDoc "tc.mod.apply" 20 $ vcat
          [ sep [ "applySection", prettyTCM m1, "=", prettyTCM m2, fsep $ map prettyTCM (vs ++ ts) ]
          , nest 2 $ pretty copyInfo
          ]
        args <- instantiateFull $ vs ++ ts
        let n = Tele (Dom Type) -> Int
    forall a. Sized a => a -> Int
    size Tele (Dom Type)
    aTel
        etaArgs <- inTopContext $ addContext aTel getContextArgs
        addContext (KeepNames aTel) $
          applySection m1 (ptel `abstract` aTel) m2 (raise n args ++ etaArgs) copyInfo

    checkSectionApplication' ModuleInfo
    _ Erased{} ModuleName
    _ A.RecordModuleInstance{} ScopeCopyInfo
    _ =
      TCM ()
    forall a. HasCallStack => a
    __IMPOSSIBLE__
    checkSectionApplication'
      ModuleInfo
    i NotErased{} ModuleName
    m1 (A.RecordModuleInstance ModuleName
    x) ScopeCopyInfo
    copyInfo = do
      let name :: QName
    name = ModuleName -> QName
    mnameToQName ModuleName
    x
      tel' <- ModuleName -> TCM (Tele (Dom Type))
    forall (m :: * -> *).
    (Functor m, ReadTCState m) =>
    ModuleName -> m (Tele (Dom Type))
    lookupSection ModuleName
    x
      vs   <- moduleParamsToApply x
      let tel = Tele (Dom Type)
    tel' Tele (Dom Type) -> [Arg Term] -> Tele (Dom Type)
    forall t. Apply t => t -> [Arg Term] -> t
    `apply` [Arg Term]
    vs
          args = Tele (Dom Type) -> [Arg Term]
    forall a t. DeBruijn a => Tele (Dom t) -> [Arg a]
    teleArgs Tele (Dom Type)
    tel

          telInst :: Telescope
          telInst = Tele (Dom Type) -> Tele (Dom Type)
    instFinal Tele (Dom Type)
    tel

          -- Locate last (rightmost) parameter and make it @Instance@.
          -- Issue #3463: also name it so it can be given by name.
          instFinal :: Telescope -> Telescope
          -- Telescopes do not have @NoAbs@.
          instFinal (ExtendTel Dom Type
    _ NoAbs{}) = Tele (Dom Type)
    forall a. HasCallStack => a
    __IMPOSSIBLE__
          -- Found last parameter: switch it to @Instance@.
          instFinal (ExtendTel Dom Type
    dom (Abs [Char]
    n Tele (Dom Type)
    EmptyTel)) =
                     Dom Type -> Abs (Tele (Dom Type)) -> Tele (Dom Type)
    forall a. a -> Abs (Tele a) -> Tele a
    ExtendTel Dom Type
    do' ([Char] -> Tele (Dom Type) -> Abs (Tele (Dom Type))
    forall a. [Char] -> a -> Abs a
    Abs [Char]
    n Tele (Dom Type)
    forall a. Tele a
    EmptyTel)
            where do' :: Dom Type
    do' = Dom Type -> Dom Type
    forall a. LensHiding a => a -> a
    makeInstance Dom Type
    dom { domName = Just $ WithOrigin Inserted $ unranged "r" }
          -- Otherwise, keep searchinf for last parameter:
          instFinal (ExtendTel Dom Type
    arg (Abs [Char]
    n Tele (Dom Type)
    tel)) =
                     Dom Type -> Abs (Tele (Dom Type)) -> Tele (Dom Type)
    forall a. a -> Abs (Tele a) -> Tele a
    ExtendTel Dom Type
    arg ([Char] -> Tele (Dom Type) -> Abs (Tele (Dom Type))
    forall a. [Char] -> a -> Abs a
    Abs [Char]
    n (Tele (Dom Type) -> Tele (Dom Type)
    instFinal Tele (Dom Type)
    tel))
          -- Before instFinal is invoked, we have checked that the @tel@ is not empty.
          instFinal Tele (Dom Type)
    EmptyTel = Tele (Dom Type)
    forall a. HasCallStack => a
    __IMPOSSIBLE__

      reportSDoc "tc.mod.apply" 20 $ vcat
        [ sep [ "applySection", prettyTCM name, "{{...}}" ]
        , nest 2 $ "x       =" <+> prettyTCM x
        , nest 2 $ "name    =" <+> prettyTCM name
        , nest 2 $ "tel     =" <+> prettyTCM tel
        , nest 2 $ "telInst =" <+> prettyTCM telInst
        , nest 2 $ "vs      =" <+> sep (map prettyTCM vs)
        -- , nest 2 $ "args    =" <+> sep (map prettyTCM args)
        ]
      reportSDoc "tc.mod.apply" 60 $ vcat
        [ nest 2 $ "vs      =" <+> text (show vs)
        -- , nest 2 $ "args    =" <+> text (show args)
        ]
      when (tel == EmptyTel) $ typeError $ ModuleArityMismatch x EmptyTel (Right vs)

      addContext telInst $ do
        vs <- moduleParamsToApply x
        reportSDoc "tc.mod.apply" 20 $ vcat
          [ nest 2 $ "vs      =" <+> sep (map prettyTCM vs)
          , nest 2 $ "args    =" <+> sep (map (parens . prettyTCM) args)
          ]
        reportSDoc "tc.mod.apply" 60 $ vcat
          [ nest 2 $ "vs      =" <+> text (show vs)
          , nest 2 $ "args    =" <+> text (show args)
          ]
        addSection m1
        applySection m1 telInst x (vs ++ args) copyInfo

    -- | Checks that @open public@ is not used in hard compile-time mode.
    checkImportDirective :: A.ImportDirective -> TCM ()
    checkImportDirective :: ImportDirective -> TCM ()
    checkImportDirective ImportDirective
    dir = do
      hard <- Lens' TCEnv Bool -> TCMT IO Bool
    forall (m :: * -> *) a. MonadTCEnv m => Lens' TCEnv a -> m a
    viewTC (Bool -> f Bool) -> TCEnv -> f TCEnv
    Lens' TCEnv Bool
    eHardCompileTimeMode
      when (hard && isJust (publicOpen dir)) $ typeError $ NotSupported $
        "open public in hard compile-time mode " ++
        "(for instance in erased modules)"

    ------------------------------------------------------------------------
    -- * Debugging
    ------------------------------------------------------------------------

    class ShowHead a where
      showHead :: a -> String

    instance ShowHead A.Declaration where
      showHead :: Declaration -> [Char]
    showHead Declaration
    d =
        case Declaration
    d of
          A.Axiom        {} -> [Char]
    "Axiom"
          A.Field        {} -> [Char]
    "Field"
          A.Primitive    {} -> [Char]
    "Primitive"
          A.Mutual       {} -> [Char]
    "Mutual"
          A.Section      {} -> [Char]
    "Section"
          A.Apply        {} -> [Char]
    "Apply"
          A.Import       {} -> [Char]
    "Import"
          A.Pragma       {} -> [Char]
    "Pragma"
          A.Open         {} -> [Char]
    "Open"
          A.FunDef       {} -> [Char]
    "FunDef"
          A.DataSig      {} -> [Char]
    "DataSig"
          A.DataDef      {} -> [Char]
    "DataDef"
          A.RecSig       {} -> [Char]
    "RecSig"
          A.RecDef       {} -> [Char]
    "RecDef"
          A.PatternSynDef{} -> [Char]
    "PatternSynDef"
          A.Generalize   {} -> [Char]
    "Generalize"
          A.UnquoteDecl  {} -> [Char]
    "UnquoteDecl"
          A.ScopedDecl   {} -> [Char]
    "ScopedDecl"
          A.UnquoteDef   {} -> [Char]
    "UnquoteDef"
          A.UnquoteData  {} -> [Char]
    "UnquoteDecl data"
          A.UnfoldingDecl{} -> [Char]
    "UnfoldingDecl"

    debugPrintDecl :: A.Declaration -> TCM ()
    debugPrintDecl :: Declaration -> TCM ()
    debugPrintDecl Declaration
    d = do
        [Char] -> Int -> TCM () -> TCM ()
    forall (m :: * -> *). MonadDebug m => [Char] -> Int -> m () -> m ()
    verboseS [Char]
    "tc.decl" Int
    45 (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ do
          [Char] -> Int -> [Char] -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> [Char] -> m ()
    reportSLn [Char]
    "tc.decl" Int
    45 ([Char] -> TCM ()) -> [Char] -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ [Char]
    "checking a " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ Declaration -> [Char]
    forall a. ShowHead a => a -> [Char]
    showHead Declaration
    d
          case Declaration
    d of
            A.Section Range
    info Erased
    erased ModuleName
    mname GeneralizeTelescope
    tel [Declaration]
    ds -> do
              [Char] -> Int -> [Char] -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> [Char] -> m ()
    reportSLn [Char]
    "tc.decl" Int
    45 ([Char] -> TCM ()) -> [Char] -> TCM ()
    forall a b. (a -> b) -> a -> b
    $
                [Char]
    "section " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ ModuleName -> [Char]
    forall a. Pretty a => a -> [Char]
    prettyShow ModuleName
    mname [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    " has "
                  [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ Int -> [Char]
    forall a. Show a => a -> [Char]
    show (Telescope -> Int
    forall a. [a] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length (Telescope -> Int) -> Telescope -> Int
    forall a b. (a -> b) -> a -> b
    $ GeneralizeTelescope -> Telescope
    A.generalizeTel GeneralizeTelescope
    tel) [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    " parameters and "
                  [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ Int -> [Char]
    forall a. Show a => a -> [Char]
    show ([Declaration] -> Int
    forall a. [a] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length [Declaration]
    ds) [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    " declarations"
              [Char] -> Int -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "tc.decl" Int
    45 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    forall a b. (a -> b) -> a -> b
    $
                Declaration -> TCMT IO Doc
    forall a (m :: * -> *).
    (ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
    a -> m Doc
    prettyA (Declaration -> TCMT IO Doc) -> Declaration -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ Range
    -> Erased
    -> ModuleName
    -> GeneralizeTelescope
    -> [Declaration]
    -> Declaration
    A.Section Range
    info Erased
    erased ModuleName
    mname GeneralizeTelescope
    tel []
              [Declaration] -> (Declaration -> TCM ()) -> TCM ()
    forall (t :: * -> *) (m :: * -> *) a b.
    (Foldable t, Monad m) =>
    t a -> (a -> m b) -> m ()
    forM_ [Declaration]
    ds ((Declaration -> TCM ()) -> TCM ())
    -> (Declaration -> TCM ()) -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ \ Declaration
    d -> do
                [Char] -> Int -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "tc.decl" Int
    45 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ Declaration -> TCMT IO Doc
    forall a (m :: * -> *).
    (ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
    a -> m Doc
    prettyA Declaration
    d
            Declaration
    _ -> () -> TCM ()
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()