    {-# LANGUAGE NondecreasingIndentation #-}

    module Agda.TypeChecking.Rules.Decl where

    import Prelude hiding ( null )

    import Control.Monad
    import Control.Monad.Writer (tell)

    import Data.Either (partitionEithers)
    import qualified Data.Foldable as Fold
    import qualified Data.IntMap as IntMap
    import qualified Data.IntSet as IntSet
    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.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.Irrelevance
    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.Functor
    import Agda.Utils.Lens
    import Agda.Utils.Maybe
    import Agda.Utils.Monad
    import Agda.Utils.Null
    import Agda.Utils.Pretty (prettyShow)
    import Agda.Utils.Size
    import Agda.Utils.Update
    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
    _ ModuleName
    mname (A.GeneralizeTel Map QName Name
    _ Telescope
    tbinds) [Declaration]
    _) = do
      Maybe (TypeCheckAction, PostScopeState)
    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)
      [Char] -> Int -> [Char] -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> [Char] -> m ()
    reportSLn [Char]
    "cache.decl" Int
    10 ([Char] -> TCM ()) -> [Char] -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ [Char]
    "checkDeclCached: " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ Bool -> [Char]
    forall a. Show a => a -> [Char]
    show (Maybe (TypeCheckAction, PostScopeState) -> Bool
    forall a. Maybe a -> Bool
    isJust Maybe (TypeCheckAction, PostScopeState)
    e)
      case Maybe (TypeCheckAction, PostScopeState)
    e of
        Just (EnterSection ModuleName
    mname' Telescope
    tbinds', PostScopeState
    _)
          | 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 (m :: * -> *) a. Monad m => a -> m a
    return ()
        Maybe (TypeCheckAction, PostScopeState)
    _ -> TCM ()
    forall (m :: * -> *). (MonadDebug m, MonadTCState m) => m ()
    cleanCachedLog
      TypeCheckAction -> TCM ()
    forall (m :: * -> *).
    (MonadDebug m, MonadTCState m, ReadTCState m) =>
    TypeCheckAction -> m ()
    writeToCurrentLog (TypeCheckAction -> TCM ()) -> TypeCheckAction -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ ModuleName -> Telescope -> TypeCheckAction
    EnterSection ModuleName
    mname Telescope
    tbinds
      Declaration -> TCM ()
    checkDecl Declaration
    d
      TCMT IO (Maybe (TypeCheckAction, PostScopeState))
    forall (m :: * -> *).
    (MonadDebug m, MonadTCState m, ReadTCState m) =>
    m (Maybe (TypeCheckAction, PostScopeState))
    readFromCachedLog TCMT IO (Maybe (TypeCheckAction, PostScopeState))
    -> (Maybe (TypeCheckAction, PostScopeState) -> TCM ()) -> TCM ()
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \case
        Just (LeaveSection ModuleName
    mname', PostScopeState
    _) | ModuleName
    mname ModuleName -> ModuleName -> Bool
    forall a. Eq a => a -> a -> Bool
    == ModuleName
    mname' -> () -> TCM ()
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
        Maybe (TypeCheckAction, PostScopeState)
    _ -> TCM ()
    forall (m :: * -> *). (MonadDebug m, MonadTCState m) => m ()
    cleanCachedLog
      TypeCheckAction -> TCM ()
    forall (m :: * -> *).
    (MonadDebug m, MonadTCState m, ReadTCState m) =>
    TypeCheckAction -> m ()
    writeToCurrentLog (TypeCheckAction -> TCM ()) -> TypeCheckAction -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ ModuleName -> TypeCheckAction
    LeaveSection ModuleName
    mname

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

        [Char] -> Int -> [Char] -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> [Char] -> m ()
    reportSLn [Char]
    "cache.decl" Int
    10 ([Char] -> TCM ()) -> [Char] -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ [Char]
    "checkDeclCached: " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ Bool -> [Char]
    forall a. Show a => a -> [Char]
    show (Maybe (TypeCheckAction, PostScopeState) -> Bool
    forall a. Maybe a -> Bool
    isJust Maybe (TypeCheckAction, PostScopeState)
    e)

        case Maybe (TypeCheckAction, PostScopeState)
    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
        TypeCheckAction -> TCM ()
    forall (m :: * -> *).
    (MonadDebug m, MonadTCState m, ReadTCState m) =>
    TypeCheckAction -> m ()
    writeToCurrentLog (TypeCheckAction -> TCM ()) -> TypeCheckAction -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ Declaration -> TypeCheckAction
    Decl Declaration
    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 (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 (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 (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m 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.

        (Maybe (TCM ())
    finalChecks, MetaStore
    metas) <- TCMT IO (Maybe (TCM ())) -> TCMT IO (Maybe (TCM ()), MetaStore)
    forall (m :: * -> *) a. ReadTCState m => m a -> m (a, MetaStore)
    metasCreatedBy (TCMT IO (Maybe (TCM ())) -> TCMT IO (Maybe (TCM ()), MetaStore))
    -> TCMT IO (Maybe (TCM ())) -> TCMT IO (Maybe (TCM ()), MetaStore)
    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 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
    $ ModuleName -> GeneralizeTelescope -> [Declaration] -> TCM ()
    checkSection ModuleName
    x GeneralizeTelescope
    tel [Declaration]
    ds
          A.Apply ModuleInfo
    i ModuleName
    x ModuleApplication
    modapp ScopeCopyInfo
    ci ImportDirective
    _adir -> 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
    -> ModuleName -> ModuleApplication -> ScopeCopyInfo -> TCM ()
    checkSectionApplication ModuleInfo
    i ModuleName
    x ModuleApplication
    modapp ScopeCopyInfo
    ci
          A.Import ModuleInfo
    i ModuleName
    x ImportDirective
    _adir       -> 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
    $ ModuleInfo -> ModuleName -> TCM ()
    checkImport ModuleInfo
    i ModuleName
    x
          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 (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 Delayed
    delayed [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) =>
    QName -> i -> m a -> m a
    check QName
    x DefInfo
    i (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ Delayed -> DefInfo -> QName -> [Clause] -> TCM ()
    checkFunDef Delayed
    delayed 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) =>
    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) =>
    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
                                        MutualId
    blockId <- QName -> TCM MutualId
    mutualBlockOf QName
    x

                                        -- Andreas, 2016-10-01 testing whether
                                        -- envMutualBlock is set correctly.
                                        -- Apparently not.
                                        [Char] -> Int -> TCM () -> TCM ()
    forall (m :: * -> *). MonadDebug m => [Char] -> Int -> m () -> m ()
    verboseS [Char]
    "tc.decl.mutual" Int
    70 (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ do
                                          Maybe MutualId
    current <- (TCEnv -> Maybe MutualId) -> TCMT IO (Maybe MutualId)
    forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
    asksTC TCEnv -> Maybe MutualId
    envMutualBlock
                                          Bool -> TCM () -> TCM ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    unless (MutualId -> Maybe MutualId
    forall a. a -> Maybe a
    Just MutualId
    blockId Maybe MutualId -> Maybe MutualId -> Bool
    forall a. Eq a => a -> a -> Bool
    == Maybe MutualId
    current) (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ do
                                            [Char] -> Int -> [[Char]] -> TCM ()
    forall a (m :: * -> *).
    (ReportS a, MonadDebug m) =>
    [Char] -> Int -> a -> m ()
    reportS [Char]
    "" Int
    0
                                              [ [Char]
    "mutual block id discrepancy for " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ QName -> [Char]
    forall a. Pretty a => a -> [Char]
    prettyShow QName
    x
                                              , [Char]
    "  current    mut. bl. = " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ Maybe MutualId -> [Char]
    forall a. Show a => a -> [Char]
    show Maybe MutualId
    current
                                              , [Char]
    "  calculated mut. bl. = " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ MutualId -> [Char]
    forall a. Show a => a -> [Char]
    show MutualId
    blockId
                                              ]

                                        (MutualId, Set QName) -> TCMT IO (MutualId, Set QName)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (MutualId
    blockId, QName -> Set QName
    forall a. a -> Set a
    Set.singleton QName
    x)
          A.DataSig DefInfo
    i 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 -> QName -> GeneralizeTelescope -> Expr -> TCM ()
    checkSig KindOfName
    DataName DefInfo
    i QName
    x GeneralizeTelescope
    ps Expr
    t
          A.RecSig DefInfo
    i 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 -> QName -> GeneralizeTelescope -> Expr -> TCM ()
    checkSig KindOfName
    RecName DefInfo
    i 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{}                 -> 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 (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 (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) =>
    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) =>
    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

        TCMT IO (Maybe MutualId) -> TCM () -> TCM ()
    forall (m :: * -> *) a. Monad m => m (Maybe a) -> m () -> m ()
    whenNothingM ((TCEnv -> Maybe MutualId) -> TCMT IO (Maybe MutualId)
    forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
    asksTC TCEnv -> Maybe MutualId
    envMutualBlock) (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ do

          -- Syntax highlighting.
          HighlightModuleContents -> Declaration -> TCM ()
    highlight_ HighlightModuleContents
    DontHightlightModuleContents Declaration
    d

          -- Defaulting of levels (only when --cumulativity)
          TCMT IO Bool -> TCM () -> TCM ()
    forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
    whenM (PragmaOptions -> Bool
    optCumulativity (PragmaOptions -> Bool) -> TCMT IO PragmaOptions -> TCMT IO Bool
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> TCMT IO PragmaOptions
    forall (m :: * -> *). HasOptions m => m PragmaOptions
    pragmaOptions) (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ MetaStore -> TCM ()
    forall (m :: * -> *).
    (PureTCM m, MonadMetaSolver m) =>
    MetaStore -> m ()
    defaultLevelsToZero MetaStore
    metas

          -- Post-typing checks.
          Maybe (TCM ()) -> (TCM () -> TCM ()) -> TCM ()
    forall (m :: * -> *) a. Monad m => Maybe a -> (a -> m ()) -> m ()
    whenJust Maybe (TCM ())
    finalChecks ((TCM () -> TCM ()) -> TCM ()) -> (TCM () -> TCM ()) -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ \ 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."
            TCM ()
    wakeupConstraints_   -- solve emptiness and instance constraints
            Bool
    checkingWhere <- (TCEnv -> Bool) -> TCMT IO Bool
    forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
    asksTC TCEnv -> Bool
    envCheckingWhere
            DefaultToInfty -> TCM ()
    solveSizeConstraints (DefaultToInfty -> TCM ()) -> DefaultToInfty -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ if Bool
    checkingWhere then DefaultToInfty
    DontDefaultToInfty else DefaultToInfty
    DefaultToInfty
            TCM ()
    wakeupConstraints_   -- Size solver might have unblocked some constraints
            case Declaration
    d of
                A.Generalize{} -> () -> TCM ()
    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 metas."
                  TCMT IO IntSet -> TCM ()
    forall (f :: * -> *) a. Functor f => f a -> f ()
    void (TCMT IO IntSet -> TCM ()) -> TCMT IO IntSet -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ MetaStore -> TCMT IO IntSet
    freezeMetas MetaStore
    metas

            TCM ()
    theMutualChecks

        where

        -- check record or data type signature
        checkSig :: KindOfName
    -> DefInfo -> QName -> GeneralizeTelescope -> Expr -> TCM ()
    checkSig KindOfName
    kind DefInfo
    i 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 [Occurrence]
    -> QName
    -> Expr
    -> Declaration
    A.Axiom KindOfName
    kind DefInfo
    i ArgInfo
    defaultArgInfo Maybe [Occurrence]
    forall a. Maybe a
    Nothing QName
    x Expr
    t

        -- 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 )
              => QName -> i -> m a -> m a
        check :: forall (m :: * -> *) i a.
    (MonadTCEnv m, MonadPretty m, MonadDebug m, MonadBench m,
     BenchPhase m ~ Phase, AnyIsAbstract 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
    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
          a
    r <- i -> m a -> m a
    forall (m :: * -> *) i a.
    (MonadTCEnv m, AnyIsAbstract i) =>
    i -> m a -> m a
    checkMaybeAbstractly i
    i m a
    m
          [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
    "Checked" 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
    prettyTCM QName
    x) TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall a. Semigroup a => a -> a -> a
    <> TCMT IO Doc
    "."
          a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return a
    r

        -- Switch to AbstractMode if any of the i is AbstractDef.
        checkMaybeAbstractly :: forall m i a . ( MonadTCEnv m , AnyIsAbstract i )
                             => i -> m a -> m a
        checkMaybeAbstractly :: forall (m :: * -> *) i a.
    (MonadTCEnv m, AnyIsAbstract i) =>
    i -> m a -> m a
    checkMaybeAbstractly = (TCEnv -> TCEnv) -> m a -> m a
    forall (m :: * -> *) a.
    MonadTCEnv m =>
    (TCEnv -> TCEnv) -> m a -> m a
    localTC ((TCEnv -> TCEnv) -> m a -> m a)
    -> (i -> TCEnv -> TCEnv) -> i -> m a -> m a
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Lens' IsAbstract TCEnv -> LensSet IsAbstract TCEnv
    forall i o. Lens' i o -> LensSet i o
    set forall a. LensIsAbstract a => Lens' IsAbstract a
    Lens' IsAbstract TCEnv
    lensIsAbstract LensSet IsAbstract TCEnv
    -> (i -> IsAbstract) -> i -> TCEnv -> TCEnv
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . i -> IsAbstract
    forall a. AnyIsAbstract a => a -> IsAbstract
    anyIsAbstract

    -- 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 (m :: * -> *) a.
    MonadTCEnv m =>
    (TCEnv -> TCEnv) -> m a -> m a
    localTC (\ TCEnv
    e -> TCEnv
    e { envMutualBlock :: Maybe MutualId
    envMutualBlock = MutualId -> Maybe MutualId
    forall a. a -> Maybe a
    Just MutualId
    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
      ([QName]
    rs, [(QName, CompiledClauses)]
    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)
    mapM QName -> TCMT IO (Maybe (Either QName (QName, CompiledClauses)))
    forall {m :: * -> *}.
    HasConstInfo m =>
    QName -> m (Maybe (Either QName (QName, CompiledClauses)))
    classify [QName]
    qs
      Bool -> TCM () -> TCM ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    unless ([QName] -> Bool
    forall a. Null a => a -> Bool
    null [QName]
    rs) (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ [(QName, CompiledClauses)]
    -> ((QName, CompiledClauses) -> TCM ()) -> TCM ()
    forall (t :: * -> *) (m :: * -> *) a b.
    (Foldable t, Monad m) =>
    t a -> (a -> m b) -> m ()
    forM_ [(QName, CompiledClauses)]
    qccs (((QName, CompiledClauses) -> TCM ()) -> TCM ())
    -> ((QName, CompiledClauses) -> TCM ()) -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ \(QName
    q,CompiledClauses
    cc) -> do
        (CompiledClauses
    cc, Bool
    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
    $ CompiledClauses -> ChangeT (TCMT IO) CompiledClauses
    forall (m :: * -> *).
    (HasConstInfo m, MonadChange m) =>
    CompiledClauses -> m CompiledClauses
    translateCompiledClauses CompiledClauses
    cc
        (Signature -> Signature) -> TCM ()
    forall (m :: * -> *).
    MonadTCState m =>
    (Signature -> Signature) -> m ()
    modifySignature ((Signature -> Signature) -> TCM ())
    -> (Signature -> Signature) -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ QName -> (Definition -> Definition) -> Signature -> Signature
    updateDefinition QName
    q
          ((Definition -> Definition) -> Signature -> Signature)
    -> (Definition -> Definition) -> Signature -> Signature
    forall a b. (a -> b) -> a -> b
    $ (Defn -> Defn) -> Definition -> Definition
    updateTheDef ((Maybe CompiledClauses -> Maybe CompiledClauses) -> Defn -> Defn
    updateCompiledClauses ((Maybe CompiledClauses -> Maybe CompiledClauses) -> Defn -> Defn)
    -> (Maybe CompiledClauses -> Maybe CompiledClauses) -> Defn -> Defn
    forall a b. (a -> b) -> a -> b
    $ Maybe CompiledClauses
    -> Maybe CompiledClauses -> Maybe CompiledClauses
    forall a b. a -> b -> a
    const (Maybe CompiledClauses
     -> Maybe CompiledClauses -> Maybe CompiledClauses)
    -> Maybe CompiledClauses
    -> Maybe CompiledClauses
    -> Maybe CompiledClauses
    forall a b. (a -> b) -> a -> b
    $ CompiledClauses -> Maybe CompiledClauses
    forall a. a -> Maybe a
    Just CompiledClauses
    cc)
          (Definition -> Definition)
    -> (Definition -> Definition) -> Definition -> Definition
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Bool -> Bool) -> Definition -> Definition
    updateDefCopatternLHS (Bool -> Bool -> Bool
    || Bool
    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 (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 -> Maybe Projection
    funProjection = Maybe Projection
    Nothing
                -- 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 (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 (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
    prettyTCM [QName]
    xs)
      Maybe (TCM ())
    forall a. Maybe a
    Nothing Maybe (TCM ()) -> TCMT IO [QName] -> TCMT IO (Maybe (TCM ()))
    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
    prettyTCM [QName]
    xs)
      () () -> TCMT IO [QName] -> TCM ()
    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
      Term
    tcm   <- TCMT IO Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primAgdaTCM
      Term
    unit  <- TCMT IO Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primUnit
      Term
    lzero <- TCMT IO Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primLevelZero
      let vArg :: a -> Arg a
    vArg = a -> Arg a
    forall a. a -> Arg a
    defaultArg
          hArg :: a -> Arg a
    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
      Term
    m    <- Quantity -> TCMT IO Term -> TCMT IO Term
    forall (tcm :: * -> *) q a.
    (MonadTCEnv tcm, LensQuantity q) =>
    q -> tcm a -> tcm a
    applyQuantityToContext Quantity
    zeroQuantity (TCMT IO Term -> TCMT IO Term) -> TCMT IO Term -> TCMT IO Term
    forall a b. (a -> b) -> a -> b
    $
                Expr -> Type -> TCMT IO Term
    checkExpr Expr
    e (Type -> TCMT IO Term) -> Type -> TCMT IO Term
    forall a b. (a -> b) -> a -> b
    $ Sort -> Term -> Type
    forall t a. Sort' t -> a -> Type'' t a
    El (Integer -> Sort
    mkType Integer
    0) (Term -> Type) -> Term -> Type
    forall a b. (a -> b) -> a -> b
    $ Term -> [Arg Term] -> Term
    forall t. Apply t => t -> [Arg Term] -> t
    apply Term
    tcm [Term -> Arg Term
    forall a. a -> Arg a
    hArg Term
    lzero, Term -> Arg Term
    forall a. a -> Arg a
    vArg Term
    unit]
      Either UnquoteError (Term, [QName])
    res  <- UnquoteM Term -> TCM (Either UnquoteError (Term, [QName]))
    forall a. UnquoteM a -> TCM (Either UnquoteError (a, [QName]))
    runUnquoteM (UnquoteM Term -> TCM (Either UnquoteError (Term, [QName])))
    -> UnquoteM Term -> TCM (Either UnquoteError (Term, [QName]))
    forall a b. (a -> b) -> a -> b
    $ [QName]
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         ()
    forall w (m :: * -> *). MonadWriter w m => w -> m ()
    tell [QName]
    xs ReaderT
      Context
      (StateT
         UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
      ()
    -> UnquoteM Term -> UnquoteM Term
    forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
    >> Term -> UnquoteM Term
    evalTCM Term
    m
      case Either UnquoteError (Term, [QName])
    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 (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
      Type
    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
      Type
    t' <- Type -> TCMT IO Type
    forall a (m :: * -> *).
    (InstantiateFull a, MonadReduce m) =>
    a -> m a
    instantiateFull Type
    t
      (Signature -> Signature) -> TCM ()
    forall (m :: * -> *).
    MonadTCState m =>
    (Signature -> Signature) -> m ()
    modifySignature ((Signature -> Signature) -> TCM ())
    -> (Signature -> Signature) -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ QName -> (Definition -> Definition) -> Signature -> Signature
    updateDefinition QName
    q ((Definition -> Definition) -> Signature -> Signature)
    -> (Definition -> Definition) -> Signature -> Signature
    forall a b. (a -> b) -> a -> b
    $ (Type -> Type) -> Definition -> Definition
    updateDefType ((Type -> Type) -> Definition -> Definition)
    -> (Type -> Type) -> Definition -> Definition
    forall a b. (a -> b) -> a -> b
    $ Type -> Type -> Type
    forall a b. a -> b -> a
    const Type
    t'
      [Char] -> Int -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "tc.decl.inst" Int
    30 (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
    "  t  = " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Type -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Type
    t
        , TCMT IO Doc
    "  t' = " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Type -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Type
    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
    /= :: HighlightModuleContents -> HighlightModuleContents -> Bool
    $c/= :: HighlightModuleContents -> HighlightModuleContents -> Bool
    == :: HighlightModuleContents -> HighlightModuleContents -> Bool
    $c== :: 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
      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 (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.Generalize{}           -> Declaration -> TCM ()
    highlight Declaration
    d
        A.UnquoteDecl{}          -> Declaration -> TCM ()
    highlight Declaration
    d
        A.UnquoteDef{}           -> Declaration -> TCM ()
    highlight Declaration
    d
        A.Section Range
    i ModuleName
    x GeneralizeTelescope
    tel [Declaration]
    ds     -> do
          Declaration -> TCM ()
    highlight (Range
    -> ModuleName
    -> GeneralizeTelescope
    -> [Declaration]
    -> Declaration
    A.Section Range
    i ModuleName
    x GeneralizeTelescope
    tel [])
          Bool -> TCM () -> TCM ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    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
    A.noDataDefParams 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 Result -> (Result -> TCM ()) -> TCM ()
    forall (m :: * -> *) a.
    (Monad m, Null a) =>
    m a -> (a -> m ()) -> m ()
    unlessNullM (Declaration -> TCMT IO Result
    termDecl Declaration
    d) ((Result -> TCM ()) -> TCM ()) -> (Result -> TCM ()) -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ \ Result
    termErrs -> do
        Warning -> TCM ()
    forall (m :: * -> *).
    (HasCallStack, MonadWarning m) =>
    Warning -> m ()
    warning (Warning -> TCM ()) -> Warning -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ Result -> Warning
    TerminationIssue Result
    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 that all coinductive records are actually recursive.
    --   (Otherwise, one can implement invalid recursion schemes just like
    --   for the old coinduction.)
    checkCoinductiveRecords :: [A.Declaration] -> TCM ()
    checkCoinductiveRecords :: [Declaration] -> TCM ()
    checkCoinductiveRecords [Declaration]
    ds = [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
    $ \case
      A.RecDef DefInfo
    _ QName
    q UniverseCheck
    _ RecordDirectives
    dir DataDefParams
    _ Expr
    _ [Declaration]
    _
        | Just (Ranged Range
    r Induction
    CoInductive) <- RecordDirectives -> Maybe (Ranged Induction)
    forall a. RecordDirectives' a -> Maybe (Ranged Induction)
    recInductive RecordDirectives
    dir -> Range -> TCM () -> TCM ()
    forall (m :: * -> *) x a.
    (MonadTrace m, HasRange x) =>
    x -> m a -> m a
    setCurrentRange Range
    r (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ do
        TCMT IO Bool -> TCM () -> TCM ()
    forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
    unlessM (QName -> TCMT IO Bool
    isRecursiveRecord QName
    q) (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ 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
    GenericError ([Char] -> TypeError) -> [Char] -> TypeError
    forall a b. (a -> b) -> a -> b
    $
          [Char]
    "Only recursive records can be coinductive"
      Declaration
    _ -> () -> TCM ()
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()

    -- | 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 -> Maybe Projection
    funProjection = Maybe 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

                FunctionInverse
    inv <- QName -> [Clause] -> TCM FunctionInverse
    checkInjectivity QName
    q [Clause]
    cs
                (Signature -> Signature) -> TCM ()
    forall (m :: * -> *).
    MonadTCState m =>
    (Signature -> Signature) -> m ()
    modifySignature ((Signature -> Signature) -> TCM ())
    -> (Signature -> Signature) -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ QName -> (Definition -> Definition) -> Signature -> Signature
    updateDefinition QName
    q ((Definition -> Definition) -> Signature -> Signature)
    -> (Definition -> Definition) -> Signature -> Signature
    forall a b. (a -> b) -> a -> b
    $ (Defn -> Defn) -> Definition -> Definition
    updateTheDef ((Defn -> Defn) -> Definition -> Definition)
    -> (Defn -> Defn) -> Definition -> Definition
    forall a b. (a -> b) -> a -> b
    $ Defn -> Defn -> Defn
    forall a b. a -> b -> a
    const (Defn -> Defn -> Defn) -> Defn -> Defn -> Defn
    forall a b. (a -> b) -> a -> b
    $
                  Defn
    d { funInv :: FunctionInverse
    funInv = FunctionInverse
    inv }

          Defn
    _ -> do
            AbstractMode
    abstr <- (TCEnv -> AbstractMode) -> TCMT IO AbstractMode
    forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
    asksTC TCEnv -> AbstractMode
    envAbstractMode
            [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
    $
              [Char]
    "we are in " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ AbstractMode -> [Char]
    forall a. Show a => a -> [Char]
    show AbstractMode
    abstr [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    " and " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++
                 QName -> [Char]
    forall a. Pretty a => a -> [Char]
    prettyShow QName
    q [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    " 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
              Definition
    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 Definition -> Defn
    theDef Definition
    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 :: forall t. DefInfo' t -> Access
    defAccess :: Access
    defAccess, IsAbstract
    defAbstract :: forall t. DefInfo' t -> IsAbstract
    defAbstract :: IsAbstract
    defAbstract} TCM a
    m = do
      if IsAbstract
    defAbstract IsAbstract -> IsAbstract -> Bool
    forall a. Eq a => a -> a -> Bool
    /= IsAbstract
    AbstractDef then TCM a
    m else do
        (a
    a, MetaStore
    ms) <- TCM a -> TCMT IO (a, MetaStore)
    forall (m :: * -> *) a. ReadTCState m => m a -> m (a, MetaStore)
    metasCreatedBy TCM a
    m
        [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."
        TCM ()
    wakeupConstraints_   -- solve emptiness and instance constraints
        IntSet
    xs <- MetaStore -> TCMT IO IntSet
    freezeMetas MetaStore
    ms
        [Char] -> Int -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "tc.decl.ax" 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
    "Abstract type signature produced new metas: " 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 ((Int -> TCMT IO Doc) -> [Int] -> [TCMT IO Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map Int -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM ([Int] -> [TCMT IO Doc]) -> [Int] -> [TCMT IO Doc]
    forall a b. (a -> b) -> a -> b
    $ MetaStore -> [Int]
    forall a. IntMap a -> [Int]
    IntMap.keys MetaStore
    ms)
          , TCMT IO Doc
    "We froze the following ones of these:       " 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 ((Int -> TCMT IO Doc) -> [Int] -> [TCMT IO Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map Int -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM ([Int] -> [TCMT IO Doc]) -> [Int] -> [TCMT IO Doc]
    forall a b. (a -> b) -> a -> b
    $ IntSet -> [Int]
    IntSet.toList IntSet
    xs)
          ]
        a -> TCM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return a
    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
    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
    prettyTCM Expr
    e
          ]

        -- Check the signature and collect the created metas.
        ([Maybe QName]
    telNames, Type
    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' DoGeneralize TCEnv
    -> (DoGeneralize -> DoGeneralize) -> TCMT IO Type -> TCMT IO Type
    forall (m :: * -> *) a b.
    MonadTCEnv m =>
    Lens' a TCEnv -> (a -> a) -> m b -> m b
    locallyTC Lens' DoGeneralize TCEnv
    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 :: Int
    n = [Maybe QName] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length [Maybe QName]
    telNames

        [Char] -> Int -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "tc.decl.gen" Int
    10 (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
    "checked 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
    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
    $ Type -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Type
    tGen
          ]

        Language
    lang <- TCMT IO Language
    forall (m :: * -> *). HasOptions m => m Language
    getLanguage
        QName -> Definition -> TCM ()
    addConstant QName
    x (Definition -> TCM ()) -> Definition -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ (ArgInfo -> QName -> Type -> Language -> Defn -> Definition
    defaultDefn ArgInfo
    info QName
    x Type
    tGen Language
    lang Defn
    GeneralizableVar)
                        { defArgGeneralizable :: NumGeneralizableArgs
    defArgGeneralizable = Int -> NumGeneralizableArgs
    SomeGeneralizableArgs Int
    n }

    -- | Type check an axiom.
    checkAxiom :: KindOfName -> A.DefInfo -> ArgInfo ->
                  Maybe [Occurrence] -> QName -> A.Expr -> TCM ()
    checkAxiom :: KindOfName
    -> DefInfo
    -> ArgInfo
    -> Maybe [Occurrence]
    -> QName
    -> Expr
    -> TCM ()
    checkAxiom = Maybe GeneralizeTelescope
    -> KindOfName
    -> DefInfo
    -> ArgInfo
    -> Maybe [Occurrence]
    -> 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 [Occurrence] -> QName -> A.Expr -> TCM ()
    checkAxiom' :: Maybe GeneralizeTelescope
    -> KindOfName
    -> DefInfo
    -> ArgInfo
    -> Maybe [Occurrence]
    -> QName
    -> Expr
    -> TCM ()
    checkAxiom' Maybe GeneralizeTelescope
    gentel KindOfName
    kind DefInfo
    i ArgInfo
    info0 Maybe [Occurrence]
    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.

      -- Andreas, 2012-04-18  if we are in irrelevant context, axioms are irrelevant
      -- even if not declared as such (Issue 610).
      -- Andreas, 2019-06-17  also for erasure (issue #3855).
      Relevance
    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
    <$> (TCEnv -> Relevance) -> TCMT IO Relevance
    forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
    asksTC TCEnv -> Relevance
    forall a. LensRelevance a => a -> Relevance
    getRelevance
      Quantity
    q   <- (TCEnv -> Quantity) -> TCMT IO Quantity
    forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
    asksTC TCEnv -> Quantity
    forall a. LensQuantity a => a -> Quantity
    getQuantity TCMT IO Quantity -> (Quantity -> Quantity) -> TCMT IO Quantity
    forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
    <&> \case
        q :: Quantity
    q@Quantity0{} -> Quantity
    q
        Quantity
    _ -> ArgInfo -> Quantity
    forall a. LensQuantity a => a -> Quantity
    getQuantity ArgInfo
    info0

      -- Andrea, 2019-07-16 Cohesion is purely based on left-division, it
      -- does not take envModality into account.
      let c :: Cohesion
    c = ArgInfo -> Cohesion
    forall a. LensCohesion a => a -> Cohesion
    getCohesion ArgInfo
    info0
      let mod :: Modality
    mod  = Relevance -> Quantity -> Cohesion -> Modality
    Modality Relevance
    rel Quantity
    q Cohesion
    c
      let info :: ArgInfo
    info = Modality -> ArgInfo -> ArgInfo
    forall a. LensModality a => Modality -> a -> a
    setModality Modality
    mod ArgInfo
    info0
      Cohesion -> TCM () -> TCM ()
    forall (tcm :: * -> *) m a.
    (MonadTCEnv tcm, LensCohesion m) =>
    m -> tcm a -> tcm a
    applyCohesionToContext Cohesion
    c (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.ax" 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
        [ [Char] -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => [Char] -> m Doc
    text ([Char] -> TCMT IO Doc) -> [Char] -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ [Char]
    "checking type signature"
        , 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
    $ (Modality -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Modality
    mod TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall a. Semigroup a => a -> a -> a
    <> QName -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> 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
    ":" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Expr -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Expr
    e
        , 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
    $ Maybe GeneralizeTelescope
    -> TCMT IO Doc
    -> (GeneralizeTelescope -> TCMT IO Doc)
    -> TCMT IO Doc
    forall a b. Maybe a -> b -> (a -> b) -> b
    caseMaybe Maybe GeneralizeTelescope
    gentel TCMT IO Doc
    "(no gentel)" ((GeneralizeTelescope -> TCMT IO Doc) -> TCMT IO Doc)
    -> (GeneralizeTelescope -> TCMT IO Doc) -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ \ GeneralizeTelescope
    _ -> TCMT IO Doc
    "(has gentel)"
        ]

      ([Maybe Name]
    genParams, Int
    npars, Type
    t) <- TCMT IO ([Maybe Name], Int, Type)
    -> TCMT IO ([Maybe Name], Int, Type)
    forall (m :: * -> *) a.
    (MonadTCEnv m, HasOptions m, MonadDebug m) =>
    m a -> m a
    workOnTypes (TCMT IO ([Maybe Name], Int, Type)
     -> TCMT IO ([Maybe Name], Int, Type))
    -> TCMT IO ([Maybe Name], Int, Type)
    -> TCMT IO ([Maybe Name], Int, Type)
    forall a b. (a -> b) -> a -> b
    $ case Maybe GeneralizeTelescope
    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 ->
              GeneralizeTelescope
    -> ([Maybe Name]
        -> Tele (Dom Type) -> TCMT IO ([Maybe Name], Int, Type))
    -> TCMT IO ([Maybe Name], Int, Type)
    forall a.
    GeneralizeTelescope
    -> ([Maybe Name] -> Tele (Dom Type) -> TCM a) -> TCM a
    checkGeneralizeTelescope 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
                Type
    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
                ([Maybe Name], Int, Type) -> TCMT IO ([Maybe Name], Int, Type)
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([Maybe Name]
    genParams, Tele (Dom Type) -> Int
    forall a. Sized a => a -> Int
    size Tele (Dom Type)
    ptel, Tele (Dom Type) -> Type -> Type
    forall t. Abstract t => Tele (Dom Type) -> t -> t
    abstract Tele (Dom Type)
    ptel Type
    t)

      [Char] -> Int -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "tc.decl.ax" Int
    10 (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
        [ [Char] -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => [Char] -> m Doc
    text ([Char] -> TCMT IO Doc) -> [Char] -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ [Char]
    "checked type signature"
        , 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
    $ (Modality -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Modality
    mod TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall a. Semigroup a => a -> a -> a
    <> QName -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> 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
    ":" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Type -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Type
    t
        , 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
    $ TCMT IO Doc
    "of sort " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Sort -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM (Type -> Sort
    forall a. LensSort a => a -> Sort
    getSort Type
    t)
        ]

      Bool -> TCM () -> TCM ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    unless ([Maybe Name] -> Bool
    forall a. Null a => a -> Bool
    null [Maybe Name]
    genParams) (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $
        [Char] -> Int -> [Char] -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> [Char] -> m ()
    reportSLn [Char]
    "tc.decl.ax" Int
    40 ([Char] -> TCM ()) -> [Char] -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ [Char]
    "  generalized params: " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ [Maybe Name] -> [Char]
    forall a. Show a => a -> [Char]
    show [Maybe Name]
    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!
      Bool -> TCM () -> TCM ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    when (KindOfName
    kind KindOfName -> KindOfName -> Bool
    forall a. Eq a => a -> a -> Bool
    == KindOfName
    AxiomName) (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ do
        TCMT IO Bool -> TCM () -> TCM ()
    forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
    whenM ((Sort -> Sort -> Bool
    forall a. Eq a => a -> a -> Bool
    == Sort
    forall t. Sort' t
    SizeUniv) (Sort -> Bool) -> TCMT IO Sort -> TCMT IO Bool
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> do Sort -> TCMT IO Sort
    forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
    reduce (Sort -> TCMT IO Sort) -> Sort -> TCMT IO Sort
    forall a b. (a -> b) -> a -> b
    $ Type -> Sort
    forall a. LensSort a => a -> Sort
    getSort Type
    t) (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ do
          TCMT IO Bool -> TCM () -> TCM ()
    forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
    whenM ((Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    > Int
    0) (Int -> Bool) -> TCMT IO Int -> TCMT IO Bool
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> TCMT IO Int
    forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Int
    getContextSize) (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ do
            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
    GenericError ([Char] -> TypeError) -> [Char] -> TypeError
    forall a b. (a -> b) -> a -> b
    $ [Char]
    "We don't like postulated sizes in parametrized modules."

      -- Ensure that polarity pragmas do not contain too many occurrences.
      ([Occurrence]
    occs, [Polarity]
    pols) <- case Maybe [Occurrence]
    mp of
        Maybe [Occurrence]
    Nothing   -> ([Occurrence], [Polarity]) -> TCMT IO ([Occurrence], [Polarity])
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([], [])
        Just [Occurrence]
    occs -> do
          TelV Tele (Dom Type)
    tel Type
    _ <- Type -> TCMT IO (TelV Type)
    forall (m :: * -> *).
    (MonadReduce m, MonadAddContext m) =>
    Type -> m (TelV Type)
    telView Type
    t
          let n :: Int
    n = [Dom ([Char], Type)] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length (Tele (Dom Type) -> [Dom ([Char], Type)]
    forall t. Tele (Dom t) -> [Dom ([Char], t)]
    telToList Tele (Dom Type)
    tel)
          Bool -> TCM () -> TCM ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    when (Int
    n Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    < [Occurrence] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length [Occurrence]
    occs) (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $
            TypeError -> TCM ()
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    TypeError -> m a
    typeError (TypeError -> TCM ()) -> TypeError -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ QName -> Int -> TypeError
    TooManyPolarities QName
    x Int
    n
          let pols :: [Polarity]
    pols = (Occurrence -> Polarity) -> [Occurrence] -> [Polarity]
    forall a b. (a -> b) -> [a] -> [b]
    map Occurrence -> Polarity
    polFromOcc [Occurrence]
    occs
          [Char] -> Int -> [Char] -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> [Char] -> m ()
    reportSLn [Char]
    "tc.polarity.pragma" Int
    10 ([Char] -> TCM ()) -> [Char] -> TCM ()
    forall a b. (a -> b) -> a -> b
    $
            [Char]
    "Setting occurrences and polarity for " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ QName -> [Char]
    forall a. Pretty a => a -> [Char]
    prettyShow QName
    x [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    ":\n  " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++
            [Occurrence] -> [Char]
    forall a. Pretty a => a -> [Char]
    prettyShow [Occurrence]
    occs [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    "\n  " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ [Polarity] -> [Char]
    forall a. Pretty a => a -> [Char]
    prettyShow [Polarity]
    pols
          ([Occurrence], [Polarity]) -> TCMT IO ([Occurrence], [Polarity])
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([Occurrence]
    occs, [Polarity]
    pols)

      -- Set blocking tag to MissingClauses if we still expect clauses
      let blk :: Blocked' Term ()
    blk = case KindOfName
    kind of
            KindOfName
    FunName   -> NotBlocked' Term -> () -> Blocked' Term ()
    forall t a. NotBlocked' t -> a -> Blocked' t a
    NotBlocked NotBlocked' Term
    forall t. NotBlocked' t
    MissingClauses   ()
            KindOfName
    MacroName -> NotBlocked' Term -> () -> Blocked' Term ()
    forall t a. NotBlocked' t -> a -> Blocked' t a
    NotBlocked NotBlocked' Term
    forall t. NotBlocked' t
    MissingClauses   ()
            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

      Language
    lang <- TCMT IO Language
    forall (m :: * -> *). HasOptions m => m Language
    getLanguage
      let defn :: Definition
    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
    emptyFunction{ funAbstr :: IsAbstract
    funAbstr = DefInfo -> IsAbstract
    forall t. DefInfo' t -> IsAbstract
    Info.defAbstract DefInfo
    i }
              KindOfName
    MacroName -> Lens' Bool Defn -> LensSet Bool Defn
    forall i o. Lens' i o -> LensSet i o
    set Lens' Bool Defn
    funMacro Bool
    True Defn
    emptyFunction{ funAbstr :: IsAbstract
    funAbstr = DefInfo -> IsAbstract
    forall t. DefInfo' t -> IsAbstract
    Info.defAbstract DefInfo
    i }
              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__

      QName -> Definition -> TCM ()
    addConstant QName
    x (Definition -> TCM ()) -> TCMT IO Definition -> TCM ()
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< do
        Definition -> TCMT IO Definition
    useTerPragma (Definition -> TCMT IO Definition)
    -> Definition -> TCMT IO Definition
    forall a b. (a -> b) -> a -> b
    $ Definition
    defn
            { defArgOccurrences :: [Occurrence]
    defArgOccurrences    = [Occurrence]
    occs
            , defPolarity :: [Polarity]
    defPolarity          = [Polarity]
    pols
            , defGeneralizedParams :: [Maybe Name]
    defGeneralizedParams = [Maybe Name]
    genParams
            , defBlocked :: Blocked' Term ()
    defBlocked           = Blocked' Term ()
    blk
            }

      -- Add the definition to the instance table, if needed
      case DefInfo -> IsInstance
    forall t. DefInfo' t -> IsInstance
    Info.defInstance DefInfo
    i of
        InstanceDef Range
    _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 (f :: * -> *) a. Applicative f => a -> f a
    pure ()

      Call -> TCM () -> TCM ()
    forall (m :: * -> *) a. MonadTrace m => Call -> m a -> m a
    traceCall (Expr -> Call
    IsType_ Expr
    e) (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ do -- need Range for error message
        -- Andreas, 2016-06-21, issue #2054
        -- Do not default size metas to ∞ in local type signatures
        Bool
    checkingWhere <- (TCEnv -> Bool) -> TCMT IO Bool
    forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
    asksTC TCEnv -> Bool
    envCheckingWhere
        DefaultToInfty -> TCM ()
    solveSizeConstraints (DefaultToInfty -> TCM ()) -> DefaultToInfty -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ if Bool
    checkingWhere then DefaultToInfty
    DontDefaultToInfty else DefaultToInfty
    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 (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
        ([Char]
    name, PrimImpl Type
    t' PrimFun
    pf) <- QName -> TCM ([Char], PrimitiveImpl)
    lookupPrimitiveFunctionQ QName
    x
        -- Certain "primitive" functions are BUILTIN rather than
        -- primitive.
        let builtinPrimitives :: [[Char]]
    builtinPrimitives =
              [ [Char]
    "primNatPlus"
              , [Char]
    "primNatMinus"
              , [Char]
    "primNatTimes"
              , [Char]
    "primNatDivSucAux"
              , [Char]
    "primNatModSucAux"
              , [Char]
    "primNatEquality"
              , [Char]
    "primNatLess"
              , [Char]
    "primLevelZero"
              , [Char]
    "primLevelSuc"
              , [Char]
    "primLevelMax"
              , [Char]
    "primSetOmega"
              , [Char]
    "primStrictSet"
              , [Char]
    "primStrictSetOmega"
              ]
        Bool -> TCM () -> TCM ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    when ([Char]
    name [Char] -> [[Char]] -> Bool
    forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
    `elem` [[Char]]
    builtinPrimitives) (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.prim" Int
    20 (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]
    name TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> TCMT IO Doc
    "is a BUILTIN, not a primitive!"
          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
    NoSuchPrimitiveFunction [Char]
    name
        Type
    t <- Expr -> TCMT IO Type
    isType_ Expr
    e
        TCM () -> TCM ()
    forall (m :: * -> *) a.
    (MonadConstraint m, MonadWarning m, MonadError TCErr m,
     MonadFresh ProblemId m) =>
    m a -> m a
    noConstraints (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ Type -> Type -> TCM ()
    forall (m :: * -> *). MonadConversion m => Type -> Type -> m ()
    equalType Type
    t Type
    t'
        let s :: [Char]
    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 modality. Currently all primitives require default
        -- modalities, and likely very few will have different modalities in the
        -- future. Thus, rather than, the arguably nicer solution of adding a
        -- modality to PrimImpl we simply check the few special primitives here.
        let expectedInfo :: ArgInfo
    expectedInfo =
              case [Char]
    name of
                -- Currently no special primitives
                [Char]
    _ -> ArgInfo
    defaultArgInfo
        Bool -> TCM () -> TCM ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    unless (ArgInfo
    info ArgInfo -> ArgInfo -> Bool
    forall a. Eq a => a -> a -> Bool
    == ArgInfo
    expectedInfo) (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ TypeError -> TCM ()
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    TypeError -> m a
    typeError (TypeError -> TCM ()) -> TypeError -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ [Char] -> ArgInfo -> ArgInfo -> TypeError
    WrongModalityForPrimitive [Char]
    name ArgInfo
    info ArgInfo
    expectedInfo
        [Char] -> PrimFun -> TCM ()
    bindPrimitive [Char]
    s PrimFun
    pf
        QName -> ArgInfo -> QName -> Type -> Defn -> TCM ()
    addConstant' QName
    x ArgInfo
    info QName
    x Type
    t (Defn -> TCM ()) -> Defn -> TCM ()
    forall a b. (a -> b) -> a -> b
    $
            Primitive :: IsAbstract
    -> [Char]
    -> [Clause]
    -> FunctionInverse
    -> Maybe CompiledClauses
    -> Defn
    Primitive { primAbstr :: IsAbstract
    primAbstr    = DefInfo -> IsAbstract
    forall t. DefInfo' t -> IsAbstract
    Info.defAbstract DefInfo
    i
                      , primName :: [Char]
    primName     = [Char]
    s
                      , primClauses :: [Clause]
    primClauses  = []
                      , primInv :: FunctionInverse
    primInv      = FunctionInverse
    forall c. FunctionInverse' c
    NotInjective
                      , primCompiled :: Maybe CompiledClauses
    primCompiled = Maybe CompiledClauses
    forall a. Maybe a
    Nothing }

    -- | Check a pragma.
    checkPragma :: Range -> A.Pragma -> TCM ()
    checkPragma :: Range -> Pragma -> TCM ()
    checkPragma Range
    r Pragma
    p =
        Call -> TCM () -> TCM ()
    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
              | [Char] -> Bool
    isUntypedBuiltin [Char]
    b -> () -> TCM ()
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
              | Bool
    otherwise          -> [Char] -> ResolvedName -> TCM ()
    bindBuiltin [Char]
    b ResolvedName
    x
              where b :: [Char]
    b = RString -> [Char]
    forall a. Ranged a -> a
    rangedThing RString
    rb
            A.BuiltinNoDefPragma RString
    b KindOfName
    _kind QName
    x -> [Char] -> QName -> TCM ()
    bindBuiltinNoDef (RString -> [Char]
    forall a. Ranged a -> a
    rangedThing RString
    b) QName
    x
            A.RewritePragma Range
    _ [QName]
    qs -> [QName] -> TCM ()
    addRewriteRules [QName]
    qs
            A.CompilePragma RString
    b QName
    x [Char]
    s -> do
              -- Check that x resides in the same module (or a child) as the pragma.
              QName
    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.
              TCMT IO Bool -> TCM () -> TCM ()
    forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
    unlessM ((QName
    x' 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) (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $
                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
    GenericError ([Char] -> TypeError) -> [Char] -> TypeError
    forall a b. (a -> b) -> a -> b
    $
                  [Char]
    "COMPILE pragmas must appear in the same module as their corresponding definitions,"
              [Char] -> QName -> [Char] -> TCM ()
    addPragma (RString -> [Char]
    forall a. Ranged a -> a
    rangedThing RString
    b) QName
    x [Char]
    s
            A.StaticPragma QName
    x -> do
              Definition
    def <- QName -> TCMT IO Definition
    forall (m :: * -> *). HasConstInfo m => QName -> m Definition
    getConstInfo QName
    x
              case Definition -> Defn
    theDef Definition
    def of
                Function{} -> QName -> TCM ()
    markStatic QName
    x
                Defn
    _          -> 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
    GenericError [Char]
    "STATIC directive only works on functions"
            A.InjectivePragma QName
    x -> QName -> TCM ()
    markInjective QName
    x
            A.InlinePragma Bool
    b QName
    x -> do
              Definition
    def <- QName -> TCMT IO Definition
    forall (m :: * -> *). HasConstInfo m => QName -> m Definition
    getConstInfo QName
    x
              case Definition -> Defn
    theDef Definition
    def of
                Function{} -> Bool -> QName -> TCM ()
    markInline Bool
    b QName
    x
                Defn
    _          -> 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
    GenericError ([Char] -> TypeError) -> [Char] -> TypeError
    forall a b. (a -> b) -> a -> b
    $ [Char]
    sINLINE [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    " directive only works on functions"
                  where sINLINE :: [Char]
    sINLINE = if Bool
    b then [Char]
    "INLINE" else [Char]
    "NOINLINE"
            A.OptionsPragma{} -> 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
    GenericError ([Char] -> TypeError) -> [Char] -> TypeError
    forall a b. (a -> b) -> a -> b
    $ [Char]
    "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.EtaPragma QName
    r -> do
              let noRecord :: TCMT IO a
    noRecord = TypeError -> TCMT IO a
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    TypeError -> m a
    typeError (TypeError -> TCMT IO a) -> TypeError -> TCMT IO a
    forall a b. (a -> b) -> a -> b
    $ [Char] -> TypeError
    GenericError ([Char] -> TypeError) -> [Char] -> TypeError
    forall a b. (a -> b) -> a -> b
    $
                    [Char]
    "ETA pragma is only applicable to coinductive records"
              TCMT IO (Maybe Defn) -> TCM () -> (Defn -> TCM ()) -> TCM ()
    forall (m :: * -> *) a b.
    Monad m =>
    m (Maybe a) -> m b -> (a -> m b) -> m b
    caseMaybeM (QName -> TCMT IO (Maybe Defn)
    forall (m :: * -> *). HasConstInfo m => QName -> m (Maybe Defn)
    isRecord QName
    r) TCM ()
    forall {a}. TCMT IO a
    noRecord ((Defn -> TCM ()) -> TCM ()) -> (Defn -> TCM ()) -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ \case
                Record{ recInduction :: Defn -> Maybe Induction
    recInduction = Maybe Induction
    ind, recEtaEquality' :: Defn -> EtaEquality
    recEtaEquality' = EtaEquality
    eta } -> do
                  Bool -> TCM () -> TCM ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    unless (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 () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ TCM ()
    forall {a}. TCMT IO a
    noRecord
                  if | Specified NoEta{} <- EtaEquality
    eta -> 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
    GenericError ([Char] -> TypeError) -> [Char] -> TypeError
    forall a b. (a -> b) -> a -> b
    $
                         [Char]
    "ETA pragma conflicts with no-eta-equality declaration"
                     | Bool
    otherwise -> () -> TCM ()
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
                Defn
    _ -> TCM ()
    forall a. HasCallStack => a
    __IMPOSSIBLE__
              (Signature -> Signature) -> TCM ()
    forall (m :: * -> *).
    MonadTCState m =>
    (Signature -> Signature) -> m ()
    modifySignature ((Signature -> Signature) -> TCM ())
    -> (Signature -> Signature) -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ QName -> (Definition -> Definition) -> Signature -> Signature
    updateDefinition QName
    r ((Definition -> Definition) -> Signature -> Signature)
    -> (Definition -> Definition) -> Signature -> Signature
    forall a b. (a -> b) -> a -> b
    $ (Defn -> Defn) -> Definition -> Definition
    updateTheDef ((Defn -> Defn) -> Definition -> Definition)
    -> (Defn -> Defn) -> Definition -> Definition
    forall a b. (a -> b) -> a -> b
    $ \case
                def :: Defn
    def@Record{} -> Defn
    def { recEtaEquality' :: EtaEquality
    recEtaEquality' = HasEta' PatternOrCopattern -> EtaEquality
    Specified HasEta' PatternOrCopattern
    forall a. HasEta' a
    YesEta }
                Defn
    _ -> Defn
    forall a. HasCallStack => a
    __IMPOSSIBLE__

    -- | 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 (m :: * -> *) a.
    MonadTCEnv m =>
    (TCEnv -> TCEnv) -> m a -> m a
    localTC ( Lens' (TerminationCheck ()) TCEnv
    -> LensSet (TerminationCheck ()) TCEnv
    forall i o. Lens' i o -> LensSet i o
    set Lens' (TerminationCheck ()) TCEnv
    eTerminationCheck (() () -> TerminationCheck Name -> TerminationCheck ()
    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' CoverageCheck TCEnv -> LensSet CoverageCheck TCEnv
    forall i o. Lens' i o -> LensSet i o
    set Lens' CoverageCheck TCEnv
    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
    lookupMutualBlock MutualId
    blockId

    -- | 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 [Occurrence]
    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 [Occurrence]
    -> QName
    -> Expr
    -> TCM ()
    checkAxiom' Maybe GeneralizeTelescope
    gtel KindOfName
    funSig DefInfo
    i ArgInfo
    info Maybe [Occurrence]
    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 :: ModuleName -> A.GeneralizeTelescope -> [A.Declaration] -> TCM ()
    checkSection :: ModuleName -> GeneralizeTelescope -> [Declaration] -> TCM ()
    checkSection ModuleName
    x GeneralizeTelescope
    tel [Declaration]
    ds = ModuleName -> GeneralizeTelescope -> TCM () -> TCM ()
    forall a. ModuleName -> GeneralizeTelescope -> TCM a -> TCM a
    newSection 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 [NamedArg Expr]
    args = Tele (Dom Type) -> [NamedArg Expr] -> TCM (Tele (Dom Type))
    check Tele (Dom Type)
    tel [NamedArg Expr]
    args
      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) -> [NamedArg Expr] -> TypeError
    ModuleArityMismatch ModuleName
    m Tele (Dom Type)
    tel [NamedArg Expr]
    args

        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 (m :: * -> *) a. Monad m => a -> m a
    return Tele (Dom Type)
    tel
        check Tele (Dom Type)
    EmptyTel (NamedArg Expr
    _:[NamedArg Expr]
    _)     = TCM (Tele (Dom Type))
    bad
        check (ExtendTel dom :: Dom Type
    dom@Dom{domInfo :: forall t e. Dom' t e -> ArgInfo
    domInfo = ArgInfo
    info} Abs (Tele (Dom Type))
    btel) args0 :: [NamedArg Expr]
    args0@(Arg ArgInfo
    info' Named_ Expr
    arg : [NamedArg Expr]
    args) =
          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 in
          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] -> TCM (Tele (Dom Type))
    check Tele (Dom Type)
    tel [NamedArg Expr]
    args0
            (Instance{}, Hiding
    Hidden, Maybe [Char]
    _)           -> Tele (Dom Type) -> [NamedArg Expr] -> TCM (Tele (Dom Type))
    check Tele (Dom Type)
    tel [NamedArg Expr]
    args0
            (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] -> TCM (Tele (Dom Type))
    check Tele (Dom Type)
    tel [NamedArg Expr]
    args0
            (Hiding
    Hidden, Hiding
    NotHidden, Maybe [Char]
    _)            -> Tele (Dom Type) -> [NamedArg Expr] -> TCM (Tele (Dom Type))
    check Tele (Dom Type)
    tel [NamedArg Expr]
    args0
            (Hiding
    Hidden, Instance{}, Maybe [Char]
    _)           -> Tele (Dom Type) -> [NamedArg Expr] -> TCM (Tele (Dom Type))
    check Tele (Dom Type)
    tel [NamedArg Expr]
    args0
            (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] -> TCM (Tele (Dom Type))
    check Tele (Dom Type)
    tel [NamedArg Expr]
    args0
            (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
      -> 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
    -> ModuleName -> ModuleApplication -> ScopeCopyInfo -> TCM ()
    checkSectionApplication ModuleInfo
    i ModuleName
    m1 ModuleApplication
    modapp ScopeCopyInfo
    copyInfo =
      Call -> TCM () -> TCM ()
    forall (m :: * -> *) a. MonadTrace m => Call -> m a -> m a
    traceCall (Range -> ModuleName -> ModuleApplication -> Call
    CheckSectionApplication (ModuleInfo -> Range
    forall a. HasRange a => a -> Range
    getRange ModuleInfo
    i) ModuleName
    m1 ModuleApplication
    modapp) (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $
      -- A section application is type-checked in a non-erased context
      -- (#5410).
      (TCEnv -> TCEnv) -> TCM () -> TCM ()
    forall (m :: * -> *) a.
    MonadTCEnv m =>
    (TCEnv -> TCEnv) -> m a -> m a
    localTC (Lens' Quantity TCEnv -> LensMap Quantity TCEnv
    forall i o. Lens' i o -> LensMap i o
    over Lens' Quantity TCEnv
    eQuantity LensMap Quantity TCEnv -> LensMap Quantity TCEnv
    forall a b. (a -> b) -> a -> b
    $ (Quantity -> Quantity) -> Quantity -> Quantity
    forall a. LensQuantity a => (Quantity -> Quantity) -> a -> a
    mapQuantity (Quantity -> Quantity -> Quantity
    `addQuantity` Quantity
    topQuantity)) (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $
      ModuleInfo
    -> ModuleName -> ModuleApplication -> ScopeCopyInfo -> TCM ()
    checkSectionApplication' ModuleInfo
    i ModuleName
    m1 ModuleApplication
    modapp ScopeCopyInfo
    copyInfo

    -- | Check an application of a section. (Do not invoke this procedure
    -- directly, use 'checkSectionApplication'.)
    checkSectionApplication'
      :: Info.ModuleInfo
      -> 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
    -> ModuleName -> ModuleApplication -> ScopeCopyInfo -> TCM ()
    checkSectionApplication' ModuleInfo
    i ModuleName
    m1 (A.SectionApp Telescope
    ptel ModuleName
    m2 [NamedArg Expr]
    args) ScopeCopyInfo
    copyInfo = do
      -- Module applications can appear in lets, in which case we treat
      -- lambda-bound variables as additional parameters to the module.
      Int
    extraParams <- do
        Int
    mfv <- TCMT IO Int
    getCurrentModuleFreeVars
        Int
    fv  <- TCMT IO Int
    forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Int
    getContextSize
        Int -> TCMT IO Int
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Int
    fv Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - Int
    mfv)
      Bool -> TCM () -> TCM ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    when (Int
    extraParams Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    > Int
    0) (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ [Char] -> Int -> [Char] -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> [Char] -> m ()
    reportSLn [Char]
    "tc.mod.apply" Int
    30 ([Char] -> TCM ()) -> [Char] -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ [Char]
    "Extra parameters to " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ ModuleName -> [Char]
    forall a. Pretty a => a -> [Char]
    prettyShow ModuleName
    m1 [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    ": " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ Int -> [Char]
    forall a. Show a => a -> [Char]
    show Int
    extraParams
      -- Type-check the LHS (ptel) of the module macro.
      Telescope -> (Tele (Dom Type) -> TCM ()) -> TCM ()
    forall a. Telescope -> (Tele (Dom Type) -> TCM a) -> TCM a
    checkTelescope Telescope
    ptel ((Tele (Dom Type) -> TCM ()) -> TCM ())
    -> (Tele (Dom Type) -> TCM ()) -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ \ 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)`.
        Tele (Dom Type)
    tel <- ModuleName -> TCM (Tele (Dom Type))
    forall (m :: * -> *).
    (Functor m, ReadTCState m) =>
    ModuleName -> m (Tele (Dom Type))
    lookupSection ModuleName
    m2
        [Arg Term]
    vs  <- ModuleName -> TCMT IO [Arg Term]
    forall (m :: * -> *).
    (Functor m, Applicative m, HasOptions m, MonadTCEnv m,
     ReadTCState m, MonadDebug m) =>
    ModuleName -> m [Arg Term]
    moduleParamsToApply ModuleName
    m2
        let tel' :: Tele (Dom Type)
    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.
        Tele (Dom Type)
    etaTel <- ModuleName
    -> Tele (Dom Type) -> [NamedArg Expr] -> TCM (Tele (Dom Type))
    checkModuleArity ModuleName
    m2 Tele (Dom Type)
    tel' [NamedArg Expr]
    args
        -- Take the module parameters that will be instantiated by @args@.
        let tel'' :: Tele (Dom Type)
    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'
        [Char] -> Int -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "tc.mod.apply" Int
    15 (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
    "applying section" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> ModuleName -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM ModuleName
    m2
          , 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
    $ TCMT IO Doc
    "args =" 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 ((NamedArg Expr -> TCMT IO Doc) -> [NamedArg Expr] -> [TCMT IO Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map NamedArg Expr -> TCMT IO Doc
    forall a (m :: * -> *).
    (ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
    a -> m Doc
    prettyA [NamedArg Expr]
    args)
          , 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
    $ TCMT IO Doc
    "ptel =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Impossible -> Int -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *) a.
    MonadAddContext m =>
    Impossible -> Int -> m a -> m a
    escapeContext Impossible
    HasCallStack => Impossible
    impossible (Tele (Dom Type) -> Int
    forall a. Sized a => a -> Int
    size Tele (Dom Type)
    ptel) (Tele (Dom Type) -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Tele (Dom Type)
    ptel)
          , 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
    $ TCMT IO Doc
    "tel  =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Tele (Dom Type) -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Tele (Dom Type)
    tel
          , 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
    $ TCMT IO Doc
    "tel' =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Tele (Dom Type) -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Tele (Dom Type)
    tel'
          , 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
    $ TCMT IO Doc
    "tel''=" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Tele (Dom Type) -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Tele (Dom Type)
    tel''
          , 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
    $ TCMT IO Doc
    "eta  =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Impossible -> Int -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *) a.
    MonadAddContext m =>
    Impossible -> Int -> m a -> m a
    escapeContext Impossible
    HasCallStack => Impossible
    impossible (Tele (Dom Type) -> Int
    forall a. Sized a => a -> Int
    size Tele (Dom Type)
    ptel) (Tele (Dom Type) -> TCMT IO Doc -> TCMT IO Doc
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    addContext Tele (Dom Type)
    tel'' (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ Tele (Dom Type) -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Tele (Dom Type)
    etaTel)
          ]
        -- Now, type check arguments.
        [Arg Term]
    ts <- TCMT IO (Elims, Tele (Dom Type))
    -> TCMT IO (Elims, Tele (Dom Type))
    forall (m :: * -> *) a.
    (MonadConstraint m, MonadWarning m, MonadError TCErr m,
     MonadFresh ProblemId m) =>
    m a -> m a
    noConstraints (Comparison
    -> ExpandHidden
    -> Range
    -> [NamedArg Expr]
    -> Tele (Dom Type)
    -> TCMT IO (Elims, Tele (Dom Type))
    checkArguments_ Comparison
    CmpEq ExpandHidden
    DontExpandLast (ModuleInfo -> Range
    forall a. HasRange a => a -> Range
    getRange ModuleInfo
    i) [NamedArg Expr]
    args Tele (Dom Type)
    tel') TCMT IO (Elims, Tele (Dom Type))
    -> ((Elims, Tele (Dom Type)) -> TCMT IO [Arg Term])
    -> TCMT IO [Arg Term]
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \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 (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)
    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
        [Char] -> Int -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "tc.mod.apply" Int
    15 (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
          [ 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
    $ TCMT IO Doc
    "aTel =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Tele (Dom Type) -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Tele (Dom Type)
    aTel
          ]
        -- Andreas, 2014-04-06, Issue 1094:
        -- Add the section with well-formed telescope.
        KeepNames (Tele (Dom Type)) -> TCM () -> TCM ()
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    addContext (Tele (Dom Type) -> KeepNames (Tele (Dom Type))
    forall a. a -> KeepNames a
    KeepNames Tele (Dom Type)
    aTel) (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.mod.apply" Int
    80 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    forall a b. (a -> b) -> a -> b
    $
            TCMT IO Doc
    "addSection" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> ModuleName -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM ModuleName
    m1 TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> (TCM (Tele (Dom Type))
    forall (m :: * -> *).
    (Applicative m, MonadTCEnv m) =>
    m (Tele (Dom Type))
    getContextTelescope TCM (Tele (Dom Type))
    -> (Tele (Dom Type) -> TCMT IO Doc) -> TCMT IO Doc
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \ 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
    prettyTCM Tele (Dom Type)
    tel))
          ModuleName -> TCM ()
    addSection ModuleName
    m1

        [Char] -> Int -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "tc.mod.apply" 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
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    sep [ TCMT IO Doc
    "applySection", ModuleName -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM ModuleName
    m1, TCMT IO Doc
    "=", ModuleName -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM ModuleName
    m2, [TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    fsep ([TCMT IO Doc] -> TCMT IO Doc) -> [TCMT IO Doc] -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ (Arg Term -> TCMT IO Doc) -> [Arg Term] -> [TCMT IO Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map Arg Term -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM ([Arg Term]
    vs [Arg Term] -> [Arg Term] -> [Arg Term]
    forall a. [a] -> [a] -> [a]
    ++ [Arg Term]
    ts) ]
          , 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
    $ ScopeCopyInfo -> TCMT IO Doc
    forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
    pretty ScopeCopyInfo
    copyInfo
          ]
        [Arg Term]
    args <- [Arg Term] -> TCMT IO [Arg Term]
    forall a (m :: * -> *).
    (InstantiateFull a, MonadReduce m) =>
    a -> m a
    instantiateFull ([Arg Term] -> TCMT IO [Arg Term])
    -> [Arg Term] -> TCMT IO [Arg Term]
    forall a b. (a -> b) -> a -> b
    $ [Arg Term]
    vs [Arg Term] -> [Arg Term] -> [Arg Term]
    forall a. [a] -> [a] -> [a]
    ++ [Arg Term]
    ts
        let n :: Int
    n = Tele (Dom Type) -> Int
    forall a. Sized a => a -> Int
    size Tele (Dom Type)
    aTel
        [Arg Term]
    etaArgs <- TCMT IO [Arg Term] -> TCMT IO [Arg Term]
    forall (tcm :: * -> *) a.
    (MonadTCEnv tcm, ReadTCState tcm) =>
    tcm a -> tcm a
    inTopContext (TCMT IO [Arg Term] -> TCMT IO [Arg Term])
    -> TCMT IO [Arg Term] -> TCMT IO [Arg Term]
    forall a b. (a -> b) -> a -> b
    $ Tele (Dom Type) -> TCMT IO [Arg Term] -> TCMT IO [Arg Term]
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    addContext Tele (Dom Type)
    aTel TCMT IO [Arg Term]
    forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m [Arg Term]
    getContextArgs
        KeepNames (Tele (Dom Type)) -> TCM () -> TCM ()
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    addContext (Tele (Dom Type) -> KeepNames (Tele (Dom Type))
    forall a. a -> KeepNames a
    KeepNames Tele (Dom Type)
    aTel) (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $
          ModuleName
    -> Tele (Dom Type)
    -> ModuleName
    -> [Arg Term]
    -> ScopeCopyInfo
    -> TCM ()
    applySection ModuleName
    m1 (Tele (Dom Type)
    ptel Tele (Dom Type) -> Tele (Dom Type) -> Tele (Dom Type)
    forall t. Abstract t => Tele (Dom Type) -> t -> t
    `abstract` Tele (Dom Type)
    aTel) ModuleName
    m2 (Int -> [Arg Term] -> [Arg Term]
    forall a. Subst a => Int -> a -> a
    raise Int
    n [Arg Term]
    args [Arg Term] -> [Arg Term] -> [Arg Term]
    forall a. [a] -> [a] -> [a]
    ++ [Arg Term]
    etaArgs) ScopeCopyInfo
    copyInfo

    checkSectionApplication' ModuleInfo
    i ModuleName
    m1 (A.RecordModuleInstance ModuleName
    x) ScopeCopyInfo
    copyInfo = do
      let name :: QName
    name = ModuleName -> QName
    mnameToQName ModuleName
    x
      Tele (Dom Type)
    tel' <- ModuleName -> TCM (Tele (Dom Type))
    forall (m :: * -> *).
    (Functor m, ReadTCState m) =>
    ModuleName -> m (Tele (Dom Type))
    lookupSection ModuleName
    x
      [Arg Term]
    vs   <- ModuleName -> TCMT IO [Arg Term]
    forall (m :: * -> *).
    (Functor m, Applicative m, HasOptions m, MonadTCEnv m,
     ReadTCState m, MonadDebug m) =>
    ModuleName -> m [Arg Term]
    moduleParamsToApply ModuleName
    x
      let tel :: Tele (Dom Type)
    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 :: [Arg Term]
    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)
    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 :: Tele (Dom Type) -> Tele (Dom Type)
    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 :: Maybe NamedName
    domName = NamedName -> Maybe NamedName
    forall a. a -> Maybe a
    Just (NamedName -> Maybe NamedName) -> NamedName -> Maybe NamedName
    forall a b. (a -> b) -> a -> b
    $ Origin -> RString -> NamedName
    forall a. Origin -> a -> WithOrigin a
    WithOrigin Origin
    Inserted (RString -> NamedName) -> RString -> NamedName
    forall a b. (a -> b) -> a -> b
    $ [Char] -> RString
    forall a. a -> Ranged a
    unranged [Char]
    "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__

      [Char] -> Int -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "tc.mod.apply" 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
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    sep [ TCMT IO Doc
    "applySection", QName -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM QName
    name, 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
    $ TCMT IO Doc
    "x       =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> ModuleName -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM ModuleName
    x
        , 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
    $ TCMT IO Doc
    "name    =" 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
    prettyTCM QName
    name
        , 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
    $ TCMT IO Doc
    "tel     =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Tele (Dom Type) -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Tele (Dom Type)
    tel
        , 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
    $ TCMT IO Doc
    "telInst =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Tele (Dom Type) -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Tele (Dom Type)
    telInst
        , 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
    $ TCMT IO Doc
    "vs      =" 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 ((Arg Term -> TCMT IO Doc) -> [Arg Term] -> [TCMT IO Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map Arg Term -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM [Arg Term]
    vs)
        -- , nest 2 $ "args    =" <+> sep (map prettyTCM args)
        ]
      [Char] -> Int -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "tc.mod.apply" Int
    60 (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
        [ 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
    $ TCMT IO Doc
    "vs      =" 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 ([Arg Term] -> [Char]
    forall a. Show a => a -> [Char]
    show [Arg Term]
    vs)
        -- , nest 2 $ "args    =" <+> text (show args)
        ]
      Bool -> TCM () -> TCM ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    when (Tele (Dom Type)
    tel Tele (Dom Type) -> Tele (Dom Type) -> Bool
    forall a. Eq a => a -> a -> Bool
    == Tele (Dom Type)
    forall a. Tele a
    EmptyTel) (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $
        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
    GenericError ([Char] -> TypeError) -> [Char] -> TypeError
    forall a b. (a -> b) -> a -> b
    $ QName -> [Char]
    forall a. Pretty a => a -> [Char]
    prettyShow (QName -> QName
    qnameToConcrete QName
    name) [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    " is not a parameterised section"

      Tele (Dom Type) -> TCM () -> TCM ()
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    addContext Tele (Dom Type)
    telInst (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ do
        [Arg Term]
    vs <- ModuleName -> TCMT IO [Arg Term]
    forall (m :: * -> *).
    (Functor m, Applicative m, HasOptions m, MonadTCEnv m,
     ReadTCState m, MonadDebug m) =>
    ModuleName -> m [Arg Term]
    moduleParamsToApply ModuleName
    x
        [Char] -> Int -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "tc.mod.apply" 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
          [ 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
    $ TCMT IO Doc
    "vs      =" 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 ((Arg Term -> TCMT IO Doc) -> [Arg Term] -> [TCMT IO Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map Arg Term -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM [Arg Term]
    vs)
          , 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
    $ TCMT IO Doc
    "args    =" 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 ((Arg Term -> TCMT IO Doc) -> [Arg Term] -> [TCMT IO Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map (TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Functor m => m Doc -> m Doc
    parens (TCMT IO Doc -> TCMT IO Doc)
    -> (Arg Term -> TCMT IO Doc) -> Arg Term -> TCMT IO Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Arg Term -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM) [Arg Term]
    args)
          ]
        [Char] -> Int -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "tc.mod.apply" Int
    60 (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
          [ 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
    $ TCMT IO Doc
    "vs      =" 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 ([Arg Term] -> [Char]
    forall a. Show a => a -> [Char]
    show [Arg Term]
    vs)
          , 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
    $ TCMT IO Doc
    "args    =" 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 ([Arg Term] -> [Char]
    forall a. Show a => a -> [Char]
    show [Arg Term]
    args)
          ]
        ModuleName -> TCM ()
    addSection ModuleName
    m1
        ModuleName
    -> Tele (Dom Type)
    -> ModuleName
    -> [Arg Term]
    -> ScopeCopyInfo
    -> TCM ()
    applySection ModuleName
    m1 Tele (Dom Type)
    telInst ModuleName
    x ([Arg Term]
    vs [Arg Term] -> [Arg Term] -> [Arg Term]
    forall a. [a] -> [a] -> [a]
    ++ [Arg Term]
    args) ScopeCopyInfo
    copyInfo

    -- | Type check an import declaration. Actually doesn't do anything, since all
    --   the work is done when scope checking.
    checkImport :: Info.ModuleInfo -> ModuleName -> TCM ()
    checkImport :: ModuleInfo -> ModuleName -> TCM ()
    checkImport ModuleInfo
    i ModuleName
    x = () -> TCM ()
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()

    ------------------------------------------------------------------------
    -- * 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"

    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 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 (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 (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
    -> ModuleName
    -> GeneralizeTelescope
    -> [Declaration]
    -> Declaration
    A.Section Range
    info 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 (m :: * -> *) a. Monad m => a -> m a
    return ()