    {-# LANGUAGE NondecreasingIndentation #-}

    module Agda.TypeChecking.Monad.Signature where

    import Prelude hiding (null)

    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.Constraints
    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.InstanceArguments
    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.TypeChecking.Opacity
    import {-# SOURCE #-} Agda.TypeChecking.Telescope

    import Agda.Utils.CallStack.Base
    import Agda.Utils.Either
    import Agda.Utils.Function ( applyWhen )
    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.Syntax.Common.Pretty (Doc, prettyShow)
    import Agda.Utils.Singleton
    import Agda.Utils.Size
    import Agda.Utils.Update

    import Agda.Utils.Impossible

    -- | If the first argument is @'Erased' something@, then hard
    -- compile-time mode is enabled when the continuation is run.

    setHardCompileTimeModeIfErased
      :: Erased
      -> TCM a
         -- ^ Continuation.
      -> TCM a
    setHardCompileTimeModeIfErased :: forall a. Erased -> TCM a -> TCM a
    setHardCompileTimeModeIfErased Erased
    erased =
      (TCEnv -> TCEnv) -> TCMT IO a -> TCMT IO a
    forall a. (TCEnv -> TCEnv) -> TCMT IO a -> TCMT IO a
    forall (m :: * -> *) a.
    MonadTCEnv m =>
    (TCEnv -> TCEnv) -> m a -> m a
    localTC
        ((TCEnv -> TCEnv) -> TCMT IO a -> TCMT IO a)
    -> (TCEnv -> TCEnv) -> TCMT IO a -> TCMT IO a
    forall a b. (a -> b) -> a -> b
    $ Bool -> (TCEnv -> TCEnv) -> TCEnv -> TCEnv
    forall b a. IsBool b => b -> (a -> a) -> a -> a
    applyWhen (Erased -> Bool
    isErased Erased
    erased) (Lens' TCEnv Bool -> LensSet TCEnv Bool
    forall o i. Lens' o i -> LensSet o i
    set (Bool -> f Bool) -> TCEnv -> f TCEnv
    Lens' TCEnv Bool
    eHardCompileTimeMode Bool
    True)
        (TCEnv -> TCEnv) -> (TCEnv -> TCEnv) -> TCEnv -> TCEnv
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Lens' TCEnv Quantity -> LensMap TCEnv Quantity
    forall o i. Lens' o i -> LensMap o i
    over (Quantity -> f Quantity) -> TCEnv -> f TCEnv
    Lens' TCEnv Quantity
    eQuantity (Quantity -> Quantity -> Quantity
    `composeQuantity` Erased -> Quantity
    asQuantity Erased
    erased)

    -- | If the quantity is \"erased\", then hard compile-time mode is
    -- enabled when the continuation is run.
    --
    -- Precondition: The quantity must not be @'Quantity1' something@.

    setHardCompileTimeModeIfErased'
      :: LensQuantity q
      => q
         -- ^ The quantity.
      -> TCM a
         -- ^ Continuation.
      -> TCM a
    setHardCompileTimeModeIfErased' :: forall q a. LensQuantity q => q -> TCM a -> TCM a
    setHardCompileTimeModeIfErased' =
      Erased -> TCM a -> TCM a
    forall a. Erased -> TCM a -> TCM a
    setHardCompileTimeModeIfErased (Erased -> TCM a -> TCM a) -> (q -> Erased) -> q -> TCM a -> TCM a
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    .
        Erased -> Maybe Erased -> Erased
    forall a. a -> Maybe a -> a
    fromMaybe Erased
    forall a. HasCallStack => a
    __IMPOSSIBLE__ (Maybe Erased -> Erased) -> (q -> Maybe Erased) -> q -> Erased
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Quantity -> Maybe Erased
    erasedFromQuantity (Quantity -> Maybe Erased) -> (q -> Quantity) -> q -> Maybe Erased
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . q -> Quantity
    forall a. LensQuantity a => a -> Quantity
    getQuantity

    -- | Use run-time mode in the continuation unless the current mode is
    -- the hard compile-time mode.

    setRunTimeModeUnlessInHardCompileTimeMode
      :: TCM a
         -- ^ Continuation.
      -> TCM a
    setRunTimeModeUnlessInHardCompileTimeMode :: forall a. TCM a -> TCM a
    setRunTimeModeUnlessInHardCompileTimeMode TCM a
    c =
      TCMT IO Bool -> TCM a -> TCM a -> TCM a
    forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
    ifM (Lens' TCEnv Bool -> TCMT IO Bool
    forall (m :: * -> *) a. MonadTCEnv m => Lens' TCEnv a -> m a
    viewTC (Bool -> f Bool) -> TCEnv -> f TCEnv
    Lens' TCEnv Bool
    eHardCompileTimeMode) TCM a
    c (TCM a -> TCM a) -> TCM a -> TCM a
    forall a b. (a -> b) -> a -> b
    $
      (TCEnv -> TCEnv) -> TCM a -> TCM a
    forall a. (TCEnv -> TCEnv) -> TCMT IO a -> TCMT IO a
    forall (m :: * -> *) a.
    MonadTCEnv m =>
    (TCEnv -> TCEnv) -> m a -> m a
    localTC (Lens' TCEnv Quantity -> LensMap TCEnv Quantity
    forall o i. Lens' o i -> LensMap o i
    over (Quantity -> f Quantity) -> TCEnv -> f TCEnv
    Lens' TCEnv Quantity
    eQuantity LensMap TCEnv Quantity -> LensMap TCEnv Quantity
    forall a b. (a -> b) -> a -> b
    $ (Quantity -> Quantity) -> Quantity -> Quantity
    forall a. LensQuantity a => (Quantity -> Quantity) -> a -> a
    mapQuantity (Quantity -> Quantity -> Quantity
    `addQuantity` Quantity
    topQuantity)) TCM a
    c

    -- | Use hard compile-time mode in the continuation if the first
    -- argument is @'Erased' something@. Use run-time mode if the first
    -- argument is @'NotErased' something@ and the current mode is not
    -- hard compile-time mode.

    setModeUnlessInHardCompileTimeMode
      :: Erased
      -> TCM a
         -- ^ Continuation.
      -> TCM a
    setModeUnlessInHardCompileTimeMode :: forall a. Erased -> TCM a -> TCM a
    setModeUnlessInHardCompileTimeMode Erased
    erased TCM a
    c = case Erased
    erased of
      Erased{}    -> Erased -> TCM a -> TCM a
    forall a. Erased -> TCM a -> TCM a
    setHardCompileTimeModeIfErased Erased
    erased TCM a
    c
      NotErased{} -> do
        Erased -> TCM ()
    warnForPlentyInHardCompileTimeMode Erased
    erased
        TCM a -> TCM a
    forall a. TCM a -> TCM a
    setRunTimeModeUnlessInHardCompileTimeMode TCM a
    c

    -- | Warn if the user explicitly wrote @@ω@ or @@plenty@ but the
    -- current mode is the hard compile-time mode.

    warnForPlentyInHardCompileTimeMode :: Erased -> TCM ()
    warnForPlentyInHardCompileTimeMode :: Erased -> TCM ()
    warnForPlentyInHardCompileTimeMode = \case
      Erased{}    -> () -> TCM ()
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
      NotErased QωOrigin
    o -> do
        let warn :: TCM ()
    warn = Warning -> TCM ()
    forall (m :: * -> *).
    (HasCallStack, MonadWarning m) =>
    Warning -> m ()
    warning (Warning -> TCM ()) -> Warning -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ QωOrigin -> Warning
    PlentyInHardCompileTimeMode QωOrigin
    o
        hard <- Lens' TCEnv Bool -> TCMT IO Bool
    forall (m :: * -> *) a. MonadTCEnv m => Lens' TCEnv a -> m a
    viewTC (Bool -> f Bool) -> TCEnv -> f TCEnv
    Lens' TCEnv Bool
    eHardCompileTimeMode
        if not hard then return () else case o of
          QωInferred{} -> () -> TCM ()
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
          Qω{}         -> TCM ()
    warn
          QωPlenty{}   -> TCM ()
    warn

    -- | 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
      ArgName -> Int -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    ArgName -> Int -> TCMT IO Doc -> m ()
    reportSDoc ArgName
    "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"

      -- Every constant that gets added to the signature in hard
      -- compile-time mode is treated as erased.
      hard <- Lens' TCEnv Bool -> TCMT IO Bool
    forall (m :: * -> *) a. MonadTCEnv m => Lens' TCEnv a -> m a
    viewTC (Bool -> f Bool) -> TCEnv -> f TCEnv
    Lens' TCEnv Bool
    eHardCompileTimeMode
      d    <- if not hard then return d else do
        case erasedFromQuantity (getQuantity d) of
          Maybe Erased
    Nothing     -> TCMT IO Definition
    forall a. HasCallStack => a
    __IMPOSSIBLE__
          Just Erased
    erased -> do
            Erased -> TCM ()
    warnForPlentyInHardCompileTimeMode Erased
    erased
            Definition -> TCMT IO Definition
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Definition -> TCMT IO Definition)
    -> Definition -> TCMT IO Definition
    forall a b. (a -> b) -> a -> b
    $ (Quantity -> Quantity) -> Definition -> Definition
    forall a. LensQuantity a => (Quantity -> Quantity) -> a -> a
    mapQuantity (Quantity
    zeroQuantity Quantity -> Quantity -> Quantity
    `composeQuantity`) Definition
    d

      tel <- getContextTelescope
      let tel' = ArgName -> Telescope -> Telescope
    forall a. ArgName -> Tele a -> Tele a
    replaceEmptyName ArgName
    "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 a b. (a -> b) -> Tele a -> Tele b
    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 -> Either ProjectionLikenessMissing Projection
    funProjection = Right Projection{ projProper :: Projection -> Maybe QName
    projProper = Just{}, projIndex :: Projection -> Int
    projIndex = Int
    n } } ->
                    let fallback :: Telescope
    fallback = (Dom Type -> Dom Type) -> Telescope -> Telescope
    forall a b. (a -> b) -> Tele a -> Tele b
    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 (ArgName, Type)]
    -> Maybe ([Dom (ArgName, Type)], Dom (ArgName, Type))
    forall a. [a] -> Maybe ([a], a)
    initLast ([Dom (ArgName, Type)]
     -> Maybe ([Dom (ArgName, Type)], Dom (ArgName, Type)))
    -> [Dom (ArgName, Type)]
    -> Maybe ([Dom (ArgName, Type)], Dom (ArgName, Type))
    forall a b. (a -> b) -> a -> b
    $ Telescope -> [Dom (ArgName, Type)]
    forall t. Tele (Dom t) -> [Dom (ArgName, t)]
    telToList Telescope
    tel of
                        Maybe ([Dom (ArgName, Type)], Dom (ArgName, Type))
    Nothing -> Telescope
    fallback
                        Just ([Dom (ArgName, Type)]
    doms, Dom (ArgName, Type)
    dom) -> [Dom (ArgName, Type)] -> Telescope
    telFromList ([Dom (ArgName, Type)] -> Telescope)
    -> [Dom (ArgName, Type)] -> Telescope
    forall a b. (a -> b) -> a -> b
    $ (Dom (ArgName, Type) -> Dom (ArgName, Type))
    -> [Dom (ArgName, Type)] -> [Dom (ArgName, Type)]
    forall a b. (a -> b) -> [a] -> [b]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap Dom (ArgName, Type) -> Dom (ArgName, Type)
    forall a. LensHiding a => a -> a
    hideOrKeepInstance [Dom (ArgName, Type)]
    doms [Dom (ArgName, Type)]
    -> [Dom (ArgName, Type)] -> [Dom (ArgName, Type)]
    forall a. [a] -> [a] -> [a]
    ++ [Dom (ArgName, Type)
    dom]
                  Defn
    _ -> Telescope
    tel
      let 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 = q }
      reportSDoc "tc.signature" 60 $ "lambda-lifted definition =" <?> pretty d'
      modifySignature $ updateDefinitions $ HMap.insertWith (+++) q d'
      i <- currentOrFreshMutualBlock
      setMutualBlock i q
      where
        Definition
    new +++ :: Definition -> Definition -> Definition
    +++ Definition
    old = Definition
    new { defDisplay        = defDisplay new ++ defDisplay old
                          , defInstance       = defInstance new `mplus` defInstance old
                          , defArgOccurrences = if null (defArgOccurrences new)
                                                  then defArgOccurrences old
                                                  else defArgOccurrences new
                          , defPolarity       = if null (defPolarity new)
                                                  then defPolarity old
                                                  else defPolarity new
                          }

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

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

    -- | Set termination info of a defined function symbol.
    setTerminates :: MonadTCState m => QName -> Bool -> m ()
    setTerminates :: forall (m :: * -> *). MonadTCState m => QName -> Bool -> m ()
    setTerminates QName
    q Bool
    b = (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
    $ (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 = Just b }
        def :: Defn
    def@Record{}   -> Defn
    def { recTerminates = Just 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 = Just 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 = Just 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 :: (MonadConstraint m, MonadTCState m) => QName -> [Clause] -> m ()
    addClauses :: forall (m :: * -> *).
    (MonadConstraint m, MonadTCState m) =>
    QName -> [Clause] -> m ()
    addClauses QName
    q [Clause]
    cls = do
      tel <- m Telescope
    forall (m :: * -> *). MonadTCEnv m => m Telescope
    getContextTelescope
      modifySignature $ updateDefinition q $
        updateTheDef (updateFunClauses (++ abstract tel cls))
        . updateDefCopatternLHS (|| isCopatternLHS cls)

      -- Jesper, 2022-10-13: unblock any constraints that were
      -- waiting for more clauses of this function
      wakeConstraints' $ wakeIfBlockedOnDef q . constraintUnblocker

    mkPragma :: String -> TCM CompilerPragma
    mkPragma :: ArgName -> TCM CompilerPragma
    mkPragma ArgName
    s = Range -> ArgName -> CompilerPragma
    CompilerPragma (Range -> ArgName -> CompilerPragma)
    -> TCMT IO Range -> TCMT IO (ArgName -> 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 (ArgName -> CompilerPragma)
    -> TCMT IO ArgName -> TCM CompilerPragma
    forall a b. TCMT IO (a -> b) -> TCMT IO a -> TCMT IO b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> ArgName -> TCMT IO ArgName
    forall a. a -> TCMT IO a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure ArgName
    s

    -- | Add a compiler pragma `{-\# COMPILE <backend> <name> <text> \#-}`
    addPragma :: BackendName -> QName -> String -> TCM ()
    addPragma :: BackendName -> QName -> ArgName -> TCM ()
    addPragma BackendName
    b QName
    q ArgName
    s = do
        pragma <- ArgName -> TCM CompilerPragma
    mkPragma ArgName
    s
        modifySignature $ updateDefinition q $ addCompilerPragma b pragma

    getUniqueCompilerPragma :: BackendName -> QName -> TCM (Maybe CompilerPragma)
    getUniqueCompilerPragma :: BackendName -> QName -> TCM (Maybe CompilerPragma)
    getUniqueCompilerPragma BackendName
    backend QName
    q = do
      ps <- BackendName -> Definition -> [CompilerPragma]
    defCompilerPragmas BackendName
    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 ps of
        []  -> Maybe CompilerPragma -> TCM (Maybe CompilerPragma)
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Maybe CompilerPragma
    forall a. Maybe a
    Nothing
        [CompilerPragma
    p] -> Maybe CompilerPragma -> TCM (Maybe CompilerPragma)
    forall a. a -> TCMT IO a
    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 do
          TypeError -> TCM (Maybe CompilerPragma)
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    TypeError -> m a
    typeError (TypeError -> TCM (Maybe CompilerPragma))
    -> (Doc -> TypeError) -> Doc -> TCM (Maybe CompilerPragma)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . BackendName -> Doc -> TypeError
    CustomBackendError BackendName
    backend (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 ([TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    hsep [ TCMT IO Doc
    "Conflicting", BackendName -> TCMT IO Doc
    forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
    pretty BackendName
    backend, TCMT IO Doc
    "pragmas for", QName -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => QName -> m Doc
    prettyTCM QName
    q, 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' Definition Bool -> LensSet Definition Bool
    forall o i. Lens' o i -> LensSet o i
    set ((Defn -> f Defn) -> Definition -> f Definition
    Lens' Definition Defn
    lensTheDef ((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' Defn Bool
    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 = True }

    markFirstOrder :: QName -> TCM ()
    markFirstOrder :: QName -> TCM ()
    markFirstOrder = FunctionFlag -> Bool -> QName -> TCM ()
    setFunctionFlag FunctionFlag
    FunFirstOrder Bool
    True

    unionSignatures :: [Signature] -> Signature
    unionSignatures :: [Signature] -> Signature
    unionSignatures [Signature]
    ss = (Signature -> Signature -> Signature)
    -> Signature -> [Signature] -> Signature
    forall a b. (a -> b -> b) -> b -> [a] -> b
    forall (t :: * -> *) a b.
    Foldable t =>
    (a -> b -> b) -> b -> t a -> b
    foldr Signature -> Signature -> Signature
    unionSignature Signature
    emptySignature [Signature]
    ss

    unionSignature :: Signature -> Signature -> Signature
    unionSignature :: Signature -> Signature -> Signature
    unionSignature (Sig Sections
    a Definitions
    b RewriteRuleMap
    c InstanceTable
    d) (Sig Sections
    a' Definitions
    b' RewriteRuleMap
    c' InstanceTable
    d') =
          Sections
    -> Definitions -> RewriteRuleMap -> InstanceTable -> 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 => 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 =>
    (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
              (InstanceTable
    d InstanceTable -> InstanceTable -> InstanceTable
    forall a. Semigroup a => a -> a -> a
    <> InstanceTable
    d')                     -- instances 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
      tel <- TCMT IO Telescope
    forall (m :: * -> *). MonadTCEnv m => m Telescope
    getContextTelescope
      let sec = Telescope -> Section
    Section Telescope
    tel
      -- Make sure we do not overwrite an existing section!
      whenJustM (getSection m) $ \ 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".
          ArgName -> Int -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    ArgName -> Int -> TCMT IO Doc -> m ()
    reportSDoc ArgName
    "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
          ArgName -> Int -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    ArgName -> Int -> TCMT IO Doc -> m ()
    reportSDoc ArgName
    "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
          ArgName -> Int -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    ArgName -> Int -> TCMT IO Doc -> m ()
    reportSDoc ArgName
    "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
          ArgName -> Int -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    ArgName -> Int -> TCMT IO Doc -> m ()
    reportSDoc ArgName
    "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'
          ArgName -> Int -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    ArgName -> Int -> TCMT IO Doc -> m ()
    reportSDoc ArgName
    "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.
      setModuleCheckpoint m
      modifySignature $ over sigSections $ Map.insert m sec

    -- | Sets the checkpoint for the given module to the current checkpoint.
    setModuleCheckpoint :: ModuleName -> TCM ()
    setModuleCheckpoint :: ModuleName -> TCM ()
    setModuleCheckpoint ModuleName
    m = do
      chkpt <- Lens' TCEnv CheckpointId -> TCMT IO CheckpointId
    forall (m :: * -> *) a. MonadTCEnv m => Lens' TCEnv a -> m a
    viewTC (CheckpointId -> f CheckpointId) -> TCEnv -> f TCEnv
    Lens' TCEnv CheckpointId
    eCurrentCheckpoint
      stModuleCheckpoints `modifyTCLens` Map.insert m 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
      sig  <- (TCState -> Lens' TCState Sections -> Sections
    forall o i. o -> Lens' o i -> i
    ^. (Signature -> f Signature) -> TCState -> f TCState
    Lens' TCState Signature
    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' Signature Sections
    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
      isig <- (^. stImports   . sigSections) <$> getTCState
      return $ Map.lookup m sig `mplus` Map.lookup m 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' Section Telescope -> Telescope
    forall o i. o -> Lens' o i -> i
    ^. (Telescope -> f Telescope) -> Section -> f Section
    Lens' Section Telescope
    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
      ArgName -> Int -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    ArgName -> Int -> TCMT IO Doc -> m ()
    reportSDoc ArgName
    "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
      def <- QName -> TCMT IO Definition
    forall (m :: * -> *). HasConstInfo m => QName -> m Definition
    getConstInfo QName
    x
      let v = case Definition -> Defn
    theDef Definition
    def of
                 Constructor{conSrcCon :: Defn -> ConHead
    conSrcCon = ConHead
    h} -> ConHead -> ConInfo -> Elims -> Term
    Con ConHead
    h{ conName = x } ConInfo
    ConOSystem []
                 Defn
    _                          -> QName -> Elims -> Term
    Def QName
    x []

      -- Compute all unfoldings of x by repeatedly calling reduceDefCopy
      vs <- unfoldings x v
      reportSDoc "tc.display.section" 20 $ nest 2 $ vcat
        [ "unfoldings:" <?> vcat [ "-" <+> pretty v | v <- vs ] ]

      -- Turn unfoldings into display forms
      npars <- subtract (projectionArgs def) <$> getContextSize
      let dfs = (Term -> (QName, DisplayForm)) -> [Term] -> [(QName, DisplayForm)]
    forall a b. (a -> b) -> [a] -> [b]
    map (Int -> Term -> Term -> (QName, DisplayForm)
    displayForm Int
    npars Term
    v) [Term]
    vs
      reportSDoc "tc.display.section" 20 $ nest 2 $ vcat
        [ "displayForms:" <?> vcat [ "-" <+> (pretty y <+> "-->" <?> pretty df) | (y, df) <- dfs ] ]

      -- and add them
      mapM_ (uncurry addDisplayForm) dfs
      where

        -- To get display forms for projections we need to unSpine here.
        view :: Term -> ([Arg ArgName], Term)
        view :: Term -> ([Arg ArgName], Term)
    view = (Term -> Term) -> ([Arg ArgName], Term) -> ([Arg ArgName], Term)
    forall b c d. (b -> c) -> (d, b) -> (d, c)
    forall (a :: * -> * -> *) b c d.
    Arrow a =>
    a b c -> a (d, b) (d, c)
    second Term -> Term
    unSpine (([Arg ArgName], Term) -> ([Arg ArgName], Term))
    -> (Term -> ([Arg ArgName], Term)) -> Term -> ([Arg ArgName], Term)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Term -> ([Arg ArgName], 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 -> (QName, DisplayForm)
        displayForm :: Int -> Term -> Term -> (QName, DisplayForm)
    displayForm Int
    npars Term
    top Term
    v =
          case Term -> ([Arg ArgName], Term)
    view Term
    v of
            ([Arg ArgName]
    xs, Def QName
    y Elims
    es)   -> (QName
    y,)         (DisplayForm -> (QName, DisplayForm))
    -> DisplayForm -> (QName, DisplayForm)
    forall a b. (a -> b) -> a -> b
    $ [Arg ArgName] -> Elims -> DisplayForm
    mkDisplay [Arg ArgName]
    xs Elims
    es
            ([Arg ArgName]
    xs, Con ConHead
    h ConInfo
    i Elims
    es) -> (ConHead -> QName
    conName ConHead
    h,) (DisplayForm -> (QName, DisplayForm))
    -> DisplayForm -> (QName, DisplayForm)
    forall a b. (a -> b) -> a -> b
    $ [Arg ArgName] -> Elims -> DisplayForm
    mkDisplay [Arg ArgName]
    xs Elims
    es
            ([Arg ArgName], Term)
    _ -> (QName, DisplayForm)
    forall a. HasCallStack => a
    __IMPOSSIBLE__
          where
            mkDisplay :: [Arg ArgName] -> Elims -> DisplayForm
    mkDisplay [Arg ArgName]
    xs Elims
    es = 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
              -- Andreas, 2023-01-26, #6476:
              -- I think this @apply@ is safe (rather than @DTerm' top (map Apply args)@).
              where
                n :: Int
    n    = [Arg ArgName] -> Int
    forall a. [a] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length [Arg ArgName]
    xs
                args :: [Arg Term]
    args = (Arg ArgName -> Int -> Arg Term)
    -> [Arg ArgName] -> [Int] -> [Arg Term]
    forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
    zipWith (\ Arg ArgName
    x Int
    i -> Int -> Term
    var Int
    i Term -> Arg ArgName -> Arg Term
    forall a b. a -> Arg b -> Arg a
    forall (f :: * -> *) a b. Functor f => a -> f b -> f a
    <$ Arg ArgName
    x) [Arg ArgName]
    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 ArgName], Term)
    view Term
    v of
          ([Arg ArgName]
    xs, Def QName
    f Elims
    es)   -> ((Reduced () Term -> Reduced () Term)
    -> TCM (Reduced () Term) -> TCM (Reduced () Term)
    forall a b. (a -> b) -> TCMT IO a -> TCMT IO b
    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 a b. (a -> b) -> Reduced () a -> Reduced () b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap) ([Arg ArgName] -> Term -> Term
    unlamView [Arg ArgName]
    xs) (QName -> Elims -> TCM (Reduced () Term)
    reduceDefCopyTCM QName
    f Elims
    es)
          ([Arg ArgName]
    xs, Con ConHead
    c ConInfo
    i Elims
    es) -> ((Reduced () Term -> Reduced () Term)
    -> TCM (Reduced () Term) -> TCM (Reduced () Term)
    forall a b. (a -> b) -> TCMT IO a -> TCMT IO b
    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 a b. (a -> b) -> Reduced () a -> Reduced () b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap) ([Arg ArgName] -> Term -> Term
    unlamView [Arg ArgName]
    xs) (QName -> Elims -> TCM (Reduced () Term)
    reduceDefCopyTCM (ConHead -> QName
    conName ConHead
    c) Elims
    es)
          ([Arg ArgName], Term)
    _                -> Reduced () Term -> TCM (Reduced () Term)
    forall a. a -> TCMT IO a
    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 a b. TCMT IO a -> (a -> TCMT IO b) -> TCMT IO b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \ case
          NoReduction{}     -> [Term] -> TCM [Term]
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return []
          YesReduction Simplification
    _ Term
    v' -> do
            let headSymbol :: Maybe QName
    headSymbol = case ([Arg ArgName], Term) -> Term
    forall a b. (a, b) -> b
    snd (([Arg ArgName], Term) -> Term) -> ([Arg ArgName], Term) -> Term
    forall a b. (a -> b) -> a -> b
    $ Term -> ([Arg ArgName], 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 a. a -> TCMT IO a
    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.
                ArgName -> Int -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    ArgName -> Int -> TCMT IO Doc -> m ()
    reportSDoc ArgName
    "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 a. a -> TCMT IO a
    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
      rd <- Ren QName -> TCM (Ren QName)
    closeConstructors Ren QName
    rd
      applySection' new ptel old ts ScopeCopyInfo{ renModules = rm, renNames = 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
            ds <- ((ModuleName, QName) -> QName)
    -> [(ModuleName, QName)] -> [(ModuleName, QName)]
    forall b a. Ord b => (a -> b) -> [a] -> [a]
    nubOn (ModuleName, QName) -> QName
    forall a b. (a, b) -> b
    snd ([(ModuleName, QName)] -> [(ModuleName, QName)])
    -> ([Maybe (ModuleName, QName)] -> [(ModuleName, QName)])
    -> [Maybe (ModuleName, QName)]
    -> [(ModuleName, QName)]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [Maybe (ModuleName, QName)] -> [(ModuleName, QName)]
    forall a. [Maybe a] -> [a]
    catMaybes ([Maybe (ModuleName, QName)] -> [(ModuleName, QName)])
    -> TCMT IO [Maybe (ModuleName, QName)]
    -> TCMT IO [(ModuleName, QName)]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> ((QName, List1 QName) -> TCMT IO (Maybe (ModuleName, QName)))
    -> [(QName, List1 QName)] -> TCMT IO [Maybe (ModuleName, QName)]
    forall (t :: * -> *) (f :: * -> *) a b.
    (Traversable t, Applicative f) =>
    (a -> f b) -> t a -> f (t b)
    forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> [a] -> f [b]
    traverse (QName, List1 QName) -> TCMT IO (Maybe (ModuleName, QName))
    constructorData (Ren QName -> [(QName, List1 QName)]
    forall k a. Map k a -> [(k, a)]
    Map.toList Ren QName
    rd)
            cs <- nubOn snd . concat    <$> traverse dataConstructors (Map.toList rd)
            new <- Map.unionsWith (<>) <$> traverse rename (ds ++ cs)
            reportSDoc "tc.mod.apply.complete" 30 $
              "also copying: " <+> pretty new
            return $ Map.unionWith (<>) new rd
          where
            rename :: (ModuleName, QName) -> TCM (Ren QName)
            rename :: (ModuleName, QName) -> TCM (Ren QName)
    rename (ModuleName
    m, 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 a. a -> TCMT IO a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Ren QName
    forall a. Monoid a => a
    mempty
              | Bool
    otherwise =
                  -- Ulf, 2024-06-24 (#7329):
                  --   Here we used to generate an unqualified name, but this breaks things if the new
                  --   module shows up in a module application later on. This is because we use the
                  --   module name to figure out which arguments from the application are relevant for
                  --   the current symbol (see argsToUse in applySection' below).
                  --
                  --   Instead we use the target module name of the thing that required x to be copied.
                  --   For instance, if we are copying a data type A.B.D to X.Y.Z.D and its constructor
                  --   mkD is not in the renaming, we add `A.B.mkD -> X.Y.Z.mkD` (instead of `A.B.mkD ->
                  --   mkD` which we did before).
                  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 a. a -> NonEmpty a
    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
    . ModuleName -> Name -> QName
    qualify ModuleName
    m (Name -> Ren QName) -> TCMT IO Name -> TCM (Ren QName)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> ArgName -> TCMT IO Name
    forall a (m :: * -> *).
    (FreshName a, MonadFresh NameId m) =>
    a -> m Name
    forall (m :: * -> *). MonadFresh NameId m => ArgName -> m Name
    freshName_ (Name -> ArgName
    forall a. Pretty a => a -> ArgName
    prettyShow (Name -> ArgName) -> Name -> ArgName
    forall a b. (a -> b) -> a -> b
    $ QName -> Name
    qnameName QName
    x)

            constructorData :: (QName, List1.List1 QName) -> TCM (Maybe (ModuleName, QName))
            constructorData :: (QName, List1 QName) -> TCMT IO (Maybe (ModuleName, QName))
    constructorData (QName
    x, QName
    y List1.:| [QName]
    _) = do  -- All new names share the same module, so we can safely grab the first one
              (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 (ModuleName, QName))
    -> TCMT IO (Maybe (ModuleName, QName))
    forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
    <&> \case
                Constructor{ conData :: Defn -> QName
    conData = QName
    d } -> (ModuleName, QName) -> Maybe (ModuleName, QName)
    forall a. a -> Maybe a
    Just (QName -> ModuleName
    qnameModule QName
    y, QName
    d)
                Defn
    _                          -> Maybe (ModuleName, QName)
    forall a. Maybe a
    Nothing

            dataConstructors :: (QName, List1.List1 QName) -> TCM [(ModuleName, QName)]
            dataConstructors :: (QName, List1 QName) -> TCMT IO [(ModuleName, QName)]
    dataConstructors (QName
    x, QName
    y List1.:| [QName]
    _) = 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 -> [(ModuleName, QName)]) -> TCMT IO [(ModuleName, QName)]
    forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
    <&> \case
                Datatype{ dataCons :: Defn -> [QName]
    dataCons = [QName]
    cs } -> (QName -> (ModuleName, QName)) -> [QName] -> [(ModuleName, QName)]
    forall a b. (a -> b) -> [a] -> [b]
    map (QName -> ModuleName
    qnameModule QName
    y,) [QName]
    cs
                Record{ recConHead :: Defn -> ConHead
    recConHead = ConHead
    h }  -> [(QName -> ModuleName
    qnameModule QName
    y, 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
        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
    <$> (PrimitiveId -> TCMT IO (Maybe QName))
    -> [PrimitiveId] -> TCMT IO [Maybe QName]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
    mapM PrimitiveId -> TCMT IO (Maybe QName)
    forall (m :: * -> *) a.
    (HasBuiltins m, IsBuiltin a) =>
    a -> m (Maybe QName)
    getName' [PrimitiveId]
    constrainedPrims
        for_ (Map.keys rd) $ \ QName
    q ->
          Bool -> TCM () -> TCM ()
    forall b (m :: * -> *). (IsBool b, Monad m) => b -> m () -> m ()
    when (QName
    q QName -> [QName] -> Bool
    forall a. Eq a => a -> [a] -> 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)

      ArgName -> Int -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    ArgName -> Int -> TCMT IO Doc -> m ()
    reportSDoc ArgName
    "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
        ]
      _ <- (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)
    forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> NonEmpty a -> f (NonEmpty 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.traverseWithKey (traverse . copySec ts) rm
      computePolarity (Map.elems rd >>= 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)

        copyConHead :: ConHead -> ConHead
    copyConHead ConHead
    c = ConHead
    c { conName = copyName (conName c) }

        argsToUse :: ModuleName -> TCMT IO Int
    argsToUse ModuleName
    x = do
          let m :: ModuleName
    m = ModuleName -> ModuleName -> ModuleName
    commonParentModule ModuleName
    old ModuleName
    x
          ArgName -> Int -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    ArgName -> Int -> TCMT IO Doc -> m ()
    reportSDoc ArgName
    "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
          def <- QName -> TCMT IO Definition
    forall (m :: * -> *). HasConstInfo m => QName -> m Definition
    getConstInfo QName
    x
          np  <- argsToUse (qnameModule 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.
          hidings <- map getHiding . telToList <$> lookupSection (qnameModule x)
          let 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
          commonTel <- lookupSection (commonParentModule old $ qnameModule x)
          reportSDoc "tc.mod.apply" 80 $ vcat
            [ "copyDef" <+> pretty x <+> "->" <+> pretty y
            , "ts' = " <+> pretty ts' ]
          -- The module telescope had been divided by some μ, so the corresponding
          -- top level definition had type μ \ Γ → B, so if we have a substitution
          -- Δ → Γ we actually want to apply μ \ - to it, so the new top-level
          -- definition we get will have signature μ \ Δ → B.  This is only valid
          -- for pure modality systems though.
          let ai = Definition -> ArgInfo
    defArgInfo Definition
    def
              m = Modality
    unitModality { modCohesion = getCohesion ai
                               , modPolarity = getModalPolarity ai
                               }
          localTC (over eContext (map (mapModality (m `inverseComposeModality`)))) $
            copyDef' ts' np def
          where
            copyDef' :: [Arg Term] -> Int -> Definition -> TCM ()
    copyDef' [Arg Term]
    ts Int
    np Definition
    d = do
              ArgName -> Int -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    ArgName -> Int -> TCMT IO Doc -> m ()
    reportSDoc ArgName
    "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
    <+> ArgName -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => ArgName -> m Doc
    text (Int -> ArgName
    forall a. Show a => a -> ArgName
    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
    <+> ArgName -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => ArgName -> m Doc
    text (IsAbstract -> ArgName
    forall a. Show a => a -> ArgName
    show (IsAbstract -> ArgName) -> IsAbstract -> ArgName
    forall a b. (a -> b) -> a -> b
    $ Definition -> IsAbstract
    defAbstract Definition
    d)
              ArgName -> Int -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    ArgName -> Int -> TCMT IO Doc -> m ()
    reportSDoc ArgName
    "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
    <+> ArgName -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => ArgName -> m Doc
    text ([Arg Term] -> ArgName
    forall a. Show a => a -> ArgName
    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) ]
              ArgName -> Int -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    ArgName -> Int -> TCMT IO Doc -> m ()
    reportSDoc ArgName
    "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 InstanceInfo -> (InstanceInfo -> TCM ()) -> TCM ()
    forall (m :: * -> *) a. Monad m => Maybe a -> (a -> m ()) -> m ()
    whenJust Maybe InstanceInfo
    inst ((InstanceInfo -> TCM ()) -> TCM ())
    -> (InstanceInfo -> TCM ()) -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ \InstanceInfo
    _ -> Bool -> Bool -> Maybe InstanceInfo -> QName -> Type -> TCM ()
    addTypedInstance' Bool
    False Bool
    False Maybe InstanceInfo
    inst QName
    y Type
    t
              -- 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 || not (null ptel)) $ do
    -}
              -- BREAKS fail/Issue1643a
              -- -- Andreas, 2015-09-09 Issue 1643:
              -- -- Do not add a display form for a bare module alias.
              -- when (not isCon && null ptel && not (null ts)) $ do
              Bool -> TCM () -> TCM ()
    forall b (m :: * -> *). (IsBool b, Monad m) => b -> m () -> m ()
    when (Telescope -> Bool
    forall a. Null a => a -> Bool
    null Telescope
    ptel) (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'
                inst :: Maybe InstanceInfo
    inst = Definition -> Maybe InstanceInfo
    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.
                  lang <- TCMT IO Language
    forall (m :: * -> *). HasOptions m => m Language
    getLanguage
                  for def $ \ Defn
    df -> 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
                        , 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 InstanceInfo
    defInstance       = Maybe InstanceInfo
    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 :: Either ProjectionLikenessMissing Projection
                proj :: Either ProjectionLikenessMissing Projection
    proj   = case Defn
    oldDef of
                  Function{funProjection :: Defn -> Either ProjectionLikenessMissing Projection
    funProjection = Right 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 -> Either ProjectionLikenessMissing Projection
    forall a b. b -> Either a b
    Right Projection
    p { projIndex = n - size ts'
                               , projLams  = projLams p `apply` ts'
                               , projProper= copyName <$> projProper p
                               }
                  -- Preserve no-projection-likeness flag if it exists, and
                  -- it's set to @Left _@. For future reference: The match
                  -- on left can't be simplified or it accidentally
                  -- circumvents the guard above.
                  Function{funProjection :: Defn -> Either ProjectionLikenessMissing Projection
    funProjection = Left ProjectionLikenessMissing
    projl} -> ProjectionLikenessMissing
    -> Either ProjectionLikenessMissing Projection
    forall a b. a -> Either a b
    Left ProjectionLikenessMissing
    projl
                  Defn
    _ -> ProjectionLikenessMissing
    -> Either ProjectionLikenessMissing Projection
    forall a b. a -> Either a b
    Left ProjectionLikenessMissing
    MaybeProjection
                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 a. a -> TCMT IO a
    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 = np - size ts'
                             , conData = copyName d
                             }
                    Datatype{ dataPars :: Defn -> Int
    dataPars = Int
    np, dataCons :: Defn -> [QName]
    dataCons = [QName]
    cs } -> Defn -> TCMT IO Defn
    forall a. a -> TCMT IO a
    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   = np - size ts'
                             , dataClause = Just cl
                             , dataCons   = map copyName cs
                             }
                    Record{ recPars :: Defn -> Int
    recPars = Int
    np, recTel :: Defn -> Telescope
    recTel = Telescope
    tel, recConHead :: Defn -> ConHead
    recConHead = ConHead
    c, recFields :: Defn -> [Dom QName]
    recFields = [Dom QName]
    fs } -> Defn -> TCMT IO Defn
    forall a. a -> TCMT IO a
    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    = np - size ts'
                             , recClause  = Just cl
                             , recTel     = apply tel ts'
                             , recConHead = copyConHead c
                             , recFields  = (map . fmap) copyName fs
                             }
                    GeneralizableVar NumGeneralizableArgs
    gv -> Defn -> TCMT IO Defn
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Defn -> TCMT IO Defn) -> Defn -> TCMT IO Defn
    forall a b. (a -> b) -> a -> b
    $ NumGeneralizableArgs -> Defn
    GeneralizableVar (NumGeneralizableArgs -> Defn) -> NumGeneralizableArgs -> Defn
    forall a b. (a -> b) -> a -> b
    $ NumGeneralizableArgs
    gv NumGeneralizableArgs -> [Arg Term] -> NumGeneralizableArgs
    forall t. Apply t => t -> [Arg Term] -> t
    `apply` [Arg Term]
    ts'
                    Defn
    _ -> do
                      (mst, _, 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
                      fun          <- emptyFunctionData
                      let newDef =
                            Lens' Defn Bool -> LensSet Defn Bool
    forall o i. Lens' o i -> LensSet o i
    set (Bool -> f Bool) -> Defn -> f Defn
    Lens' Defn Bool
    funProj   (Defn
    oldDef Defn -> Lens' Defn Bool -> Bool
    forall o i. o -> Lens' o i -> i
    ^. (Bool -> f Bool) -> Defn -> f Defn
    Lens' Defn Bool
    funProj) (Defn -> Defn) -> Defn -> Defn
    forall a b. (a -> b) -> a -> b
    $
                            Lens' Defn Bool -> LensSet Defn Bool
    forall o i. Lens' o i -> LensSet o i
    set (Bool -> f Bool) -> Defn -> f Defn
    Lens' Defn Bool
    funMacro  (Defn
    oldDef Defn -> Lens' Defn Bool -> Bool
    forall o i. o -> Lens' o i -> i
    ^. (Bool -> f Bool) -> Defn -> f Defn
    Lens' Defn Bool
    funMacro) (Defn -> Defn) -> Defn -> Defn
    forall a b. (a -> b) -> a -> b
    $
                            Lens' Defn Bool -> LensSet Defn Bool
    forall o i. Lens' o i -> LensSet o i
    set (Bool -> f Bool) -> Defn -> f Defn
    Lens' Defn Bool
    funStatic (Defn
    oldDef Defn -> Lens' Defn Bool -> Bool
    forall o i. o -> Lens' o i -> i
    ^. (Bool -> f Bool) -> Defn -> f Defn
    Lens' Defn Bool
    funStatic) (Defn -> Defn) -> Defn -> Defn
    forall a b. (a -> b) -> a -> b
    $
                            Lens' Defn Bool -> LensSet Defn Bool
    forall o i. Lens' o i -> LensSet o i
    set (Bool -> f Bool) -> Defn -> f Defn
    Lens' Defn Bool
    funInline Bool
    True (Defn -> Defn) -> Defn -> Defn
    forall a b. (a -> b) -> a -> b
    $
                            FunctionData -> Defn
    FunctionDefn FunctionData
    fun
                            { _funClauses        = [cl]
                            , _funCompiled       = Just cc
                            , _funSplitTree      = mst
                            , _funMutual         = mutual
                            , _funProjection     = proj
                            , _funTerminates     = Just True
                            , _funExtLam         = extlam
                            , _funWith           = with
                            }
                      reportSDoc "tc.mod.apply" 80 $ ("new def for" <+> pretty x) <?> pretty newDef
                      return newDef

                cl :: Clause
    cl = 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 -> Either ProjectionLikenessMissing Projection
    funProjection = Right 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) -> [Arg Term] -> Elims
    forall a b. (a -> b) -> [a] -> [b]
    map Arg Term -> Elim
    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 :: Catchall
    clauseCatchall    = Catchall
    forall a. Null a => a
    empty
                            , 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
                            , clauseWhereModule :: Maybe ModuleName
    clauseWhereModule = Maybe ModuleName
    forall a. Maybe a
    Nothing
                            }
                  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
    $ (ProjectionLikenessMissing -> Int)
    -> (Projection -> Int)
    -> Either ProjectionLikenessMissing Projection
    -> Int
    forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
    either (Int -> ProjectionLikenessMissing -> Int
    forall a b. a -> b -> a
    const 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) Either ProjectionLikenessMissing 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
          totalArgs <- ModuleName -> TCMT IO Int
    argsToUse ModuleName
    x
          tel       <- lookupSection x
          let 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
          reportSDoc "tc.mod.apply" 80 $ "Copying section" <+> pretty x <+> "to" <+> pretty y
          reportSDoc "tc.mod.apply" 80 $ "  ts           = " <+> mconcat (List.intersperse "; " (map pretty ts))
          reportSDoc "tc.mod.apply" 80 $ "  totalArgs    = " <+> text (show totalArgs)
          reportSDoc "tc.mod.apply" 80 $ "  tel          = " <+> text (unwords (map (fst . unDom) $ telToList tel))  -- only names
          reportSDoc "tc.mod.apply" 80 $ "  sectionTel   = " <+> text (unwords (map (fst . unDom) $ telToList ptel)) -- only names
          addContext sectionTel $ addSection 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
      -- Check whether display form is recursive and thus illegal.
      xs <- DisplayForm -> Set QName -> TCM (Set QName)
    forall a. ChaseDisplayForms a => a -> Set QName -> TCM (Set QName)
    chaseDisplayForms DisplayForm
    df Set QName
    forall a. Set a
    Set.empty
      if x `Set.member` xs then warning $ InvalidDisplayForm x "it is recursive" else do
      d <- makeOpen df
      let 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 = d : defDisplay def }
      ifM (isLocal x)
        {-then-} (modifySignature add)
        {-else-} (stImportsDisplayForms `modifyTCLens` HMap.insertWith (++) x [d])

    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' TCState Definitions -> m Definitions
    forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
    useR ((Signature -> f Signature) -> TCState -> f TCState
    Lens' TCState Signature
    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' Signature Definitions
    sigDefinitions)

    getDisplayForms :: (HasConstInfo m, ReadTCState m) => QName -> m [LocalDisplayForm]
    getDisplayForms :: forall (m :: * -> *).
    (HasConstInfo m, ReadTCState m) =>
    QName -> m [LocalDisplayForm]
    getDisplayForms QName
    q = do
      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
      ds1 <- HMap.lookupDefault [] q <$> useR stImportsDisplayForms
      ds2 <- HMap.lookupDefault [] q <$> useR stImportedDisplayForms
      ifM (isLocal q) (return $ ds ++ ds1 ++ ds2)
                      (return $ ds1 ++ ds ++ ds2)

    hasDisplayForms :: (HasConstInfo m, ReadTCState m) => QName -> m Bool
    hasDisplayForms :: forall (m :: * -> *).
    (HasConstInfo m, ReadTCState m) =>
    QName -> m Bool
    hasDisplayForms = ([LocalDisplayForm] -> Bool) -> m [LocalDisplayForm] -> m Bool
    forall a b. (a -> b) -> m a -> m b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (Bool -> Bool
    not (Bool -> Bool)
    -> ([LocalDisplayForm] -> Bool) -> [LocalDisplayForm] -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [LocalDisplayForm] -> Bool
    forall a. Null a => a -> Bool
    null) (m [LocalDisplayForm] -> m Bool)
    -> (QName -> m [LocalDisplayForm]) -> QName -> m Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . QName -> m [LocalDisplayForm]
    forall (m :: * -> *).
    (HasConstInfo m, ReadTCState m) =>
    QName -> m [LocalDisplayForm]
    getDisplayForms

    -- | Find all names used (recursively) by display forms of a given name.
    --
    class ChaseDisplayForms a where
      chaseDisplayForms ::
           a                 -- ^ Search this recursively for display form names.
        -> Set QName         -- ^ Already processed names (accumulator).
        -> TCM (Set QName)   -- ^ Found names (superset of accumulator)

    instance ChaseDisplayForms QName where
      chaseDisplayForms :: QName -> Set QName -> TCM (Set QName)
    chaseDisplayForms QName
    q Set QName
    used
        | QName
    q QName -> Set QName -> Bool
    forall a. Ord a => a -> Set a -> Bool
    `Set.member` Set QName
    used = Set QName -> TCM (Set QName)
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Set QName
    used
        | Bool
    otherwise           = do
            ArgName -> Int -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    ArgName -> Int -> TCMT IO Doc -> m ()
    reportSDoc ArgName
    "tc.display.recursive" Int
    90 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ [TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    sep
              [ TCMT IO Doc
    "Chasing display form", QName -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => QName -> m Doc
    prettyTCM QName
    q, TCMT IO Doc
    "with accumulator", [QName] -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => [QName] -> m Doc
    prettyTCM (Set QName -> [QName]
    forall a. Set a -> [a]
    Set.toList Set QName
    used) ]
            xs <- 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_` TCMT IO [LocalDisplayForm] -> TCErr -> TCMT IO [LocalDisplayForm]
    forall a b. a -> b -> a
    const ([LocalDisplayForm] -> TCMT IO [LocalDisplayForm]
    forall a. a -> TCMT IO a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure [])  -- might be a pattern synonym
            chaseDisplayForms xs (Set.insert q used)

    instance ChaseDisplayForms DisplayTerm where
      chaseDisplayForms :: DisplayTerm -> Set QName -> TCM (Set QName)
    chaseDisplayForms DisplayTerm
    e Set QName
    used = do
        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
        let ds :: 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
    e
        Set QName -> Set QName -> TCM (Set QName)
    forall a. ChaseDisplayForms a => a -> Set QName -> TCM (Set QName)
    chaseDisplayForms Set QName
    ds Set QName
    used

    instance ChaseDisplayForms DisplayForm where
      -- Only look at names in the right-hand side (#1870)
      chaseDisplayForms :: DisplayForm -> Set QName -> TCM (Set QName)
    chaseDisplayForms = DisplayTerm -> Set QName -> TCM (Set QName)
    forall a. ChaseDisplayForms a => a -> Set QName -> TCM (Set QName)
    chaseDisplayForms (DisplayTerm -> Set QName -> TCM (Set QName))
    -> (DisplayForm -> DisplayTerm)
    -> DisplayForm
    -> Set QName
    -> TCM (Set QName)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . DisplayForm -> DisplayTerm
    dfRHS

    instance ChaseDisplayForms a => ChaseDisplayForms (Open a) where
      chaseDisplayForms :: Open a -> Set QName -> TCM (Set QName)
    chaseDisplayForms = a -> Set QName -> TCM (Set QName)
    forall a. ChaseDisplayForms a => a -> Set QName -> TCM (Set QName)
    chaseDisplayForms (a -> Set QName -> TCM (Set QName))
    -> (Open a -> a) -> Open a -> Set QName -> TCM (Set QName)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Open a -> a
    forall a. Open a -> a
    openThing

    instance ChaseDisplayForms a => ChaseDisplayForms (Set a) where
      chaseDisplayForms :: Set a -> Set QName -> TCM (Set QName)
    chaseDisplayForms Set a
    s = case Set a -> Maybe (a, Set a)
    forall a. Set a -> Maybe (a, Set a)
    Set.minView Set a
    s of
        Maybe (a, Set a)
    Nothing      -> Set QName -> TCM (Set QName)
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return
        Just (a
    x, Set a
    s') -> a -> Set QName -> TCM (Set QName)
    forall a. ChaseDisplayForms a => a -> Set QName -> TCM (Set QName)
    chaseDisplayForms a
    x (Set QName -> TCM (Set QName))
    -> (Set QName -> TCM (Set QName)) -> Set QName -> TCM (Set QName)
    forall (m :: * -> *) a b c.
    Monad m =>
    (a -> m b) -> (b -> m c) -> a -> m c
    >=> Set a -> Set QName -> TCM (Set QName)
    forall a. ChaseDisplayForms a => a -> Set QName -> TCM (Set QName)
    chaseDisplayForms Set a
    s'

    instance ChaseDisplayForms a => ChaseDisplayForms [a] where
      chaseDisplayForms :: [a] -> Set QName -> TCM (Set QName)
    chaseDisplayForms []     = Set QName -> TCM (Set QName)
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return
      chaseDisplayForms (a
    x:[a]
    xs) = a -> Set QName -> TCM (Set QName)
    forall a. ChaseDisplayForms a => a -> Set QName -> TCM (Set QName)
    chaseDisplayForms a
    x (Set QName -> TCM (Set QName))
    -> (Set QName -> TCM (Set QName)) -> Set QName -> TCM (Set QName)
    forall (m :: * -> *) a b c.
    Monad m =>
    (a -> m b) -> (b -> m c) -> a -> m c
    >=> [a] -> Set QName -> TCM (Set QName)
    forall a. ChaseDisplayForms a => a -> Set QName -> TCM (Set QName)
    chaseDisplayForms [a]
    xs
      -- NB: The following does not work because of lacking instance Ord LocalDisplayForm:
      -- chaseDisplayForms = chaseDisplayForms . Set.toList

    canonicalName :: HasConstInfo m => QName -> m QName
    canonicalName :: forall (m :: * -> *). HasConstInfo m => QName -> m QName
    canonicalName QName
    x = do
      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 def of
        Constructor{conSrcCon :: Defn -> ConHead
    conSrcCon = ConHead
    c}                                -> QName -> m QName
    forall a. a -> m a
    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 a. a -> m a
    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
      c1 <- QName -> m QName
    forall (m :: * -> *). HasConstInfo m => QName -> m QName
    canonicalName QName
    d1
      c2 <- canonicalName d2
      if (c1 == c2) then return $ Just c1 else return Nothing

    -- | 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
      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 d of
        Record {}                   -> Bool -> TCMT IO Bool
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Bool
    True
        Constructor { conData :: Defn -> QName
    conData = QName
    d } -> do
          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
          return $ case di of
            Record {}                  -> Bool
    True
            Datatype { dataCons :: Defn -> [QName]
    dataCons = [QName]
    cs } -> [QName] -> Peano
    forall a. Sized a => a -> Peano
    natSize [QName]
    cs Peano -> Peano -> Bool
    forall a. Eq a => a -> a -> Bool
    == Peano
    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.
      | SigCubicalNotErasure
        -- ^ The name is not available because it was defined in Cubical
        -- Agda, but the current language is Erased Cubical Agda, and
        -- @--erasure@ is not active.

    -- | Generates a string error message corresponding to
    -- 'SigCubicalNotErasure' for a given 'QName'.
    notSoPrettySigCubicalNotErasure :: QName -> String
    notSoPrettySigCubicalNotErasure :: QName -> ArgName
    notSoPrettySigCubicalNotErasure QName
    q =
      ArgName
    "The name " ArgName -> ArgName -> ArgName
    forall a. [a] -> [a] -> [a]
    ++ QName -> ArgName
    forall a. Pretty a => a -> ArgName
    prettyShow QName
    q ArgName -> ArgName -> ArgName
    forall a. [a] -> [a] -> [a]
    ++ ArgName
    " which was defined in Cubical " ArgName -> ArgName -> ArgName
    forall a. [a] -> [a] -> [a]
    ++
      ArgName
    "Agda can only be used in Erased Cubical Agda if the option " ArgName -> ArgName -> ArgName
    forall a. [a] -> [a] -> [a]
    ++
      ArgName
    "--erasure is used"

    -- | Generates an error message corresponding to
    -- 'SigCubicalNotErasure' for a given 'QName'.
    prettySigCubicalNotErasure :: MonadPretty m => QName -> m Doc
    prettySigCubicalNotErasure :: forall (m :: * -> *). MonadPretty m => QName -> m Doc
    prettySigCubicalNotErasure QName
    q = [m Doc] -> m Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
    forall a b. (a -> b) -> a -> b
    $
      ArgName -> [m Doc]
    forall (m :: * -> *). Applicative m => ArgName -> [m Doc]
    pwords ArgName
    "The name" [m Doc] -> [m Doc] -> [m Doc]
    forall a. [a] -> [a] -> [a]
    ++
      [QName -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => QName -> m Doc
    prettyTCM QName
    q] [m Doc] -> [m Doc] -> [m Doc]
    forall a. [a] -> [a] -> [a]
    ++
      ArgName -> [m Doc]
    forall (m :: * -> *). Applicative m => ArgName -> [m Doc]
    pwords ArgName
    "which was defined in Cubical Agda can only be used in" [m Doc] -> [m Doc] -> [m Doc]
    forall a. [a] -> [a] -> [a]
    ++
      ArgName -> [m Doc]
    forall (m :: * -> *). Applicative m => ArgName -> [m Doc]
    pwords ArgName
    "Erased Cubical Agda if the option --erasure is used"

    -- | An eliminator for 'SigError'. All constructors except for
    -- 'SigAbstract' are assumed to be impossible.
    sigError :: (HasCallStack, MonadDebug m) => QName -> m a -> SigError -> m a
    sigError :: forall (m :: * -> *) a.
    (HasCallStack, MonadDebug m) =>
    QName -> m a -> SigError -> m a
    sigError QName
    q m a
    a = \case
      SigUnknown ArgName
    s         -> ArgName -> m a
    forall (m :: * -> *) a.
    (HasCallStack, MonadDebug m) =>
    ArgName -> m a
    __IMPOSSIBLE_VERBOSE__ ArgName
    s
      SigError
    SigAbstract          -> m a
    a
      SigError
    SigCubicalNotErasure -> ArgName -> m a
    forall (m :: * -> *) a.
    (HasCallStack, MonadDebug m) =>
    ArgName -> m a
    __IMPOSSIBLE_VERBOSE__ (ArgName -> m a) -> ArgName -> m a
    forall a b. (a -> b) -> a -> b
    $
        QName -> ArgName
    notSoPrettySigCubicalNotErasure QName
    q

    class ( Functor m
          , Applicative 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 a b. m a -> (a -> m b) -> m b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \case
          Right Definition
    d -> Definition -> m Definition
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Definition
    d
          Left SigError
    err -> (m Definition -> SigError -> m Definition)
    -> SigError -> m Definition -> m Definition
    forall a b c. (a -> b -> c) -> b -> a -> c
    flip (QName -> m Definition -> SigError -> m Definition
    forall (m :: * -> *) a.
    (HasCallStack, MonadDebug m) =>
    QName -> m a -> SigError -> m a
    sigError QName
    q) SigError
    err (m Definition -> m Definition) -> m Definition -> m Definition
    forall a b. (a -> b) -> a -> b
    $
            ArgName -> m Definition
    forall (m :: * -> *) a.
    (HasCallStack, MonadDebug m) =>
    ArgName -> m a
    __IMPOSSIBLE_VERBOSE__ (ArgName -> m Definition) -> ArgName -> m Definition
    forall a b. (a -> b) -> a -> b
    $
            ArgName
    "Abstract, thus, not in scope: " ArgName -> ArgName -> ArgName
    forall a. [a] -> [a] -> [a]
    ++ QName -> ArgName
    forall a. Pretty a => a -> ArgName
    prettyShow QName
    q

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

      -- | Return the rewrite rules for the given head symbol that could be tried.
      --   Not categorically all rewrite rules are returned, in particular, none when
      --   reduction of the head symbol is disabled.
      --   Rewrite rules that only happen to be in the signature but are not in scope
      --   are also not returned.
      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) -> m (Either SigError Definition)
    n (Either SigError Definition) -> t n (Either SigError Definition)
    forall (m :: * -> *) a. Monad m => m a -> t m a
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (n (Either SigError Definition) -> m (Either SigError Definition))
    -> (QName -> n (Either SigError Definition))
    -> QName
    -> m (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 -> m RewriteRules
    n RewriteRules -> t n RewriteRules
    forall (m :: * -> *) a. Monad m => m a -> t m a
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (n RewriteRules -> m RewriteRules)
    -> (QName -> n RewriteRules) -> QName -> m 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 #-}

    {-# SPECIALIZE getOriginalConstInfo :: 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
      def  <- QName -> m Definition
    forall (m :: * -> *). HasConstInfo m => QName -> m Definition
    getConstInfo QName
    q
      lang <- getLanguage
      case (lang, defLanguage def) of
        (Cubical Cubical
    CErased, Cubical Cubical
    CFull) ->
          Lens' TCState (Maybe Cubical)
    -> (Maybe Cubical -> Maybe Cubical) -> m Definition -> m Definition
    forall a b. Lens' TCState a -> (a -> a) -> m b -> m b
    forall (m :: * -> *) a b.
    ReadTCState m =>
    Lens' TCState a -> (a -> a) -> m b -> m b
    locallyTCState
            ((PragmaOptions -> f PragmaOptions) -> TCState -> f TCState
    Lens' TCState PragmaOptions
    stPragmaOptions ((PragmaOptions -> f PragmaOptions) -> TCState -> f TCState)
    -> ((Maybe Cubical -> f (Maybe Cubical))
        -> PragmaOptions -> f PragmaOptions)
    -> (Maybe Cubical -> f (Maybe Cubical))
    -> TCState
    -> f TCState
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Maybe Cubical -> f (Maybe Cubical))
    -> PragmaOptions -> f PragmaOptions
    forall (f :: * -> *).
    Functor f =>
    (Maybe Cubical -> f (Maybe Cubical))
    -> PragmaOptions -> f PragmaOptions
    lensOptCubical)
            (Maybe Cubical -> Maybe Cubical -> Maybe Cubical
    forall a b. a -> b -> a
    const (Maybe Cubical -> Maybe Cubical -> Maybe Cubical)
    -> Maybe Cubical -> Maybe Cubical -> Maybe Cubical
    forall a b. (a -> b) -> a -> b
    $ 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 a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Definition
    def

    -- | Return the rewrite rules for the given head symbol that could be tried.
    --   Not categorically all rewrite rules are returned, e.g. none when
    --   reduction of the head symbol is disabled.
    --   Rewrite rules that only happen to be in the signature but are not in scope
    --   are also not returned.
    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 a. a -> m a
    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
      Bool -> QName -> m RewriteRules
    forall (m :: * -> *).
    (ReadTCState m, MonadTCEnv m) =>
    Bool -> QName -> m RewriteRules
    getFilteredRewriteRulesFor Bool
    True QName
    q

    -- | If the 'Bool' parameter is 'True', get the rules in scope,
    --   otherwise, get *all* rules unfiltered.
    getFilteredRewriteRulesFor :: (ReadTCState m, MonadTCEnv m)
      => Bool            -- ^ Only return rewrite rules that are in scope?
      -> QName           -- ^ Head symbol.
      -> m RewriteRules  -- ^ Rules for the head symbol.
    getFilteredRewriteRulesFor :: forall (m :: * -> *).
    (ReadTCState m, MonadTCEnv m) =>
    Bool -> QName -> m RewriteRules
    getFilteredRewriteRulesFor Bool
    filt QName
    q = do
      st <- m TCState
    forall (m :: * -> *). ReadTCState m => m TCState
    getTCState
      let
        look :: Lens' TCState Signature -> Maybe RewriteRules
        look Lens' TCState Signature
    l = 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
    $ TCState
    st TCState -> Lens' TCState RewriteRuleMap -> RewriteRuleMap
    forall o i. o -> Lens' o i -> i
    ^. ((Signature -> f Signature) -> TCState -> f TCState
    Lens' TCState Signature
    l ((Signature -> f Signature) -> TCState -> f TCState)
    -> ((RewriteRuleMap -> f RewriteRuleMap)
        -> Signature -> f Signature)
    -> (RewriteRuleMap -> f RewriteRuleMap)
    -> TCState
    -> f TCState
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (RewriteRuleMap -> f RewriteRuleMap) -> Signature -> f Signature
    Lens' Signature RewriteRuleMap
    sigRewriteRules)

      -- Restrict "imported" rewrite rules to those defined in modules we currently (transitively) import.
      let imps = TCState
    st TCState
    -> Lens' TCState (Set TopLevelModuleName) -> Set TopLevelModuleName
    forall o i. o -> Lens' o i -> i
    ^. (Set TopLevelModuleName -> f (Set TopLevelModuleName))
    -> TCState -> f TCState
    Lens' TCState (Set TopLevelModuleName)
    stImportedModulesTransitive
      let inScope RewriteRule
    rew = RewriteRule -> TopLevelModuleName
    rewTopModule RewriteRule
    rew TopLevelModuleName -> Set TopLevelModuleName -> Bool
    forall a. Ord a => a -> Set a -> Bool
    `Set.member` Set TopLevelModuleName
    imps
      let rewImported = Bool
    -> (RewriteRules -> RewriteRules) -> RewriteRules -> RewriteRules
    forall b a. IsBool b => b -> (a -> a) -> a -> a
    applyWhen Bool
    filt ((RewriteRule -> Bool) -> RewriteRules -> RewriteRules
    forall a. (a -> Bool) -> [a] -> [a]
    filter RewriteRule -> Bool
    inScope) (RewriteRules -> RewriteRules)
    -> Maybe RewriteRules -> Maybe RewriteRules
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Lens' TCState Signature -> Maybe RewriteRules
    look (Signature -> f Signature) -> TCState -> f TCState
    Lens' TCState Signature
    stImports  -- stImports is actually a superset of imported symbols.

      return $ mconcat $ catMaybes [look stSignature, rewImported]

    -- | 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
        st  <- TCMT IO TCState
    forall (m :: * -> *). MonadTCState m => m TCState
    getTC
        env <- askTC
        defaultGetConstInfo st env 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 a b. TCMT IO a -> (a -> TCMT IO b) -> TCMT IO b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \case
          Right Definition
    d -> Definition -> TCMT IO Definition
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Definition
    d
          Left (SigUnknown ArgName
    err)     -> ArgName -> TCMT IO Definition
    forall a. ArgName -> TCMT IO a
    forall (m :: * -> *) a. MonadFail m => ArgName -> m a
    fail ArgName
    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
          Left SigError
    SigCubicalNotErasure -> TypeError -> TCMT IO Definition
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    TypeError -> m a
    typeError (TypeError -> TCMT IO Definition)
    -> TypeError -> TCMT IO Definition
    forall a b. (a -> b) -> a -> b
    $ QName -> TypeError
    CubicalNotErasure 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
    st TCState -> Lens' TCState Definitions -> Definitions
    forall o i. o -> Lens' o i -> i
    ^. (Signature -> f Signature) -> TCState -> f TCState
    Lens' TCState Signature
    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' Signature Definitions
    sigDefinitions
            idefs :: Definitions
    idefs = TCState
    st TCState -> Lens' TCState Definitions -> Definitions
    forall o i. o -> Lens' o i -> i
    ^. (Signature -> f Signature) -> TCState -> f TCState
    Lens' TCState Signature
    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' Signature Definitions
    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 a. a -> m a
    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
    $ ArgName -> SigError
    SigUnknown (ArgName -> SigError) -> ArgName -> SigError
    forall a b. (a -> b) -> a -> b
    $ ArgName
    "Unbound name: " ArgName -> ArgName -> ArgName
    forall a. [a] -> [a] -> [a]
    ++ QName -> ArgName
    forall a. Pretty a => a -> ArgName
    prettyShow QName
    q ArgName -> ArgName -> ArgName
    forall a. [a] -> [a] -> [a]
    ++ QName -> ArgName
    showQNameId QName
    q
            [Definition
    d] -> Definition -> m (Either SigError Definition)
    forall {m :: * -> *}.
    HasOptions m =>
    Definition -> m (Either SigError Definition)
    checkErasureFixQuantity Definition
    d m (Either SigError Definition)
    -> (Either SigError Definition -> m (Either SigError Definition))
    -> m (Either SigError Definition)
    forall a b. m a -> (a -> m b) -> m b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \case
                     Left SigError
    err -> Either SigError Definition -> m (Either SigError Definition)
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (SigError -> Either SigError Definition
    forall a b. a -> Either a b
    Left SigError
    err)
                     Right Definition
    d  -> TCEnv -> Definition -> m (Either SigError Definition)
    mkAbs TCEnv
    env Definition
    d
            [Definition]
    ds  -> ArgName -> m (Either SigError Definition)
    forall (m :: * -> *) a.
    (HasCallStack, MonadDebug m) =>
    ArgName -> m a
    __IMPOSSIBLE_VERBOSE__ (ArgName -> m (Either SigError Definition))
    -> ArgName -> m (Either SigError Definition)
    forall a b. (a -> b) -> a -> b
    $ ArgName
    "Ambiguous name: " ArgName -> ArgName -> ArgName
    forall a. [a] -> [a] -> [a]
    ++ QName -> ArgName
    forall a. Pretty a => a -> ArgName
    prettyShow QName
    q
        where
          mkAbs :: TCEnv -> Definition -> m (Either SigError Definition)
    mkAbs TCEnv
    env Definition
    d
            -- Apply the reducibility rules (abstract, opaque) to check
            -- whether the definition should be hidden behind an
            -- 'AbstractDef'.
            | Bool -> Bool
    not (TCEnv -> TCState -> Definition -> Bool
    isAccessibleDef TCEnv
    env TCState
    st Definition
    d{defName = q'}) =
              case Definition -> Maybe Definition
    alwaysMakeAbstract Definition
    d of
                Just Definition
    d      -> Either SigError Definition -> m (Either SigError Definition)
    forall a. a -> m a
    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 a. a -> m a
    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 a. a -> m a
    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 = mnameFromList $
                     initWithDefault __IMPOSSIBLE__ $ mnameToList m
                 }

          -- Names defined in Cubical Agda may only be used in Erased
          -- Cubical Agda if --erasure is used. In that case they are (to
          -- a large degree) treated as erased.
          checkErasureFixQuantity :: Definition -> m (Either SigError Definition)
    checkErasureFixQuantity Definition
    d = do
            current <- m Language
    forall (m :: * -> *). HasOptions m => m Language
    getLanguage
            if defLanguage d == Cubical CFull &&
               current == Cubical CErased
            then do
              erasure <- optErasure <$> pragmaOptions
              return $
                if erasure
                then Right $ setQuantity zeroQuantity d
                else Left SigCubicalNotErasure
            else return $ Right 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
      ArgName -> Int -> TCMT IO Doc -> m ()
    forall (m :: * -> *).
    MonadDebug m =>
    ArgName -> Int -> TCMT IO Doc -> m ()
    reportSDoc ArgName
    "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

    -- | Returns the occurences given explicitely as polarity annotations in the function type
    getOccurrencesFromType :: Type -> TCM [Occurrence]
    getOccurrencesFromType :: Type -> TCM [Occurrence]
    getOccurrencesFromType Type
    t = do
      polarityEnabled <- PragmaOptions -> Bool
    optPolarity (PragmaOptions -> Bool) -> TCMT IO PragmaOptions -> TCMT IO Bool
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> TCMT IO PragmaOptions
    forall (m :: * -> *). HasOptions m => m PragmaOptions
    pragmaOptions
      if polarityEnabled then do
        telList <- telToList . theTel <$> telView t
        return $ modalPolarityToOccurrence . modPolarityAnn . getModalPolarity <$> telList
      else return []

    -- | 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
      def <- QName -> TCMT IO Definition
    forall (m :: * -> *). HasConstInfo m => QName -> m Definition
    getConstInfo QName
    d
      case theDef def of
        Constructor{} -> Occurrence -> TCM Occurrence
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Occurrence
    StrictPos

        -- If the polarity checker has filled in the positivities of
        -- arguments for this function then we believe it, because it should
        -- agree with the signature.
        Defn
    _ | Just Occurrence
    pol <- Definition -> [Occurrence]
    defArgOccurrences Definition
    def [Occurrence] -> Int -> Maybe Occurrence
    forall a. [a] -> Int -> Maybe a
    !!! Int
    i ->
          Occurrence -> TCM Occurrence
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Occurrence
    pol

        -- Otherwise we use them from the type. Since telView can do
        -- reduction we'd rather not do this very often.
        Defn
    _ -> do
          occs <- Type -> TCM [Occurrence]
    getOccurrencesFromType (Definition -> Type
    defType Definition
    def)

          pure $! fromMaybe Mixed $ occs !!! 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 = Just $ Compiled t 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 = funTreeless fun <&> \ Compiled
    c -> Compiled
    c { cArgUsage = Just 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 (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f 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
      def <- QName -> m Definition
    forall (m :: * -> *). HasConstInfo m => QName -> m Definition
    getConstInfo QName
    q
      case theDef def of
        Constructor{ Int
    conArity :: Defn -> Int
    conArity :: Int
    conArity, Maybe [Bool]
    conErased :: Maybe [Bool]
    conErased :: Defn -> Maybe [Bool]
    conErased } -> [Bool] -> m [Bool]
    forall a. a -> m a
    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 :: Defn -> Int
    conArity :: Int
    conArity }
          | [Bool] -> Int
    forall a. [a] -> 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 = Just 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 a b. (a -> b) -> Maybe a -> Maybe b
    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 = 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.
    --
    --   TODO: This produces data of quadratic size (which has to be processed upon serialization).
    --   Presumably qs is usually short, but in some cases (for instance for generated code) it may be
    --   long. It would be better to assign a unique identifier to each SCC, and store the names
    --   separately.
    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 = Just m }
        Datatype{} -> Defn
    def {dataMutual = Just m }
        Record{}   -> Defn
    def { recMutual = Just 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 a. Eq a => a -> [a] -> 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
      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 null vs then return [] else do
      t <- defType <$> getConstInfo q
      let TelV tel _ = telView'UpTo (size vs) t
      unless (size tel == size vs) __IMPOSSIBLE__
      return $ zipWith (\ Arg Term
    arg Dom (ArgName, Type)
    dom -> Arg Term -> Term
    forall e. Arg e -> e
    unArg Arg Term
    arg Term -> Arg (ArgName, Type) -> Arg Term
    forall a b. a -> Arg b -> Arg a
    forall (f :: * -> *) a b. Functor f => a -> f b -> f a
    <$ Dom (ArgName, Type) -> Arg (ArgName, Type)
    forall t a. Dom' t a -> Arg a
    argFromDom Dom (ArgName, Type)
    dom) vs $ telToList 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
      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
      (+) <$> getAnonymousVariables m <*> (size <$> lookupSection 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

      ArgName -> Int -> TCMT IO Doc -> m [Arg Term] -> m [Arg Term]
    forall (m :: * -> *) a.
    MonadDebug m =>
    ArgName -> Int -> TCMT IO Doc -> m a -> m a
    traceSDoc ArgName
    "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 a. a -> m a
    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

      ArgName -> Int -> TCMT IO Doc -> m [Arg Term] -> m [Arg Term]
    forall (m :: * -> *) a.
    MonadDebug m =>
    ArgName -> Int -> TCMT IO Doc -> m a -> m a
    traceSDoc ArgName
    "tc.sig.param" Int
    60 (do
        cxt <- TCMT IO [ContextEntry]
    forall (m :: * -> *). MonadTCEnv m => m [ContextEntry]
    getContext
        nest 2 $ vcat
          [ "cxt  = " <+> prettyTCM (PrettyContext cxt)
          , "sub  = " <+> pretty 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@.
      n   <- ModuleName -> m Int
    forall (m :: * -> *).
    (Functor m, Applicative m, MonadTCEnv m, ReadTCState m) =>
    ModuleName -> m Int
    getModuleFreeVars ModuleName
    m
      traceSDoc "tc.sig.param" 60 (nest 2 $ "n    = " <+> text (show n)) $ do
      tel <- take n . telToList <$> lookupSection m
      traceSDoc "tc.sig.param" 60 (nest 2 $ "tel  = " <+> pretty tel) $ do
      unless (size tel == n) __IMPOSSIBLE__
      let 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 (ArgName, Type) -> Arg Term)
    -> [Int] -> [Dom (ArgName, Type)] -> [Arg Term]
    forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
    zipWith (\ Int
    i Dom (ArgName, Type)
    a -> Int -> Term
    var Int
    i Term -> Arg (ArgName, Type) -> Arg Term
    forall a b. a -> Arg b -> Arg a
    forall (f :: * -> *) a b. Functor f => a -> f b -> f a
    <$ Dom (ArgName, Type) -> Arg (ArgName, Type)
    forall t a. Dom' t a -> Arg a
    argFromDom Dom (ArgName, Type)
    a) (Int -> [Int]
    forall a. Integral a => a -> [a]
    downFrom Int
    n) [Dom (ArgName, Type)]
    tel
      traceSDoc "tc.sig.param" 60 (nest 2 $ "args = " <+> prettyList_ (map pretty args)) $ do

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

      getSection m >>= \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 a. a -> m a
    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 b (m :: * -> *). (IsBool b, Monad m) => b -> m () -> m ()
    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 a. a -> m a
    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 (ArgName, Type) -> Arg Term -> Arg Term)
    -> [Dom (ArgName, Type)] -> [Arg Term] -> [Arg Term]
    forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
    zipWith (\ !Dom (ArgName, Type)
    dom (Arg ArgInfo
    _ Term
    v) -> Term
    v Term -> Arg (ArgName, Type) -> Arg Term
    forall a b. a -> Arg b -> Arg a
    forall (f :: * -> *) a b. Functor f => a -> f b -> f a
    <$ Dom (ArgName, Type) -> Arg (ArgName, Type)
    forall t a. Dom' t a -> Arg a
    argFromDom Dom (ArgName, Type)
    dom) (Telescope -> [Dom (ArgName, Type)]
    forall t. Tele (Dom t) -> [Dom (ArgName, 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
      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 isNothing msub || msub == Just IdS then k else do
        m  <- currentModule
        m' <- qualifyM m . mnameFromList1 . singleton <$>
                freshName_ ("_" :: String)
        addSection m'
        withCurrentModule m' 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
      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
      verboseS "tc.sig.inst" 30 $ do
        ctx <- getContextNames
        m   <- currentModule
        reportSDoc "tc.sig.inst" 30 $
          "instDef in" <+> pretty m <> ":" <+> pretty (defName d) <+>
          fsep (map pretty $ zipWith (<$) ctx vs)
      return $ d `apply` 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
      ArgName -> Int -> TCMT IO Doc -> m RewriteRule -> m RewriteRule
    forall (m :: * -> *) a.
    MonadDebug m =>
    ArgName -> Int -> TCMT IO Doc -> m a -> m a
    traceSDoc ArgName
    "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
      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 -> [Arg Term] -> RewriteRule
    forall t. Apply t => t -> [Arg Term] -> t
    `apply` [Arg Term]
    vs
      traceSLn "rewriting" 95 ("instantiated rewrite rule: ") $ do
      traceSLn "rewriting" 95 (show rew') $ do
      return 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)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
    mapM RewriteRule -> m RewriteRule
    forall (m :: * -> *).
    (Functor m, HasConstInfo m, HasOptions m, ReadTCState m,
     MonadTCEnv m, MonadDebug m) =>
    RewriteRule -> m RewriteRule
    instantiateRewriteRule

    -- | Return the abstract view of a definition, /regardless/ of whether
    -- the definition would be treated abstractly.
    alwaysMakeAbstract :: Definition -> Maybe Definition
    alwaysMakeAbstract :: Definition -> Maybe Definition
    alwaysMakeAbstract Definition
    d =
      do
        def <- Defn -> Maybe Defn
    makeAbs (Defn -> Maybe Defn) -> Defn -> Maybe Defn
    forall a b. (a -> b) -> a -> b
    $ Definition -> Defn
    theDef Definition
    d
        pure d { defArgOccurrences = [] -- no positivity info for abstract things!
               , defPolarity       = [] -- no polarity info for abstract things!
               , theDef = 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 a. (TCEnv -> TCEnv) -> m a -> m a
    forall (m :: * -> *) a.
    MonadTCEnv m =>
    (TCEnv -> TCEnv) -> m a -> m a
    localTC ((TCEnv -> TCEnv) -> m a -> m a) -> (TCEnv -> TCEnv) -> m a -> m a
    forall a b. (a -> b) -> a -> b
    $ \TCEnv
    e -> TCEnv
    e { envAbstractMode = 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 a. (TCEnv -> TCEnv) -> m a -> m a
    forall (m :: * -> *) a.
    MonadTCEnv m =>
    (TCEnv -> TCEnv) -> m a -> m a
    localTC ((TCEnv -> TCEnv) -> m a -> m a) -> (TCEnv -> TCEnv) -> m a -> m a
    forall a b. (a -> b) -> a -> b
    $ \TCEnv
    e -> TCEnv
    e { envAbstractMode = 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 a. (TCEnv -> TCEnv) -> m a -> m a
    forall (m :: * -> *) a.
    MonadTCEnv m =>
    (TCEnv -> TCEnv) -> m a -> m a
    localTC ((TCEnv -> TCEnv) -> m a -> m a) -> (TCEnv -> TCEnv) -> m a -> m a
    forall a b. (a -> b) -> a -> b
    $ \TCEnv
    e -> TCEnv
    e { envAbstractMode = IgnoreAbstractMode }

    -- | Go under the given opaque block. The unfolding set will turn opaque
    -- definitions transparent.
    {-# SPECIALIZE underOpaqueId :: OpaqueId -> TCM a -> TCM a #-}
    underOpaqueId :: MonadTCEnv m => OpaqueId -> m a -> m a
    underOpaqueId :: forall (m :: * -> *) a. MonadTCEnv m => OpaqueId -> m a -> m a
    underOpaqueId OpaqueId
    i = (TCEnv -> TCEnv) -> m a -> m a
    forall a. (TCEnv -> TCEnv) -> m a -> m a
    forall (m :: * -> *) a.
    MonadTCEnv m =>
    (TCEnv -> TCEnv) -> m a -> m a
    localTC ((TCEnv -> TCEnv) -> m a -> m a) -> (TCEnv -> TCEnv) -> m a -> m a
    forall a b. (a -> b) -> a -> b
    $ \TCEnv
    e -> TCEnv
    e { envCurrentOpaqueId = Just i }

    -- | Outside of any opaque blocks.
    {-# SPECIALIZE notUnderOpaque :: TCM a -> TCM a #-}
    notUnderOpaque :: MonadTCEnv m => m a -> m a
    notUnderOpaque :: forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
    notUnderOpaque = (TCEnv -> TCEnv) -> m a -> m a
    forall a. (TCEnv -> TCEnv) -> m a -> m a
    forall (m :: * -> *) a.
    MonadTCEnv m =>
    (TCEnv -> TCEnv) -> m a -> m a
    localTC ((TCEnv -> TCEnv) -> m a -> m a) -> (TCEnv -> TCEnv) -> m a -> m a
    forall a b. (a -> b) -> a -> b
    $ \TCEnv
    e -> TCEnv
    e { envCurrentOpaqueId = Nothing }

    -- | Enter the reducibility environment associated with a definition:
    -- The environment will have the same concreteness as the name, and we
    -- will be in the opaque block enclosing the name, if any.
    {-# 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.
      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
      let
        k1 = case Definition -> IsAbstract
    defAbstract Definition
    def of
          IsAbstract
    AbstractDef -> m a -> m a
    forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
    inAbstractMode
          IsAbstract
    ConcreteDef -> m a -> m a
    forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
    inConcreteMode

        k2 = case Definition -> IsOpaque
    defOpaque Definition
    def of
          OpaqueDef OpaqueId
    i    -> OpaqueId -> m a -> m a
    forall (m :: * -> *) a. MonadTCEnv m => OpaqueId -> m a -> m a
    underOpaqueId OpaqueId
    i
          IsOpaque
    TransparentDef -> m a -> m a
    forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
    notUnderOpaque
      k2 (k1 (cont def))

    -- | 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
    0 -- not impossible when quoting, PR #7828

    -- | 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 -> Either ProjectionLikenessMissing Projection
    funProjection = Right Projection
    result } -> Projection -> Maybe Projection
    forall a. a -> Maybe a
    Just 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' Defn Bool -> Bool
    forall o i. o -> Lens' o i -> i
    ^. (Bool -> f Bool) -> Defn -> f Defn
    Lens' Defn Bool
    funStatic)

    -- | Is it a function marked INLINE?
    isInlineFun :: Defn -> Bool
    isInlineFun :: Defn -> Bool
    isInlineFun = (Defn -> Lens' Defn Bool -> Bool
    forall o i. o -> Lens' o i -> i
    ^. (Bool -> f Bool) -> Defn -> f Defn
    Lens' Defn Bool
    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, HasBuiltins m) => QName -> m Bool
    usesCopatterns :: forall (m :: * -> *).
    (HasConstInfo m, HasBuiltins 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 a. a -> m a
    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
    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 a. a -> m a
    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
    forall a. ProjOrigin -> QName -> Elim' a
    Proj ProjOrigin
    o (QName -> Elim) -> QName -> Elim
    forall a b. (a -> b) -> a -> b
    $ Projection -> QName
    projOrig Projection
    isP]