    {-# LANGUAGE NondecreasingIndentation #-}

    module Agda.TypeChecking.Monad.Signature where

    import Prelude hiding (null)

    import qualified Control.Monad.Fail as Fail

    import Control.Arrow                 ( first, second )
    import Control.Monad.Except          ( ExceptT )
    import Control.Monad.State           ( StateT  )
    import Control.Monad.Reader          ( ReaderT )
    import Control.Monad.Writer          ( WriterT )
    import Control.Monad.Trans.Maybe     ( MaybeT  )
    import Control.Monad.Trans.Identity  ( IdentityT )
    import Control.Monad.Trans           ( MonadTrans, lift )

    import Data.Foldable (for_)
    import qualified Data.List as List
    import Data.Set (Set)
    import qualified Data.Set as Set
    import qualified Data.Map as Map
    import qualified Data.HashMap.Strict as HMap
    import Data.Maybe
    import Data.Semigroup ((<>))

    import Agda.Interaction.Options

    import Agda.Syntax.Abstract.Name
    import Agda.Syntax.Abstract (Ren, ScopeCopyInfo(..))
    import Agda.Syntax.Common
    import Agda.Syntax.Internal as I
    import Agda.Syntax.Internal.Names
    import Agda.Syntax.Position
    import Agda.Syntax.Treeless (Compiled(..), TTerm, ArgUsage)

    import Agda.TypeChecking.Monad.Base
    import Agda.TypeChecking.Monad.Builtin
    import Agda.TypeChecking.Monad.Debug
    import Agda.TypeChecking.Monad.Context
    import Agda.TypeChecking.Monad.Env
    import Agda.TypeChecking.Monad.Mutual
    import Agda.TypeChecking.Monad.Open
    import Agda.TypeChecking.Monad.Options
    import Agda.TypeChecking.Monad.State
    import Agda.TypeChecking.Monad.Trace
    import Agda.TypeChecking.DropArgs
    import Agda.TypeChecking.Warnings
    import Agda.TypeChecking.Positivity.Occurrence
    import Agda.TypeChecking.Substitute
    import Agda.TypeChecking.CompiledClause
    import Agda.TypeChecking.Coverage.SplitTree
    import {-# SOURCE #-} Agda.TypeChecking.CompiledClause.Compile
    import {-# SOURCE #-} Agda.TypeChecking.Polarity
    import {-# SOURCE #-} Agda.TypeChecking.Pretty
    import {-# SOURCE #-} Agda.TypeChecking.ProjectionLike
    import {-# SOURCE #-} Agda.TypeChecking.Reduce

    import {-# SOURCE #-} Agda.Compiler.Treeless.Erase
    import {-# SOURCE #-} Agda.Compiler.Builtin

    import Agda.Utils.Either
    import Agda.Utils.Functor
    import Agda.Utils.Lens
    import Agda.Utils.List
    import qualified Agda.Utils.List1 as List1
    import Agda.Utils.ListT
    import Agda.Utils.Maybe
    import Agda.Utils.Monad
    import Agda.Utils.Null
    import Agda.Utils.Pretty (prettyShow)
    import Agda.Utils.Singleton
    import Agda.Utils.Size
    import Agda.Utils.Update

    import Agda.Utils.Impossible

    -- | Add a constant to the signature. Lifts the definition to top level.
    addConstant :: QName -> Definition -> TCM ()
    addConstant :: QName -> Definition -> TCM ()
    addConstant QName
    q Definition
    d = do
      [Char] -> Int -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "tc.signature" Int
    20 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Doc
    "adding constant " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> QName -> TCMT IO Doc
    forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
    pretty QName
    q TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> TCMT IO Doc
    " to signature"
      Telescope
    tel <- TCMT IO Telescope
    forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Telescope
    getContextTelescope
      let tel' :: Telescope
    tel' = [Char] -> Telescope -> Telescope
    forall a. [Char] -> Tele a -> Tele a
    replaceEmptyName [Char]
    "r" (Telescope -> Telescope) -> Telescope -> Telescope
    forall a b. (a -> b) -> a -> b
    $ Telescope -> Telescope
    forall a. KillRange a => KillRangeT a
    killRange (Telescope -> Telescope) -> Telescope -> Telescope
    forall a b. (a -> b) -> a -> b
    $ case Definition -> Defn
    theDef Definition
    d of
                  Constructor{} -> (Dom Type -> Dom Type) -> Telescope -> Telescope
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap Dom Type -> Dom Type
    forall a. LensHiding a => a -> a
    hideOrKeepInstance Telescope
    tel
                  Function{ funProjection :: Defn -> Maybe Projection
    funProjection = Just Projection{ projProper :: Projection -> Maybe QName
    projProper = Just{}, projIndex :: Projection -> Int
    projIndex = Int
    n } } ->
                    let fallback :: Telescope
    fallback = (Dom Type -> Dom Type) -> Telescope -> Telescope
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap Dom Type -> Dom Type
    forall a. LensHiding a => a -> a
    hideOrKeepInstance Telescope
    tel in
                    if Int
    n Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    > Int
    0 then Telescope
    fallback else
                    -- if the record value is part of the telescope, its hiding should left unchanged
                      case [Dom ([Char], Type)]
    -> Maybe ([Dom ([Char], Type)], Dom ([Char], Type))
    forall a. [a] -> Maybe ([a], a)
    initLast ([Dom ([Char], Type)]
     -> Maybe ([Dom ([Char], Type)], Dom ([Char], Type)))
    -> [Dom ([Char], Type)]
    -> Maybe ([Dom ([Char], Type)], Dom ([Char], Type))
    forall a b. (a -> b) -> a -> b
    $ Telescope -> [Dom ([Char], Type)]
    forall t. Tele (Dom t) -> [Dom ([Char], t)]
    telToList Telescope
    tel of
                        Maybe ([Dom ([Char], Type)], Dom ([Char], Type))
    Nothing -> Telescope
    fallback
                        Just ([Dom ([Char], Type)]
    doms, Dom ([Char], Type)
    dom) -> [Dom ([Char], Type)] -> Telescope
    telFromList ([Dom ([Char], Type)] -> Telescope)
    -> [Dom ([Char], Type)] -> Telescope
    forall a b. (a -> b) -> a -> b
    $ (Dom ([Char], Type) -> Dom ([Char], Type))
    -> [Dom ([Char], Type)] -> [Dom ([Char], Type)]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap Dom ([Char], Type) -> Dom ([Char], Type)
    forall a. LensHiding a => a -> a
    hideOrKeepInstance [Dom ([Char], Type)]
    doms [Dom ([Char], Type)]
    -> [Dom ([Char], Type)] -> [Dom ([Char], Type)]
    forall a. [a] -> [a] -> [a]
    ++ [Dom ([Char], Type)
    dom]
                  Defn
    _ -> Telescope
    tel
      let d' :: Definition
    d' = Telescope -> Definition -> Definition
    forall t. Abstract t => Telescope -> t -> t
    abstract Telescope
    tel' (Definition -> Definition) -> Definition -> Definition
    forall a b. (a -> b) -> a -> b
    $ Definition
    d { defName :: QName
    defName = QName
    q }
      [Char] -> Int -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "tc.signature" Int
    60 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Doc
    "lambda-lifted definition =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <?> Definition -> TCMT IO Doc
    forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
    pretty Definition
    d'
      (Signature -> Signature) -> TCM ()
    forall (m :: * -> *).
    MonadTCState m =>
    (Signature -> Signature) -> m ()
    modifySignature ((Signature -> Signature) -> TCM ())
    -> (Signature -> Signature) -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ (Definitions -> Definitions) -> Signature -> Signature
    updateDefinitions ((Definitions -> Definitions) -> Signature -> Signature)
    -> (Definitions -> Definitions) -> Signature -> Signature
    forall a b. (a -> b) -> a -> b
    $ (Definition -> Definition -> Definition)
    -> QName -> Definition -> Definitions -> Definitions
    forall k v.
    (Eq k, Hashable k) =>
    (v -> v -> v) -> k -> v -> HashMap k v -> HashMap k v
    HMap.insertWith Definition -> Definition -> Definition
    (+++) QName
    q Definition
    d'
      MutualId
    i <- TCM MutualId
    currentOrFreshMutualBlock
      MutualId -> QName -> TCM ()
    setMutualBlock MutualId
    i QName
    q
      where
        Definition
    new +++ :: Definition -> Definition -> Definition
    +++ Definition
    old = Definition
    new { defDisplay :: [LocalDisplayForm]
    defDisplay = Definition -> [LocalDisplayForm]
    defDisplay Definition
    new [LocalDisplayForm] -> [LocalDisplayForm] -> [LocalDisplayForm]
    forall a. [a] -> [a] -> [a]
    ++ Definition -> [LocalDisplayForm]
    defDisplay Definition
    old
                          , defInstance :: Maybe QName
    defInstance = Definition -> Maybe QName
    defInstance Definition
    new Maybe QName -> Maybe QName -> Maybe QName
    forall (m :: * -> *) a. MonadPlus m => m a -> m a -> m a
    `mplus` Definition -> Maybe QName
    defInstance Definition
    old }

    -- | A combination of 'addConstant' and 'defaultDefn'. The 'Language'
    -- does not need to be supplied.

    addConstant' ::
      QName -> ArgInfo -> QName -> Type -> Defn -> TCM ()
    addConstant' :: QName -> ArgInfo -> QName -> Type -> Defn -> TCM ()
    addConstant' QName
    q ArgInfo
    info QName
    x Type
    t Defn
    def = do
      Language
    lang <- TCMT IO Language
    forall (m :: * -> *). HasOptions m => m Language
    getLanguage
      QName -> Definition -> TCM ()
    addConstant QName
    q (Definition -> TCM ()) -> Definition -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ ArgInfo -> QName -> Type -> Language -> Defn -> Definition
    defaultDefn ArgInfo
    info QName
    x Type
    t Language
    lang Defn
    def

    -- | Set termination info of a defined function symbol.
    setTerminates :: QName -> Bool -> TCM ()
    setTerminates :: QName -> Bool -> TCM ()
    setTerminates QName
    q Bool
    b = (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
    $ \case
        def :: Defn
    def@Function{} -> Defn
    def { funTerminates :: Maybe Bool
    funTerminates = Bool -> Maybe Bool
    forall a. a -> Maybe a
    Just Bool
    b }
        Defn
    def -> Defn
    def

    -- | Set CompiledClauses of a defined function symbol.
    setCompiledClauses :: QName -> CompiledClauses -> TCM ()
    setCompiledClauses :: QName -> CompiledClauses -> TCM ()
    setCompiledClauses QName
    q 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 ((Defn -> Defn) -> Definition -> Definition)
    -> (Defn -> Defn) -> Definition -> Definition
    forall a b. (a -> b) -> a -> b
    $ Defn -> Defn
    setT
      where
        setT :: Defn -> Defn
    setT def :: Defn
    def@Function{} = Defn
    def { funCompiled :: Maybe CompiledClauses
    funCompiled = CompiledClauses -> Maybe CompiledClauses
    forall a. a -> Maybe a
    Just CompiledClauses
    cc }
        setT Defn
    def            = Defn
    def

    -- | Set SplitTree of a defined function symbol.
    setSplitTree :: QName -> SplitTree -> TCM ()
    setSplitTree :: QName -> SplitTree -> TCM ()
    setSplitTree QName
    q SplitTree
    st = (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
    setT
      where
        setT :: Defn -> Defn
    setT def :: Defn
    def@Function{} = Defn
    def { funSplitTree :: Maybe SplitTree
    funSplitTree = SplitTree -> Maybe SplitTree
    forall a. a -> Maybe a
    Just SplitTree
    st }
        setT Defn
    def            = Defn
    def

    -- | Modify the clauses of a function.
    modifyFunClauses :: QName -> ([Clause] -> [Clause]) -> TCM ()
    modifyFunClauses :: QName -> ([Clause] -> [Clause]) -> TCM ()
    modifyFunClauses QName
    q [Clause] -> [Clause]
    f =
      (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
    $ ([Clause] -> [Clause]) -> Defn -> Defn
    updateFunClauses [Clause] -> [Clause]
    f

    -- | Lifts clauses to the top-level and adds them to definition.
    --   Also adjusts the 'funCopatternLHS' field if necessary.
    addClauses :: QName -> [Clause] -> TCM ()
    addClauses :: QName -> [Clause] -> TCM ()
    addClauses QName
    q [Clause]
    cls = do
      Telescope
    tel <- TCMT IO Telescope
    forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Telescope
    getContextTelescope
      (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 (([Clause] -> [Clause]) -> Defn -> Defn
    updateFunClauses ([Clause] -> [Clause] -> [Clause]
    forall a. [a] -> [a] -> [a]
    ++ Telescope -> [Clause] -> [Clause]
    forall t. Abstract t => Telescope -> t -> t
    abstract Telescope
    tel [Clause]
    cls))
        (Definition -> Definition)
    -> (Definition -> Definition) -> Definition -> Definition
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Bool -> Bool) -> Definition -> Definition
    updateDefCopatternLHS (Bool -> Bool -> Bool
    || [Clause] -> Bool
    isCopatternLHS [Clause]
    cls)

    mkPragma :: String -> TCM CompilerPragma
    mkPragma :: [Char] -> TCM CompilerPragma
    mkPragma [Char]
    s = Range -> [Char] -> CompilerPragma
    CompilerPragma (Range -> [Char] -> CompilerPragma)
    -> TCMT IO Range -> TCMT IO ([Char] -> CompilerPragma)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> TCMT IO Range
    forall (m :: * -> *). MonadTCEnv m => m Range
    getCurrentRange TCMT IO ([Char] -> CompilerPragma)
    -> TCMT IO [Char] -> TCM CompilerPragma
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> [Char] -> TCMT IO [Char]
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure [Char]
    s

    -- | Add a compiler pragma `{-\# COMPILE <backend> <name> <text> \#-}`
    addPragma :: BackendName -> QName -> String -> TCM ()
    addPragma :: [Char] -> QName -> [Char] -> TCM ()
    addPragma [Char]
    b QName
    q [Char]
    s = TCMT IO Bool -> TCM () -> TCM () -> TCM ()
    forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
    ifM TCMT IO Bool
    erased
      {- then -} (Warning -> TCM ()
    forall (m :: * -> *).
    (HasCallStack, MonadWarning m) =>
    Warning -> m ()
    warning (Warning -> TCM ()) -> Warning -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ [Char] -> QName -> Warning
    PragmaCompileErased [Char]
    b QName
    q)
      {- else -} (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ do
        CompilerPragma
    pragma <- [Char] -> TCM CompilerPragma
    mkPragma [Char]
    s
        (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
    $ [Char] -> CompilerPragma -> Definition -> Definition
    addCompilerPragma [Char]
    b CompilerPragma
    pragma

      where

      erased :: TCM Bool
      erased :: TCMT IO Bool
    erased = do
        Defn
    def <- Definition -> Defn
    theDef (Definition -> Defn) -> TCMT IO Definition -> TCMT IO Defn
    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
    q
        case Defn
    def of
          -- If we have a defined symbol, we check whether it is erasable
          Function{} ->
            Lens' (Maybe [Char]) TCEnv
    -> (Maybe [Char] -> Maybe [Char]) -> TCMT IO Bool -> TCMT IO Bool
    forall (m :: * -> *) a b.
    MonadTCEnv m =>
    Lens' a TCEnv -> (a -> a) -> m b -> m b
    locallyTC      Lens' (Maybe [Char]) TCEnv
    eActiveBackendName (Maybe [Char] -> Maybe [Char] -> Maybe [Char]
    forall a b. a -> b -> a
    const (Maybe [Char] -> Maybe [Char] -> Maybe [Char])
    -> Maybe [Char] -> Maybe [Char] -> Maybe [Char]
    forall a b. (a -> b) -> a -> b
    $ [Char] -> Maybe [Char]
    forall a. a -> Maybe a
    Just [Char]
    b) (TCMT IO Bool -> TCMT IO Bool) -> TCMT IO Bool -> TCMT IO Bool
    forall a b. (a -> b) -> a -> b
    $
            Lens' [Backend] TCState
    -> ([Backend] -> [Backend]) -> TCMT IO Bool -> TCMT IO Bool
    forall (m :: * -> *) a b.
    ReadTCState m =>
    Lens' a TCState -> (a -> a) -> m b -> m b
    locallyTCState Lens' [Backend] TCState
    stBackends         ([Backend] -> [Backend] -> [Backend]
    forall a b. a -> b -> a
    const ([Backend] -> [Backend] -> [Backend])
    -> [Backend] -> [Backend] -> [Backend]
    forall a b. (a -> b) -> a -> b
    $ [Backend]
    builtinBackends) (TCMT IO Bool -> TCMT IO Bool) -> TCMT IO Bool -> TCMT IO Bool
    forall a b. (a -> b) -> a -> b
    $
            QName -> TCMT IO Bool
    isErasable QName
    q
         -- Otherwise (Axiom, Datatype, Record type, etc.) we keep it
          Defn
    _ -> Bool -> TCMT IO Bool
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Bool
    False

    getUniqueCompilerPragma :: BackendName -> QName -> TCM (Maybe CompilerPragma)
    getUniqueCompilerPragma :: [Char] -> QName -> TCM (Maybe CompilerPragma)
    getUniqueCompilerPragma [Char]
    backend QName
    q = do
      [CompilerPragma]
    ps <- [Char] -> Definition -> [CompilerPragma]
    defCompilerPragmas [Char]
    backend (Definition -> [CompilerPragma])
    -> TCMT IO Definition -> TCMT IO [CompilerPragma]
    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
    q
      case [CompilerPragma]
    ps of
        []  -> Maybe CompilerPragma -> TCM (Maybe CompilerPragma)
    forall (m :: * -> *) a. Monad m => a -> m a
    return Maybe CompilerPragma
    forall a. Maybe a
    Nothing
        [CompilerPragma
    p] -> Maybe CompilerPragma -> TCM (Maybe CompilerPragma)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Maybe CompilerPragma -> TCM (Maybe CompilerPragma))
    -> Maybe CompilerPragma -> TCM (Maybe CompilerPragma)
    forall a b. (a -> b) -> a -> b
    $ CompilerPragma -> Maybe CompilerPragma
    forall a. a -> Maybe a
    Just CompilerPragma
    p
        (CompilerPragma
    _:CompilerPragma
    p1:[CompilerPragma]
    _) ->
          CompilerPragma
    -> TCM (Maybe CompilerPragma) -> TCM (Maybe CompilerPragma)
    forall (m :: * -> *) x a.
    (MonadTrace m, HasRange x) =>
    x -> m a -> m a
    setCurrentRange CompilerPragma
    p1 (TCM (Maybe CompilerPragma) -> TCM (Maybe CompilerPragma))
    -> TCM (Maybe CompilerPragma) -> TCM (Maybe CompilerPragma)
    forall a b. (a -> b) -> a -> b
    $
                Doc -> TCM (Maybe CompilerPragma)
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    Doc -> m a
    genericDocError (Doc -> TCM (Maybe CompilerPragma))
    -> TCMT IO Doc -> TCM (Maybe CompilerPragma)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< do
                      TCMT IO Doc -> Int -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *).
    Applicative m =>
    m Doc -> Int -> m Doc -> m Doc
    hang ([Char] -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => [Char] -> m Doc
    text ([Char]
    "Conflicting " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    backend [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    " pragmas for") TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> QName -> TCMT IO Doc
    forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
    pretty QName
    q TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> TCMT IO Doc
    "at") Int
    2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
    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 (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Range -> TCMT IO Doc
    forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
    pretty (CompilerPragma -> Range
    forall a. HasRange a => a -> Range
    getRange CompilerPragma
    p) | CompilerPragma
    p <- [CompilerPragma]
    ps ]

    setFunctionFlag :: FunctionFlag -> Bool -> QName -> TCM ()
    setFunctionFlag :: FunctionFlag -> Bool -> QName -> TCM ()
    setFunctionFlag FunctionFlag
    flag Bool
    val QName
    q = QName -> (Definition -> Definition) -> TCM ()
    forall (m :: * -> *).
    MonadTCState m =>
    QName -> (Definition -> Definition) -> m ()
    modifyGlobalDefinition QName
    q ((Definition -> Definition) -> TCM ())
    -> (Definition -> Definition) -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ Lens' Bool Definition -> LensSet Bool Definition
    forall i o. Lens' i o -> LensSet i o
    set ((Defn -> f Defn) -> Definition -> f Definition
    Lens' Defn Definition
    theDefLens ((Defn -> f Defn) -> Definition -> f Definition)
    -> ((Bool -> f Bool) -> Defn -> f Defn)
    -> (Bool -> f Bool)
    -> Definition
    -> f Definition
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . FunctionFlag -> Lens' Bool Defn
    funFlag FunctionFlag
    flag) Bool
    val

    markStatic :: QName -> TCM ()
    markStatic :: QName -> TCM ()
    markStatic = FunctionFlag -> Bool -> QName -> TCM ()
    setFunctionFlag FunctionFlag
    FunStatic Bool
    True

    markInline :: Bool -> QName -> TCM ()
    markInline :: Bool -> QName -> TCM ()
    markInline Bool
    b = FunctionFlag -> Bool -> QName -> TCM ()
    setFunctionFlag FunctionFlag
    FunInline Bool
    b

    markInjective :: QName -> TCM ()
    markInjective :: QName -> TCM ()
    markInjective QName
    q = QName -> (Definition -> Definition) -> TCM ()
    forall (m :: * -> *).
    MonadTCState m =>
    QName -> (Definition -> Definition) -> m ()
    modifyGlobalDefinition QName
    q ((Definition -> Definition) -> TCM ())
    -> (Definition -> Definition) -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ \Definition
    def -> Definition
    def { defInjective :: Bool
    defInjective = Bool
    True }

    unionSignatures :: [Signature] -> Signature
    unionSignatures :: [Signature] -> Signature
    unionSignatures [Signature]
    ss = (Signature -> Signature -> Signature)
    -> Signature -> [Signature] -> Signature
    forall (t :: * -> *) a b.
    Foldable t =>
    (a -> b -> b) -> b -> t a -> b
    foldr Signature -> Signature -> Signature
    unionSignature Signature
    emptySignature [Signature]
    ss
      where
        unionSignature :: Signature -> Signature -> Signature
    unionSignature (Sig Sections
    a Definitions
    b RewriteRuleMap
    c) (Sig Sections
    a' Definitions
    b' RewriteRuleMap
    c') =
          Sections -> Definitions -> RewriteRuleMap -> Signature
    Sig (Sections -> Sections -> Sections
    forall k a. Ord k => Map k a -> Map k a -> Map k a
    Map.union Sections
    a Sections
    a')
              (Definitions -> Definitions -> Definitions
    forall k v.
    (Eq k, Hashable k) =>
    HashMap k v -> HashMap k v -> HashMap k v
    HMap.union Definitions
    b Definitions
    b')              -- definitions are unique (in at most one module)
              ((RewriteRules -> RewriteRules -> RewriteRules)
    -> RewriteRuleMap -> RewriteRuleMap -> RewriteRuleMap
    forall k v.
    (Eq k, Hashable k) =>
    (v -> v -> v) -> HashMap k v -> HashMap k v -> HashMap k v
    HMap.unionWith RewriteRules -> RewriteRules -> RewriteRules
    forall a. Monoid a => a -> a -> a
    mappend RewriteRuleMap
    c RewriteRuleMap
    c')  -- rewrite rules are accumulated

    -- | Add a section to the signature.
    --
    --   The current context will be stored as the cumulative module parameters
    --   for this section.
    addSection :: ModuleName -> TCM ()
    addSection :: ModuleName -> TCM ()
    addSection ModuleName
    m = do
      Telescope
    tel <- TCMT IO Telescope
    forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Telescope
    getContextTelescope
      let sec :: Section
    sec = Telescope -> Section
    Section Telescope
    tel
      -- Make sure we do not overwrite an existing section!
      TCMT IO (Maybe Section) -> (Section -> TCM ()) -> TCM ()
    forall (m :: * -> *) a.
    Monad m =>
    m (Maybe a) -> (a -> m ()) -> m ()
    whenJustM (ModuleName -> TCMT IO (Maybe Section)
    forall (m :: * -> *).
    (Functor m, ReadTCState m) =>
    ModuleName -> m (Maybe Section)
    getSection ModuleName
    m) ((Section -> TCM ()) -> TCM ()) -> (Section -> TCM ()) -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ \ Section
    sec' -> do
        -- At least not with different content!
        if (Section
    sec Section -> Section -> Bool
    forall a. Eq a => a -> a -> Bool
    == Section
    sec') then do
          -- Andreas, 2015-12-02: test/Succeed/Issue1701II.agda
          -- reports a "redundantly adding existing section".
          [Char] -> Int -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "tc.section" Int
    10 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Doc
    "warning: redundantly adding existing 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 (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
    pretty ModuleName
    m
          [Char] -> Int -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "tc.section" Int
    60 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Doc
    "with content" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Section -> TCMT IO Doc
    forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
    pretty Section
    sec
        else do
          [Char] -> Int -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "impossible" Int
    10 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Doc
    "overwriting existing 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 (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
    pretty ModuleName
    m
          [Char] -> Int -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "impossible" Int
    60 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Doc
    "of content  " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Section -> TCMT IO Doc
    forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
    pretty Section
    sec'
          [Char] -> Int -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "impossible" Int
    60 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Doc
    "with content" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Section -> TCMT IO Doc
    forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
    pretty Section
    sec
          TCM ()
    forall a. HasCallStack => a
    __IMPOSSIBLE__
      -- Add the new section.
      ModuleName -> TCM ()
    setModuleCheckpoint ModuleName
    m
      (Signature -> Signature) -> TCM ()
    forall (m :: * -> *).
    MonadTCState m =>
    (Signature -> Signature) -> m ()
    modifySignature ((Signature -> Signature) -> TCM ())
    -> (Signature -> Signature) -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ Lens' Sections Signature -> LensMap Sections Signature
    forall i o. Lens' i o -> LensMap i o
    over Lens' Sections Signature
    sigSections LensMap Sections Signature -> LensMap Sections Signature
    forall a b. (a -> b) -> a -> b
    $ ModuleName -> Section -> Sections -> Sections
    forall k a. Ord k => k -> a -> Map k a -> Map k a
    Map.insert ModuleName
    m Section
    sec

    -- | Sets the checkpoint for the given module to the current checkpoint.
    setModuleCheckpoint :: ModuleName -> TCM ()
    setModuleCheckpoint :: ModuleName -> TCM ()
    setModuleCheckpoint ModuleName
    m = do
      CheckpointId
    chkpt <- Lens' CheckpointId TCEnv -> TCMT IO CheckpointId
    forall (m :: * -> *) a. MonadTCEnv m => Lens' a TCEnv -> m a
    viewTC Lens' CheckpointId TCEnv
    eCurrentCheckpoint
      Lens' (Map ModuleName CheckpointId) TCState
    stModuleCheckpoints Lens' (Map ModuleName CheckpointId) TCState
    -> (Map ModuleName CheckpointId -> Map ModuleName CheckpointId)
    -> TCM ()
    forall (m :: * -> *) a.
    MonadTCState m =>
    Lens' a TCState -> (a -> a) -> m ()
    `modifyTCLens` ModuleName
    -> CheckpointId
    -> Map ModuleName CheckpointId
    -> Map ModuleName CheckpointId
    forall k a. Ord k => k -> a -> Map k a -> Map k a
    Map.insert ModuleName
    m CheckpointId
    chkpt

    -- | Get a section.
    --
    --   Why Maybe? The reason is that we look up all prefixes of a module to
    --   compute number of parameters, and for hierarchical top-level modules,
    --   A.B.C say, A and A.B do not exist.
    {-# SPECIALIZE getSection :: ModuleName -> TCM (Maybe Section) #-}
    {-# SPECIALIZE getSection :: ModuleName -> ReduceM (Maybe Section) #-}
    getSection :: (Functor m, ReadTCState m) => ModuleName -> m (Maybe Section)
    getSection :: forall (m :: * -> *).
    (Functor m, ReadTCState m) =>
    ModuleName -> m (Maybe Section)
    getSection ModuleName
    m = do
      Sections
    sig  <- (TCState -> Lens' Sections TCState -> Sections
    forall o i. o -> Lens' i o -> i
    ^. (Signature -> f Signature) -> TCState -> f TCState
    Lens' Signature TCState
    stSignature ((Signature -> f Signature) -> TCState -> f TCState)
    -> ((Sections -> f Sections) -> Signature -> f Signature)
    -> (Sections -> f Sections)
    -> TCState
    -> f TCState
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Sections -> f Sections) -> Signature -> f Signature
    Lens' Sections Signature
    sigSections) (TCState -> Sections) -> m TCState -> m Sections
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> m TCState
    forall (m :: * -> *). ReadTCState m => m TCState
    getTCState
      Sections
    isig <- (TCState -> Lens' Sections TCState -> Sections
    forall o i. o -> Lens' i o -> i
    ^. (Signature -> f Signature) -> TCState -> f TCState
    Lens' Signature TCState
    stImports   ((Signature -> f Signature) -> TCState -> f TCState)
    -> ((Sections -> f Sections) -> Signature -> f Signature)
    -> (Sections -> f Sections)
    -> TCState
    -> f TCState
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Sections -> f Sections) -> Signature -> f Signature
    Lens' Sections Signature
    sigSections) (TCState -> Sections) -> m TCState -> m Sections
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> m TCState
    forall (m :: * -> *). ReadTCState m => m TCState
    getTCState
      Maybe Section -> m (Maybe Section)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Maybe Section -> m (Maybe Section))
    -> Maybe Section -> m (Maybe Section)
    forall a b. (a -> b) -> a -> b
    $ ModuleName -> Sections -> Maybe Section
    forall k a. Ord k => k -> Map k a -> Maybe a
    Map.lookup ModuleName
    m Sections
    sig Maybe Section -> Maybe Section -> Maybe Section
    forall (m :: * -> *) a. MonadPlus m => m a -> m a -> m a
    `mplus` ModuleName -> Sections -> Maybe Section
    forall k a. Ord k => k -> Map k a -> Maybe a
    Map.lookup ModuleName
    m Sections
    isig

    -- | Lookup a section telescope.
    --
    --   If it doesn't exist, like in hierarchical top-level modules,
    --   the section telescope is empty.
    {-# SPECIALIZE lookupSection :: ModuleName -> TCM Telescope #-}
    {-# SPECIALIZE lookupSection :: ModuleName -> ReduceM Telescope #-}
    lookupSection :: (Functor m, ReadTCState m) => ModuleName -> m Telescope
    lookupSection :: forall (m :: * -> *).
    (Functor m, ReadTCState m) =>
    ModuleName -> m Telescope
    lookupSection ModuleName
    m = Telescope -> (Section -> Telescope) -> Maybe Section -> Telescope
    forall b a. b -> (a -> b) -> Maybe a -> b
    maybe Telescope
    forall a. Tele a
    EmptyTel (Section -> Lens' Telescope Section -> Telescope
    forall o i. o -> Lens' i o -> i
    ^. Lens' Telescope Section
    secTelescope) (Maybe Section -> Telescope) -> m (Maybe Section) -> m Telescope
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> ModuleName -> m (Maybe Section)
    forall (m :: * -> *).
    (Functor m, ReadTCState m) =>
    ModuleName -> m (Maybe Section)
    getSection ModuleName
    m

    -- | Add display forms for a name @f@ copied by a module application. Essentially if @f@ can reduce to
    --
    -- @
    -- λ xs → A.B.C.f vs
    -- @
    --
    -- by unfolding module application copies (`defCopy`), then we add a display form
    --
    -- @
    -- A.B.C.f vs ==> f xs
    -- @
    addDisplayForms :: QName -> TCM ()
    addDisplayForms :: QName -> TCM ()
    addDisplayForms QName
    x = do
      [Char] -> Int -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "tc.display.section" Int
    20 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Doc
    "Computing display forms for" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> QName -> TCMT IO Doc
    forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
    pretty QName
    x
      Definition
    def <- QName -> TCMT IO Definition
    forall (m :: * -> *). HasConstInfo m => QName -> m Definition
    getConstInfo QName
    x
      let v :: Term
    v = case Definition -> Defn
    theDef Definition
    def of
                 Constructor{conSrcCon :: Defn -> ConHead
    conSrcCon = ConHead
    h} -> ConHead -> ConInfo -> Elims -> Term
    Con ConHead
    h{ conName :: QName
    conName = QName
    x } ConInfo
    ConOSystem []
                 Defn
    _                          -> QName -> Elims -> Term
    Def QName
    x []

      -- Compute all unfoldings of x by repeatedly calling reduceDefCopy
      [Term]
    vs <- QName -> Term -> TCM [Term]
    unfoldings QName
    x Term
    v
      [Char] -> Int -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "tc.display.section" Int
    20 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ 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] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    vcat
        [ TCMT IO Doc
    "unfoldings:" 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
    vcat [ TCMT IO Doc
    "-" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Term -> TCMT IO Doc
    forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
    pretty Term
    v | Term
    v <- [Term]
    vs ] ]

      -- Turn unfoldings into display forms
      Int
    npars <- Int -> Int -> Int
    forall a. Num a => a -> a -> a
    subtract (Definition -> Int
    projectionArgs Definition
    def) (Int -> Int) -> TCMT IO Int -> TCMT IO Int
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> TCMT IO Int
    forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Int
    getContextSize
      let dfs :: [(QName, DisplayForm)]
    dfs = [Maybe (QName, DisplayForm)] -> [(QName, DisplayForm)]
    forall a. [Maybe a] -> [a]
    catMaybes ([Maybe (QName, DisplayForm)] -> [(QName, DisplayForm)])
    -> [Maybe (QName, DisplayForm)] -> [(QName, DisplayForm)]
    forall a b. (a -> b) -> a -> b
    $ (Term -> Maybe (QName, DisplayForm))
    -> [Term] -> [Maybe (QName, DisplayForm)]
    forall a b. (a -> b) -> [a] -> [b]
    map (Int -> Term -> Term -> Maybe (QName, DisplayForm)
    displayForm Int
    npars Term
    v) [Term]
    vs
      [Char] -> Int -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "tc.display.section" Int
    20 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ 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] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    vcat
        [ TCMT IO Doc
    "displayForms:" 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
    vcat [ TCMT IO Doc
    "-" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> (QName -> TCMT IO Doc
    forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
    pretty QName
    y 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
    <?> DisplayForm -> TCMT IO Doc
    forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
    pretty DisplayForm
    df) | (QName
    y, DisplayForm
    df) <- [(QName, DisplayForm)]
    dfs ] ]

      -- and add them
      ((QName, DisplayForm) -> TCM ())
    -> [(QName, DisplayForm)] -> TCM ()
    forall (t :: * -> *) (m :: * -> *) a b.
    (Foldable t, Monad m) =>
    (a -> m b) -> t a -> m ()
    mapM_ ((QName -> DisplayForm -> TCM ()) -> (QName, DisplayForm) -> TCM ()
    forall a b c. (a -> b -> c) -> (a, b) -> c
    uncurry QName -> DisplayForm -> TCM ()
    addDisplayForm) [(QName, DisplayForm)]
    dfs
      where

        -- To get display forms for projections we need to unSpine here.
        view :: Term -> ([Arg ArgName], Term)
        view :: Term -> ([Arg [Char]], Term)
    view = (Term -> Term) -> ([Arg [Char]], Term) -> ([Arg [Char]], Term)
    forall (a :: * -> * -> *) b c d.
    Arrow a =>
    a b c -> a (d, b) (d, c)
    second Term -> Term
    unSpine (([Arg [Char]], Term) -> ([Arg [Char]], Term))
    -> (Term -> ([Arg [Char]], Term)) -> Term -> ([Arg [Char]], Term)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Term -> ([Arg [Char]], Term)
    lamView

        -- Given an unfolding `top = λ xs → y es` generate a display form
        -- `y es ==> top xs`. The first `npars` variables in `xs` are module parameters
        -- and should not be pattern variables, but matched literally.
        displayForm :: Nat -> Term -> Term -> Maybe (QName, DisplayForm)
        displayForm :: Int -> Term -> Term -> Maybe (QName, DisplayForm)
    displayForm Int
    npars Term
    top Term
    v =
          case Term -> ([Arg [Char]], Term)
    view Term
    v of
            ([Arg [Char]]
    xs, Def QName
    y Elims
    es)   -> (QName
    y,)         (DisplayForm -> (QName, DisplayForm))
    -> Maybe DisplayForm -> Maybe (QName, DisplayForm)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> [Arg [Char]] -> Elims -> Maybe DisplayForm
    mkDisplay [Arg [Char]]
    xs Elims
    es
            ([Arg [Char]]
    xs, Con ConHead
    h ConInfo
    i Elims
    es) -> (ConHead -> QName
    conName ConHead
    h,) (DisplayForm -> (QName, DisplayForm))
    -> Maybe DisplayForm -> Maybe (QName, DisplayForm)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> [Arg [Char]] -> Elims -> Maybe DisplayForm
    mkDisplay [Arg [Char]]
    xs Elims
    es
            ([Arg [Char]], Term)
    _ -> Maybe (QName, DisplayForm)
    forall a. HasCallStack => a
    __IMPOSSIBLE__
          where
            mkDisplay :: [Arg [Char]] -> Elims -> Maybe DisplayForm
    mkDisplay [Arg [Char]]
    xs Elims
    es = DisplayForm -> Maybe DisplayForm
    forall a. a -> Maybe a
    Just (Int -> Elims -> DisplayTerm -> DisplayForm
    Display (Int
    n Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - Int
    npars) Elims
    es (DisplayTerm -> DisplayForm) -> DisplayTerm -> DisplayForm
    forall a b. (a -> b) -> a -> b
    $ Term -> DisplayTerm
    DTerm (Term -> DisplayTerm) -> Term -> DisplayTerm
    forall a b. (a -> b) -> a -> b
    $ Term
    top Term -> [Arg Term] -> Term
    forall t. Apply t => t -> [Arg Term] -> t
    `apply` [Arg Term]
    args)
              where
                n :: Int
    n    = [Arg [Char]] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length [Arg [Char]]
    xs
                args :: [Arg Term]
    args = (Arg [Char] -> Int -> Arg Term)
    -> [Arg [Char]] -> [Int] -> [Arg Term]
    forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
    zipWith (\ Arg [Char]
    x Int
    i -> Int -> Term
    var Int
    i Term -> Arg [Char] -> Arg Term
    forall (f :: * -> *) a b. Functor f => a -> f b -> f a
    <$ Arg [Char]
    x) [Arg [Char]]
    xs (Int -> [Int]
    forall a. Integral a => a -> [a]
    downFrom Int
    n)

        -- Unfold a single defCopy.
        unfoldOnce :: Term -> TCM (Reduced () Term)
        unfoldOnce :: Term -> TCM (Reduced () Term)
    unfoldOnce Term
    v = case Term -> ([Arg [Char]], Term)
    view Term
    v of
          ([Arg [Char]]
    xs, Def QName
    f Elims
    es)   -> ((Reduced () Term -> Reduced () Term)
    -> TCM (Reduced () Term) -> TCM (Reduced () Term)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap ((Reduced () Term -> Reduced () Term)
     -> TCM (Reduced () Term) -> TCM (Reduced () Term))
    -> ((Term -> Term) -> Reduced () Term -> Reduced () Term)
    -> (Term -> Term)
    -> TCM (Reduced () Term)
    -> TCM (Reduced () Term)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Term -> Term) -> Reduced () Term -> Reduced () Term
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap) ([Arg [Char]] -> Term -> Term
    unlamView [Arg [Char]]
    xs) (QName -> Elims -> TCM (Reduced () Term)
    reduceDefCopyTCM QName
    f Elims
    es)
          ([Arg [Char]]
    xs, Con ConHead
    c ConInfo
    i Elims
    es) -> ((Reduced () Term -> Reduced () Term)
    -> TCM (Reduced () Term) -> TCM (Reduced () Term)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap ((Reduced () Term -> Reduced () Term)
     -> TCM (Reduced () Term) -> TCM (Reduced () Term))
    -> ((Term -> Term) -> Reduced () Term -> Reduced () Term)
    -> (Term -> Term)
    -> TCM (Reduced () Term)
    -> TCM (Reduced () Term)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Term -> Term) -> Reduced () Term -> Reduced () Term
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap) ([Arg [Char]] -> Term -> Term
    unlamView [Arg [Char]]
    xs) (QName -> Elims -> TCM (Reduced () Term)
    reduceDefCopyTCM (ConHead -> QName
    conName ConHead
    c) Elims
    es)
          ([Arg [Char]], Term)
    _                -> Reduced () Term -> TCM (Reduced () Term)
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Reduced () Term -> TCM (Reduced () Term))
    -> Reduced () Term -> TCM (Reduced () Term)
    forall a b. (a -> b) -> a -> b
    $ () -> Reduced () Term
    forall no yes. no -> Reduced no yes
    NoReduction ()

        -- Compute all reduceDefCopy unfoldings of `x`. Stop when we hit a non-copy.
        unfoldings :: QName -> Term -> TCM [Term]
        unfoldings :: QName -> Term -> TCM [Term]
    unfoldings QName
    x Term
    v = Term -> TCM (Reduced () Term)
    unfoldOnce Term
    v TCM (Reduced () Term)
    -> (Reduced () Term -> TCM [Term]) -> TCM [Term]
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \ case
          NoReduction{}     -> [Term] -> TCM [Term]
    forall (m :: * -> *) a. Monad m => a -> m a
    return []
          YesReduction Simplification
    _ Term
    v' -> do
            let headSymbol :: Maybe QName
    headSymbol = case ([Arg [Char]], Term) -> Term
    forall a b. (a, b) -> b
    snd (([Arg [Char]], Term) -> Term) -> ([Arg [Char]], Term) -> Term
    forall a b. (a -> b) -> a -> b
    $ Term -> ([Arg [Char]], Term)
    view Term
    v' of
                  Def QName
    y Elims
    _   -> QName -> Maybe QName
    forall a. a -> Maybe a
    Just QName
    y
                  Con ConHead
    y ConInfo
    _ Elims
    _ -> QName -> Maybe QName
    forall a. a -> Maybe a
    Just (ConHead -> QName
    conName ConHead
    y)
                  Term
    _         -> Maybe QName
    forall a. Maybe a
    Nothing
            case Maybe QName
    headSymbol of
              Maybe QName
    Nothing -> [Term] -> TCM [Term]
    forall (m :: * -> *) a. Monad m => a -> m a
    return []
              Just QName
    y | QName
    x QName -> QName -> Bool
    forall a. Eq a => a -> a -> Bool
    == QName
    y -> do
                -- This should never happen, but if it does, getting an __IMPOSSIBLE__ is much better
                -- than looping.
                [Char] -> Int -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "impossible" Int
    10 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ 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] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    vcat
                  [ TCMT IO Doc
    "reduceDefCopy said YesReduction but the head symbol is the same!?"
                  , 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
    "v  =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Term -> TCMT IO Doc
    forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
    pretty Term
    v
                  , 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
    "v' =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Term -> TCMT IO Doc
    forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
    pretty Term
    v'
                  ]
                TCM [Term]
    forall a. HasCallStack => a
    __IMPOSSIBLE__
              Just QName
    y -> do
                TCMT IO Bool -> TCM [Term] -> TCM [Term] -> TCM [Term]
    forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
    ifM (Definition -> Bool
    defCopy (Definition -> Bool) -> TCMT IO Definition -> TCMT IO Bool
    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
    y)
                    ((Term
    v' Term -> [Term] -> [Term]
    forall a. a -> [a] -> [a]
    :) ([Term] -> [Term]) -> TCM [Term] -> TCM [Term]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> QName -> Term -> TCM [Term]
    unfoldings QName
    y Term
    v')  -- another copy so keep going
                    ([Term] -> TCM [Term]
    forall (m :: * -> *) a. Monad m => a -> m a
    return [Term
    v'])                 -- not a copy, we stop

    -- | Module application (followed by module parameter abstraction).
    applySection
      :: ModuleName     -- ^ Name of new module defined by the module macro.
      -> Telescope      -- ^ Parameters of new module.
      -> ModuleName     -- ^ Name of old module applied to arguments.
      -> Args           -- ^ Arguments of module application.
      -> ScopeCopyInfo  -- ^ Imported names and modules
      -> TCM ()
    applySection :: ModuleName
    -> Telescope -> ModuleName -> [Arg Term] -> ScopeCopyInfo -> TCM ()
    applySection ModuleName
    new Telescope
    ptel ModuleName
    old [Arg Term]
    ts ScopeCopyInfo{ renModules :: ScopeCopyInfo -> Ren ModuleName
    renModules = Ren ModuleName
    rm, renNames :: ScopeCopyInfo -> Ren QName
    renNames = Ren QName
    rd } = do
      Ren QName
    rd <- Ren QName -> TCM (Ren QName)
    closeConstructors Ren QName
    rd
      ModuleName
    -> Telescope -> ModuleName -> [Arg Term] -> ScopeCopyInfo -> TCM ()
    applySection' ModuleName
    new Telescope
    ptel ModuleName
    old [Arg Term]
    ts ScopeCopyInfo :: Ren ModuleName -> Ren QName -> ScopeCopyInfo
    ScopeCopyInfo{ renModules :: Ren ModuleName
    renModules = Ren ModuleName
    rm, renNames :: Ren QName
    renNames = Ren QName
    rd }
      where
        -- If a datatype is being copied, all its constructors need to be copied,
        -- and if a constructor is copied its datatype needs to be.
        closeConstructors :: Ren QName -> TCM (Ren QName)
        closeConstructors :: Ren QName -> TCM (Ren QName)
    closeConstructors Ren QName
    rd = do
            [QName]
    ds <- (QName -> QName) -> [QName] -> [QName]
    forall b a. Ord b => (a -> b) -> [a] -> [a]
    nubOn QName -> QName
    forall a. a -> a
    id ([QName] -> [QName])
    -> ([Maybe QName] -> [QName]) -> [Maybe QName] -> [QName]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [Maybe QName] -> [QName]
    forall a. [Maybe a] -> [a]
    catMaybes ([Maybe QName] -> [QName])
    -> TCMT IO [Maybe QName] -> TCMT IO [QName]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (QName -> TCMT IO (Maybe QName))
    -> [QName] -> TCMT IO [Maybe QName]
    forall (t :: * -> *) (f :: * -> *) a b.
    (Traversable t, Applicative f) =>
    (a -> f b) -> t a -> f (t b)
    traverse QName -> TCMT IO (Maybe QName)
    constructorData (Ren QName -> [QName]
    forall k a. Map k a -> [k]
    Map.keys Ren QName
    rd)
            [QName]
    cs <- (QName -> QName) -> [QName] -> [QName]
    forall b a. Ord b => (a -> b) -> [a] -> [a]
    nubOn QName -> QName
    forall a. a -> a
    id ([QName] -> [QName])
    -> ([[QName]] -> [QName]) -> [[QName]] -> [QName]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [[QName]] -> [QName]
    forall (t :: * -> *) a. Foldable t => t [a] -> [a]
    concat    ([[QName]] -> [QName]) -> TCMT IO [[QName]] -> TCMT IO [QName]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (QName -> TCMT IO [QName]) -> [QName] -> TCMT IO [[QName]]
    forall (t :: * -> *) (f :: * -> *) a b.
    (Traversable t, Applicative f) =>
    (a -> f b) -> t a -> f (t b)
    traverse QName -> TCMT IO [QName]
    dataConstructors (Ren QName -> [QName]
    forall k a. Map k a -> [k]
    Map.keys Ren QName
    rd)
            Ren QName
    new <- (List1 QName -> List1 QName -> List1 QName)
    -> [Ren QName] -> Ren QName
    forall (f :: * -> *) k a.
    (Foldable f, Ord k) =>
    (a -> a -> a) -> f (Map k a) -> Map k a
    Map.unionsWith List1 QName -> List1 QName -> List1 QName
    forall a. Semigroup a => a -> a -> a
    (<>) ([Ren QName] -> Ren QName)
    -> TCMT IO [Ren QName] -> TCM (Ren QName)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (QName -> TCM (Ren QName)) -> [QName] -> TCMT IO [Ren QName]
    forall (t :: * -> *) (f :: * -> *) a b.
    (Traversable t, Applicative f) =>
    (a -> f b) -> t a -> f (t b)
    traverse QName -> TCM (Ren QName)
    rename ([QName]
    ds [QName] -> [QName] -> [QName]
    forall a. [a] -> [a] -> [a]
    ++ [QName]
    cs)
            [Char] -> Int -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "tc.mod.apply.complete" Int
    30 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    forall a b. (a -> b) -> a -> b
    $
              TCMT IO Doc
    "also copying: " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Ren QName -> TCMT IO Doc
    forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
    pretty Ren QName
    new
            Ren QName -> TCM (Ren QName)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Ren QName -> TCM (Ren QName)) -> Ren QName -> TCM (Ren QName)
    forall a b. (a -> b) -> a -> b
    $ (List1 QName -> List1 QName -> List1 QName)
    -> Ren QName -> Ren QName -> Ren QName
    forall k a. Ord k => (a -> a -> a) -> Map k a -> Map k a -> Map k a
    Map.unionWith List1 QName -> List1 QName -> List1 QName
    forall a. Semigroup a => a -> a -> a
    (<>) Ren QName
    new Ren QName
    rd
          where
            rename :: QName -> TCM (Ren QName)
            rename :: QName -> TCM (Ren QName)
    rename QName
    x
              | QName
    x QName -> Ren QName -> Bool
    forall k a. Ord k => k -> Map k a -> Bool
    `Map.member` Ren QName
    rd = Ren QName -> TCM (Ren QName)
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Ren QName
    forall a. Monoid a => a
    mempty
              | Bool
    otherwise =
                  QName -> List1 QName -> Ren QName
    forall k a. k -> a -> Map k a
    Map.singleton QName
    x (List1 QName -> Ren QName)
    -> (Name -> List1 QName) -> Name -> Ren QName
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . QName -> List1 QName
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (QName -> List1 QName) -> (Name -> QName) -> Name -> List1 QName
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . List1 Name -> QName
    qnameFromList (List1 Name -> QName) -> (Name -> List1 Name) -> Name -> QName
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Name -> List1 Name
    forall el coll. Singleton el coll => el -> coll
    singleton (Name -> Ren QName) -> TCMT IO Name -> TCM (Ren QName)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> [Char] -> TCMT IO Name
    forall a (m :: * -> *).
    (FreshName a, MonadFresh NameId m) =>
    a -> m Name
    freshName_ (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)

            constructorData :: QName -> TCM (Maybe QName)
            constructorData :: QName -> TCMT IO (Maybe QName)
    constructorData QName
    x = do
              (Definition -> Defn
    theDef (Definition -> Defn) -> TCMT IO Definition -> TCMT IO Defn
    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) TCMT IO Defn -> (Defn -> Maybe QName) -> TCMT IO (Maybe QName)
    forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
    <&> \case
                Constructor{ conData :: Defn -> QName
    conData = QName
    d } -> QName -> Maybe QName
    forall a. a -> Maybe a
    Just QName
    d
                Defn
    _                          -> Maybe QName
    forall a. Maybe a
    Nothing

            dataConstructors :: QName -> TCM [QName]
            dataConstructors :: QName -> TCMT IO [QName]
    dataConstructors QName
    x = do
              (Definition -> Defn
    theDef (Definition -> Defn) -> TCMT IO Definition -> TCMT IO Defn
    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) TCMT IO Defn -> (Defn -> [QName]) -> TCMT IO [QName]
    forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
    <&> \case
                Datatype{ dataCons :: Defn -> [QName]
    dataCons = [QName]
    cs } -> [QName]
    cs
                Record{ recConHead :: Defn -> ConHead
    recConHead = ConHead
    h }  -> [ConHead -> QName
    conName ConHead
    h]
                Defn
    _                         -> []

    applySection' :: ModuleName -> Telescope -> ModuleName -> Args -> ScopeCopyInfo -> TCM ()
    applySection' :: ModuleName
    -> Telescope -> ModuleName -> [Arg Term] -> ScopeCopyInfo -> TCM ()
    applySection' ModuleName
    new Telescope
    ptel ModuleName
    old [Arg Term]
    ts ScopeCopyInfo{ renNames :: ScopeCopyInfo -> Ren QName
    renNames = Ren QName
    rd, renModules :: ScopeCopyInfo -> Ren ModuleName
    renModules = Ren ModuleName
    rm } = do
      do
        [QName]
    noCopyList <- [Maybe QName] -> [QName]
    forall a. [Maybe a] -> [a]
    catMaybes ([Maybe QName] -> [QName])
    -> TCMT IO [Maybe QName] -> TCMT IO [QName]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> ([Char] -> TCMT IO (Maybe QName))
    -> [[Char]] -> TCMT IO [Maybe QName]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    mapM [Char] -> TCMT IO (Maybe QName)
    forall (m :: * -> *). HasBuiltins m => [Char] -> m (Maybe QName)
    getName' [[Char]]
    constrainedPrims
        [QName] -> (QName -> TCM ()) -> TCM ()
    forall (t :: * -> *) (f :: * -> *) a b.
    (Foldable t, Applicative f) =>
    t a -> (a -> f b) -> f ()
    for_ (Ren QName -> [QName]
    forall k a. Map k a -> [k]
    Map.keys Ren QName
    rd) ((QName -> TCM ()) -> TCM ()) -> (QName -> TCM ()) -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ \ QName
    q ->
          Bool -> TCM () -> TCM ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    when (QName
    q QName -> [QName] -> Bool
    forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
    `elem` [QName]
    noCopyList) (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ TypeError -> TCM ()
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    TypeError -> m a
    typeError (QName -> TypeError
    TriedToCopyConstrainedPrim QName
    q)

      [Char] -> Int -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "tc.mod.apply" 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
    vcat
        [ TCMT IO Doc
    "applySection"
        , TCMT IO Doc
    "new  =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> ModuleName -> TCMT IO Doc
    forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
    pretty ModuleName
    new
        , TCMT IO Doc
    "ptel =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Telescope -> TCMT IO Doc
    forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
    pretty Telescope
    ptel
        , TCMT IO Doc
    "old  =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> ModuleName -> TCMT IO Doc
    forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
    pretty ModuleName
    old
        , TCMT IO Doc
    "ts   =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> [Arg Term] -> TCMT IO Doc
    forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
    pretty [Arg Term]
    ts
        ]
      Map QName (NonEmpty ())
    _ <- (QName -> List1 QName -> TCMT IO (NonEmpty ()))
    -> Ren QName -> TCMT IO (Map QName (NonEmpty ()))
    forall (t :: * -> *) k a b.
    Applicative t =>
    (k -> a -> t b) -> Map k a -> t (Map k b)
    Map.traverseWithKey ((QName -> TCM ()) -> List1 QName -> TCMT IO (NonEmpty ())
    forall (t :: * -> *) (f :: * -> *) a b.
    (Traversable t, Applicative f) =>
    (a -> f b) -> t a -> f (t b)
    traverse ((QName -> TCM ()) -> List1 QName -> TCMT IO (NonEmpty ()))
    -> (QName -> QName -> TCM ())
    -> QName
    -> List1 QName
    -> TCMT IO (NonEmpty ())
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [Arg Term] -> QName -> QName -> TCM ()
    copyDef [Arg Term]
    ts) Ren QName
    rd
      Map ModuleName (NonEmpty ())
    _ <- (ModuleName -> NonEmpty ModuleName -> TCMT IO (NonEmpty ()))
    -> Ren ModuleName -> TCMT IO (Map ModuleName (NonEmpty ()))
    forall (t :: * -> *) k a b.
    Applicative t =>
    (k -> a -> t b) -> Map k a -> t (Map k b)
    Map.traverseWithKey ((ModuleName -> TCM ())
    -> NonEmpty ModuleName -> TCMT IO (NonEmpty ())
    forall (t :: * -> *) (f :: * -> *) a b.
    (Traversable t, Applicative f) =>
    (a -> f b) -> t a -> f (t b)
    traverse ((ModuleName -> TCM ())
     -> NonEmpty ModuleName -> TCMT IO (NonEmpty ()))
    -> (ModuleName -> ModuleName -> TCM ())
    -> ModuleName
    -> NonEmpty ModuleName
    -> TCMT IO (NonEmpty ())
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [Arg Term] -> ModuleName -> ModuleName -> TCM ()
    copySec [Arg Term]
    ts) Ren ModuleName
    rm
      [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 (Ren QName -> [List1 QName]
    forall k a. Map k a -> [a]
    Map.elems Ren QName
    rd [List1 QName] -> (List1 QName -> [QName]) -> [QName]
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= List1 QName -> [QName]
    forall a. NonEmpty a -> [a]
    List1.toList)
      where
        -- Andreas, 2013-10-29
        -- Here, if the name x is not imported, it persists as
        -- old, possibly out-of-scope name.
        -- This old name may used by the case split tactic, leading to
        -- names that cannot be printed properly.
        -- I guess it would make sense to mark non-imported names
        -- as such (out-of-scope) and let splitting fail if it would
        -- produce out-of-scope constructors.
        --
        -- Taking 'List1.head' because 'Module.Data.cons' and 'Module.cons' are
        -- equivalent valid names and either can be used.
        copyName :: QName -> QName
    copyName QName
    x = QName -> (List1 QName -> QName) -> Maybe (List1 QName) -> QName
    forall b a. b -> (a -> b) -> Maybe a -> b
    maybe QName
    x List1 QName -> QName
    forall a. NonEmpty a -> a
    List1.head (QName -> Ren QName -> Maybe (List1 QName)
    forall k a. Ord k => k -> Map k a -> Maybe a
    Map.lookup QName
    x Ren QName
    rd)

        argsToUse :: ModuleName -> TCMT IO Int
    argsToUse ModuleName
    x = do
          let m :: ModuleName
    m = ModuleName -> ModuleName -> ModuleName
    commonParentModule ModuleName
    old ModuleName
    x
          [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
    "Common prefix: " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> ModuleName -> TCMT IO Doc
    forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
    pretty ModuleName
    m
          Telescope -> Int
    forall a. Sized a => a -> Int
    size (Telescope -> Int) -> TCMT IO Telescope -> TCMT IO Int
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> ModuleName -> TCMT IO Telescope
    forall (m :: * -> *).
    (Functor m, ReadTCState m) =>
    ModuleName -> m Telescope
    lookupSection ModuleName
    m

        copyDef :: Args -> QName -> QName -> TCM ()
        copyDef :: [Arg Term] -> QName -> QName -> TCM ()
    copyDef [Arg Term]
    ts QName
    x QName
    y = do
          Definition
    def <- QName -> TCMT IO Definition
    forall (m :: * -> *). HasConstInfo m => QName -> m Definition
    getConstInfo QName
    x
          Int
    np  <- ModuleName -> TCMT IO Int
    argsToUse (QName -> ModuleName
    qnameModule QName
    x)
          -- Issue #3083: We need to use the hiding from the telescope of the
          -- original module. This can be different than the hiding for the common
          -- parent in the case of record modules.
          [Hiding]
    hidings <- (Dom ([Char], Type) -> Hiding) -> [Dom ([Char], Type)] -> [Hiding]
    forall a b. (a -> b) -> [a] -> [b]
    map Dom ([Char], Type) -> Hiding
    forall a. LensHiding a => a -> Hiding
    getHiding ([Dom ([Char], Type)] -> [Hiding])
    -> (Telescope -> [Dom ([Char], Type)]) -> Telescope -> [Hiding]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Telescope -> [Dom ([Char], Type)]
    forall t. Tele (Dom t) -> [Dom ([Char], t)]
    telToList (Telescope -> [Hiding]) -> TCMT IO Telescope -> TCMT IO [Hiding]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> ModuleName -> TCMT IO Telescope
    forall (m :: * -> *).
    (Functor m, ReadTCState m) =>
    ModuleName -> m Telescope
    lookupSection (QName -> ModuleName
    qnameModule QName
    x)
          let ts' :: [Arg Term]
    ts' = (Hiding -> Arg Term -> Arg Term)
    -> [Hiding] -> [Arg Term] -> [Arg Term]
    forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
    zipWith Hiding -> Arg Term -> Arg Term
    forall a. LensHiding a => Hiding -> a -> a
    setHiding [Hiding]
    hidings [Arg Term]
    ts
          Telescope
    commonTel <- ModuleName -> TCMT IO Telescope
    forall (m :: * -> *).
    (Functor m, ReadTCState m) =>
    ModuleName -> m Telescope
    lookupSection (ModuleName -> ModuleName -> ModuleName
    commonParentModule ModuleName
    old (ModuleName -> ModuleName) -> ModuleName -> ModuleName
    forall a b. (a -> b) -> a -> b
    $ QName -> ModuleName
    qnameModule QName
    x)
          [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] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    vcat
            [ TCMT IO Doc
    "copyDef" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> QName -> TCMT IO Doc
    forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
    pretty 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
    <+> QName -> TCMT IO Doc
    forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
    pretty QName
    y
            , TCMT IO Doc
    "ts' = " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> [Arg Term] -> TCMT IO Doc
    forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
    pretty [Arg Term]
    ts' ]
          [Arg Term] -> Int -> Definition -> TCM ()
    copyDef' [Arg Term]
    ts' Int
    np Definition
    def
          where
            copyDef' :: [Arg Term] -> Int -> Definition -> TCM ()
    copyDef' [Arg Term]
    ts Int
    np Definition
    d = do
              [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
    "making new def for" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> QName -> TCMT IO Doc
    forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
    pretty QName
    y TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> TCMT IO Doc
    "from" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> QName -> TCMT IO Doc
    forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
    pretty QName
    x TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> TCMT IO Doc
    "with" 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 (Int -> [Char]
    forall a. Show a => a -> [Char]
    show Int
    np) TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> 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 (IsAbstract -> [Char]
    forall a. Show a => a -> [Char]
    show (IsAbstract -> [Char]) -> IsAbstract -> [Char]
    forall a b. (a -> b) -> a -> b
    $ Definition -> IsAbstract
    defAbstract Definition
    d)
              [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] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    vcat
                [ 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]
    ts')
                , TCMT IO Doc
    "old type = " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Type -> TCMT IO Doc
    forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
    pretty (Definition -> Type
    defType Definition
    d) ]
              [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
    "new type = " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Type -> TCMT IO Doc
    forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
    pretty Type
    t
              QName -> Definition -> TCM ()
    addConstant QName
    y (Definition -> TCM ()) -> TCMT IO Definition -> TCM ()
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< QName -> TCMT IO Definition
    nd QName
    y
              QName -> TCM ()
    makeProjection QName
    y
              -- Issue1238: the copied def should be an 'instance' if the original
              -- def is one. Skip constructors since the original constructor will
              -- still work as an instance.
              -- Issue5583: Don't skip constructures, because the original constructor doesn't always
              -- work. For instance if it's only available in an anonymous module generated by
              -- `open import M args`.
              Maybe QName -> (QName -> TCM ()) -> TCM ()
    forall (m :: * -> *) a. Monad m => Maybe a -> (a -> m ()) -> m ()
    whenJust Maybe QName
    inst ((QName -> TCM ()) -> TCM ()) -> (QName -> TCM ()) -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ \ QName
    c -> QName -> QName -> TCM ()
    addNamedInstance QName
    y QName
    c
              -- Set display form for the old name if it's not a constructor.
    {- BREAKS fail/Issue478
              -- Andreas, 2012-10-20 and if we are not an anonymous module
              -- unless (isAnonymousModuleName new || isCon || size ptel > 0) $ do
    -}
              -- BREAKS fail/Issue1643a
              -- -- Andreas, 2015-09-09 Issue 1643:
              -- -- Do not add a display form for a bare module alias.
              -- when (not isCon && size ptel == 0 && not (null ts)) $ do
              Bool -> TCM () -> TCM ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    when (Telescope -> Int
    forall a. Sized a => a -> Int
    size Telescope
    ptel Int -> Int -> Bool
    forall a. Eq a => a -> a -> Bool
    == Int
    0) (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ do
                QName -> TCM ()
    addDisplayForms QName
    y
              where
                ts' :: [Arg Term]
    ts' = Int -> [Arg Term] -> [Arg Term]
    forall a. Int -> [a] -> [a]
    take Int
    np [Arg Term]
    ts
                t :: Type
    t   = Definition -> Type
    defType Definition
    d Type -> [Arg Term] -> Type
    `piApply` [Arg Term]
    ts'
                pol :: [Polarity]
    pol = Definition -> [Polarity]
    defPolarity Definition
    d [Polarity] -> [Arg Term] -> [Polarity]
    forall t. Apply t => t -> [Arg Term] -> t
    `apply` [Arg Term]
    ts'
                occ :: [Occurrence]
    occ = Definition -> [Occurrence]
    defArgOccurrences Definition
    d [Occurrence] -> [Arg Term] -> [Occurrence]
    forall t. Apply t => t -> [Arg Term] -> t
    `apply` [Arg Term]
    ts'
                gen :: NumGeneralizableArgs
    gen = Definition -> NumGeneralizableArgs
    defArgGeneralizable Definition
    d NumGeneralizableArgs -> [Arg Term] -> NumGeneralizableArgs
    forall t. Apply t => t -> [Arg Term] -> t
    `apply` [Arg Term]
    ts'
                inst :: Maybe QName
    inst = Definition -> Maybe QName
    defInstance Definition
    d
                -- the name is set by the addConstant function
                nd :: QName -> TCM Definition
                nd :: QName -> TCMT IO Definition
    nd QName
    y = do
                  -- The arguments may use some feature of the current
                  -- language.
                  Language
    lang <- TCMT IO Language
    forall (m :: * -> *). HasOptions m => m Language
    getLanguage
                  TCMT IO Defn -> (Defn -> Definition) -> TCMT IO Definition
    forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
    for TCMT IO Defn
    def ((Defn -> Definition) -> TCMT IO Definition)
    -> (Defn -> Definition) -> TCMT IO Definition
    forall a b. (a -> b) -> a -> b
    $ \ Defn
    df -> Defn :: ArgInfo
    -> QName
    -> Type
    -> [Polarity]
    -> [Occurrence]
    -> NumGeneralizableArgs
    -> [Maybe Name]
    -> [LocalDisplayForm]
    -> MutualId
    -> CompiledRepresentation
    -> Maybe QName
    -> Bool
    -> Set QName
    -> Bool
    -> Bool
    -> Bool
    -> Blocked_
    -> Language
    -> Defn
    -> Definition
    Defn
                        { defArgInfo :: ArgInfo
    defArgInfo        = Definition -> ArgInfo
    defArgInfo Definition
    d
                        , defName :: QName
    defName           = QName
    y
                        , defType :: Type
    defType           = Type
    t
                        , defPolarity :: [Polarity]
    defPolarity       = [Polarity]
    pol
                        , defArgOccurrences :: [Occurrence]
    defArgOccurrences = [Occurrence]
    occ
                        , defArgGeneralizable :: NumGeneralizableArgs
    defArgGeneralizable = NumGeneralizableArgs
    gen
                        , defGeneralizedParams :: [Maybe Name]
    defGeneralizedParams = [] -- This is only needed for type checking data/record defs so no need to copy it.
                        , defDisplay :: [LocalDisplayForm]
    defDisplay        = []
                        , defMutual :: MutualId
    defMutual         = -MutualId
    1   -- TODO: mutual block?
                        , defCompiledRep :: CompiledRepresentation
    defCompiledRep    = CompiledRepresentation
    noCompiledRep
                        , defInstance :: Maybe QName
    defInstance       = Maybe QName
    inst
                        , defCopy :: Bool
    defCopy           = Bool
    True
                        , defMatchable :: Set QName
    defMatchable      = Set QName
    forall a. Set a
    Set.empty
                        , defNoCompilation :: Bool
    defNoCompilation  = Definition -> Bool
    defNoCompilation Definition
    d
                        , defInjective :: Bool
    defInjective      = Bool
    False
                        , defCopatternLHS :: Bool
    defCopatternLHS   = [Clause] -> Bool
    isCopatternLHS [Clause
    cl]
                        , defBlocked :: Blocked_
    defBlocked        = Definition -> Blocked_
    defBlocked Definition
    d
                        , defLanguage :: Language
    defLanguage       =
                          case Definition -> Language
    defLanguage Definition
    d of
                            -- Note that Cubical Agda code can be imported
                            -- when --erased-cubical is used.
                            l :: Language
    l@(Cubical Cubical
    CFull) -> Language
    l
                            Cubical Cubical
    CErased   -> Language
    lang
                            Language
    WithoutK          -> Language
    lang
                            Language
    WithK             -> Language
    lang
                        , theDef :: Defn
    theDef            = Defn
    df }
                oldDef :: Defn
    oldDef = Definition -> Defn
    theDef Definition
    d
                isCon :: Bool
    isCon  = case Defn
    oldDef of { Constructor{} -> Bool
    True ; Defn
    _ -> Bool
    False }
                mutual :: Maybe [QName]
    mutual = case Defn
    oldDef of { Function{funMutual :: Defn -> Maybe [QName]
    funMutual = Maybe [QName]
    m} -> Maybe [QName]
    m              ; Defn
    _ -> Maybe [QName]
    forall a. Maybe a
    Nothing }
                extlam :: Maybe ExtLamInfo
    extlam = case Defn
    oldDef of { Function{funExtLam :: Defn -> Maybe ExtLamInfo
    funExtLam = Maybe ExtLamInfo
    e} -> Maybe ExtLamInfo
    e              ; Defn
    _ -> Maybe ExtLamInfo
    forall a. Maybe a
    Nothing }
                with :: Maybe QName
    with   = case Defn
    oldDef of { Function{funWith :: Defn -> Maybe QName
    funWith = Maybe QName
    w}   -> QName -> QName
    copyName (QName -> QName) -> Maybe QName -> Maybe QName
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Maybe QName
    w ; Defn
    _ -> Maybe QName
    forall a. Maybe a
    Nothing }
                -- Andreas, 2015-05-11, to fix issue 1413:
                -- Even if we apply the record argument (must be @var 0@), we stay a projection.
                -- This is because we may abstract the record argument later again.
                -- See succeed/ProjectionNotNormalized.agda
                isVar0 :: Arg Term -> Bool
    isVar0 Arg Term
    t = case Arg Term -> Term
    forall e. Arg e -> e
    unArg Arg Term
    t of Var Int
    0 [] -> Bool
    True; Term
    _ -> Bool
    False
                proj :: Maybe Projection
    proj   = case Defn
    oldDef of
                  Function{funProjection :: Defn -> Maybe Projection
    funProjection = Just p :: Projection
    p@Projection{projIndex :: Projection -> Int
    projIndex = Int
    n}}
                    | [Arg Term] -> Int
    forall a. Sized a => a -> Int
    size [Arg Term]
    ts' Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    < Int
    n Bool -> Bool -> Bool
    || ([Arg Term] -> Int
    forall a. Sized a => a -> Int
    size [Arg Term]
    ts' Int -> Int -> Bool
    forall a. Eq a => a -> a -> Bool
    == Int
    n Bool -> Bool -> Bool
    && Bool -> (Arg Term -> Bool) -> Maybe (Arg Term) -> Bool
    forall b a. b -> (a -> b) -> Maybe a -> b
    maybe Bool
    True Arg Term -> Bool
    isVar0 ([Arg Term] -> Maybe (Arg Term)
    forall a. [a] -> Maybe a
    lastMaybe [Arg Term]
    ts'))
                    -> Projection -> Maybe Projection
    forall a. a -> Maybe a
    Just (Projection -> Maybe Projection) -> Projection -> Maybe Projection
    forall a b. (a -> b) -> a -> b
    $ Projection
    p { projIndex :: Int
    projIndex = Int
    n Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - [Arg Term] -> Int
    forall a. Sized a => a -> Int
    size [Arg Term]
    ts'
                                , projLams :: ProjLams
    projLams  = Projection -> ProjLams
    projLams Projection
    p ProjLams -> [Arg Term] -> ProjLams
    forall t. Apply t => t -> [Arg Term] -> t
    `apply` [Arg Term]
    ts'
                                , projProper :: Maybe QName
    projProper= QName -> QName
    copyName (QName -> QName) -> Maybe QName -> Maybe QName
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Projection -> Maybe QName
    projProper Projection
    p
                                }
                  Defn
    _ -> Maybe Projection
    forall a. Maybe a
    Nothing
                def :: TCMT IO Defn
    def =
                  case Defn
    oldDef of
                    Constructor{ conPars :: Defn -> Int
    conPars = Int
    np, conData :: Defn -> QName
    conData = QName
    d } -> Defn -> TCMT IO Defn
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Defn -> TCMT IO Defn) -> Defn -> TCMT IO Defn
    forall a b. (a -> b) -> a -> b
    $
                      Defn
    oldDef { conPars :: Int
    conPars = Int
    np Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - [Arg Term] -> Int
    forall a. Sized a => a -> Int
    size [Arg Term]
    ts'
                             , conData :: QName
    conData = QName -> QName
    copyName QName
    d
                             }
                    Datatype{ dataPars :: Defn -> Int
    dataPars = Int
    np, dataCons :: Defn -> [QName]
    dataCons = [QName]
    cs } -> Defn -> TCMT IO Defn
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Defn -> TCMT IO Defn) -> Defn -> TCMT IO Defn
    forall a b. (a -> b) -> a -> b
    $
                      Defn
    oldDef { dataPars :: Int
    dataPars   = Int
    np Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - [Arg Term] -> Int
    forall a. Sized a => a -> Int
    size [Arg Term]
    ts'
                             , dataClause :: Maybe Clause
    dataClause = Clause -> Maybe Clause
    forall a. a -> Maybe a
    Just Clause
    cl
                             , dataCons :: [QName]
    dataCons   = (QName -> QName) -> [QName] -> [QName]
    forall a b. (a -> b) -> [a] -> [b]
    map QName -> QName
    copyName [QName]
    cs
                             }
                    Record{ recPars :: Defn -> Int
    recPars = Int
    np, recTel :: Defn -> Telescope
    recTel = Telescope
    tel } -> Defn -> TCMT IO Defn
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Defn -> TCMT IO Defn) -> Defn -> TCMT IO Defn
    forall a b. (a -> b) -> a -> b
    $
                      Defn
    oldDef { recPars :: Int
    recPars    = Int
    np Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - [Arg Term] -> Int
    forall a. Sized a => a -> Int
    size [Arg Term]
    ts'
                             , recClause :: Maybe Clause
    recClause  = Clause -> Maybe Clause
    forall a. a -> Maybe a
    Just Clause
    cl
                             , recTel :: Telescope
    recTel     = Telescope -> [Arg Term] -> Telescope
    forall t. Apply t => t -> [Arg Term] -> t
    apply Telescope
    tel [Arg Term]
    ts'
                             }
                    Defn
    GeneralizableVar -> Defn -> TCMT IO Defn
    forall (m :: * -> *) a. Monad m => a -> m a
    return Defn
    GeneralizableVar
                    Defn
    _ -> do
                      (Maybe SplitTree
    mst, Bool
    _, CompiledClauses
    cc) <- Maybe (QName, Type)
    -> [Clause] -> TCM (Maybe SplitTree, Bool, CompiledClauses)
    compileClauses Maybe (QName, Type)
    forall a. Maybe a
    Nothing [Clause
    cl] -- Andreas, 2012-10-07 non need for record pattern translation
                      let newDef :: Defn
    newDef =
                            Lens' Bool Defn -> LensSet Bool Defn
    forall i o. Lens' i o -> LensSet i o
    set Lens' Bool Defn
    funMacro  (Defn
    oldDef Defn -> Lens' Bool Defn -> Bool
    forall o i. o -> Lens' i o -> i
    ^. Lens' Bool Defn
    funMacro) (Defn -> Defn) -> Defn -> Defn
    forall a b. (a -> b) -> a -> b
    $
                            Lens' Bool Defn -> LensSet Bool Defn
    forall i o. Lens' i o -> LensSet i o
    set Lens' Bool Defn
    funStatic (Defn
    oldDef Defn -> Lens' Bool Defn -> Bool
    forall o i. o -> Lens' i o -> i
    ^. Lens' Bool Defn
    funStatic) (Defn -> Defn) -> Defn -> Defn
    forall a b. (a -> b) -> a -> b
    $
                            Lens' Bool Defn -> LensSet Bool Defn
    forall i o. Lens' i o -> LensSet i o
    set Lens' Bool Defn
    funInline Bool
    True (Defn -> Defn) -> Defn -> Defn
    forall a b. (a -> b) -> a -> b
    $
                            Defn
    emptyFunction
                            { funClauses :: [Clause]
    funClauses        = [Clause
    cl]
                            , funCompiled :: Maybe CompiledClauses
    funCompiled       = CompiledClauses -> Maybe CompiledClauses
    forall a. a -> Maybe a
    Just CompiledClauses
    cc
                            , funSplitTree :: Maybe SplitTree
    funSplitTree      = Maybe SplitTree
    mst
                            , funMutual :: Maybe [QName]
    funMutual         = Maybe [QName]
    mutual
                            , funProjection :: Maybe Projection
    funProjection     = Maybe Projection
    proj
                            , funTerminates :: Maybe Bool
    funTerminates     = Bool -> Maybe Bool
    forall a. a -> Maybe a
    Just Bool
    True
                            , funExtLam :: Maybe ExtLamInfo
    funExtLam         = Maybe ExtLamInfo
    extlam
                            , funWith :: Maybe QName
    funWith           = Maybe QName
    with
                            }
                      [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
    "new def for" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> QName -> TCMT IO Doc
    forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
    pretty QName
    x) TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <?> Defn -> TCMT IO Doc
    forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
    pretty Defn
    newDef
                      Defn -> TCMT IO Defn
    forall (m :: * -> *) a. Monad m => a -> m a
    return Defn
    newDef

                cl :: Clause
    cl = Clause :: Range
    -> Range
    -> Telescope
    -> NAPs
    -> Maybe Term
    -> Maybe (Arg Type)
    -> Bool
    -> Maybe Bool
    -> Maybe Bool
    -> Maybe Bool
    -> ExpandedEllipsis
    -> Clause
    Clause { clauseLHSRange :: Range
    clauseLHSRange  = [Clause] -> Range
    forall a. HasRange a => a -> Range
    getRange ([Clause] -> Range) -> [Clause] -> Range
    forall a b. (a -> b) -> a -> b
    $ Definition -> [Clause]
    defClauses Definition
    d
                            , clauseFullRange :: Range
    clauseFullRange = [Clause] -> Range
    forall a. HasRange a => a -> Range
    getRange ([Clause] -> Range) -> [Clause] -> Range
    forall a b. (a -> b) -> a -> b
    $ Definition -> [Clause]
    defClauses Definition
    d
                            , clauseTel :: Telescope
    clauseTel       = Telescope
    forall a. Tele a
    EmptyTel
                            , namedClausePats :: NAPs
    namedClausePats = []
                            , clauseBody :: Maybe Term
    clauseBody      = Term -> Maybe Term
    forall a. a -> Maybe a
    Just (Term -> Maybe Term) -> Term -> Maybe Term
    forall a b. (a -> b) -> a -> b
    $ Int -> Term -> Term
    forall a. DropArgs a => Int -> a -> a
    dropArgs Int
    pars (Term -> Term) -> Term -> Term
    forall a b. (a -> b) -> a -> b
    $ case Defn
    oldDef of
                                Function{funProjection :: Defn -> Maybe Projection
    funProjection = Just Projection
    p} -> Projection -> ProjOrigin -> Relevance -> [Arg Term] -> Term
    projDropParsApply Projection
    p ProjOrigin
    ProjSystem Relevance
    rel [Arg Term]
    ts'
                                Defn
    _ -> QName -> Elims -> Term
    Def QName
    x (Elims -> Term) -> Elims -> Term
    forall a b. (a -> b) -> a -> b
    $ (Arg Term -> Elim' Term) -> [Arg Term] -> Elims
    forall a b. (a -> b) -> [a] -> [b]
    map Arg Term -> Elim' Term
    forall a. Arg a -> Elim' a
    Apply [Arg Term]
    ts'
                            , clauseType :: Maybe (Arg Type)
    clauseType      = Arg Type -> Maybe (Arg Type)
    forall a. a -> Maybe a
    Just (Arg Type -> Maybe (Arg Type)) -> Arg Type -> Maybe (Arg Type)
    forall a b. (a -> b) -> a -> b
    $ Type -> Arg Type
    forall a. a -> Arg a
    defaultArg Type
    t
                            , clauseCatchall :: Bool
    clauseCatchall  = Bool
    False
                            , clauseExact :: Maybe Bool
    clauseExact       = Bool -> Maybe Bool
    forall a. a -> Maybe a
    Just Bool
    True
                            , clauseRecursive :: Maybe Bool
    clauseRecursive   = Bool -> Maybe Bool
    forall a. a -> Maybe a
    Just Bool
    False -- definitely not recursive
                            , clauseUnreachable :: Maybe Bool
    clauseUnreachable = Bool -> Maybe Bool
    forall a. a -> Maybe a
    Just Bool
    False -- definitely not unreachable
                            , clauseEllipsis :: ExpandedEllipsis
    clauseEllipsis  = ExpandedEllipsis
    NoEllipsis
                            }
                  where
                    -- The number of remaining parameters. We need to drop the
                    -- lambdas corresponding to these from the clause body above.
                    pars :: Int
    pars = Int -> Int -> Int
    forall a. Ord a => a -> a -> a
    max Int
    0 (Int -> Int) -> Int -> Int
    forall a b. (a -> b) -> a -> b
    $ Int -> (Projection -> Int) -> Maybe Projection -> Int
    forall b a. b -> (a -> b) -> Maybe a -> b
    maybe Int
    0 (Int -> Int
    forall a. Enum a => a -> a
    pred (Int -> Int) -> (Projection -> Int) -> Projection -> Int
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Projection -> Int
    projIndex) Maybe Projection
    proj
                    rel :: Relevance
    rel  = ArgInfo -> Relevance
    forall a. LensRelevance a => a -> Relevance
    getRelevance (ArgInfo -> Relevance) -> ArgInfo -> Relevance
    forall a b. (a -> b) -> a -> b
    $ Definition -> ArgInfo
    defArgInfo Definition
    d

        {- Example

        module Top Θ where
          module A Γ where
            module M Φ where
          module B Δ where
            module N Ψ where
              module O Ψ' where
            open A public     -- introduces only M --> A.M into the *scope*
        module C Ξ = Top.B ts

        new section C
          tel = Ξ.(Θ.Δ)[ts]

        calls
          1. copySec ts Top.A.M C.M
          2. copySec ts Top.B.N C.N
          3. copySec ts Top.B.N.O C.N.O
        with
          old = Top.B

        For 1.
          Common prefix is: Top
          totalArgs = |Θ|   (section Top)
          tel       = Θ.Γ.Φ (section Top.A.M)
          ts'       = take totalArgs ts
          Θ₂        = drop totalArgs Θ
          new section C.M
            tel =  Θ₂.Γ.Φ[ts']
        -}
        copySec :: Args -> ModuleName -> ModuleName -> TCM ()
        copySec :: [Arg Term] -> ModuleName -> ModuleName -> TCM ()
    copySec [Arg Term]
    ts ModuleName
    x ModuleName
    y = do
          Int
    totalArgs <- ModuleName -> TCMT IO Int
    argsToUse ModuleName
    x
          Telescope
    tel       <- ModuleName -> TCMT IO Telescope
    forall (m :: * -> *).
    (Functor m, ReadTCState m) =>
    ModuleName -> m Telescope
    lookupSection ModuleName
    x
          let sectionTel :: Telescope
    sectionTel =  Telescope -> [Arg Term] -> Telescope
    forall t. Apply t => t -> [Arg Term] -> t
    apply Telescope
    tel ([Arg Term] -> Telescope) -> [Arg Term] -> Telescope
    forall a b. (a -> b) -> a -> b
    $ Int -> [Arg Term] -> [Arg Term]
    forall a. Int -> [a] -> [a]
    take Int
    totalArgs [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
    80 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Doc
    "Copying 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 (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
    pretty ModuleName
    x TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> TCMT IO Doc
    "to" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> ModuleName -> TCMT IO Doc
    forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
    pretty ModuleName
    y
          [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
    "  ts           = " 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 a. Monoid a => [a] -> a
    mconcat (TCMT IO Doc -> [TCMT IO Doc] -> [TCMT IO Doc]
    forall a. a -> [a] -> [a]
    List.intersperse TCMT IO Doc
    "; " ((Arg Term -> TCMT IO Doc) -> [Arg Term] -> [TCMT IO Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map Arg Term -> TCMT IO Doc
    forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
    pretty [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
    80 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Doc
    "  totalArgs    = " 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 (Int -> [Char]
    forall a. Show a => a -> [Char]
    show Int
    totalArgs)
          [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
    "  tel          = " 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 ([[Char]] -> [Char]
    unwords ((Dom ([Char], Type) -> [Char]) -> [Dom ([Char], Type)] -> [[Char]]
    forall a b. (a -> b) -> [a] -> [b]
    map (([Char], Type) -> [Char]
    forall a b. (a, b) -> a
    fst (([Char], Type) -> [Char])
    -> (Dom ([Char], Type) -> ([Char], Type))
    -> Dom ([Char], Type)
    -> [Char]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Dom ([Char], Type) -> ([Char], Type)
    forall t e. Dom' t e -> e
    unDom) ([Dom ([Char], Type)] -> [[Char]])
    -> [Dom ([Char], Type)] -> [[Char]]
    forall a b. (a -> b) -> a -> b
    $ Telescope -> [Dom ([Char], Type)]
    forall t. Tele (Dom t) -> [Dom ([Char], t)]
    telToList Telescope
    tel))  -- only names
          [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
    "  sectionTel   = " 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 ([[Char]] -> [Char]
    unwords ((Dom ([Char], Type) -> [Char]) -> [Dom ([Char], Type)] -> [[Char]]
    forall a b. (a -> b) -> [a] -> [b]
    map (([Char], Type) -> [Char]
    forall a b. (a, b) -> a
    fst (([Char], Type) -> [Char])
    -> (Dom ([Char], Type) -> ([Char], Type))
    -> Dom ([Char], Type)
    -> [Char]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Dom ([Char], Type) -> ([Char], Type)
    forall t e. Dom' t e -> e
    unDom) ([Dom ([Char], Type)] -> [[Char]])
    -> [Dom ([Char], Type)] -> [[Char]]
    forall a b. (a -> b) -> a -> b
    $ Telescope -> [Dom ([Char], Type)]
    forall t. Tele (Dom t) -> [Dom ([Char], t)]
    telToList Telescope
    ptel)) -- only names
          Telescope -> TCM () -> TCM ()
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    addContext Telescope
    sectionTel (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ ModuleName -> TCM ()
    addSection ModuleName
    y

    -- | Add a display form to a definition (could be in this or imported signature).
    addDisplayForm :: QName -> DisplayForm -> TCM ()
    addDisplayForm :: QName -> DisplayForm -> TCM ()
    addDisplayForm QName
    x DisplayForm
    df = do
      LocalDisplayForm
    d <- DisplayForm -> TCMT IO LocalDisplayForm
    forall (m :: * -> *) a.
    (ReadTCState m, MonadTCEnv m) =>
    a -> m (Open a)
    makeOpen DisplayForm
    df
      let add :: Signature -> Signature
    add = QName -> (Definition -> Definition) -> Signature -> Signature
    updateDefinition QName
    x ((Definition -> Definition) -> Signature -> Signature)
    -> (Definition -> Definition) -> Signature -> Signature
    forall a b. (a -> b) -> a -> b
    $ \ Definition
    def -> Definition
    def{ defDisplay :: [LocalDisplayForm]
    defDisplay = LocalDisplayForm
    d LocalDisplayForm -> [LocalDisplayForm] -> [LocalDisplayForm]
    forall a. a -> [a] -> [a]
    : Definition -> [LocalDisplayForm]
    defDisplay Definition
    def }
      TCMT IO Bool -> TCM () -> TCM () -> TCM ()
    forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
    ifM (QName -> TCMT IO Bool
    forall (m :: * -> *). ReadTCState m => QName -> m Bool
    isLocal QName
    x)
        {-then-} ((Signature -> Signature) -> TCM ()
    forall (m :: * -> *).
    MonadTCState m =>
    (Signature -> Signature) -> m ()
    modifySignature Signature -> Signature
    add)
        {-else-} (Lens' DisplayForms TCState
    stImportsDisplayForms Lens' DisplayForms TCState
    -> (DisplayForms -> DisplayForms) -> TCM ()
    forall (m :: * -> *) a.
    MonadTCState m =>
    Lens' a TCState -> (a -> a) -> m ()
    `modifyTCLens` ([LocalDisplayForm] -> [LocalDisplayForm] -> [LocalDisplayForm])
    -> QName -> [LocalDisplayForm] -> DisplayForms -> DisplayForms
    forall k v.
    (Eq k, Hashable k) =>
    (v -> v -> v) -> k -> v -> HashMap k v -> HashMap k v
    HMap.insertWith [LocalDisplayForm] -> [LocalDisplayForm] -> [LocalDisplayForm]
    forall a. [a] -> [a] -> [a]
    (++) QName
    x [LocalDisplayForm
    d])
      TCMT IO Bool -> TCM () -> TCM ()
    forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
    whenM (QName -> TCMT IO Bool
    hasLoopingDisplayForm QName
    x) (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 ()) -> (Doc -> TypeError) -> Doc -> TCM ()
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Doc -> TypeError
    GenericDocError (Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< do TCMT IO Doc
    "Cannot add recursive display form for" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> QName -> TCMT IO Doc
    forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
    pretty QName
    x

    isLocal :: ReadTCState m => QName -> m Bool
    isLocal :: forall (m :: * -> *). ReadTCState m => QName -> m Bool
    isLocal QName
    x = QName -> Definitions -> Bool
    forall k a. (Eq k, Hashable k) => k -> HashMap k a -> Bool
    HMap.member QName
    x (Definitions -> Bool) -> m Definitions -> m Bool
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Lens' Definitions TCState -> m Definitions
    forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
    useR ((Signature -> f Signature) -> TCState -> f TCState
    Lens' Signature TCState
    stSignature ((Signature -> f Signature) -> TCState -> f TCState)
    -> ((Definitions -> f Definitions) -> Signature -> f Signature)
    -> (Definitions -> f Definitions)
    -> TCState
    -> f TCState
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Definitions -> f Definitions) -> Signature -> f Signature
    Lens' Definitions Signature
    sigDefinitions)

    getDisplayForms :: (HasConstInfo m, ReadTCState m) => QName -> m [LocalDisplayForm]
    getDisplayForms :: forall (m :: * -> *).
    (HasConstInfo m, ReadTCState m) =>
    QName -> m [LocalDisplayForm]
    getDisplayForms QName
    q = do
      [LocalDisplayForm]
    ds  <- (SigError -> [LocalDisplayForm])
    -> (Definition -> [LocalDisplayForm])
    -> Either SigError Definition
    -> [LocalDisplayForm]
    forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
    either ([LocalDisplayForm] -> SigError -> [LocalDisplayForm]
    forall a b. a -> b -> a
    const []) Definition -> [LocalDisplayForm]
    defDisplay (Either SigError Definition -> [LocalDisplayForm])
    -> m (Either SigError Definition) -> m [LocalDisplayForm]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> QName -> m (Either SigError Definition)
    forall (m :: * -> *).
    HasConstInfo m =>
    QName -> m (Either SigError Definition)
    getConstInfo' QName
    q
      [LocalDisplayForm]
    ds1 <- [LocalDisplayForm] -> QName -> DisplayForms -> [LocalDisplayForm]
    forall k v. (Eq k, Hashable k) => v -> k -> HashMap k v -> v
    HMap.lookupDefault [] QName
    q (DisplayForms -> [LocalDisplayForm])
    -> m DisplayForms -> m [LocalDisplayForm]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Lens' DisplayForms TCState -> m DisplayForms
    forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
    useR Lens' DisplayForms TCState
    stImportsDisplayForms
      [LocalDisplayForm]
    ds2 <- [LocalDisplayForm] -> QName -> DisplayForms -> [LocalDisplayForm]
    forall k v. (Eq k, Hashable k) => v -> k -> HashMap k v -> v
    HMap.lookupDefault [] QName
    q (DisplayForms -> [LocalDisplayForm])
    -> m DisplayForms -> m [LocalDisplayForm]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Lens' DisplayForms TCState -> m DisplayForms
    forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
    useR Lens' DisplayForms TCState
    stImportedDisplayForms
      m Bool
    -> m [LocalDisplayForm]
    -> m [LocalDisplayForm]
    -> m [LocalDisplayForm]
    forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
    ifM (QName -> m Bool
    forall (m :: * -> *). ReadTCState m => QName -> m Bool
    isLocal QName
    q) ([LocalDisplayForm] -> m [LocalDisplayForm]
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([LocalDisplayForm] -> m [LocalDisplayForm])
    -> [LocalDisplayForm] -> m [LocalDisplayForm]
    forall a b. (a -> b) -> a -> b
    $ [LocalDisplayForm]
    ds [LocalDisplayForm] -> [LocalDisplayForm] -> [LocalDisplayForm]
    forall a. [a] -> [a] -> [a]
    ++ [LocalDisplayForm]
    ds1 [LocalDisplayForm] -> [LocalDisplayForm] -> [LocalDisplayForm]
    forall a. [a] -> [a] -> [a]
    ++ [LocalDisplayForm]
    ds2)
                      ([LocalDisplayForm] -> m [LocalDisplayForm]
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([LocalDisplayForm] -> m [LocalDisplayForm])
    -> [LocalDisplayForm] -> m [LocalDisplayForm]
    forall a b. (a -> b) -> a -> b
    $ [LocalDisplayForm]
    ds1 [LocalDisplayForm] -> [LocalDisplayForm] -> [LocalDisplayForm]
    forall a. [a] -> [a] -> [a]
    ++ [LocalDisplayForm]
    ds [LocalDisplayForm] -> [LocalDisplayForm] -> [LocalDisplayForm]
    forall a. [a] -> [a] -> [a]
    ++ [LocalDisplayForm]
    ds2)

    -- | Find all names used (recursively) by display forms of a given name.
    chaseDisplayForms :: QName -> TCM (Set QName)
    chaseDisplayForms :: QName -> TCM (Set QName)
    chaseDisplayForms QName
    q = Set QName -> [QName] -> TCM (Set QName)
    go Set QName
    forall a. Set a
    Set.empty [QName
    q]
      where
        go :: Set QName        -- Accumulator.
           -> [QName]          -- Work list.  TODO: make work set to avoid duplicate chasing?
           -> TCM (Set QName)
        go :: Set QName -> [QName] -> TCM (Set QName)
    go Set QName
    used []       = Set QName -> TCM (Set QName)
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Set QName
    used
        go Set QName
    used (QName
    q : [QName]
    qs) = do
          let rhs :: DisplayForm -> DisplayTerm
    rhs (Display Int
    _ Elims
    _ DisplayTerm
    e) = DisplayTerm
    e   -- Only look at names in the right-hand side (#1870)
          let notYetUsed :: QName -> Set QName
    notYetUsed QName
    x = if QName
    x QName -> Set QName -> Bool
    forall a. Ord a => a -> Set a -> Bool
    `Set.member` Set QName
    used then Set QName
    forall a. Set a
    Set.empty else QName -> Set QName
    forall a. a -> Set a
    Set.singleton QName
    x
          Set QName
    ds <- (QName -> Set QName) -> [DisplayTerm] -> Set QName
    forall a m. (NamesIn a, Monoid m) => (QName -> m) -> a -> m
    namesIn' QName -> Set QName
    notYetUsed ([DisplayTerm] -> Set QName)
    -> ([LocalDisplayForm] -> [DisplayTerm])
    -> [LocalDisplayForm]
    -> Set QName
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (LocalDisplayForm -> DisplayTerm)
    -> [LocalDisplayForm] -> [DisplayTerm]
    forall a b. (a -> b) -> [a] -> [b]
    map (DisplayForm -> DisplayTerm
    rhs (DisplayForm -> DisplayTerm)
    -> (LocalDisplayForm -> DisplayForm)
    -> LocalDisplayForm
    -> DisplayTerm
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . LocalDisplayForm -> DisplayForm
    forall (t :: * -> *) a. Decoration t => t a -> a
    dget)
                ([LocalDisplayForm] -> Set QName)
    -> TCMT IO [LocalDisplayForm] -> TCM (Set QName)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (QName -> TCMT IO [LocalDisplayForm]
    forall (m :: * -> *).
    (HasConstInfo m, ReadTCState m) =>
    QName -> m [LocalDisplayForm]
    getDisplayForms QName
    q TCMT IO [LocalDisplayForm]
    -> (TCErr -> TCMT IO [LocalDisplayForm])
    -> TCMT IO [LocalDisplayForm]
    forall a. TCM a -> (TCErr -> TCM a) -> TCM a
    `catchError_` \ TCErr
    _ -> [LocalDisplayForm] -> TCMT IO [LocalDisplayForm]
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure [])  -- might be a pattern synonym
          Set QName -> [QName] -> TCM (Set QName)
    go (Set QName -> Set QName -> Set QName
    forall a. Ord a => Set a -> Set a -> Set a
    Set.union Set QName
    ds Set QName
    used) (Set QName -> [QName]
    forall a. Set a -> [a]
    Set.toList Set QName
    ds [QName] -> [QName] -> [QName]
    forall a. [a] -> [a] -> [a]
    ++ [QName]
    qs)

    -- | Check if a display form is looping.
    hasLoopingDisplayForm :: QName -> TCM Bool
    hasLoopingDisplayForm :: QName -> TCMT IO Bool
    hasLoopingDisplayForm QName
    q = QName -> Set QName -> Bool
    forall a. Ord a => a -> Set a -> Bool
    Set.member QName
    q (Set QName -> Bool) -> TCM (Set QName) -> TCMT IO Bool
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> QName -> TCM (Set QName)
    chaseDisplayForms QName
    q

    canonicalName :: HasConstInfo m => QName -> m QName
    canonicalName :: forall (m :: * -> *). HasConstInfo m => QName -> m QName
    canonicalName QName
    x = do
      Defn
    def <- Definition -> Defn
    theDef (Definition -> Defn) -> m Definition -> m Defn
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> QName -> m Definition
    forall (m :: * -> *). HasConstInfo m => QName -> m Definition
    getConstInfo QName
    x
      case Defn
    def of
        Constructor{conSrcCon :: Defn -> ConHead
    conSrcCon = ConHead
    c}                                -> QName -> m QName
    forall (m :: * -> *) a. Monad m => a -> m a
    return (QName -> m QName) -> QName -> m QName
    forall a b. (a -> b) -> a -> b
    $ ConHead -> QName
    conName ConHead
    c
        Record{recClause :: Defn -> Maybe Clause
    recClause = Just (Clause{ clauseBody :: Clause -> Maybe Term
    clauseBody = Maybe Term
    body })}    -> Maybe Term -> m QName
    forall {m :: * -> *}. HasConstInfo m => Maybe Term -> m QName
    can Maybe Term
    body
        Datatype{dataClause :: Defn -> Maybe Clause
    dataClause = Just (Clause{ clauseBody :: Clause -> Maybe Term
    clauseBody = Maybe Term
    body })} -> Maybe Term -> m QName
    forall {m :: * -> *}. HasConstInfo m => Maybe Term -> m QName
    can Maybe Term
    body
        Defn
    _                                                         -> QName -> m QName
    forall (m :: * -> *) a. Monad m => a -> m a
    return QName
    x
      where
        can :: Maybe Term -> m QName
    can Maybe Term
    body = QName -> m QName
    forall (m :: * -> *). HasConstInfo m => QName -> m QName
    canonicalName (QName -> m QName) -> QName -> m QName
    forall a b. (a -> b) -> a -> b
    $ Term -> QName
    extract (Term -> QName) -> Term -> QName
    forall a b. (a -> b) -> a -> b
    $ Term -> Maybe Term -> Term
    forall a. a -> Maybe a -> a
    fromMaybe Term
    forall a. HasCallStack => a
    __IMPOSSIBLE__ Maybe Term
    body
        extract :: Term -> QName
    extract (Def QName
    x Elims
    _)  = QName
    x
        extract Term
    _          = QName
    forall a. HasCallStack => a
    __IMPOSSIBLE__

    sameDef :: HasConstInfo m => QName -> QName -> m (Maybe QName)
    sameDef :: forall (m :: * -> *).
    HasConstInfo m =>
    QName -> QName -> m (Maybe QName)
    sameDef QName
    d1 QName
    d2 = do
      QName
    c1 <- QName -> m QName
    forall (m :: * -> *). HasConstInfo m => QName -> m QName
    canonicalName QName
    d1
      QName
    c2 <- QName -> m QName
    forall (m :: * -> *). HasConstInfo m => QName -> m QName
    canonicalName QName
    d2
      if (QName
    c1 QName -> QName -> Bool
    forall a. Eq a => a -> a -> Bool
    == QName
    c2) then Maybe QName -> m (Maybe QName)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Maybe QName -> m (Maybe QName)) -> Maybe QName -> m (Maybe QName)
    forall a b. (a -> b) -> a -> b
    $ QName -> Maybe QName
    forall a. a -> Maybe a
    Just QName
    c1 else Maybe QName -> m (Maybe QName)
    forall (m :: * -> *) a. Monad m => a -> m a
    return Maybe QName
    forall a. Maybe a
    Nothing

    -- | Can be called on either a (co)datatype, a record type or a
    --   (co)constructor.
    whatInduction :: MonadTCM tcm => QName -> tcm Induction
    whatInduction :: forall (tcm :: * -> *). MonadTCM tcm => QName -> tcm Induction
    whatInduction QName
    c = TCM Induction -> tcm Induction
    forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
    liftTCM (TCM Induction -> tcm Induction) -> TCM Induction -> tcm Induction
    forall a b. (a -> b) -> a -> b
    $ do
      Defn
    def <- Definition -> Defn
    theDef (Definition -> Defn) -> TCMT IO Definition -> TCMT IO Defn
    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
    c
      Maybe QName
    mz <- [Char] -> TCMT IO (Maybe QName)
    forall (m :: * -> *). HasBuiltins m => [Char] -> m (Maybe QName)
    getBuiltinName' [Char]
    builtinIZero
      Maybe QName
    mo <- [Char] -> TCMT IO (Maybe QName)
    forall (m :: * -> *). HasBuiltins m => [Char] -> m (Maybe QName)
    getBuiltinName' [Char]
    builtinIOne
      case Defn
    def of
        Datatype{}                    -> Induction -> TCM Induction
    forall (m :: * -> *) a. Monad m => a -> m a
    return Induction
    Inductive
        Record{} | Bool -> Bool
    not (Defn -> Bool
    recRecursive Defn
    def) -> Induction -> TCM Induction
    forall (m :: * -> *) a. Monad m => a -> m a
    return Induction
    Inductive
        Record{ recInduction :: Defn -> Maybe Induction
    recInduction = Maybe Induction
    i    } -> Induction -> TCM Induction
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Induction -> TCM Induction) -> Induction -> TCM Induction
    forall a b. (a -> b) -> a -> b
    $ Induction -> Maybe Induction -> Induction
    forall a. a -> Maybe a -> a
    fromMaybe Induction
    Inductive Maybe Induction
    i
        Constructor{ conInd :: Defn -> Induction
    conInd = Induction
    i }     -> Induction -> TCM Induction
    forall (m :: * -> *) a. Monad m => a -> m a
    return Induction
    i
        Defn
    _ | QName -> Maybe QName
    forall a. a -> Maybe a
    Just QName
    c Maybe QName -> Maybe QName -> Bool
    forall a. Eq a => a -> a -> Bool
    == Maybe QName
    mz Bool -> Bool -> Bool
    || QName -> Maybe QName
    forall a. a -> Maybe a
    Just QName
    c Maybe QName -> Maybe QName -> Bool
    forall a. Eq a => a -> a -> Bool
    == Maybe QName
    mo
                                      -> Induction -> TCM Induction
    forall (m :: * -> *) a. Monad m => a -> m a
    return Induction
    Inductive
        Defn
    _                             -> TCM Induction
    forall a. HasCallStack => a
    __IMPOSSIBLE__

    -- | Does the given constructor come from a single-constructor type?
    --
    -- Precondition: The name has to refer to a constructor.
    singleConstructorType :: QName -> TCM Bool
    singleConstructorType :: QName -> TCMT IO Bool
    singleConstructorType QName
    q = do
      Defn
    d <- Definition -> Defn
    theDef (Definition -> Defn) -> TCMT IO Definition -> TCMT IO Defn
    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
    q
      case Defn
    d of
        Record {}                   -> Bool -> TCMT IO Bool
    forall (m :: * -> *) a. Monad m => a -> m a
    return Bool
    True
        Constructor { conData :: Defn -> QName
    conData = QName
    d } -> do
          Defn
    di <- Definition -> Defn
    theDef (Definition -> Defn) -> TCMT IO Definition -> TCMT IO Defn
    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
    d
          Bool -> TCMT IO Bool
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Bool -> TCMT IO Bool) -> Bool -> TCMT IO Bool
    forall a b. (a -> b) -> a -> b
    $ case Defn
    di of
            Record {}                  -> Bool
    True
            Datatype { dataCons :: Defn -> [QName]
    dataCons = [QName]
    cs } -> [QName] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length [QName]
    cs Int -> Int -> Bool
    forall a. Eq a => a -> a -> Bool
    == Int
    1
            Defn
    _                          -> Bool
    forall a. HasCallStack => a
    __IMPOSSIBLE__
        Defn
    _ -> TCMT IO Bool
    forall a. HasCallStack => a
    __IMPOSSIBLE__

    -- | Signature lookup errors.
    data SigError
      = SigUnknown String -- ^ The name is not in the signature; default error message.
      | SigAbstract       -- ^ The name is not available, since it is abstract.

    -- | Standard eliminator for 'SigError'.
    sigError :: (String -> a) -> a -> SigError -> a
    sigError :: forall a. ([Char] -> a) -> a -> SigError -> a
    sigError [Char] -> a
    f a
    a = \case
      SigUnknown [Char]
    s -> [Char] -> a
    f [Char]
    s
      SigError
    SigAbstract  -> a
    a

    class ( Functor m
          , Applicative m
          , Fail.MonadFail m
          , HasOptions m
          , MonadDebug m
          , MonadTCEnv m
          ) => HasConstInfo m where
      -- | Lookup the definition of a name. The result is a closed thing, all free
      --   variables have been abstracted over.
      getConstInfo :: QName -> m Definition
      getConstInfo QName
    q = QName -> m (Either SigError Definition)
    forall (m :: * -> *).
    HasConstInfo m =>
    QName -> m (Either SigError Definition)
    getConstInfo' QName
    q m (Either SigError Definition)
    -> (Either SigError Definition -> m Definition) -> m Definition
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \case
          Right Definition
    d -> Definition -> m Definition
    forall (m :: * -> *) a. Monad m => a -> m a
    return Definition
    d
          Left (SigUnknown [Char]
    err) -> [Char] -> m Definition
    forall (m :: * -> *) a.
    (HasCallStack, MonadDebug m) =>
    [Char] -> m a
    __IMPOSSIBLE_VERBOSE__ [Char]
    err
          Left SigError
    SigAbstract      -> [Char] -> m Definition
    forall (m :: * -> *) a.
    (HasCallStack, MonadDebug m) =>
    [Char] -> m a
    __IMPOSSIBLE_VERBOSE__ ([Char] -> m Definition) -> [Char] -> m Definition
    forall a b. (a -> b) -> a -> b
    $
            [Char]
    "Abstract, thus, not in scope: " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ QName -> [Char]
    forall a. Pretty a => a -> [Char]
    prettyShow QName
    q

      -- | Version that reports exceptions:
      getConstInfo' :: QName -> m (Either SigError Definition)
      -- getConstInfo' q = Right <$> getConstInfo q -- conflicts with default signature

      -- | Lookup the rewrite rules with the given head symbol.
      getRewriteRulesFor :: QName -> m RewriteRules

      -- Lifting HasConstInfo through monad transformers:

      default getConstInfo'
        :: (HasConstInfo n, MonadTrans t, m ~ t n)
        => QName -> m (Either SigError Definition)
      getConstInfo' = n (Either SigError Definition) -> t n (Either SigError Definition)
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (n (Either SigError Definition)
     -> t n (Either SigError Definition))
    -> (QName -> n (Either SigError Definition))
    -> QName
    -> t n (Either SigError Definition)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . QName -> n (Either SigError Definition)
    forall (m :: * -> *).
    HasConstInfo m =>
    QName -> m (Either SigError Definition)
    getConstInfo'

      default getRewriteRulesFor
        :: (HasConstInfo n, MonadTrans t, m ~ t n)
        => QName -> m RewriteRules
      getRewriteRulesFor = n RewriteRules -> t n RewriteRules
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (n RewriteRules -> t n RewriteRules)
    -> (QName -> n RewriteRules) -> QName -> t n RewriteRules
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . QName -> n RewriteRules
    forall (m :: * -> *). HasConstInfo m => QName -> m RewriteRules
    getRewriteRulesFor

    {-# SPECIALIZE getConstInfo :: QName -> TCM Definition #-}

    -- | The computation 'getConstInfo' sometimes tweaks the returned
    -- 'Definition', depending on the current 'Language' and the
    -- 'Language' of the 'Definition'. This variant of 'getConstInfo' does
    -- not perform any tweaks.

    getOriginalConstInfo ::
      (ReadTCState m, HasConstInfo m) => QName -> m Definition
    getOriginalConstInfo :: forall (m :: * -> *).
    (ReadTCState m, HasConstInfo m) =>
    QName -> m Definition
    getOriginalConstInfo QName
    q = do
      Definition
    def  <- QName -> m Definition
    forall (m :: * -> *). HasConstInfo m => QName -> m Definition
    getConstInfo QName
    q
      Language
    lang <- m Language
    forall (m :: * -> *). HasOptions m => m Language
    getLanguage
      case (Language
    lang, Definition -> Language
    defLanguage Definition
    def) of
        (Cubical Cubical
    CErased, Cubical Cubical
    CFull) ->
          Lens' PragmaOptions TCState
    -> (PragmaOptions -> PragmaOptions) -> m Definition -> m Definition
    forall (m :: * -> *) a b.
    ReadTCState m =>
    Lens' a TCState -> (a -> a) -> m b -> m b
    locallyTCState
            Lens' PragmaOptions TCState
    stPragmaOptions
            (\PragmaOptions
    opts -> PragmaOptions
    opts { optCubical :: Maybe Cubical
    optCubical = Cubical -> Maybe Cubical
    forall a. a -> Maybe a
    Just Cubical
    CFull })
            (QName -> m Definition
    forall (m :: * -> *). HasConstInfo m => QName -> m Definition
    getConstInfo QName
    q)
        (Language, Language)
    _ -> Definition -> m Definition
    forall (m :: * -> *) a. Monad m => a -> m a
    return Definition
    def

    defaultGetRewriteRulesFor :: (ReadTCState m, MonadTCEnv m) => QName -> m RewriteRules
    defaultGetRewriteRulesFor :: forall (m :: * -> *).
    (ReadTCState m, MonadTCEnv m) =>
    QName -> m RewriteRules
    defaultGetRewriteRulesFor QName
    q = m Bool -> m RewriteRules -> m RewriteRules -> m RewriteRules
    forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
    ifNotM (QName -> m Bool
    forall (m :: * -> *). MonadTCEnv m => QName -> m Bool
    shouldReduceDef QName
    q) (RewriteRules -> m RewriteRules
    forall (m :: * -> *) a. Monad m => a -> m a
    return []) (m RewriteRules -> m RewriteRules)
    -> m RewriteRules -> m RewriteRules
    forall a b. (a -> b) -> a -> b
    $ do
      TCState
    st <- m TCState
    forall (m :: * -> *). ReadTCState m => m TCState
    getTCState
      let sig :: Signature
    sig = TCState
    stTCState -> Lens' Signature TCState -> Signature
    forall o i. o -> Lens' i o -> i
    ^.Lens' Signature TCState
    stSignature
          imp :: Signature
    imp = TCState
    stTCState -> Lens' Signature TCState -> Signature
    forall o i. o -> Lens' i o -> i
    ^.Lens' Signature TCState
    stImports
          look :: Signature -> Maybe RewriteRules
    look Signature
    s = QName -> RewriteRuleMap -> Maybe RewriteRules
    forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
    HMap.lookup QName
    q (RewriteRuleMap -> Maybe RewriteRules)
    -> RewriteRuleMap -> Maybe RewriteRules
    forall a b. (a -> b) -> a -> b
    $ Signature
    s Signature -> Lens' RewriteRuleMap Signature -> RewriteRuleMap
    forall o i. o -> Lens' i o -> i
    ^. Lens' RewriteRuleMap Signature
    sigRewriteRules
      RewriteRules -> m RewriteRules
    forall (m :: * -> *) a. Monad m => a -> m a
    return (RewriteRules -> m RewriteRules) -> RewriteRules -> m RewriteRules
    forall a b. (a -> b) -> a -> b
    $ [RewriteRules] -> RewriteRules
    forall a. Monoid a => [a] -> a
    mconcat ([RewriteRules] -> RewriteRules) -> [RewriteRules] -> RewriteRules
    forall a b. (a -> b) -> a -> b
    $ [Maybe RewriteRules] -> [RewriteRules]
    forall a. [Maybe a] -> [a]
    catMaybes [Signature -> Maybe RewriteRules
    look Signature
    sig, Signature -> Maybe RewriteRules
    look Signature
    imp]

    -- | Get the original name of the projection
    --   (the current one could be from a module application).
    getOriginalProjection :: HasConstInfo m => QName -> m QName
    getOriginalProjection :: forall (m :: * -> *). HasConstInfo m => QName -> m QName
    getOriginalProjection QName
    q = Projection -> QName
    projOrig (Projection -> QName)
    -> (Maybe Projection -> Projection) -> Maybe Projection -> QName
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Projection -> Maybe Projection -> Projection
    forall a. a -> Maybe a -> a
    fromMaybe Projection
    forall a. HasCallStack => a
    __IMPOSSIBLE__ (Maybe Projection -> QName) -> m (Maybe Projection) -> m QName
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> QName -> m (Maybe Projection)
    forall (m :: * -> *).
    HasConstInfo m =>
    QName -> m (Maybe Projection)
    isProjection QName
    q

    instance HasConstInfo (TCMT IO) where
      getRewriteRulesFor :: QName -> TCMT IO RewriteRules
    getRewriteRulesFor = QName -> TCMT IO RewriteRules
    forall (m :: * -> *).
    (ReadTCState m, MonadTCEnv m) =>
    QName -> m RewriteRules
    defaultGetRewriteRulesFor
      getConstInfo' :: QName -> TCMT IO (Either SigError Definition)
    getConstInfo' QName
    q = do
        TCState
    st  <- TCMT IO TCState
    forall (m :: * -> *). MonadTCState m => m TCState
    getTC
        TCEnv
    env <- TCMT IO TCEnv
    forall (m :: * -> *). MonadTCEnv m => m TCEnv
    askTC
        TCState -> TCEnv -> QName -> TCMT IO (Either SigError Definition)
    forall (m :: * -> *).
    (HasOptions m, MonadDebug m, MonadTCEnv m) =>
    TCState -> TCEnv -> QName -> m (Either SigError Definition)
    defaultGetConstInfo TCState
    st TCEnv
    env QName
    q
      getConstInfo :: QName -> TCMT IO Definition
    getConstInfo QName
    q = QName -> TCMT IO (Either SigError Definition)
    forall (m :: * -> *).
    HasConstInfo m =>
    QName -> m (Either SigError Definition)
    getConstInfo' QName
    q TCMT IO (Either SigError Definition)
    -> (Either SigError Definition -> TCMT IO Definition)
    -> TCMT IO Definition
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \case
          Right Definition
    d -> Definition -> TCMT IO Definition
    forall (m :: * -> *) a. Monad m => a -> m a
    return Definition
    d
          Left (SigUnknown [Char]
    err) -> [Char] -> TCMT IO Definition
    forall (m :: * -> *) a. MonadFail m => [Char] -> m a
    fail [Char]
    err
          Left SigError
    SigAbstract      -> QName -> TCMT IO Definition
    forall a. QName -> TCM a
    notInScopeError (QName -> TCMT IO Definition) -> QName -> TCMT IO Definition
    forall a b. (a -> b) -> a -> b
    $ QName -> QName
    qnameToConcrete QName
    q

    defaultGetConstInfo
      :: (HasOptions m, MonadDebug m, MonadTCEnv m)
      => TCState -> TCEnv -> QName -> m (Either SigError Definition)
    defaultGetConstInfo :: forall (m :: * -> *).
    (HasOptions m, MonadDebug m, MonadTCEnv m) =>
    TCState -> TCEnv -> QName -> m (Either SigError Definition)
    defaultGetConstInfo TCState
    st TCEnv
    env QName
    q = do
        let defs :: Definitions
    defs  = TCState
    stTCState -> Lens' Definitions TCState -> Definitions
    forall o i. o -> Lens' i o -> i
    ^.((Signature -> f Signature) -> TCState -> f TCState
    Lens' Signature TCState
    stSignature ((Signature -> f Signature) -> TCState -> f TCState)
    -> ((Definitions -> f Definitions) -> Signature -> f Signature)
    -> (Definitions -> f Definitions)
    -> TCState
    -> f TCState
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Definitions -> f Definitions) -> Signature -> f Signature
    Lens' Definitions Signature
    sigDefinitions)
            idefs :: Definitions
    idefs = TCState
    stTCState -> Lens' Definitions TCState -> Definitions
    forall o i. o -> Lens' i o -> i
    ^.((Signature -> f Signature) -> TCState -> f TCState
    Lens' Signature TCState
    stImports ((Signature -> f Signature) -> TCState -> f TCState)
    -> ((Definitions -> f Definitions) -> Signature -> f Signature)
    -> (Definitions -> f Definitions)
    -> TCState
    -> f TCState
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Definitions -> f Definitions) -> Signature -> f Signature
    Lens' Definitions Signature
    sigDefinitions)
        case [Maybe Definition] -> [Definition]
    forall a. [Maybe a] -> [a]
    catMaybes [QName -> Definitions -> Maybe Definition
    forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
    HMap.lookup QName
    q Definitions
    defs, QName -> Definitions -> Maybe Definition
    forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
    HMap.lookup QName
    q Definitions
    idefs] of
            []  -> Either SigError Definition -> m (Either SigError Definition)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Either SigError Definition -> m (Either SigError Definition))
    -> Either SigError Definition -> m (Either SigError Definition)
    forall a b. (a -> b) -> a -> b
    $ SigError -> Either SigError Definition
    forall a b. a -> Either a b
    Left (SigError -> Either SigError Definition)
    -> SigError -> Either SigError Definition
    forall a b. (a -> b) -> a -> b
    $ [Char] -> SigError
    SigUnknown ([Char] -> SigError) -> [Char] -> SigError
    forall a b. (a -> b) -> a -> b
    $ [Char]
    "Unbound name: " [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]
    ++ QName -> [Char]
    showQNameId QName
    q
            [Definition
    d] -> TCEnv -> Definition -> m (Either SigError Definition)
    mkAbs TCEnv
    env (Definition -> m (Either SigError Definition))
    -> m Definition -> m (Either SigError Definition)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< Definition -> m Definition
    forall {m :: * -> *}. HasOptions m => Definition -> m Definition
    fixQuantity Definition
    d
            [Definition]
    ds  -> [Char] -> m (Either SigError Definition)
    forall (m :: * -> *) a.
    (HasCallStack, MonadDebug m) =>
    [Char] -> m a
    __IMPOSSIBLE_VERBOSE__ ([Char] -> m (Either SigError Definition))
    -> [Char] -> m (Either SigError Definition)
    forall a b. (a -> b) -> a -> b
    $ [Char]
    "Ambiguous name: " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ QName -> [Char]
    forall a. Pretty a => a -> [Char]
    prettyShow QName
    q
        where
          mkAbs :: TCEnv -> Definition -> m (Either SigError Definition)
    mkAbs TCEnv
    env Definition
    d
            | QName -> TCEnv -> Bool
    treatAbstractly' QName
    q' TCEnv
    env =
              case Definition -> Maybe Definition
    makeAbstract Definition
    d of
                Just Definition
    d      -> Either SigError Definition -> m (Either SigError Definition)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Either SigError Definition -> m (Either SigError Definition))
    -> Either SigError Definition -> m (Either SigError Definition)
    forall a b. (a -> b) -> a -> b
    $ Definition -> Either SigError Definition
    forall a b. b -> Either a b
    Right Definition
    d
                Maybe Definition
    Nothing     -> Either SigError Definition -> m (Either SigError Definition)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Either SigError Definition -> m (Either SigError Definition))
    -> Either SigError Definition -> m (Either SigError Definition)
    forall a b. (a -> b) -> a -> b
    $ SigError -> Either SigError Definition
    forall a b. a -> Either a b
    Left SigError
    SigAbstract
                  -- the above can happen since the scope checker is a bit sloppy with 'abstract'
            | Bool
    otherwise = Either SigError Definition -> m (Either SigError Definition)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Either SigError Definition -> m (Either SigError Definition))
    -> Either SigError Definition -> m (Either SigError Definition)
    forall a b. (a -> b) -> a -> b
    $ Definition -> Either SigError Definition
    forall a b. b -> Either a b
    Right Definition
    d
            where
              q' :: QName
    q' = case Definition -> Defn
    theDef Definition
    d of
                -- Hack to make abstract constructors work properly. The constructors
                -- live in a module with the same name as the datatype, but for 'abstract'
                -- purposes they're considered to be in the same module as the datatype.
                Constructor{} -> QName -> QName
    dropLastModule QName
    q
                Defn
    _             -> QName
    q

              dropLastModule :: QName -> QName
    dropLastModule q :: QName
    q@QName{ qnameModule :: QName -> ModuleName
    qnameModule = ModuleName
    m } =
                QName
    q{ qnameModule :: ModuleName
    qnameModule = [Name] -> ModuleName
    mnameFromList ([Name] -> ModuleName) -> [Name] -> ModuleName
    forall a b. (a -> b) -> a -> b
    $
                     [Name] -> [Name] -> [Name]
    forall a. [a] -> [a] -> [a]
    initWithDefault [Name]
    forall a. HasCallStack => a
    __IMPOSSIBLE__ ([Name] -> [Name]) -> [Name] -> [Name]
    forall a b. (a -> b) -> a -> b
    $ ModuleName -> [Name]
    mnameToList ModuleName
    m
                 }

          -- Names defined when --cubical is active are (to a large
          -- degree) treated as erased when --erased-cubical is used.
          fixQuantity :: Definition -> m Definition
    fixQuantity Definition
    d = do
            Language
    current <- m Language
    forall (m :: * -> *). HasOptions m => m Language
    getLanguage
            Definition -> m Definition
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Definition -> m Definition) -> Definition -> m Definition
    forall a b. (a -> b) -> a -> b
    $
              if Definition -> Language
    defLanguage Definition
    d Language -> Language -> Bool
    forall a. Eq a => a -> a -> Bool
    == Cubical -> Language
    Cubical Cubical
    CFull Bool -> Bool -> Bool
    &&
                 Language
    current Language -> Language -> Bool
    forall a. Eq a => a -> a -> Bool
    == Cubical -> Language
    Cubical Cubical
    CErased
              then Quantity -> Definition -> Definition
    forall a. LensQuantity a => Quantity -> a -> a
    setQuantity Quantity
    zeroQuantity Definition
    d
              else Definition
    d

    -- HasConstInfo lifts through monad transformers
    -- (see default signatures in HasConstInfo class).

    instance HasConstInfo m => HasConstInfo (ChangeT m)
    instance HasConstInfo m => HasConstInfo (ExceptT err m)
    instance HasConstInfo m => HasConstInfo (IdentityT m)
    instance HasConstInfo m => HasConstInfo (ListT m)
    instance HasConstInfo m => HasConstInfo (MaybeT m)
    instance HasConstInfo m => HasConstInfo (ReaderT r m)
    instance HasConstInfo m => HasConstInfo (StateT s m)
    instance (Monoid w, HasConstInfo m) => HasConstInfo (WriterT w m)
    instance HasConstInfo m => HasConstInfo (BlockT m)

    {-# INLINE getConInfo #-}
    getConInfo :: HasConstInfo m => ConHead -> m Definition
    getConInfo :: forall (m :: * -> *). HasConstInfo m => ConHead -> m Definition
    getConInfo = QName -> m Definition
    forall (m :: * -> *). HasConstInfo m => QName -> m Definition
    getConstInfo (QName -> m Definition)
    -> (ConHead -> QName) -> ConHead -> m Definition
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ConHead -> QName
    conName

    -- | Look up the polarity of a definition.
    getPolarity :: HasConstInfo m => QName -> m [Polarity]
    getPolarity :: forall (m :: * -> *). HasConstInfo m => QName -> m [Polarity]
    getPolarity QName
    q = Definition -> [Polarity]
    defPolarity (Definition -> [Polarity]) -> m Definition -> m [Polarity]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> QName -> m Definition
    forall (m :: * -> *). HasConstInfo m => QName -> m Definition
    getConstInfo QName
    q

    -- | Look up polarity of a definition and compose with polarity
    --   represented by 'Comparison'.
    getPolarity' :: HasConstInfo m => Comparison -> QName -> m [Polarity]
    getPolarity' :: forall (m :: * -> *).
    HasConstInfo m =>
    Comparison -> QName -> m [Polarity]
    getPolarity' Comparison
    CmpEq  QName
    q = (Polarity -> Polarity) -> [Polarity] -> [Polarity]
    forall a b. (a -> b) -> [a] -> [b]
    map (Polarity -> Polarity -> Polarity
    composePol Polarity
    Invariant) ([Polarity] -> [Polarity]) -> m [Polarity] -> m [Polarity]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> QName -> m [Polarity]
    forall (m :: * -> *). HasConstInfo m => QName -> m [Polarity]
    getPolarity QName
    q -- return []
    getPolarity' Comparison
    CmpLeq QName
    q = QName -> m [Polarity]
    forall (m :: * -> *). HasConstInfo m => QName -> m [Polarity]
    getPolarity QName
    q -- composition with Covariant is identity

    -- | Set the polarity of a definition.
    setPolarity :: (MonadTCState m, MonadDebug m) => QName -> [Polarity] -> m ()
    setPolarity :: forall (m :: * -> *).
    (MonadTCState m, MonadDebug m) =>
    QName -> [Polarity] -> m ()
    setPolarity QName
    q [Polarity]
    pol = do
      [Char] -> Int -> TCMT IO Doc -> m ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "tc.polarity.set" Int
    20 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
    forall a b. (a -> b) -> a -> b
    $
        TCMT IO Doc
    "Setting polarity of" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> QName -> TCMT IO Doc
    forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
    pretty QName
    q TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> TCMT IO Doc
    "to" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> [Polarity] -> TCMT IO Doc
    forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
    pretty [Polarity]
    pol TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall a. Semigroup a => a -> a -> a
    <> TCMT IO Doc
    "."
      (Signature -> Signature) -> m ()
    forall (m :: * -> *).
    MonadTCState m =>
    (Signature -> Signature) -> m ()
    modifySignature ((Signature -> Signature) -> m ())
    -> (Signature -> Signature) -> m ()
    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
    $ ([Polarity] -> [Polarity]) -> Definition -> Definition
    updateDefPolarity (([Polarity] -> [Polarity]) -> Definition -> Definition)
    -> ([Polarity] -> [Polarity]) -> Definition -> Definition
    forall a b. (a -> b) -> a -> b
    $ [Polarity] -> [Polarity] -> [Polarity]
    forall a b. a -> b -> a
    const [Polarity]
    pol

    -- | Look up the forced arguments of a definition.
    getForcedArgs :: HasConstInfo m => QName -> m [IsForced]
    getForcedArgs :: forall (m :: * -> *). HasConstInfo m => QName -> m [IsForced]
    getForcedArgs QName
    q = Definition -> [IsForced]
    defForced (Definition -> [IsForced]) -> m Definition -> m [IsForced]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> QName -> m Definition
    forall (m :: * -> *). HasConstInfo m => QName -> m Definition
    getConstInfo QName
    q

    -- | Get argument occurrence info for argument @i@ of definition @d@ (never fails).
    getArgOccurrence :: QName -> Nat -> TCM Occurrence
    getArgOccurrence :: QName -> Int -> TCM Occurrence
    getArgOccurrence QName
    d Int
    i = do
      Definition
    def <- QName -> TCMT IO Definition
    forall (m :: * -> *). HasConstInfo m => QName -> m Definition
    getConstInfo QName
    d
      Occurrence -> TCM Occurrence
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Occurrence -> TCM Occurrence) -> Occurrence -> TCM Occurrence
    forall a b. (a -> b) -> a -> b
    $! case Definition -> Defn
    theDef Definition
    def of
        Constructor{} -> Occurrence
    StrictPos
        Defn
    _             -> Occurrence -> Maybe Occurrence -> Occurrence
    forall a. a -> Maybe a -> a
    fromMaybe Occurrence
    Mixed (Maybe Occurrence -> Occurrence) -> Maybe Occurrence -> Occurrence
    forall a b. (a -> b) -> a -> b
    $ Definition -> [Occurrence]
    defArgOccurrences Definition
    def [Occurrence] -> Int -> Maybe Occurrence
    forall a. [a] -> Int -> Maybe a
    !!! Int
    i

    -- | Sets the 'defArgOccurrences' for the given identifier (which
    -- should already exist in the signature).
    setArgOccurrences :: MonadTCState m => QName -> [Occurrence] -> m ()
    setArgOccurrences :: forall (m :: * -> *).
    MonadTCState m =>
    QName -> [Occurrence] -> m ()
    setArgOccurrences QName
    d [Occurrence]
    os = QName -> ([Occurrence] -> [Occurrence]) -> m ()
    forall (m :: * -> *).
    MonadTCState m =>
    QName -> ([Occurrence] -> [Occurrence]) -> m ()
    modifyArgOccurrences QName
    d (([Occurrence] -> [Occurrence]) -> m ())
    -> ([Occurrence] -> [Occurrence]) -> m ()
    forall a b. (a -> b) -> a -> b
    $ [Occurrence] -> [Occurrence] -> [Occurrence]
    forall a b. a -> b -> a
    const [Occurrence]
    os

    modifyArgOccurrences :: MonadTCState m => QName -> ([Occurrence] -> [Occurrence]) -> m ()
    modifyArgOccurrences :: forall (m :: * -> *).
    MonadTCState m =>
    QName -> ([Occurrence] -> [Occurrence]) -> m ()
    modifyArgOccurrences QName
    d [Occurrence] -> [Occurrence]
    f =
      (Signature -> Signature) -> m ()
    forall (m :: * -> *).
    MonadTCState m =>
    (Signature -> Signature) -> m ()
    modifySignature ((Signature -> Signature) -> m ())
    -> (Signature -> Signature) -> m ()
    forall a b. (a -> b) -> a -> b
    $ QName -> (Definition -> Definition) -> Signature -> Signature
    updateDefinition QName
    d ((Definition -> Definition) -> Signature -> Signature)
    -> (Definition -> Definition) -> Signature -> Signature
    forall a b. (a -> b) -> a -> b
    $ ([Occurrence] -> [Occurrence]) -> Definition -> Definition
    updateDefArgOccurrences [Occurrence] -> [Occurrence]
    f

    setTreeless :: QName -> TTerm -> TCM ()
    setTreeless :: QName -> TTerm -> TCM ()
    setTreeless QName
    q TTerm
    t =
      QName -> (Definition -> Definition) -> TCM ()
    forall (m :: * -> *).
    MonadTCState m =>
    QName -> (Definition -> Definition) -> m ()
    modifyGlobalDefinition QName
    q ((Definition -> Definition) -> TCM ())
    -> (Definition -> Definition) -> TCM ()
    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
        fun :: Defn
    fun@Function{} -> Defn
    fun{ funTreeless :: Maybe Compiled
    funTreeless = Compiled -> Maybe Compiled
    forall a. a -> Maybe a
    Just (Compiled -> Maybe Compiled) -> Compiled -> Maybe Compiled
    forall a b. (a -> b) -> a -> b
    $ TTerm -> Maybe [ArgUsage] -> Compiled
    Compiled TTerm
    t Maybe [ArgUsage]
    forall a. Maybe a
    Nothing }
        Defn
    _ -> Defn
    forall a. HasCallStack => a
    __IMPOSSIBLE__

    setCompiledArgUse :: QName -> [ArgUsage] -> TCM ()
    setCompiledArgUse :: QName -> [ArgUsage] -> TCM ()
    setCompiledArgUse QName
    q [ArgUsage]
    use =
      QName -> (Definition -> Definition) -> TCM ()
    forall (m :: * -> *).
    MonadTCState m =>
    QName -> (Definition -> Definition) -> m ()
    modifyGlobalDefinition QName
    q ((Definition -> Definition) -> TCM ())
    -> (Definition -> Definition) -> TCM ()
    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
        fun :: Defn
    fun@Function{} ->
          Defn
    fun{ funTreeless :: Maybe Compiled
    funTreeless = Defn -> Maybe Compiled
    funTreeless Defn
    fun Maybe Compiled -> (Compiled -> Compiled) -> Maybe Compiled
    forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
    <&> \ Compiled
    c -> Compiled
    c { cArgUsage :: Maybe [ArgUsage]
    cArgUsage = [ArgUsage] -> Maybe [ArgUsage]
    forall a. a -> Maybe a
    Just [ArgUsage]
    use } }
        Defn
    _ -> Defn
    forall a. HasCallStack => a
    __IMPOSSIBLE__

    getCompiled :: HasConstInfo m => QName -> m (Maybe Compiled)
    getCompiled :: forall (m :: * -> *). HasConstInfo m => QName -> m (Maybe Compiled)
    getCompiled QName
    q = do
      (Definition -> Defn
    theDef (Definition -> Defn) -> m Definition -> m Defn
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> QName -> m Definition
    forall (m :: * -> *). HasConstInfo m => QName -> m Definition
    getConstInfo QName
    q) m Defn -> (Defn -> Maybe Compiled) -> m (Maybe Compiled)
    forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
    <&> \case
        Function{ funTreeless :: Defn -> Maybe Compiled
    funTreeless = Maybe Compiled
    t } -> Maybe Compiled
    t
        Defn
    _                           -> Maybe Compiled
    forall a. Maybe a
    Nothing

    -- | Returns a list of length 'conArity'.
    --   If no erasure analysis has been performed yet, this will be a list of 'False's.
    getErasedConArgs :: HasConstInfo m => QName -> m [Bool]
    getErasedConArgs :: forall (m :: * -> *). HasConstInfo m => QName -> m [Bool]
    getErasedConArgs QName
    q = do
      Definition
    def <- QName -> m Definition
    forall (m :: * -> *). HasConstInfo m => QName -> m Definition
    getConstInfo QName
    q
      case Definition -> Defn
    theDef Definition
    def of
        Constructor{ Int
    conArity :: Defn -> Int
    conArity :: Int
    conArity, Maybe [Bool]
    conErased :: Defn -> Maybe [Bool]
    conErased :: Maybe [Bool]
    conErased } -> [Bool] -> m [Bool]
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([Bool] -> m [Bool]) -> [Bool] -> m [Bool]
    forall a b. (a -> b) -> a -> b
    $
          [Bool] -> Maybe [Bool] -> [Bool]
    forall a. a -> Maybe a -> a
    fromMaybe (Int -> Bool -> [Bool]
    forall a. Int -> a -> [a]
    replicate Int
    conArity Bool
    False) Maybe [Bool]
    conErased
        Defn
    _ -> m [Bool]
    forall a. HasCallStack => a
    __IMPOSSIBLE__

    setErasedConArgs :: QName -> [Bool] -> TCM ()
    setErasedConArgs :: QName -> [Bool] -> TCM ()
    setErasedConArgs QName
    q [Bool]
    args = QName -> (Definition -> Definition) -> TCM ()
    forall (m :: * -> *).
    MonadTCState m =>
    QName -> (Definition -> Definition) -> m ()
    modifyGlobalDefinition QName
    q ((Definition -> Definition) -> TCM ())
    -> (Definition -> Definition) -> TCM ()
    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@Constructor{ Int
    conArity :: Int
    conArity :: Defn -> Int
    conArity }
          | [Bool] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length [Bool]
    args Int -> Int -> Bool
    forall a. Eq a => a -> a -> Bool
    == Int
    conArity -> Defn
    def{ conErased :: Maybe [Bool]
    conErased = [Bool] -> Maybe [Bool]
    forall a. a -> Maybe a
    Just [Bool]
    args }
          | Bool
    otherwise               -> Defn
    forall a. HasCallStack => a
    __IMPOSSIBLE__
        Defn
    def -> Defn
    def   -- no-op for non-constructors

    getTreeless :: HasConstInfo m => QName -> m (Maybe TTerm)
    getTreeless :: forall (m :: * -> *). HasConstInfo m => QName -> m (Maybe TTerm)
    getTreeless QName
    q = (Compiled -> TTerm) -> Maybe Compiled -> Maybe TTerm
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap Compiled -> TTerm
    cTreeless (Maybe Compiled -> Maybe TTerm)
    -> m (Maybe Compiled) -> m (Maybe TTerm)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> QName -> m (Maybe Compiled)
    forall (m :: * -> *). HasConstInfo m => QName -> m (Maybe Compiled)
    getCompiled QName
    q

    getCompiledArgUse :: HasConstInfo m => QName -> m (Maybe [ArgUsage])
    getCompiledArgUse :: forall (m :: * -> *).
    HasConstInfo m =>
    QName -> m (Maybe [ArgUsage])
    getCompiledArgUse QName
    q = (Compiled -> Maybe [ArgUsage]
    cArgUsage (Compiled -> Maybe [ArgUsage])
    -> Maybe Compiled -> Maybe [ArgUsage]
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<<) (Maybe Compiled -> Maybe [ArgUsage])
    -> m (Maybe Compiled) -> m (Maybe [ArgUsage])
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> QName -> m (Maybe Compiled)
    forall (m :: * -> *). HasConstInfo m => QName -> m (Maybe Compiled)
    getCompiled QName
    q

    -- | add data constructors to a datatype
    addDataCons :: QName -> [QName] -> TCM ()
    addDataCons :: QName -> [QName] -> TCM ()
    addDataCons QName
    d [QName]
    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
    d ((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
    def ->
      let !cs' :: [QName]
    cs' = [QName]
    cs [QName] -> [QName] -> [QName]
    forall a. [a] -> [a] -> [a]
    ++ Defn -> [QName]
    dataCons Defn
    def in
      case Defn
    def of
        Datatype{} -> Defn
    def {dataCons :: [QName]
    dataCons = [QName]
    cs' }
        Defn
    _          -> Defn
    forall a. HasCallStack => a
    __IMPOSSIBLE__

    -- | Get the mutually recursive identifiers of a symbol from the signature.
    getMutual :: QName -> TCM (Maybe [QName])
    getMutual :: QName -> TCM (Maybe [QName])
    getMutual QName
    d = Defn -> Maybe [QName]
    getMutual_ (Defn -> Maybe [QName])
    -> (Definition -> Defn) -> Definition -> Maybe [QName]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Definition -> Defn
    theDef (Definition -> Maybe [QName])
    -> TCMT IO Definition -> TCM (Maybe [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
    d

    -- | Get the mutually recursive identifiers from a `Definition`.
    getMutual_ :: Defn -> Maybe [QName]
    getMutual_ :: Defn -> Maybe [QName]
    getMutual_ = \case
        Function {  funMutual :: Defn -> Maybe [QName]
    funMutual = Maybe [QName]
    m } -> Maybe [QName]
    m
        Datatype { dataMutual :: Defn -> Maybe [QName]
    dataMutual = Maybe [QName]
    m } -> Maybe [QName]
    m
        Record   {  recMutual :: Defn -> Maybe [QName]
    recMutual = Maybe [QName]
    m } -> Maybe [QName]
    m
        Defn
    _ -> Maybe [QName]
    forall a. Maybe a
    Nothing

    -- | Set the mutually recursive identifiers.
    setMutual :: QName -> [QName] -> TCM ()
    setMutual :: QName -> [QName] -> TCM ()
    setMutual QName
    d [QName]
    m = (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
    d ((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
    def ->
      case Defn
    def of
        Function{} -> Defn
    def { funMutual :: Maybe [QName]
    funMutual = [QName] -> Maybe [QName]
    forall a. a -> Maybe a
    Just [QName]
    m }
        Datatype{} -> Defn
    def {dataMutual :: Maybe [QName]
    dataMutual = [QName] -> Maybe [QName]
    forall a. a -> Maybe a
    Just [QName]
    m }
        Record{}   -> Defn
    def { recMutual :: Maybe [QName]
    recMutual = [QName] -> Maybe [QName]
    forall a. a -> Maybe a
    Just [QName]
    m }
        Defn
    _          -> if [QName] -> Bool
    forall a. Null a => a -> Bool
    null [QName]
    m then Defn
    def else Defn
    forall a. HasCallStack => a
    __IMPOSSIBLE__ -- nothing to do

    -- | Check whether two definitions are mutually recursive.
    mutuallyRecursive :: QName -> QName -> TCM Bool
    mutuallyRecursive :: QName -> QName -> TCMT IO Bool
    mutuallyRecursive QName
    d QName
    d1 = (QName
    d QName -> [QName] -> Bool
    forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
    `elem`) ([QName] -> Bool)
    -> (Maybe [QName] -> [QName]) -> Maybe [QName] -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [QName] -> Maybe [QName] -> [QName]
    forall a. a -> Maybe a -> a
    fromMaybe [QName]
    forall a. HasCallStack => a
    __IMPOSSIBLE__ (Maybe [QName] -> Bool) -> TCM (Maybe [QName]) -> TCMT IO Bool
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> QName -> TCM (Maybe [QName])
    getMutual QName
    d1

    -- | A function/data/record definition is nonRecursive if it is not even mutually
    --   recursive with itself.
    definitelyNonRecursive_ :: Defn -> Bool
    definitelyNonRecursive_ :: Defn -> Bool
    definitelyNonRecursive_ = Bool -> ([QName] -> Bool) -> Maybe [QName] -> Bool
    forall b a. b -> (a -> b) -> Maybe a -> b
    maybe Bool
    False [QName] -> Bool
    forall a. Null a => a -> Bool
    null (Maybe [QName] -> Bool) -> (Defn -> Maybe [QName]) -> Defn -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Defn -> Maybe [QName]
    getMutual_

    -- | Get the number of parameters to the current module.
    getCurrentModuleFreeVars :: TCM Nat
    getCurrentModuleFreeVars :: TCMT IO Int
    getCurrentModuleFreeVars = Telescope -> Int
    forall a. Sized a => a -> Int
    size (Telescope -> Int) -> TCMT IO Telescope -> TCMT IO Int
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (ModuleName -> TCMT IO Telescope
    forall (m :: * -> *).
    (Functor m, ReadTCState m) =>
    ModuleName -> m Telescope
    lookupSection (ModuleName -> TCMT IO Telescope)
    -> TCMT IO ModuleName -> TCMT IO Telescope
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< TCMT IO ModuleName
    forall (m :: * -> *). MonadTCEnv m => m ModuleName
    currentModule)

    --   For annoying reasons the qnameModule of a pattern lambda is not correct
    --   (#2883), so make sure to grab the right module for those.
    getDefModule :: HasConstInfo m => QName -> m (Either SigError ModuleName)
    getDefModule :: forall (m :: * -> *).
    HasConstInfo m =>
    QName -> m (Either SigError ModuleName)
    getDefModule QName
    f = (Definition -> ModuleName)
    -> Either SigError Definition -> Either SigError ModuleName
    forall b d a. (b -> d) -> Either a b -> Either a d
    mapRight Definition -> ModuleName
    modName (Either SigError Definition -> Either SigError ModuleName)
    -> m (Either SigError Definition) -> m (Either SigError ModuleName)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> QName -> m (Either SigError Definition)
    forall (m :: * -> *).
    HasConstInfo m =>
    QName -> m (Either SigError Definition)
    getConstInfo' QName
    f
      where
        modName :: Definition -> ModuleName
    modName Definition
    def = case Definition -> Defn
    theDef Definition
    def of
          Function{ funExtLam :: Defn -> Maybe ExtLamInfo
    funExtLam = Just (ExtLamInfo ModuleName
    m Bool
    _ Maybe System
    _) } -> ModuleName
    m
          Defn
    _                                               -> QName -> ModuleName
    qnameModule QName
    f

    -- | Compute the number of free variables of a defined name. This is the sum of
    --   number of parameters shared with the current module and the number of
    --   anonymous variables (if the name comes from a let-bound module).
    getDefFreeVars :: (Functor m, Applicative m, ReadTCState m, MonadTCEnv m) => QName -> m Nat
    getDefFreeVars :: forall (m :: * -> *).
    (Functor m, Applicative m, ReadTCState m, MonadTCEnv m) =>
    QName -> m Int
    getDefFreeVars = ModuleName -> m Int
    forall (m :: * -> *).
    (Functor m, Applicative m, MonadTCEnv m, ReadTCState m) =>
    ModuleName -> m Int
    getModuleFreeVars (ModuleName -> m Int) -> (QName -> ModuleName) -> QName -> m Int
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . QName -> ModuleName
    qnameModule

    freeVarsToApply :: (Functor m, HasConstInfo m, HasOptions m,
                        ReadTCState m, MonadTCEnv m, MonadDebug m)
                    => QName -> m Args
    freeVarsToApply :: forall (m :: * -> *).
    (Functor m, HasConstInfo m, HasOptions m, ReadTCState m,
     MonadTCEnv m, MonadDebug m) =>
    QName -> m [Arg Term]
    freeVarsToApply QName
    q = do
      [Arg Term]
    vs <- ModuleName -> m [Arg Term]
    forall (m :: * -> *).
    (Functor m, Applicative m, HasOptions m, MonadTCEnv m,
     ReadTCState m, MonadDebug m) =>
    ModuleName -> m [Arg Term]
    moduleParamsToApply (ModuleName -> m [Arg Term]) -> ModuleName -> m [Arg Term]
    forall a b. (a -> b) -> a -> b
    $ QName -> ModuleName
    qnameModule QName
    q
      -- Andreas, 2021-07-14, issue #5470
      -- getConstInfo will fail if q is not in scope,
      -- but in this case there are no free vars to apply, since
      -- we cannot be in a child module of its defining module.
      -- So if we short cut the nil-case here, we avoid the internal error of #5470.
      if [Arg Term] -> Bool
    forall a. Null a => a -> Bool
    null [Arg Term]
    vs then [Arg Term] -> m [Arg Term]
    forall (m :: * -> *) a. Monad m => a -> m a
    return [] else do
      Type
    t <- Definition -> Type
    defType (Definition -> Type) -> m Definition -> m Type
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> QName -> m Definition
    forall (m :: * -> *). HasConstInfo m => QName -> m Definition
    getConstInfo QName
    q
      let TelV Telescope
    tel Type
    _ = Int -> Type -> TelV Type
    telView'UpTo ([Arg Term] -> Int
    forall a. Sized a => a -> Int
    size [Arg Term]
    vs) Type
    t
      Bool -> m () -> m ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    unless (Telescope -> Int
    forall a. Sized a => a -> Int
    size Telescope
    tel Int -> Int -> Bool
    forall a. Eq a => a -> a -> Bool
    == [Arg Term] -> Int
    forall a. Sized a => a -> Int
    size [Arg Term]
    vs) m ()
    forall a. HasCallStack => a
    __IMPOSSIBLE__
      [Arg Term] -> m [Arg Term]
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([Arg Term] -> m [Arg Term]) -> [Arg Term] -> m [Arg Term]
    forall a b. (a -> b) -> a -> b
    $ (Arg Term -> Dom ([Char], Type) -> Arg Term)
    -> [Arg Term] -> [Dom ([Char], Type)] -> [Arg Term]
    forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
    zipWith (\ Arg Term
    arg Dom ([Char], Type)
    dom -> Arg Term -> Term
    forall e. Arg e -> e
    unArg Arg Term
    arg Term -> Arg ([Char], Type) -> Arg Term
    forall (f :: * -> *) a b. Functor f => a -> f b -> f a
    <$ Dom ([Char], Type) -> Arg ([Char], Type)
    forall t a. Dom' t a -> Arg a
    argFromDom Dom ([Char], Type)
    dom) [Arg Term]
    vs ([Dom ([Char], Type)] -> [Arg Term])
    -> [Dom ([Char], Type)] -> [Arg Term]
    forall a b. (a -> b) -> a -> b
    $ Telescope -> [Dom ([Char], Type)]
    forall t. Tele (Dom t) -> [Dom ([Char], t)]
    telToList Telescope
    tel

    {-# SPECIALIZE getModuleFreeVars :: ModuleName -> TCM Nat #-}
    {-# SPECIALIZE getModuleFreeVars :: ModuleName -> ReduceM Nat #-}
    getModuleFreeVars :: (Functor m, Applicative m, MonadTCEnv m, ReadTCState m)
                      => ModuleName -> m Nat
    getModuleFreeVars :: forall (m :: * -> *).
    (Functor m, Applicative m, MonadTCEnv m, ReadTCState m) =>
    ModuleName -> m Int
    getModuleFreeVars ModuleName
    m = do
      ModuleName
    m0   <- ModuleName -> ModuleName -> ModuleName
    commonParentModule ModuleName
    m (ModuleName -> ModuleName) -> m ModuleName -> m ModuleName
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> m ModuleName
    forall (m :: * -> *). MonadTCEnv m => m ModuleName
    currentModule
      Int -> Int -> Int
    forall a. Num a => a -> a -> a
    (+) (Int -> Int -> Int) -> m Int -> m (Int -> Int)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> ModuleName -> m Int
    forall (m :: * -> *). MonadTCEnv m => ModuleName -> m Int
    getAnonymousVariables ModuleName
    m m (Int -> Int) -> m Int -> m Int
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> (Telescope -> Int
    forall a. Sized a => a -> Int
    size (Telescope -> Int) -> m Telescope -> m Int
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> ModuleName -> m Telescope
    forall (m :: * -> *).
    (Functor m, ReadTCState m) =>
    ModuleName -> m Telescope
    lookupSection ModuleName
    m0)

    -- | Compute the context variables to apply a definition to.
    --
    --   We have to insert the module telescope of the common prefix
    --   of the current module and the module where the definition comes from.
    --   (Properly raised to the current context.)
    --
    --   Example:
    --   @
    --      module M₁ Γ where
    --        module M₁ Δ where
    --          f = ...
    --        module M₃ Θ where
    --          ... M₁.M₂.f [insert Γ raised by Θ]
    --   @
    moduleParamsToApply :: (Functor m, Applicative m, HasOptions m,
                            MonadTCEnv m, ReadTCState m, MonadDebug m)
                        => ModuleName -> m Args
    moduleParamsToApply :: forall (m :: * -> *).
    (Functor m, Applicative m, HasOptions m, MonadTCEnv m,
     ReadTCState m, MonadDebug m) =>
    ModuleName -> m [Arg Term]
    moduleParamsToApply ModuleName
    m = do

      [Char] -> Int -> TCMT IO Doc -> m [Arg Term] -> m [Arg Term]
    forall (m :: * -> *) a.
    MonadDebug m =>
    [Char] -> Int -> TCMT IO Doc -> m a -> m a
    traceSDoc [Char]
    "tc.sig.param" Int
    90 (TCMT IO Doc
    "computing module parameters of " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> ModuleName -> TCMT IO Doc
    forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
    pretty ModuleName
    m) (m [Arg Term] -> m [Arg Term]) -> m [Arg Term] -> m [Arg Term]
    forall a b. (a -> b) -> a -> b
    $ do

      -- Jesper, 2020-01-22: If the module parameter substitution for the
      -- module cannot be found, that likely means we are within a call to
      -- @inTopContext@. In that case we should provide no arguments for
      -- the module parameters (see #4383).
      m (Maybe Substitution)
    -> m [Arg Term] -> (Substitution -> m [Arg Term]) -> m [Arg Term]
    forall (m :: * -> *) a b.
    Monad m =>
    m (Maybe a) -> m b -> (a -> m b) -> m b
    caseMaybeM (ModuleName -> m (Maybe Substitution)
    forall (m :: * -> *).
    (MonadTCEnv m, ReadTCState m) =>
    ModuleName -> m (Maybe Substitution)
    getModuleParameterSub ModuleName
    m) ([Arg Term] -> m [Arg Term]
    forall (m :: * -> *) a. Monad m => a -> m a
    return []) ((Substitution -> m [Arg Term]) -> m [Arg Term])
    -> (Substitution -> m [Arg Term]) -> m [Arg Term]
    forall a b. (a -> b) -> a -> b
    $ \Substitution
    sub -> do

      [Char] -> Int -> TCMT IO Doc -> m [Arg Term] -> m [Arg Term]
    forall (m :: * -> *) a.
    MonadDebug m =>
    [Char] -> Int -> TCMT IO Doc -> m a -> m a
    traceSDoc [Char]
    "tc.sig.param" Int
    60 (do
        [Dom (Name, Type)]
    cxt <- TCMT IO [Dom (Name, Type)]
    forall (m :: * -> *). MonadTCEnv m => m [Dom (Name, Type)]
    getContext
        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] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    vcat
          [ TCMT IO Doc
    "cxt  = " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> PrettyContext -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM ([Dom (Name, Type)] -> PrettyContext
    PrettyContext [Dom (Name, Type)]
    cxt)
          , TCMT IO Doc
    "sub  = " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Substitution -> TCMT IO Doc
    forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
    pretty Substitution
    sub
          ]) (m [Arg Term] -> m [Arg Term]) -> m [Arg Term] -> m [Arg Term]
    forall a b. (a -> b) -> a -> b
    $ do

      -- Get the correct number of free variables (correctly raised) of @m@.
      Int
    n   <- ModuleName -> m Int
    forall (m :: * -> *).
    (Functor m, Applicative m, MonadTCEnv m, ReadTCState m) =>
    ModuleName -> m Int
    getModuleFreeVars ModuleName
    m
      [Char] -> Int -> TCMT IO Doc -> m [Arg Term] -> m [Arg Term]
    forall (m :: * -> *) a.
    MonadDebug m =>
    [Char] -> Int -> TCMT IO Doc -> m a -> m a
    traceSDoc [Char]
    "tc.sig.param" Int
    60 (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
    "n    = " 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 (Int -> [Char]
    forall a. Show a => a -> [Char]
    show Int
    n)) (m [Arg Term] -> m [Arg Term]) -> m [Arg Term] -> m [Arg Term]
    forall a b. (a -> b) -> a -> b
    $ do
      [Dom ([Char], Type)]
    tel <- Int -> [Dom ([Char], Type)] -> [Dom ([Char], Type)]
    forall a. Int -> [a] -> [a]
    take Int
    n ([Dom ([Char], Type)] -> [Dom ([Char], Type)])
    -> (Telescope -> [Dom ([Char], Type)])
    -> Telescope
    -> [Dom ([Char], Type)]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Telescope -> [Dom ([Char], Type)]
    forall t. Tele (Dom t) -> [Dom ([Char], t)]
    telToList (Telescope -> [Dom ([Char], Type)])
    -> m Telescope -> m [Dom ([Char], Type)]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> ModuleName -> m Telescope
    forall (m :: * -> *).
    (Functor m, ReadTCState m) =>
    ModuleName -> m Telescope
    lookupSection ModuleName
    m
      [Char] -> Int -> TCMT IO Doc -> m [Arg Term] -> m [Arg Term]
    forall (m :: * -> *) a.
    MonadDebug m =>
    [Char] -> Int -> TCMT IO Doc -> m a -> m a
    traceSDoc [Char]
    "tc.sig.param" Int
    60 (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
    <+> [Dom ([Char], Type)] -> TCMT IO Doc
    forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
    pretty [Dom ([Char], Type)]
    tel) (m [Arg Term] -> m [Arg Term]) -> m [Arg Term] -> m [Arg Term]
    forall a b. (a -> b) -> a -> b
    $ do
      Bool -> m () -> m ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    unless ([Dom ([Char], Type)] -> Int
    forall a. Sized a => a -> Int
    size [Dom ([Char], Type)]
    tel Int -> Int -> Bool
    forall a. Eq a => a -> a -> Bool
    == Int
    n) m ()
    forall a. HasCallStack => a
    __IMPOSSIBLE__
      let args :: [Arg Term]
    args = Substitution' (SubstArg [Arg Term]) -> [Arg Term] -> [Arg Term]
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    applySubst Substitution
    Substitution' (SubstArg [Arg Term])
    sub ([Arg Term] -> [Arg Term]) -> [Arg Term] -> [Arg Term]
    forall a b. (a -> b) -> a -> b
    $ (Int -> Dom ([Char], Type) -> Arg Term)
    -> [Int] -> [Dom ([Char], Type)] -> [Arg Term]
    forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
    zipWith (\ Int
    i Dom ([Char], Type)
    a -> Int -> Term
    var Int
    i Term -> Arg ([Char], Type) -> Arg Term
    forall (f :: * -> *) a b. Functor f => a -> f b -> f a
    <$ Dom ([Char], Type) -> Arg ([Char], Type)
    forall t a. Dom' t a -> Arg a
    argFromDom Dom ([Char], Type)
    a) (Int -> [Int]
    forall a. Integral a => a -> [a]
    downFrom Int
    n) [Dom ([Char], Type)]
    tel
      [Char] -> Int -> TCMT IO Doc -> m [Arg Term] -> m [Arg Term]
    forall (m :: * -> *) a.
    MonadDebug m =>
    [Char] -> Int -> TCMT IO Doc -> m a -> m a
    traceSDoc [Char]
    "tc.sig.param" Int
    60 (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, Semigroup (m Doc), Foldable t) =>
    t (m Doc) -> m Doc
    prettyList_ ((Arg Term -> TCMT IO Doc) -> [Arg Term] -> [TCMT IO Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map Arg Term -> TCMT IO Doc
    forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
    pretty [Arg Term]
    args)) (m [Arg Term] -> m [Arg Term]) -> m [Arg Term] -> m [Arg Term]
    forall a b. (a -> b) -> a -> b
    $ do

      -- Apply the original ArgInfo, as the hiding information in the current
      -- context might be different from the hiding information expected by @m@.

      ModuleName -> m (Maybe Section)
    forall (m :: * -> *).
    (Functor m, ReadTCState m) =>
    ModuleName -> m (Maybe Section)
    getSection ModuleName
    m m (Maybe Section)
    -> (Maybe Section -> m [Arg Term]) -> m [Arg Term]
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \case
        Maybe Section
    Nothing -> do
          -- We have no section for @m@.
          -- This should only happen for toplevel definitions, and then there
          -- are no free vars to apply, or?
          -- unless (null args) __IMPOSSIBLE__
          -- No, this invariant is violated by private modules, see Issue1701a.
          [Arg Term] -> m [Arg Term]
    forall (m :: * -> *) a. Monad m => a -> m a
    return [Arg Term]
    args
        Just (Section Telescope
    stel) -> do
          -- The section telescope of @m@ should be as least
          -- as long as the number of free vars @m@ is applied to.
          -- We still check here as in no case, we want @zipWith@ to silently
          -- drop some @args@.
          -- And there are also anonymous modules, thus, the invariant is not trivial.
          Bool -> m () -> m ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    when (Telescope -> Int
    forall a. Sized a => a -> Int
    size Telescope
    stel Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    < [Arg Term] -> Int
    forall a. Sized a => a -> Int
    size [Arg Term]
    args) m ()
    forall a. HasCallStack => a
    __IMPOSSIBLE__
          [Arg Term] -> m [Arg Term]
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([Arg Term] -> m [Arg Term]) -> [Arg Term] -> m [Arg Term]
    forall a b. (a -> b) -> a -> b
    $ (Dom ([Char], Type) -> Arg Term -> Arg Term)
    -> [Dom ([Char], Type)] -> [Arg Term] -> [Arg Term]
    forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
    zipWith (\ !Dom ([Char], Type)
    dom (Arg ArgInfo
    _ Term
    v) -> Term
    v Term -> Arg ([Char], Type) -> Arg Term
    forall (f :: * -> *) a b. Functor f => a -> f b -> f a
    <$ Dom ([Char], Type) -> Arg ([Char], Type)
    forall t a. Dom' t a -> Arg a
    argFromDom Dom ([Char], Type)
    dom) (Telescope -> [Dom ([Char], Type)]
    forall t. Tele (Dom t) -> [Dom ([Char], t)]
    telToList Telescope
    stel) [Arg Term]
    args

    -- | Unless all variables in the context are module parameters, create a fresh
    --   module to capture the non-module parameters. Used when unquoting to make
    --   sure generated definitions work properly.
    inFreshModuleIfFreeParams :: TCM a -> TCM a
    inFreshModuleIfFreeParams :: forall a. TCM a -> TCM a
    inFreshModuleIfFreeParams TCM a
    k = do
      Maybe Substitution
    msub <- ModuleName -> TCMT IO (Maybe Substitution)
    forall (m :: * -> *).
    (MonadTCEnv m, ReadTCState m) =>
    ModuleName -> m (Maybe Substitution)
    getModuleParameterSub (ModuleName -> TCMT IO (Maybe Substitution))
    -> TCMT IO ModuleName -> TCMT IO (Maybe Substitution)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< TCMT IO ModuleName
    forall (m :: * -> *). MonadTCEnv m => m ModuleName
    currentModule
      if Maybe Substitution -> Bool
    forall a. Maybe a -> Bool
    isNothing Maybe Substitution
    msub Bool -> Bool -> Bool
    || Maybe Substitution
    msub Maybe Substitution -> Maybe Substitution -> Bool
    forall a. Eq a => a -> a -> Bool
    == Substitution -> Maybe Substitution
    forall a. a -> Maybe a
    Just Substitution
    forall a. Substitution' a
    IdS then TCM a
    k else do
        ModuleName
    m  <- TCMT IO ModuleName
    forall (m :: * -> *). MonadTCEnv m => m ModuleName
    currentModule
        ModuleName
    m' <- ModuleName -> ModuleName -> ModuleName
    qualifyM ModuleName
    m (ModuleName -> ModuleName)
    -> (Name -> ModuleName) -> Name -> ModuleName
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . List1 Name -> ModuleName
    mnameFromList1 (List1 Name -> ModuleName)
    -> (Name -> List1 Name) -> Name -> ModuleName
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Name -> List1 Name
    forall el coll. Singleton el coll => el -> coll
    singleton (Name -> ModuleName) -> TCMT IO Name -> TCMT IO ModuleName
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$>
                [Char] -> TCMT IO Name
    forall a (m :: * -> *).
    (FreshName a, MonadFresh NameId m) =>
    a -> m Name
    freshName_ ([Char]
    "_" :: String)
        ModuleName -> TCM ()
    addSection ModuleName
    m'
        ModuleName -> TCM a -> TCM a
    forall (m :: * -> *) a. MonadTCEnv m => ModuleName -> m a -> m a
    withCurrentModule ModuleName
    m' TCM a
    k

    -- | Instantiate a closed definition with the correct part of the current
    --   context.
    {-# SPECIALIZE instantiateDef :: Definition -> TCM Definition #-}
    instantiateDef
      :: ( Functor m, HasConstInfo m, HasOptions m
         , ReadTCState m, MonadTCEnv m, MonadDebug m )
      => Definition -> m Definition
    instantiateDef :: forall (m :: * -> *).
    (Functor m, HasConstInfo m, HasOptions m, ReadTCState m,
     MonadTCEnv m, MonadDebug m) =>
    Definition -> m Definition
    instantiateDef Definition
    d = do
      [Arg Term]
    vs  <- QName -> m [Arg Term]
    forall (m :: * -> *).
    (Functor m, HasConstInfo m, HasOptions m, ReadTCState m,
     MonadTCEnv m, MonadDebug m) =>
    QName -> m [Arg Term]
    freeVarsToApply (QName -> m [Arg Term]) -> QName -> m [Arg Term]
    forall a b. (a -> b) -> a -> b
    $ Definition -> QName
    defName Definition
    d
      [Char] -> Int -> m () -> m ()
    forall (m :: * -> *). MonadDebug m => [Char] -> Int -> m () -> m ()
    verboseS [Char]
    "tc.sig.inst" Int
    30 (m () -> m ()) -> m () -> m ()
    forall a b. (a -> b) -> a -> b
    $ do
        [Dom (Name, Type)]
    ctx <- m [Dom (Name, Type)]
    forall (m :: * -> *). MonadTCEnv m => m [Dom (Name, Type)]
    getContext
        ModuleName
    m   <- m ModuleName
    forall (m :: * -> *). MonadTCEnv m => m ModuleName
    currentModule
        [Char] -> Int -> TCMT IO Doc -> m ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "tc.sig.inst" Int
    30 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
    forall a b. (a -> b) -> a -> b
    $
          TCMT IO Doc
    "instDef in" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> ModuleName -> TCMT IO Doc
    forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
    pretty ModuleName
    m 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 (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> QName -> TCMT IO Doc
    forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
    pretty (Definition -> QName
    defName Definition
    d) 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
    fsep ((Arg Name -> TCMT IO Doc) -> [Arg Name] -> [TCMT IO Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map Arg Name -> TCMT IO Doc
    forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
    pretty ([Arg Name] -> [TCMT IO Doc]) -> [Arg Name] -> [TCMT IO Doc]
    forall a b. (a -> b) -> a -> b
    $ (Name -> Arg Term -> Arg Name)
    -> [Name] -> [Arg Term] -> [Arg Name]
    forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
    zipWith Name -> Arg Term -> Arg Name
    forall (f :: * -> *) a b. Functor f => a -> f b -> f a
    (<$) ([Name] -> [Name]
    forall a. [a] -> [a]
    reverse ([Name] -> [Name]) -> [Name] -> [Name]
    forall a b. (a -> b) -> a -> b
    $ (Dom (Name, Type) -> Name) -> [Dom (Name, Type)] -> [Name]
    forall a b. (a -> b) -> [a] -> [b]
    map ((Name, Type) -> Name
    forall a b. (a, b) -> a
    fst ((Name, Type) -> Name)
    -> (Dom (Name, Type) -> (Name, Type)) -> Dom (Name, Type) -> Name
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Dom (Name, Type) -> (Name, Type)
    forall t e. Dom' t e -> e
    unDom) [Dom (Name, Type)]
    ctx) [Arg Term]
    vs)
      Definition -> m Definition
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Definition -> m Definition) -> Definition -> m Definition
    forall a b. (a -> b) -> a -> b
    $ Definition
    d Definition -> [Arg Term] -> Definition
    forall t. Apply t => t -> [Arg Term] -> t
    `apply` [Arg Term]
    vs

    instantiateRewriteRule :: (Functor m, HasConstInfo m, HasOptions m,
                               ReadTCState m, MonadTCEnv m, MonadDebug m)
                           => RewriteRule -> m RewriteRule
    instantiateRewriteRule :: forall (m :: * -> *).
    (Functor m, HasConstInfo m, HasOptions m, ReadTCState m,
     MonadTCEnv m, MonadDebug m) =>
    RewriteRule -> m RewriteRule
    instantiateRewriteRule RewriteRule
    rew = do
      [Char] -> Int -> TCMT IO Doc -> m RewriteRule -> m RewriteRule
    forall (m :: * -> *) a.
    MonadDebug m =>
    [Char] -> Int -> TCMT IO Doc -> m a -> m a
    traceSDoc [Char]
    "rewriting" Int
    95 (TCMT IO Doc
    "instantiating rewrite rule" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> QName -> TCMT IO Doc
    forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
    pretty (RewriteRule -> QName
    rewName RewriteRule
    rew) TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> TCMT IO Doc
    "to the local context.") (m RewriteRule -> m RewriteRule) -> m RewriteRule -> m RewriteRule
    forall a b. (a -> b) -> a -> b
    $ do
      [Arg Term]
    vs  <- QName -> m [Arg Term]
    forall (m :: * -> *).
    (Functor m, HasConstInfo m, HasOptions m, ReadTCState m,
     MonadTCEnv m, MonadDebug m) =>
    QName -> m [Arg Term]
    freeVarsToApply (QName -> m [Arg Term]) -> QName -> m [Arg Term]
    forall a b. (a -> b) -> a -> b
    $ RewriteRule -> QName
    rewName RewriteRule
    rew
      let rew' :: RewriteRule
    rew' = RewriteRule
    rew RewriteRule -> [Arg Term] -> RewriteRule
    forall t. Apply t => t -> [Arg Term] -> t
    `apply` [Arg Term]
    vs
      [Char] -> Int -> [Char] -> m RewriteRule -> m RewriteRule
    forall (m :: * -> *) a.
    MonadDebug m =>
    [Char] -> Int -> [Char] -> m a -> m a
    traceSLn [Char]
    "rewriting" Int
    95 ([Char]
    "instantiated rewrite rule: ") (m RewriteRule -> m RewriteRule) -> m RewriteRule -> m RewriteRule
    forall a b. (a -> b) -> a -> b
    $ do
      [Char] -> Int -> [Char] -> m RewriteRule -> m RewriteRule
    forall (m :: * -> *) a.
    MonadDebug m =>
    [Char] -> Int -> [Char] -> m a -> m a
    traceSLn [Char]
    "rewriting" Int
    95 (RewriteRule -> [Char]
    forall a. Show a => a -> [Char]
    show RewriteRule
    rew') (m RewriteRule -> m RewriteRule) -> m RewriteRule -> m RewriteRule
    forall a b. (a -> b) -> a -> b
    $ do
      RewriteRule -> m RewriteRule
    forall (m :: * -> *) a. Monad m => a -> m a
    return RewriteRule
    rew'

    instantiateRewriteRules :: (Functor m, HasConstInfo m, HasOptions m,
                                ReadTCState m, MonadTCEnv m, MonadDebug m)
                            => RewriteRules -> m RewriteRules
    instantiateRewriteRules :: forall (m :: * -> *).
    (Functor m, HasConstInfo m, HasOptions m, ReadTCState m,
     MonadTCEnv m, MonadDebug m) =>
    RewriteRules -> m RewriteRules
    instantiateRewriteRules = (RewriteRule -> m RewriteRule) -> RewriteRules -> m RewriteRules
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    mapM RewriteRule -> m RewriteRule
    forall (m :: * -> *).
    (Functor m, HasConstInfo m, HasOptions m, ReadTCState m,
     MonadTCEnv m, MonadDebug m) =>
    RewriteRule -> m RewriteRule
    instantiateRewriteRule

    -- | Give the abstract view of a definition.
    makeAbstract :: Definition -> Maybe Definition
    makeAbstract :: Definition -> Maybe Definition
    makeAbstract Definition
    d =
      case Definition -> IsAbstract
    defAbstract Definition
    d of
        IsAbstract
    ConcreteDef -> Definition -> Maybe Definition
    forall (m :: * -> *) a. Monad m => a -> m a
    return Definition
    d
        IsAbstract
    AbstractDef -> do
          Defn
    def <- Defn -> Maybe Defn
    makeAbs (Defn -> Maybe Defn) -> Defn -> Maybe Defn
    forall a b. (a -> b) -> a -> b
    $ Definition -> Defn
    theDef Definition
    d
          Definition -> Maybe Definition
    forall (m :: * -> *) a. Monad m => a -> m a
    return Definition
    d { defArgOccurrences :: [Occurrence]
    defArgOccurrences = [] -- no positivity info for abstract things!
                   , defPolarity :: [Polarity]
    defPolarity       = [] -- no polarity info for abstract things!
                   , theDef :: Defn
    theDef = Defn
    def
                   }
      where
        makeAbs :: Defn -> Maybe Defn
    makeAbs d :: Defn
    d@Axiom{}            = Defn -> Maybe Defn
    forall a. a -> Maybe a
    Just Defn
    d
        makeAbs d :: Defn
    d@DataOrRecSig{}     = Defn -> Maybe Defn
    forall a. a -> Maybe a
    Just Defn
    d
        makeAbs d :: Defn
    d@GeneralizableVar{} = Defn -> Maybe Defn
    forall a. a -> Maybe a
    Just Defn
    d
        makeAbs d :: Defn
    d@Datatype {} = Defn -> Maybe Defn
    forall a. a -> Maybe a
    Just (Defn -> Maybe Defn) -> Defn -> Maybe Defn
    forall a b. (a -> b) -> a -> b
    $ Defn -> Defn
    AbstractDefn Defn
    d
        makeAbs d :: Defn
    d@Function {} = Defn -> Maybe Defn
    forall a. a -> Maybe a
    Just (Defn -> Maybe Defn) -> Defn -> Maybe Defn
    forall a b. (a -> b) -> a -> b
    $ Defn -> Defn
    AbstractDefn Defn
    d
        makeAbs Constructor{} = Maybe Defn
    forall a. Maybe a
    Nothing
        -- Andreas, 2012-11-18:  Make record constructor and projections abstract.
        -- Andreas, 2017-08-14:  Projections are actually not abstract (issue #2682).
        -- Return the Defn under a wrapper to allow e.g. eligibleForProjectionLike
        -- to see whether the abstract thing is a record type or not.
        makeAbs d :: Defn
    d@Record{}    = Defn -> Maybe Defn
    forall a. a -> Maybe a
    Just (Defn -> Maybe Defn) -> Defn -> Maybe Defn
    forall a b. (a -> b) -> a -> b
    $ Defn -> Defn
    AbstractDefn Defn
    d
        makeAbs Primitive{}   = Maybe Defn
    forall a. HasCallStack => a
    __IMPOSSIBLE__
        makeAbs PrimitiveSort{} = Maybe Defn
    forall a. HasCallStack => a
    __IMPOSSIBLE__
        makeAbs AbstractDefn{}= Maybe Defn
    forall a. HasCallStack => a
    __IMPOSSIBLE__

    -- | Enter abstract mode. Abstract definition in the current module are transparent.
    {-# SPECIALIZE inAbstractMode :: TCM a -> TCM a #-}
    inAbstractMode :: MonadTCEnv m => m a -> m a
    inAbstractMode :: forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
    inAbstractMode = (TCEnv -> TCEnv) -> m a -> m a
    forall (m :: * -> *) a.
    MonadTCEnv m =>
    (TCEnv -> TCEnv) -> m a -> m a
    localTC ((TCEnv -> TCEnv) -> m a -> m a) -> (TCEnv -> TCEnv) -> m a -> m a
    forall a b. (a -> b) -> a -> b
    $ \TCEnv
    e -> TCEnv
    e { envAbstractMode :: AbstractMode
    envAbstractMode = AbstractMode
    AbstractMode }

    -- | Not in abstract mode. All abstract definitions are opaque.
    {-# SPECIALIZE inConcreteMode :: TCM a -> TCM a #-}
    inConcreteMode :: MonadTCEnv m => m a -> m a
    inConcreteMode :: forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
    inConcreteMode = (TCEnv -> TCEnv) -> m a -> m a
    forall (m :: * -> *) a.
    MonadTCEnv m =>
    (TCEnv -> TCEnv) -> m a -> m a
    localTC ((TCEnv -> TCEnv) -> m a -> m a) -> (TCEnv -> TCEnv) -> m a -> m a
    forall a b. (a -> b) -> a -> b
    $ \TCEnv
    e -> TCEnv
    e { envAbstractMode :: AbstractMode
    envAbstractMode = AbstractMode
    ConcreteMode }

    -- | Ignore abstract mode. All abstract definitions are transparent.
    ignoreAbstractMode :: MonadTCEnv m => m a -> m a
    ignoreAbstractMode :: forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
    ignoreAbstractMode = (TCEnv -> TCEnv) -> m a -> m a
    forall (m :: * -> *) a.
    MonadTCEnv m =>
    (TCEnv -> TCEnv) -> m a -> m a
    localTC ((TCEnv -> TCEnv) -> m a -> m a) -> (TCEnv -> TCEnv) -> m a -> m a
    forall a b. (a -> b) -> a -> b
    $ \TCEnv
    e -> TCEnv
    e { envAbstractMode :: AbstractMode
    envAbstractMode = AbstractMode
    IgnoreAbstractMode }

    -- | Enter concrete or abstract mode depending on whether the given identifier
    --   is concrete or abstract.
    {-# SPECIALIZE inConcreteOrAbstractMode :: QName -> (Definition -> TCM a) -> TCM a #-}
    inConcreteOrAbstractMode :: (MonadTCEnv m, HasConstInfo m) => QName -> (Definition -> m a) -> m a
    inConcreteOrAbstractMode :: forall (m :: * -> *) a.
    (MonadTCEnv m, HasConstInfo m) =>
    QName -> (Definition -> m a) -> m a
    inConcreteOrAbstractMode QName
    q Definition -> m a
    cont = do
      -- Andreas, 2015-07-01: If we do not ignoreAbstractMode here,
      -- we will get ConcreteDef for abstract things, as they are turned into axioms.
      Definition
    def <- m Definition -> m Definition
    forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
    ignoreAbstractMode (m Definition -> m Definition) -> m Definition -> m Definition
    forall a b. (a -> b) -> a -> b
    $ QName -> m Definition
    forall (m :: * -> *). HasConstInfo m => QName -> m Definition
    getConstInfo QName
    q
      case Definition -> IsAbstract
    defAbstract Definition
    def of
        IsAbstract
    AbstractDef -> m a -> m a
    forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
    inAbstractMode (m a -> m a) -> m a -> m a
    forall a b. (a -> b) -> a -> b
    $ Definition -> m a
    cont Definition
    def
        IsAbstract
    ConcreteDef -> m a -> m a
    forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
    inConcreteMode (m a -> m a) -> m a -> m a
    forall a b. (a -> b) -> a -> b
    $ Definition -> m a
    cont Definition
    def

    -- | Check whether a name might have to be treated abstractly (either if we're
    --   'inAbstractMode' or it's not a local name). Returns true for things not
    --   declared abstract as well, but for those 'makeAbstract' will have no effect.
    treatAbstractly :: MonadTCEnv m => QName -> m Bool
    treatAbstractly :: forall (m :: * -> *). MonadTCEnv m => QName -> m Bool
    treatAbstractly QName
    q = (TCEnv -> Bool) -> m Bool
    forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
    asksTC ((TCEnv -> Bool) -> m Bool) -> (TCEnv -> Bool) -> m Bool
    forall a b. (a -> b) -> a -> b
    $ QName -> TCEnv -> Bool
    treatAbstractly' QName
    q

    -- | Andreas, 2015-07-01:
    --   If the @current@ module is a weak suffix of the identifier module,
    --   we can see through its abstract definition if we are abstract.
    --   (Then @treatAbstractly'@ returns @False@).
    --
    --   If I am not mistaken, then we cannot see definitions in the @where@
    --   block of an abstract function from the perspective of the function,
    --   because then the current module is a strict prefix of the module
    --   of the local identifier.
    --   This problem is fixed by removing trailing anonymous module name parts
    --   (underscores) from both names.
    treatAbstractly' :: QName -> TCEnv -> Bool
    treatAbstractly' :: QName -> TCEnv -> Bool
    treatAbstractly' QName
    q TCEnv
    env = case TCEnv -> AbstractMode
    envAbstractMode TCEnv
    env of
      AbstractMode
    ConcreteMode       -> Bool
    True
      AbstractMode
    IgnoreAbstractMode -> Bool
    False
      AbstractMode
    AbstractMode       -> Bool -> Bool
    not (Bool -> Bool) -> Bool -> Bool
    forall a b. (a -> b) -> a -> b
    $ ModuleName
    current ModuleName -> ModuleName -> Bool
    `isLeChildModuleOf` ModuleName
    m
      where
        current :: ModuleName
    current = ModuleName -> ModuleName
    dropAnon (ModuleName -> ModuleName) -> ModuleName -> ModuleName
    forall a b. (a -> b) -> a -> b
    $ TCEnv -> ModuleName
    envCurrentModule TCEnv
    env
        m :: ModuleName
    m       = ModuleName -> ModuleName
    dropAnon (ModuleName -> ModuleName) -> ModuleName -> ModuleName
    forall a b. (a -> b) -> a -> b
    $ QName -> ModuleName
    qnameModule QName
    q
        dropAnon :: ModuleName -> ModuleName
    dropAnon (MName [Name]
    ms) = [Name] -> ModuleName
    MName ([Name] -> ModuleName) -> [Name] -> ModuleName
    forall a b. (a -> b) -> a -> b
    $ (Name -> Bool) -> [Name] -> [Name]
    forall a. (a -> Bool) -> [a] -> [a]
    List.dropWhileEnd Name -> Bool
    forall a. IsNoName a => a -> Bool
    isNoName [Name]
    ms

    -- | Get type of a constant, instantiated to the current context.
    {-# SPECIALIZE typeOfConst :: QName -> TCM Type #-}
    typeOfConst :: (HasConstInfo m, ReadTCState m) => QName -> m Type
    typeOfConst :: forall (m :: * -> *).
    (HasConstInfo m, ReadTCState m) =>
    QName -> m Type
    typeOfConst QName
    q = Definition -> Type
    defType (Definition -> Type) -> m Definition -> m Type
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (Definition -> m Definition
    forall (m :: * -> *).
    (Functor m, HasConstInfo m, HasOptions m, ReadTCState m,
     MonadTCEnv m, MonadDebug m) =>
    Definition -> m Definition
    instantiateDef (Definition -> m Definition) -> m Definition -> m Definition
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< QName -> m Definition
    forall (m :: * -> *). HasConstInfo m => QName -> m Definition
    getConstInfo QName
    q)

    -- | Get relevance of a constant.
    {-# SPECIALIZE relOfConst :: QName -> TCM Relevance #-}
    relOfConst :: HasConstInfo m => QName -> m Relevance
    relOfConst :: forall (m :: * -> *). HasConstInfo m => QName -> m Relevance
    relOfConst QName
    q = Definition -> Relevance
    forall a. LensRelevance a => a -> Relevance
    getRelevance (Definition -> Relevance) -> m Definition -> m Relevance
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> QName -> m Definition
    forall (m :: * -> *). HasConstInfo m => QName -> m Definition
    getConstInfo QName
    q

    -- | Get modality of a constant.
    {-# SPECIALIZE modalityOfConst :: QName -> TCM Modality #-}
    modalityOfConst :: HasConstInfo m => QName -> m Modality
    modalityOfConst :: forall (m :: * -> *). HasConstInfo m => QName -> m Modality
    modalityOfConst QName
    q = Definition -> Modality
    forall a. LensModality a => a -> Modality
    getModality (Definition -> Modality) -> m Definition -> m Modality
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> QName -> m Definition
    forall (m :: * -> *). HasConstInfo m => QName -> m Definition
    getConstInfo QName
    q

    -- | The number of dropped parameters for a definition.
    --   0 except for projection(-like) functions and constructors.
    droppedPars :: Definition -> Int
    droppedPars :: Definition -> Int
    droppedPars Definition
    d = case Definition -> Defn
    theDef Definition
    d of
        Axiom{}                  -> Int
    0
        DataOrRecSig{}           -> Int
    0
        GeneralizableVar{}       -> Int
    0
        def :: Defn
    def@Function{}           -> Definition -> Int
    projectionArgs Definition
    d
        Datatype  {dataPars :: Defn -> Int
    dataPars = Int
    _} -> Int
    0  -- not dropped
        Record     {recPars :: Defn -> Int
    recPars = Int
    _} -> Int
    0  -- not dropped
        Constructor{conPars :: Defn -> Int
    conPars = Int
    n} -> Int
    n
        Primitive{}              -> Int
    0
        PrimitiveSort{}          -> Int
    0
        AbstractDefn{}           -> Int
    forall a. HasCallStack => a
    __IMPOSSIBLE__

    -- | Is it the name of a record projection?
    {-# SPECIALIZE isProjection :: QName -> TCM (Maybe Projection) #-}
    isProjection :: HasConstInfo m => QName -> m (Maybe Projection)
    isProjection :: forall (m :: * -> *).
    HasConstInfo m =>
    QName -> m (Maybe Projection)
    isProjection QName
    qn = Defn -> Maybe Projection
    isProjection_ (Defn -> Maybe Projection)
    -> (Definition -> Defn) -> Definition -> Maybe Projection
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Definition -> Defn
    theDef (Definition -> Maybe Projection)
    -> m Definition -> m (Maybe Projection)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> QName -> m Definition
    forall (m :: * -> *). HasConstInfo m => QName -> m Definition
    getConstInfo QName
    qn

    isProjection_ :: Defn -> Maybe Projection
    isProjection_ :: Defn -> Maybe Projection
    isProjection_ Defn
    def =
      case Defn
    def of
        Function { funProjection :: Defn -> Maybe Projection
    funProjection = Maybe Projection
    result } -> Maybe Projection
    result
        Defn
    _                                   -> Maybe Projection
    forall a. Maybe a
    Nothing

    -- | Is it the name of a non-irrelevant record projection?
    {-# SPECIALIZE isProjection :: QName -> TCM (Maybe Projection) #-}
    isRelevantProjection :: HasConstInfo m => QName -> m (Maybe Projection)
    isRelevantProjection :: forall (m :: * -> *).
    HasConstInfo m =>
    QName -> m (Maybe Projection)
    isRelevantProjection QName
    qn = Definition -> Maybe Projection
    isRelevantProjection_ (Definition -> Maybe Projection)
    -> m Definition -> m (Maybe Projection)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> QName -> m Definition
    forall (m :: * -> *). HasConstInfo m => QName -> m Definition
    getConstInfo QName
    qn

    isRelevantProjection_ :: Definition -> Maybe Projection
    isRelevantProjection_ :: Definition -> Maybe Projection
    isRelevantProjection_ Definition
    def =
      if Definition -> Bool
    forall a. LensRelevance a => a -> Bool
    isIrrelevant Definition
    def then Maybe Projection
    forall a. Maybe a
    Nothing else Defn -> Maybe Projection
    isProjection_ (Defn -> Maybe Projection) -> Defn -> Maybe Projection
    forall a b. (a -> b) -> a -> b
    $ Definition -> Defn
    theDef Definition
    def

    -- | Is it a function marked STATIC?
    isStaticFun :: Defn -> Bool
    isStaticFun :: Defn -> Bool
    isStaticFun = (Defn -> Lens' Bool Defn -> Bool
    forall o i. o -> Lens' i o -> i
    ^. Lens' Bool Defn
    funStatic)

    -- | Is it a function marked INLINE?
    isInlineFun :: Defn -> Bool
    isInlineFun :: Defn -> Bool
    isInlineFun = (Defn -> Lens' Bool Defn -> Bool
    forall o i. o -> Lens' i o -> i
    ^. Lens' Bool Defn
    funInline)

    -- | Returns @True@ if we are dealing with a proper projection,
    --   i.e., not a projection-like function nor a record field value
    --   (projection applied to argument).
    isProperProjection :: Defn -> Bool
    isProperProjection :: Defn -> Bool
    isProperProjection Defn
    d = Maybe Projection -> Bool -> (Projection -> Bool) -> Bool
    forall a b. Maybe a -> b -> (a -> b) -> b
    caseMaybe (Defn -> Maybe Projection
    isProjection_ Defn
    d) Bool
    False ((Projection -> Bool) -> Bool) -> (Projection -> Bool) -> Bool
    forall a b. (a -> b) -> a -> b
    $ \ Projection
    isP ->
      (Projection -> Int
    projIndex Projection
    isP Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    > Int
    0) Bool -> Bool -> Bool
    && Maybe QName -> Bool
    forall a. Maybe a -> Bool
    isJust (Projection -> Maybe QName
    projProper Projection
    isP)

    -- | Number of dropped initial arguments of a projection(-like) function.
    projectionArgs :: Definition -> Int
    projectionArgs :: Definition -> Int
    projectionArgs = Int -> (Projection -> Int) -> Maybe Projection -> Int
    forall b a. b -> (a -> b) -> Maybe a -> b
    maybe Int
    0 (Int -> Int -> Int
    forall a. Ord a => a -> a -> a
    max Int
    0 (Int -> Int) -> (Projection -> Int) -> Projection -> Int
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Int -> Int
    forall a. Enum a => a -> a
    pred (Int -> Int) -> (Projection -> Int) -> Projection -> Int
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Projection -> Int
    projIndex) (Maybe Projection -> Int)
    -> (Definition -> Maybe Projection) -> Definition -> Int
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Definition -> Maybe Projection
    isRelevantProjection_

    -- | Check whether a definition uses copatterns.
    usesCopatterns :: (HasConstInfo m) => QName -> m Bool
    usesCopatterns :: forall (m :: * -> *). HasConstInfo m => QName -> m Bool
    usesCopatterns QName
    q = Definition -> Bool
    defCopatternLHS (Definition -> Bool) -> m Definition -> m Bool
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> QName -> m Definition
    forall (m :: * -> *). HasConstInfo m => QName -> m Definition
    getConstInfo QName
    q

    -- | Apply a function @f@ to its first argument, producing the proper
    --   postfix projection if @f@ is a projection which is not irrelevant.
    applyDef :: (HasConstInfo m)
             => ProjOrigin -> QName -> Arg Term -> m Term
    applyDef :: forall (m :: * -> *).
    HasConstInfo m =>
    ProjOrigin -> QName -> Arg Term -> m Term
    applyDef ProjOrigin
    o QName
    f Arg Term
    a = do
      let fallback :: m Term
    fallback = Term -> m Term
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Term -> m Term) -> Term -> m Term
    forall a b. (a -> b) -> a -> b
    $ QName -> Elims -> Term
    Def QName
    f [Arg Term -> Elim' Term
    forall a. Arg a -> Elim' a
    Apply Arg Term
    a]
      -- Andreas, 2022-03-07, issue #5809: don't drop parameters of irrelevant projections.
      m (Maybe Projection) -> m Term -> (Projection -> m Term) -> m Term
    forall (m :: * -> *) a b.
    Monad m =>
    m (Maybe a) -> m b -> (a -> m b) -> m b
    caseMaybeM (QName -> m (Maybe Projection)
    forall (m :: * -> *).
    HasConstInfo m =>
    QName -> m (Maybe Projection)
    isRelevantProjection QName
    f) m Term
    fallback ((Projection -> m Term) -> m Term)
    -> (Projection -> m Term) -> m Term
    forall a b. (a -> b) -> a -> b
    $ \ Projection
    isP -> do
        if Projection -> Int
    projIndex Projection
    isP Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    <= Int
    0 then m Term
    fallback else do
          -- Get the original projection, if existing.
          if Maybe QName -> Bool
    forall a. Maybe a -> Bool
    isNothing (Projection -> Maybe QName
    projProper Projection
    isP) then m Term
    fallback else do
            Term -> m Term
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Term -> m Term) -> Term -> m Term
    forall a b. (a -> b) -> a -> b
    $ Arg Term -> Term
    forall e. Arg e -> e
    unArg Arg Term
    a Term -> Elims -> Term
    forall t. Apply t => t -> Elims -> t
    `applyE` [ProjOrigin -> QName -> Elim' Term
    forall a. ProjOrigin -> QName -> Elim' a
    Proj ProjOrigin
    o (QName -> Elim' Term) -> QName -> Elim' Term
    forall a b. (a -> b) -> a -> b
    $ Projection -> QName
    projOrig Projection
    isP]