    {-# LANGUAGE NondecreasingIndentation #-}

    module Agda.TypeChecking.Rules.Def where

    import Prelude hiding ( null )

    import Control.Monad        ( forM, forM_ )
    import Control.Monad.Except ( MonadError(..) )

    import Data.Bifunctor
    import Data.Function (on)
    import Data.IntSet (IntSet)
    import qualified Data.IntSet as IntSet
    import qualified Data.List as List
    import Data.Maybe
    import Data.Map (Map)
    import qualified Data.Map as Map
    import Data.Semigroup ( sconcat )

    import Agda.Interaction.Options

    import Agda.Syntax.Common
    import qualified Agda.Syntax.Concrete as C
    import qualified Agda.Syntax.Concrete.Pretty as C
    import Agda.Syntax.Position
    import Agda.Syntax.Abstract.Pattern as A
    import qualified Agda.Syntax.Abstract as A
    import qualified Agda.Syntax.Abstract.Views as A
    import Agda.Syntax.Internal as I
    import Agda.Syntax.Internal.Pattern as I
    import Agda.Syntax.Internal.MetaVars (allMetasList)
    import qualified Agda.Syntax.Info as Info
    import Agda.Syntax.Info hiding (defAbstract)

    import Agda.TypeChecking.Monad
    import qualified Agda.TypeChecking.Monad.Benchmark as Bench
    import Agda.TypeChecking.Warnings ( warning )

    import Agda.TypeChecking.Constraints
    import Agda.TypeChecking.Conversion
    import Agda.TypeChecking.Coverage.SplitTree
    import Agda.TypeChecking.Inlining
    import Agda.TypeChecking.Reduce
    import Agda.TypeChecking.Patterns.Abstract (expandPatternSynonyms)
    import Agda.TypeChecking.Pretty
    import Agda.TypeChecking.Substitute
    import Agda.TypeChecking.CheckInternal
    import Agda.TypeChecking.With
    import Agda.TypeChecking.Telescope
    import Agda.TypeChecking.Telescope.Path
    import Agda.TypeChecking.Injectivity
    import Agda.TypeChecking.InstanceArguments
    import Agda.TypeChecking.SizedTypes.Solve
    import Agda.TypeChecking.Rewriting.Confluence
    import Agda.TypeChecking.CompiledClause (CompiledClauses'(..), hasProjectionPatterns)
    import Agda.TypeChecking.CompiledClause.Compile
    import Agda.TypeChecking.Primitive hiding (Nat)
    import Agda.TypeChecking.RecordPatterns ( recordRHSToCopatterns )
    import Agda.TypeChecking.Sort

    import Agda.TypeChecking.Rules.Term
    import Agda.TypeChecking.Rules.LHS                 ( checkLeftHandSide, LHSResult(..), bindAsPatterns )
    import {-# SOURCE #-} Agda.TypeChecking.Rules.Decl ( checkDecls )

    import Agda.Utils.Function ( applyWhen, applyWhenM )
    import Agda.Utils.Functor
    import Agda.Utils.Lens
    import Agda.Utils.List
    import Agda.Utils.List1 ( List1, pattern (:|), (<|) )
    import qualified Agda.Utils.List1 as List1
    import Agda.Utils.Maybe
    import Agda.Utils.Monad
    import Agda.Utils.Null
    import Agda.Utils.Permutation
    import Agda.Syntax.Common.Pretty ( prettyShow )
    import qualified Agda.Syntax.Common.Pretty as P
    import Agda.Utils.Singleton
    import Agda.Utils.Size
    import qualified Agda.Utils.SmallSet as SmallSet
    import Agda.Utils.Update

    import Agda.Utils.Impossible

    ---------------------------------------------------------------------------
    -- * Definitions by pattern matching
    ---------------------------------------------------------------------------

    checkFunDef :: A.DefInfo -> QName -> [A.Clause] -> TCM ()
    checkFunDef :: DefInfo -> QName -> [Clause' LHS] -> TCM ()
    checkFunDef DefInfo
    i QName
    name [Clause' LHS]
    cs = do
            -- Reset blocking tag (in case a previous attempt was blocked)
            (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
    name ((Definition -> Definition) -> Signature -> Signature)
    -> (Definition -> Definition) -> Signature -> Signature
    forall a b. (a -> b) -> a -> b
    $ (Blocked_ -> Blocked_) -> Definition -> Definition
    updateDefBlocked ((Blocked_ -> Blocked_) -> Definition -> Definition)
    -> (Blocked_ -> Blocked_) -> Definition -> Definition
    forall a b. (a -> b) -> a -> b
    $ Blocked_ -> Blocked_ -> Blocked_
    forall a b. a -> b -> a
    const (Blocked_ -> Blocked_ -> Blocked_)
    -> Blocked_ -> Blocked_ -> Blocked_
    forall a b. (a -> b) -> a -> b
    $
              NotBlocked' Term -> () -> Blocked_
    forall t a. NotBlocked' t -> a -> Blocked' t a
    NotBlocked (QName -> NotBlocked' Term
    forall t. QName -> NotBlocked' t
    MissingClauses QName
    name) ()
            -- Get the type and relevance of the function
            def <- Definition -> TCMT IO Definition
    forall (m :: * -> *).
    (Functor m, HasConstInfo m, HasOptions m, ReadTCState m,
     MonadTCEnv m, MonadDebug m) =>
    Definition -> m Definition
    instantiateDef (Definition -> TCMT IO Definition)
    -> TCMT IO Definition -> TCMT IO Definition
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< QName -> TCMT IO Definition
    forall (m :: * -> *). HasConstInfo m => QName -> m Definition
    getConstInfo QName
    name
            let t    = Definition -> Type
    defType Definition
    def
            let info = Definition -> ArgInfo
    forall a. LensArgInfo a => a -> ArgInfo
    getArgInfo Definition
    def

            -- If the function is erased, then hard compile-time mode is
            -- entered.
            setHardCompileTimeModeIfErased' info $ do

            case isAlias cs t of  -- #418: Don't use checkAlias for abstract definitions, since the type
                                  -- of an abstract function must not be informed by its definition.
              Just (Expr
    e, Maybe Expr
    mc, MetaId
    x)
                | DefInfo -> IsAbstract
    forall t. DefInfo' t -> IsAbstract
    Info.defAbstract DefInfo
    i IsAbstract -> IsAbstract -> Bool
    forall a. Eq a => a -> a -> Bool
    == IsAbstract
    ConcreteDef, DefInfo -> IsOpaque
    forall t. DefInfo' t -> IsOpaque
    Info.defOpaque DefInfo
    i IsOpaque -> IsOpaque -> Bool
    forall a. Eq a => a -> a -> Bool
    == IsOpaque
    TransparentDef ->
                  Call -> TCM () -> TCM ()
    forall a. Call -> TCMT IO a -> TCMT IO a
    forall (m :: * -> *) a. MonadTrace m => Call -> m a -> m a
    traceCall (Range -> QName -> [Clause' LHS] -> Bool -> Call
    CheckFunDefCall (DefInfo -> Range
    forall a. HasRange a => a -> Range
    getRange DefInfo
    i) QName
    name [Clause' LHS]
    cs Bool
    True) (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ do
                    -- Andreas, 2012-11-22: if the alias is in an abstract block
                    -- it has been frozen.  We unfreeze it to enable type inference.
                    -- See issue 729.
                    -- Ulf, 2021-02-09: also unfreeze metas in the sort of this type
                    TCMT IO Bool -> TCM () -> TCM ()
    forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
    whenM (MetaId -> TCMT IO Bool
    forall (m :: * -> *).
    (HasCallStack, MonadDebug m, ReadTCState m) =>
    MetaId -> m Bool
    isFrozen MetaId
    x) (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ do
                      xs <- Type -> [MetaId]
    forall a. AllMetas a => a -> [MetaId]
    allMetasList (Type -> [MetaId])
    -> (MetaVariable -> Type) -> MetaVariable -> [MetaId]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Judgement MetaId -> Type
    forall a. Judgement a -> Type
    jMetaType (Judgement MetaId -> Type)
    -> (MetaVariable -> Judgement MetaId) -> MetaVariable -> Type
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . MetaVariable -> Judgement MetaId
    mvJudgement (MetaVariable -> [MetaId])
    -> TCMT IO MetaVariable -> TCMT IO [MetaId]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> MetaId -> TCMT IO MetaVariable
    forall (m :: * -> *).
    (HasCallStack, MonadDebug m, ReadTCState m) =>
    MetaId -> m MetaVariable
    lookupLocalMeta MetaId
    x
                      mapM_ unfreezeMeta (x : xs)
                    Type -> ArgInfo -> DefInfo -> QName -> Expr -> Maybe Expr -> TCM ()
    checkAlias Type
    t ArgInfo
    info DefInfo
    i QName
    name Expr
    e Maybe Expr
    mc
                | Bool
    otherwise -> do -- Warn about abstract alias (will never work!)
                  -- Ulf, 2021-11-18, #5620: Don't warn if the meta is solved. A more intuitive solution
                  -- would be to not treat definitions with solved meta types as aliases, but in mutual
                  -- blocks you might actually have solved the type of an alias by the time you get to
                  -- the definition. See test/Succeed/SizeInfinity.agda for an example where this
                  -- happens.
                  TCMT IO Bool -> TCM () -> TCM ()
    forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
    whenM (MetaInstantiation -> Bool
    isOpenMeta (MetaInstantiation -> Bool)
    -> TCMT IO MetaInstantiation -> TCMT IO Bool
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> MetaId -> TCMT IO MetaInstantiation
    forall (m :: * -> *).
    ReadTCState m =>
    MetaId -> m MetaInstantiation
    lookupMetaInstantiation MetaId
    x) (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $
                    DefInfo -> TCM () -> TCM ()
    forall (m :: * -> *) x a.
    (MonadTrace m, HasRange x) =>
    x -> m a -> m a
    setCurrentRange DefInfo
    i (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ Warning -> TCM ()
    forall (m :: * -> *).
    (HasCallStack, MonadWarning m) =>
    Warning -> m ()
    warning (Warning -> TCM ()) -> Warning -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ QName -> IsOpaque -> Warning
    MissingTypeSignatureForOpaque QName
    name (DefInfo -> IsOpaque
    forall t. DefInfo' t -> IsOpaque
    Info.defOpaque DefInfo
    i)
                  Type
    -> ArgInfo
    -> Maybe ExtLamInfo
    -> Maybe QName
    -> DefInfo
    -> QName
    -> [Clause' LHS]
    -> TCM ()
    checkFunDef' Type
    t ArgInfo
    info Maybe ExtLamInfo
    forall a. Maybe a
    Nothing Maybe QName
    forall a. Maybe a
    Nothing DefInfo
    i QName
    name [Clause' LHS]
    cs
              Maybe (Expr, Maybe Expr, MetaId)
    _ -> Type
    -> ArgInfo
    -> Maybe ExtLamInfo
    -> Maybe QName
    -> DefInfo
    -> QName
    -> [Clause' LHS]
    -> TCM ()
    checkFunDef' Type
    t ArgInfo
    info Maybe ExtLamInfo
    forall a. Maybe a
    Nothing Maybe QName
    forall a. Maybe a
    Nothing DefInfo
    i QName
    name [Clause' LHS]
    cs

            -- If it's a macro check that it ends in Term → TC ⊤
            let ismacro = Defn -> Bool
    isMacro (Defn -> Bool) -> (Definition -> Defn) -> Definition -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Definition -> Defn
    theDef (Definition -> Bool) -> Definition -> Bool
    forall a b. (a -> b) -> a -> b
    $ Definition
    def
            when (ismacro || Info.defMacro i == MacroDef) $ checkMacroType t
        TCM () -> ((TCErr, Blocker) -> TCM ()) -> TCM ()
    forall a. TCM a -> ((TCErr, Blocker) -> TCM a) -> TCM a
    `catchIlltypedPatternBlockedOnMeta` \ (TCErr
    err, Blocker
    blocker) -> do
            [Char] -> Int -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "tc.def" Int
    20 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ [TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    vcat ([TCMT IO Doc] -> TCMT IO Doc) -> [TCMT IO Doc] -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $
              [ TCMT IO Doc
    "checking function definition got stuck on: " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Blocker -> TCMT IO Doc
    forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
    pretty Blocker
    blocker ]
            (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
    name ((Definition -> Definition) -> Signature -> Signature)
    -> (Definition -> Definition) -> Signature -> Signature
    forall a b. (a -> b) -> a -> b
    $ (Blocked_ -> Blocked_) -> Definition -> Definition
    updateDefBlocked ((Blocked_ -> Blocked_) -> Definition -> Definition)
    -> (Blocked_ -> Blocked_) -> Definition -> Definition
    forall a b. (a -> b) -> a -> b
    $ Blocked_ -> Blocked_ -> Blocked_
    forall a b. a -> b -> a
    const (Blocked_ -> Blocked_ -> Blocked_)
    -> Blocked_ -> Blocked_ -> Blocked_
    forall a b. (a -> b) -> a -> b
    $ Blocker -> () -> Blocked_
    forall t a. Blocker -> a -> Blocked' t a
    Blocked Blocker
    blocker ()
            Blocker -> Constraint -> TCM ()
    forall (m :: * -> *).
    MonadConstraint m =>
    Blocker -> Constraint -> m ()
    addConstraint Blocker
    blocker (Constraint -> TCM ()) -> Constraint -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ DefInfo -> QName -> [Clause' LHS] -> TCErr -> Constraint
    CheckFunDef DefInfo
    i QName
    name [Clause' LHS]
    cs TCErr
    err

    checkMacroType :: Type -> TCM ()
    checkMacroType :: Type -> TCM ()
    checkMacroType Type
    t = do
      TelV tel tr <- Type -> TCMT IO (TelV Type)
    forall (m :: * -> *).
    (MonadReduce m, MonadAddContext m) =>
    Type -> m (TelV Type)
    telView Type
    t

      let telList = Tele (Dom Type) -> [Dom ([Char], Type)]
    forall t. Tele (Dom t) -> [Dom ([Char], t)]
    telToList Tele (Dom Type)
    tel
          resType = Tele (Dom Type) -> Type -> Type
    forall t. Abstract t => Tele (Dom Type) -> t -> t
    abstract ([Dom ([Char], Type)] -> Tele (Dom Type)
    telFromList (Int -> [Dom ([Char], Type)] -> [Dom ([Char], Type)]
    forall a. Int -> [a] -> [a]
    drop ([Dom ([Char], Type)] -> Int
    forall a. [a] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length [Dom ([Char], Type)]
    telList Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - Int
    1) [Dom ([Char], Type)]
    telList)) Type
    tr
      expectedType <- el primAgdaTerm --> el (primAgdaTCM <#> primLevelZero <@> primUnit)
      equalType resType expectedType
        `catchError` \ TCErr
    _ -> TypeError -> TCM ()
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    TypeError -> m a
    typeError (TypeError -> TCM ()) -> TypeError -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ Type -> TypeError
    MacroResultTypeMismatch Type
    expectedType

    -- | A single clause without arguments and without type signature is an alias.
    isAlias :: [A.Clause] -> Type -> Maybe (A.Expr, Maybe C.Expr, MetaId)
    isAlias :: [Clause' LHS] -> Type -> Maybe (Expr, Maybe Expr, MetaId)
    isAlias [Clause' LHS]
    cs Type
    t =
            case [Clause' LHS] -> Maybe (Expr, Maybe Expr)
    trivialClause [Clause' LHS]
    cs of
              -- if we have just one clause without pattern matching and
              -- without a type signature, then infer, to allow
              -- "aliases" for things starting with hidden abstractions
              Just (Expr
    e, Maybe Expr
    mc) | Just MetaId
    x <- Term -> Maybe MetaId
    isMeta (Type -> Term
    forall t a. Type'' t a -> a
    unEl Type
    t) -> (Expr, Maybe Expr, MetaId) -> Maybe (Expr, Maybe Expr, MetaId)
    forall a. a -> Maybe a
    Just (Expr
    e, Maybe Expr
    mc, MetaId
    x)
              Maybe (Expr, Maybe Expr)
    _ -> Maybe (Expr, Maybe Expr, MetaId)
    forall a. Maybe a
    Nothing
      where
        isMeta :: Term -> Maybe MetaId
    isMeta (MetaV MetaId
    x Elims
    _) = MetaId -> Maybe MetaId
    forall a. a -> Maybe a
    Just MetaId
    x
        isMeta Term
    _           = Maybe MetaId
    forall a. Maybe a
    Nothing
        trivialClause :: [Clause' LHS] -> Maybe (Expr, Maybe Expr)
    trivialClause [A.Clause (A.LHS LHSInfo
    i (A.LHSHead QName
    f [])) [ProblemEq]
    _ (A.RHS Expr
    e Maybe Expr
    mc) WhereDeclarations
    wh Catchall
    _]
          | WhereDeclarations -> Bool
    forall a. Null a => a -> Bool
    null WhereDeclarations
    wh     = (Expr, Maybe Expr) -> Maybe (Expr, Maybe Expr)
    forall a. a -> Maybe a
    Just (Expr
    e, Maybe Expr
    mc)
        trivialClause [Clause' LHS]
    _ = Maybe (Expr, Maybe Expr)
    forall a. Maybe a
    Nothing

    -- | Check a trivial definition of the form @f = e@
    checkAlias :: Type -> ArgInfo -> A.DefInfo -> QName -> A.Expr -> Maybe C.Expr -> TCM ()
    checkAlias :: Type -> ArgInfo -> DefInfo -> QName -> Expr -> Maybe Expr -> TCM ()
    checkAlias Type
    t ArgInfo
    ai DefInfo
    i QName
    name Expr
    e Maybe Expr
    mc =
      let clause :: SpineClause
    clause = A.Clause { clauseLHS :: SpineLHS
    clauseLHS          = LHSInfo -> QName -> [NamedArg (Pattern' Expr)] -> SpineLHS
    A.SpineLHS (Range -> ExpandedEllipsis -> LHSInfo
    LHSInfo (DefInfo -> Range
    forall a. HasRange a => a -> Range
    getRange DefInfo
    i) ExpandedEllipsis
    NoEllipsis) QName
    name []
                            , clauseStrippedPats :: [ProblemEq]
    clauseStrippedPats = []
                            , clauseRHS :: RHS
    clauseRHS          = Expr -> Maybe Expr -> RHS
    A.RHS Expr
    e Maybe Expr
    mc
                            , clauseWhereDecls :: WhereDeclarations
    clauseWhereDecls   = WhereDeclarations
    A.noWhereDecls
                            , clauseCatchall :: Catchall
    clauseCatchall     = Catchall
    forall a. Null a => a
    empty } in
      QName
    -> Int
    -> Type
    -> Maybe Substitution
    -> SpineClause
    -> TCM ()
    -> TCM ()
    forall a.
    QName
    -> Int
    -> Type
    -> Maybe Substitution
    -> SpineClause
    -> TCM a
    -> TCM a
    atClause QName
    name Int
    0 Type
    t Maybe Substitution
    forall a. Maybe a
    Nothing SpineClause
    clause (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ do
      [Char] -> Int -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "tc.def.alias" Int
    10 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Doc
    "checkAlias" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> [TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    vcat
        [ [Char] -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => [Char] -> m Doc
    text (QName -> [Char]
    forall a. Pretty a => a -> [Char]
    prettyShow QName
    name) TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc
    colon  TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Type -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => Type -> m Doc
    prettyTCM Type
    t
        , [Char] -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => [Char] -> m Doc
    text (QName -> [Char]
    forall a. Pretty a => a -> [Char]
    prettyShow QName
    name) TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc
    equals TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Expr -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => Expr -> m Doc
    prettyTCM Expr
    e
        ]

      -- Infer the type of the rhs.
      -- Andreas, 2018-06-09, issue #2170.
      -- The context will only be resurrected if we have --irrelevant-projections.
      v <- ArgInfo -> TCMT IO Term -> TCMT IO Term
    forall (tcm :: * -> *) r a.
    (MonadTCM tcm, LensModality r) =>
    r -> tcm a -> tcm a
    applyModalityToContextFunBody ArgInfo
    ai (TCMT IO Term -> TCMT IO Term) -> TCMT IO Term -> TCMT IO Term
    forall a b. (a -> b) -> a -> b
    $ Comparison -> Expr -> Type -> TCMT IO Term
    checkDontExpandLast Comparison
    CmpLeq Expr
    e Type
    t

      reportSDoc "tc.def.alias" 20 $ "checkAlias: finished checking"

      solveSizeConstraints DontDefaultToInfty

      v <- instantiateFull v  -- if we omit this, we loop (stdlib: Relation.Binary.Sum)
        -- or the termination checker might stumble over levels in sorts
        -- that cannot be converted to expressions without the level built-ins
        -- (test/succeed/Issue655.agda)

      -- compute body modification for irrelevant definitions, see issue 610
      let bodyMod = Bool -> (Term -> Term) -> Term -> Term
    forall b a. IsBool b => b -> (a -> a) -> a -> a
    applyWhen (ArgInfo -> Bool
    forall a. LensRelevance a => a -> Bool
    isIrrelevant ArgInfo
    ai) Term -> Term
    dontCare

      -- Add the definition
      fun <- emptyFunctionData
      addConstant' name ai t $ FunctionDefn $
        set funMacro_ (Info.defMacro i == MacroDef) $
        set funAbstr_ (Info.defAbstract i) $
          fun { _funClauses   = [ Clause  -- trivial clause @name = v@
                  { clauseLHSRange    = getRange i
                  , clauseFullRange   = getRange i
                  , clauseTel         = EmptyTel
                  , namedClausePats   = []
                  , clauseBody        = Just $ bodyMod v
                  , clauseType        = Just $ Arg ai t
                  , clauseCatchall    = empty
                  , clauseRecursive   = Nothing   -- we don't know yet
                  , clauseUnreachable = Just False
                  , clauseEllipsis    = NoEllipsis
                  , clauseWhereModule = Nothing
                  } ]
              , _funCompiled  = Just $ Done [] $ bodyMod v
              , _funSplitTree = Just $ SplittingDone 0
              , _funOpaque    = Info.defOpaque i
              }

      -- Andreas, 2017-01-01, issue #2372:
      -- Add the definition to the instance table, if needed, to update its type.
      case Info.defInstance i of
        InstanceDef KwRange
    _r -> QName -> TCM () -> TCM ()
    forall (m :: * -> *) x a.
    (MonadTrace m, HasRange x) =>
    x -> m a -> m a
    setCurrentRange QName
    name (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ QName -> Type -> TCM ()
    readdTypedInstance QName
    name Type
    t
          -- Put highlighting on the name only;
          -- @(getRange (r, name))@ does not give good results.
        IsInstance
    NotInstanceDef -> () -> TCM ()
    forall a. a -> TCMT IO a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure ()

      reportSDoc "tc.def.alias" 20 $ "checkAlias: leaving"

    -- | Type check a definition by pattern matching.
    checkFunDef' :: Type             -- ^ the type we expect the function to have
                 -> ArgInfo          -- ^ is it irrelevant (for instance)
                 -> Maybe ExtLamInfo -- ^ does the definition come from an extended lambda
                                     --   (if so, we need to know some stuff about lambda-lifted args)
                 -> Maybe QName      -- ^ is it a with function (if so, what's the name of the parent function)
                 -> A.DefInfo        -- ^ range info
                 -> QName            -- ^ the name of the function
                 -> [A.Clause]       -- ^ the clauses to check
                 -> TCM ()
    checkFunDef' :: Type
    -> ArgInfo
    -> Maybe ExtLamInfo
    -> Maybe QName
    -> DefInfo
    -> QName
    -> [Clause' LHS]
    -> TCM ()
    checkFunDef' Type
    t ArgInfo
    ai Maybe ExtLamInfo
    extlam Maybe QName
    with DefInfo
    i QName
    name [Clause' LHS]
    cs =
      Type
    -> ArgInfo
    -> Maybe ExtLamInfo
    -> Maybe QName
    -> DefInfo
    -> QName
    -> Maybe (Substitution, Map Name LetBinding)
    -> [Clause' LHS]
    -> TCM ()
    checkFunDefS Type
    t ArgInfo
    ai Maybe ExtLamInfo
    extlam Maybe QName
    with DefInfo
    i QName
    name Maybe (Substitution, Map Name LetBinding)
    forall a. Maybe a
    Nothing [Clause' LHS]
    cs

    -- | Type check a definition by pattern matching.
    checkFunDefS :: Type             -- ^ the type we expect the function to have
                 -> ArgInfo          -- ^ is it irrelevant (for instance)
                 -> Maybe ExtLamInfo -- ^ does the definition come from an extended lambda
                                     --   (if so, we need to know some stuff about lambda-lifted args)
                 -> Maybe QName      -- ^ is it a with function (if so, what's the name of the parent function)
                 -> A.DefInfo        -- ^ range info
                 -> QName            -- ^ the name of the function
                 -> Maybe (Substitution, Map Name LetBinding)
                                     -- ^ substitution (from with abstraction) that needs to be applied
                                     --   to module parameters, and let-bindings inherited from parent
                                     --   clause
                 -> [A.Clause]       -- ^ the clauses to check
                 -> TCM ()
    checkFunDefS :: Type
    -> ArgInfo
    -> Maybe ExtLamInfo
    -> Maybe QName
    -> DefInfo
    -> QName
    -> Maybe (Substitution, Map Name LetBinding)
    -> [Clause' LHS]
    -> TCM ()
    checkFunDefS Type
    t ArgInfo
    ai Maybe ExtLamInfo
    extlam Maybe QName
    with DefInfo
    i QName
    name Maybe (Substitution, Map Name LetBinding)
    withSubAndLets [Clause' LHS]
    cs = do

        Call -> TCM () -> TCM ()
    forall a. Call -> TCMT IO a -> TCMT IO a
    forall (m :: * -> *) a. MonadTrace m => Call -> m a -> m a
    traceCall (Range -> QName -> [Clause' LHS] -> Bool -> Call
    CheckFunDefCall (DefInfo -> Range
    forall a. HasRange a => a -> Range
    getRange DefInfo
    i) QName
    name [Clause' LHS]
    cs Bool
    True) (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ do
            [Char] -> Int -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "tc.def.fun" Int
    10 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    forall a b. (a -> b) -> a -> b
    $
              [TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    sep [ TCMT IO Doc
    "checking body 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 a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => QName -> m Doc
    prettyTCM QName
    name
                  , Int -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
    nest Int
    2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Doc
    ":" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Type -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => Type -> m Doc
    prettyTCM Type
    t
                  , Int -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
    nest Int
    2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Doc
    "full 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 a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => Type -> m Doc
    prettyTCM (Type -> TCMT IO Doc)
    -> (Definition -> Type) -> Definition -> TCMT IO Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Definition -> Type
    defType (Definition -> TCMT IO Doc) -> TCMT IO Definition -> TCMT IO Doc
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< QName -> TCMT IO Definition
    forall (m :: * -> *). HasConstInfo m => QName -> m Definition
    getConstInfo QName
    name)
                  ]

            [Char] -> Int -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "tc.def.fun" Int
    70 (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] -> TCMT IO Doc) -> [TCMT IO Doc] -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Doc
    "clauses:" TCMT IO Doc -> [TCMT IO Doc] -> [TCMT IO Doc]
    forall a. a -> [a] -> [a]
    : (Clause' LHS -> TCMT IO Doc) -> [Clause' LHS] -> [TCMT IO Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map (Int -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
    nest Int
    2 (TCMT IO Doc -> TCMT IO Doc)
    -> (Clause' LHS -> TCMT IO Doc) -> Clause' LHS -> TCMT IO Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [Char] -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => [Char] -> m Doc
    text ([Char] -> TCMT IO Doc)
    -> (Clause' LHS -> [Char]) -> Clause' LHS -> TCMT IO Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Clause' LHS -> [Char]
    forall a. Show a => a -> [Char]
    show (Clause' LHS -> [Char])
    -> (Clause' LHS -> Clause' LHS) -> Clause' LHS -> [Char]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Clause' LHS -> Clause' LHS
    forall a. ExprLike a => a -> a
    A.deepUnscope) [Clause' LHS]
    cs

            cs <- [SpineClause] -> TCMT IO [SpineClause]
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([SpineClause] -> TCMT IO [SpineClause])
    -> [SpineClause] -> TCMT IO [SpineClause]
    forall a b. (a -> b) -> a -> b
    $ (Clause' LHS -> SpineClause) -> [Clause' LHS] -> [SpineClause]
    forall a b. (a -> b) -> [a] -> [b]
    map Clause' LHS -> SpineClause
    forall a b. LHSToSpine a b => a -> b
    A.lhsToSpine [Clause' LHS]
    cs

            reportSDoc "tc.def.fun" 70 $
              sep $ "spine clauses:" : map (nest 2 . text . show . A.deepUnscope) cs

            -- Ensure that all clauses have the same number of trailing hidden patterns
            -- This is necessary since trailing implicits are no longer eagerly inserted.
            -- Andreas, 2013-10-13
            -- Since we have flexible function arity, it is no longer necessary
            -- to patch clauses to same arity
            -- cs <- trailingImplicits t cs

            -- Check the clauses
            cs <- traceCall NoHighlighting $ do -- To avoid flicker.
              forM (zip cs [0..]) $ \ (SpineClause
    c, Int
    clauseNo) -> do
                QName
    -> Int
    -> Type
    -> Maybe Substitution
    -> SpineClause
    -> TCMT IO (Clause, ClausesPostChecks)
    -> TCMT IO (Clause, ClausesPostChecks)
    forall a.
    QName
    -> Int
    -> Type
    -> Maybe Substitution
    -> SpineClause
    -> TCM a
    -> TCM a
    atClause QName
    name Int
    clauseNo Type
    t ((Substitution, Map Name LetBinding) -> Substitution
    forall a b. (a, b) -> a
    fst ((Substitution, Map Name LetBinding) -> Substitution)
    -> Maybe (Substitution, Map Name LetBinding) -> Maybe Substitution
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Maybe (Substitution, Map Name LetBinding)
    withSubAndLets) SpineClause
    c (TCMT IO (Clause, ClausesPostChecks)
     -> TCMT IO (Clause, ClausesPostChecks))
    -> TCMT IO (Clause, ClausesPostChecks)
    -> TCMT IO (Clause, ClausesPostChecks)
    forall a b. (a -> b) -> a -> b
    $ do
                  (c,b) <- ArgInfo
    -> TCMT IO (Clause, ClausesPostChecks)
    -> TCMT IO (Clause, ClausesPostChecks)
    forall (tcm :: * -> *) r a.
    (MonadTCM tcm, LensModality r) =>
    r -> tcm a -> tcm a
    applyModalityToContextFunBody ArgInfo
    ai (TCMT IO (Clause, ClausesPostChecks)
     -> TCMT IO (Clause, ClausesPostChecks))
    -> TCMT IO (Clause, ClausesPostChecks)
    -> TCMT IO (Clause, ClausesPostChecks)
    forall a b. (a -> b) -> a -> b
    $ do
                    Type
    -> Maybe (Substitution, Map Name LetBinding)
    -> SpineClause
    -> TCMT IO (Clause, ClausesPostChecks)
    checkClause Type
    t Maybe (Substitution, Map Name LetBinding)
    withSubAndLets SpineClause
    c
                  -- Andreas, 2013-11-23 do not solve size constraints here yet
                  -- in case we are checking the body of an extended lambda.
                  -- 2014-04-24: The size solver requires each clause to be
                  -- checked individually, since otherwise we get constraints
                  -- in typing contexts which are not prefixes of each other.
                  whenNothing extlam $ solveSizeConstraints DontDefaultToInfty
                  -- Andreas, 2013-10-27 add clause as soon it is type-checked
                  -- TODO: instantiateFull?
                  inTopContext $ addClauses name [c]
                  return (c,b)

            (cs, CPC isOneIxs) <- return $ (second mconcat . unzip) cs

            -- If there is a partial match ("system"), no proper (co)pattern matching is allowed.
            let isSystem = Bool -> Bool
    not (Bool -> Bool) -> (IntSet -> Bool) -> IntSet -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . IntSet -> Bool
    forall a. Null a => a -> Bool
    null (IntSet -> Bool) -> IntSet -> Bool
    forall a b. (a -> b) -> a -> b
    $ IntSet
    isOneIxs
            when isSystem do
              -- allow VarP and ConP i0/i1 fallThrough = yes, DotP
              let pss = (Clause -> [NamedArg DeBruijnPattern])
    -> [Clause] -> [[NamedArg DeBruijnPattern]]
    forall a b. (a -> b) -> [a] -> [b]
    map Clause -> [NamedArg DeBruijnPattern]
    namedClausePats [Clause]
    cs
                  allowed = \case
                    VarP{} -> Bool
    True
                    -- pattern inserted by splitPartial
                    ConP ConHead
    _ ConPatternInfo
    cpi [] | ConPatternInfo -> Bool
    conPFallThrough ConPatternInfo
    cpi -> Bool
    True
                    DotP{} -> Bool
    True
                    Pattern' x
    _      -> Bool
    False
              unless (all (all $ allowed . namedArg) pss) $
                typeError PatternInSystem

            reportSDoc "tc.def.fun" 70 $ inTopContext $ do
              sep $ "checked clauses:" : map (nest 2 . text . show) cs

            reportSDoc "tc.cc" 25 $ inTopContext $ do
              sep [ "clauses before injectivity test"
                  , nest 2 $ prettyTCM $ map (QNamed name) cs  -- broken, reify (QNamed n cl) expect cl to live at top level
                  ]
            reportSDoc "tc.cc" 60 $ inTopContext $ do
              sep [ "raw clauses: "
                  , nest 2 $ sep $ map (text . show . QNamed name) cs
                  ]

            -- Needed to calculate the proper fullType below.
            applyWhenM (optPolarity <$> pragmaOptions) (applyPolarityToContext ai) $
              applyCohesionToContext ai $ do

            -- Systems have their own coverage and "coherence" check, we
            -- also add an absurd clause for the cases not needed.
            (cs,sys) <- if not isSystem then return (cs, empty) else do
                     fullType <- flip abstract t <$> getContextTelescope
                     sys <- inTopContext $ checkSystemCoverage name (IntSet.toList isOneIxs) fullType cs
                     tel <- getContextTelescope
                     let c = Clause
                           { clauseFullRange :: Range
    clauseFullRange = Range
    forall a. Range' a
    noRange
                           , clauseLHSRange :: Range
    clauseLHSRange  = Range
    forall a. Range' a
    noRange
                           , clauseTel :: Tele (Dom Type)
    clauseTel       = Tele (Dom Type)
    tel
                           , namedClausePats :: [NamedArg DeBruijnPattern]
    namedClausePats = Tele (Dom Type) -> [NamedArg DeBruijnPattern]
    forall a t. DeBruijn a => Tele (Dom t) -> [NamedArg a]
    teleNamedArgs Tele (Dom Type)
    tel
                           , clauseBody :: Maybe Term
    clauseBody      = Maybe Term
    forall a. Maybe a
    Nothing
                           , clauseType :: Maybe (Arg Type)
    clauseType      = Arg Type -> Maybe (Arg Type)
    forall a. a -> Maybe a
    Just (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
                           , clauseUnreachable :: Maybe Bool
    clauseUnreachable = Bool -> Maybe Bool
    forall a. a -> Maybe a
    Just Bool
    False
                           , clauseEllipsis :: ExpandedEllipsis
    clauseEllipsis    = ExpandedEllipsis
    NoEllipsis
                           , clauseWhereModule :: Maybe ModuleName
    clauseWhereModule = Maybe ModuleName
    forall a. Maybe a
    Nothing
                           }
                     return (cs ++ [c], pure sys)

            -- The macro or inline tags might be on the type signature
            info <- getConstInfo name
            let
              ismacro  = Defn -> Bool
    isMacro (Definition -> Defn
    theDef Definition
    info)
              isinline = Defn -> Bool
    isInlineFun (Definition -> Defn
    theDef Definition
    info)

            -- Annotate the clauses with which arguments are actually used.
            cs <- instantiateFull {- =<< mapM rebindClause -} cs

            -- Andreas, 2010-11-12
            -- rebindClause is the identity, and instantiateFull eta-contracts
            -- removing this eta-contraction fixes issue 361
            -- however, Data.Star.Decoration.gmapAll no longer type-checks
            -- possibly due to missing eta-contraction!?

            -- Inline copattern record constructors on demand, unless the
            -- function is marked inline.
            cs <- if isinline then pure cs else concat <$> do
              forM cs $ \ Clause
    cl -> do
                (cls, nonExactSplit) <- ChangeT (TCMT IO) [Clause] -> TCMT IO ([Clause], Bool)
    forall (m :: * -> *) a. Functor m => ChangeT m a -> m (a, Bool)
    runChangeT (ChangeT (TCMT IO) [Clause] -> TCMT IO ([Clause], Bool))
    -> ChangeT (TCMT IO) [Clause] -> TCMT IO ([Clause], Bool)
    forall a b. (a -> b) -> a -> b
    $ Clause -> ChangeT (TCMT IO) [Clause]
    forall (m :: * -> *).
    (MonadChange m, PureTCM m) =>
    Clause -> m [Clause]
    recordRHSToCopatterns Clause
    cl
                when nonExactSplit do
                  -- If we inlined a non-eta constructor,
                  -- issue a warning that the clause does not hold as definitional equality.
                  warning $ InlineNoExactSplit name cl
                return cls

            -- After checking, remove the clauses again.
            -- (Otherwise, @checkInjectivity@ loops for issue 801).
            --
            -- Amy, 2025-04-03: We can't remove the clauses before doing
            -- record→copattern translation, since we might need the
            -- previous clauses to come up with the types of the projected
            -- fields; see 'test/Succeed/IApplyRecConstrInline'.
            modifyFunClauses name (const [])

            -- Check if the function is injective.
            -- Andreas, 2015-07-01 we do it here in order to resolve metas
            -- in mutual definitions, e.g. the U/El definition in succeed/Issue439.agda
            -- We do it again for the mutual block after termination checking, see Rules.Decl.
            reportSLn "tc.inj.def" 20 $ "checkFunDef': checking injectivity..."
            inv <- Bench.billTo [Bench.Injectivity] $
              checkInjectivity name cs

            reportSDoc "tc.cc" 15 $ inTopContext $ do
              sep [ "clauses before compilation"
                  , nest 2 $ sep $ map (prettyTCM . QNamed name) cs
                  ]

            reportSDoc "tc.cc.raw" 65 $ do
              sep [ "clauses before compilation"
                  , nest 2 $ sep $ map (text . show) cs
                  ]

            -- add clauses for the coverage (& confluence) checker (needs to reduce)
            inTopContext $ addClauses name cs

            reportSDoc "tc.cc.type" 60 $ "  type   : " <+> (text . prettyShow) t
            reportSDoc "tc.cc.type" 60 $ "  context: " <+> (text . prettyShow =<< getContextTelescope)

            fullType <- flip telePi t <$> getContextTelescope

            reportSLn  "tc.cc.type" 80 $ show fullType

            -- Coverage check and compile the clauses
            (mst, _recordExpressionBecameCopatternLHS, cc) <- Bench.billTo [Bench.Coverage] $
              unsafeInTopContext $ compileClauses (if isSystem then Nothing else (Just (name, fullType)))
                                            cs
            -- Andreas, 2019-10-21 (see also issue #4142):
            -- We ignore whether the clause compilation turned some
            -- record expressions into copatterns
            -- (_recordExpressionsBecameCopatternLHS),
            -- since the defCopatternLHS flag is anyway set by traversing
            -- the compiled clauses looking for a copattern match
            -- (hasProjectionPatterns).

            -- Clause compilation runs the coverage checker, which might add
            -- some extra clauses.
            cs <- defClauses <$> getConstInfo name

            reportSDoc "tc.cc" 60 $ inTopContext $ do
              sep [ "compiled clauses of" <+> prettyTCM name
                  , nest 2 $ pretty cc
                  ]

            covering <- funCovering . theDef <$> getConstInfo name

            -- Add the definition
            inTopContext $ addConstant name =<< do

              reportSDoc "tc.def.fun.clauses" 15 $ inTopContext $ do
                vcat [ "final clauses for" <+> prettyTCM name <+>  ":"
                     , nest 2 $ vcat $ map (prettyTCM . QNamed name) cs
                     ]

              -- If there was a pragma for this definition, we can set the
              -- funTerminates field directly.
              --
              -- Amy, 2025-04-03: If the function was marked INLINE before
              -- the clauses were checked the result should also be INLINE.
              fun  <- emptyFunctionData
              defn <- autoInline $ set funInline isinline $ FunctionDefn $
               set funMacro_ (ismacro || Info.defMacro i == MacroDef) $
               set funAbstr_ (Info.defAbstract i) $
               fun
                 { _funClauses        = cs
                 , _funCompiled       = Just cc
                 , _funSplitTree      = mst
                 , _funInv            = inv
                 , _funOpaque         = Info.defOpaque i
                 , _funExtLam         = (\ ExtLamInfo
    e -> ExtLamInfo
    e { extLamSys = sys }) <$> extlam
                 , _funWith           = with
                 , _funCovering       = covering
                 }
              lang <- getLanguage
              useTerPragma $
                updateDefCopatternLHS (const $ hasProjectionPatterns cc) $
                (defaultDefn ai name fullType lang defn)

            reportSDoc "tc.def.fun" 10 $ do
              sep [ "added " <+> prettyTCM name <+> ":"
                  , nest 2 $ prettyTCM . defType =<< getConstInfo name
                  ]

            -- Jesper, 2019-05-30: if the constructors used in the
            -- lhs of a clause have rewrite rules, we need to check
            -- confluence here
            whenJustM (optConfluenceCheck <$> pragmaOptions) $ \ConfluenceCheck
    confChk -> TCM () -> TCM ()
    forall (tcm :: * -> *) a.
    (MonadTCEnv tcm, ReadTCState tcm) =>
    tcm a -> tcm a
    inTopContext (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $
              ConfluenceCheck -> QName -> TCM ()
    checkConfluenceOfClauses ConfluenceCheck
    confChk QName
    name

    -- | Set 'funTerminates' according to termination info in 'TCEnv',
    --   which comes from a possible termination pragma.
    useTerPragma :: Definition -> TCM Definition
    useTerPragma :: Definition -> TCMT IO Definition
    useTerPragma def :: Definition
    def@Defn{ defName :: Definition -> QName
    defName = QName
    name, theDef :: Definition -> Defn
    theDef = fun :: Defn
    fun@Function{}} = do
      tc <- Lens' TCEnv (TerminationCheck ()) -> TCMT IO (TerminationCheck ())
    forall (m :: * -> *) a. MonadTCEnv m => Lens' TCEnv a -> m a
    viewTC (TerminationCheck () -> f (TerminationCheck ()))
    -> TCEnv -> f TCEnv
    Lens' TCEnv (TerminationCheck ())
    eTerminationCheck
      let terminates = case TerminationCheck ()
    tc of
            TerminationCheck ()
    NonTerminating -> Bool -> Maybe Bool
    forall a. a -> Maybe a
    Just Bool
    False
            TerminationCheck ()
    Terminating    -> Bool -> Maybe Bool
    forall a. a -> Maybe a
    Just Bool
    True
            TerminationCheck ()
    _              -> Maybe Bool
    forall a. Maybe a
    Nothing
      reportS "tc.fundef" 30 $
        [ "funTerminates of " ++ prettyShow name ++ " set to " ++ show terminates
        , "  tc = " ++ show tc
        ]
      return $ def { theDef = fun { funTerminates = terminates }}
    useTerPragma Definition
    def = Definition -> TCMT IO Definition
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Definition
    def

    -- | Modify all the LHSCore of the given RHS.
    -- (Used to insert patterns for @rewrite@ or the inspect idiom)
    mapLHSCores :: (A.LHSCore -> A.LHSCore) -> (A.RHS -> A.RHS)
    mapLHSCores :: (LHSCore' Expr -> LHSCore' Expr) -> RHS -> RHS
    mapLHSCores LHSCore' Expr -> LHSCore' Expr
    f = \case
      A.WithRHS QName
    aux List1 WithExpr
    es List1 (Clause' LHS)
    cs -> QName -> List1 WithExpr -> List1 (Clause' LHS) -> RHS
    A.WithRHS QName
    aux List1 WithExpr
    es (List1 (Clause' LHS) -> RHS) -> List1 (Clause' LHS) -> RHS
    forall a b. (a -> b) -> a -> b
    $ List1 (Clause' LHS)
    -> (Clause' LHS -> Clause' LHS) -> List1 (Clause' LHS)
    forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
    for List1 (Clause' LHS)
    cs ((Clause' LHS -> Clause' LHS) -> List1 (Clause' LHS))
    -> (Clause' LHS -> Clause' LHS) -> List1 (Clause' LHS)
    forall a b. (a -> b) -> a -> b
    $
        \ (A.Clause (A.LHS LHSInfo
    info LHSCore' Expr
    core)     [ProblemEq]
    spats RHS
    rhs                 WhereDeclarations
    ds Catchall
    catchall) ->
           LHS
    -> [ProblemEq]
    -> RHS
    -> WhereDeclarations
    -> Catchall
    -> Clause' LHS
    forall lhs.
    lhs
    -> [ProblemEq]
    -> RHS
    -> WhereDeclarations
    -> Catchall
    -> Clause' lhs
    A.Clause (LHSInfo -> LHSCore' Expr -> LHS
    A.LHS LHSInfo
    info (LHSCore' Expr -> LHSCore' Expr
    f LHSCore' Expr
    core)) [ProblemEq]
    spats ((LHSCore' Expr -> LHSCore' Expr) -> RHS -> RHS
    mapLHSCores LHSCore' Expr -> LHSCore' Expr
    f RHS
    rhs) WhereDeclarations
    ds Catchall
    catchall
      A.RewriteRHS [RewriteEqn]
    qes [ProblemEq]
    spats RHS
    rhs WhereDeclarations
    wh -> [RewriteEqn] -> [ProblemEq] -> RHS -> WhereDeclarations -> RHS
    A.RewriteRHS [RewriteEqn]
    qes [ProblemEq]
    spats ((LHSCore' Expr -> LHSCore' Expr) -> RHS -> RHS
    mapLHSCores LHSCore' Expr -> LHSCore' Expr
    f RHS
    rhs) WhereDeclarations
    wh
      rhs :: RHS
    rhs@RHS
    A.AbsurdRHS -> RHS
    rhs
      rhs :: RHS
    rhs@A.RHS{}     -> RHS
    rhs

    -- | Insert some names into the with-clauses LHS of the given RHS.
    -- (Used for the inspect idiom)
    insertNames :: List1 (Arg (Maybe A.BindName)) -> A.RHS -> A.RHS
    insertNames :: List1 (Arg (Maybe BindName)) -> RHS -> RHS
    insertNames = (LHSCore' Expr -> LHSCore' Expr) -> RHS -> RHS
    mapLHSCores ((LHSCore' Expr -> LHSCore' Expr) -> RHS -> RHS)
    -> (List1 (Arg (Maybe BindName)) -> LHSCore' Expr -> LHSCore' Expr)
    -> List1 (Arg (Maybe BindName))
    -> RHS
    -> RHS
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . List1 (Arg (Maybe BindName)) -> LHSCore' Expr -> LHSCore' Expr
    insertInspects

    insertInspects :: List1 (Arg (Maybe A.BindName)) -> A.LHSCore -> A.LHSCore
    insertInspects :: List1 (Arg (Maybe BindName)) -> LHSCore' Expr -> LHSCore' Expr
    insertInspects List1 (Arg (Maybe BindName))
    ps = \case
      A.LHSWith LHSCore' Expr
    core List1 (Arg (Pattern' Expr))
    wps [] ->
        let ps' :: NonEmpty (Arg (Maybe (Arg (Pattern' Expr))))
    ps' = (Arg (Maybe BindName) -> Arg (Maybe (Arg (Pattern' Expr))))
    -> List1 (Arg (Maybe BindName))
    -> NonEmpty (Arg (Maybe (Arg (Pattern' Expr))))
    forall a b. (a -> b) -> NonEmpty a -> NonEmpty b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap ((Maybe BindName -> Maybe (Arg (Pattern' Expr)))
    -> Arg (Maybe BindName) -> Arg (Maybe (Arg (Pattern' Expr)))
    forall a b. (a -> b) -> Arg a -> Arg b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap ((Maybe BindName -> Maybe (Arg (Pattern' Expr)))
     -> Arg (Maybe BindName) -> Arg (Maybe (Arg (Pattern' Expr))))
    -> (Maybe BindName -> Maybe (Arg (Pattern' Expr)))
    -> Arg (Maybe BindName)
    -> Arg (Maybe (Arg (Pattern' Expr)))
    forall a b. (a -> b) -> a -> b
    $ (BindName -> Arg (Pattern' Expr))
    -> Maybe BindName -> Maybe (Arg (Pattern' Expr))
    forall a b. (a -> b) -> Maybe a -> Maybe b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap BindName -> Arg (Pattern' Expr)
    patOfName) List1 (Arg (Maybe BindName))
    ps in
        LHSCore' Expr
    -> List1 (Arg (Pattern' Expr))
    -> [NamedArg (Pattern' Expr)]
    -> LHSCore' Expr
    forall e.
    LHSCore' e
    -> List1 (Arg (Pattern' e))
    -> [NamedArg (Pattern' e)]
    -> LHSCore' e
    A.LHSWith LHSCore' Expr
    core (List1 (Arg (Pattern' Expr))
    -> [Arg (Pattern' Expr)] -> List1 (Arg (Pattern' Expr))
    forall a. List1 a -> [a] -> List1 a
    List1.fromListSafe List1 (Arg (Pattern' Expr))
    forall a. HasCallStack => a
    __IMPOSSIBLE__ ([Arg (Pattern' Expr)] -> List1 (Arg (Pattern' Expr)))
    -> [Arg (Pattern' Expr)] -> List1 (Arg (Pattern' Expr))
    forall a b. (a -> b) -> a -> b
    $ [Arg (Maybe (Arg (Pattern' Expr)))]
    -> [Arg (Pattern' Expr)] -> [Arg (Pattern' Expr)]
    forall a. [Arg (Maybe (Arg a))] -> [Arg a] -> [Arg a]
    insertIn (NonEmpty (Arg (Maybe (Arg (Pattern' Expr))))
    -> [Item (NonEmpty (Arg (Maybe (Arg (Pattern' Expr)))))]
    forall l. IsList l => l -> [Item l]
    List1.toList NonEmpty (Arg (Maybe (Arg (Pattern' Expr))))
    ps') (List1 (Arg (Pattern' Expr)) -> [Item (List1 (Arg (Pattern' Expr)))]
    forall l. IsList l => l -> [Item l]
    List1.toList List1 (Arg (Pattern' Expr))
    wps)) []
      -- Andreas, AIM XXXV, 2022-05-09, issue #5728:
      -- Cases other than LHSWith actually do not make sense, but let them
      -- through to get a proper error later.
      LHSCore' Expr
    lhs -> LHSCore' Expr
    lhs

      where

        patOfName :: A.BindName -> Arg A.Pattern
        patOfName :: BindName -> Arg (Pattern' Expr)
    patOfName = Pattern' Expr -> Arg (Pattern' Expr)
    forall a. a -> Arg a
    defaultArg (Pattern' Expr -> Arg (Pattern' Expr))
    -> (BindName -> Pattern' Expr) -> BindName -> Arg (Pattern' Expr)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . BindName -> Pattern' Expr
    forall e. BindName -> Pattern' e
    A.VarP

        insertIn :: [Arg (Maybe (Arg a))]
                 -> [Arg a] -> [Arg a]
        insertIn :: forall a. [Arg (Maybe (Arg a))] -> [Arg a] -> [Arg a]
    insertIn []                 [Arg a]
    wps  = [Arg a]
    wps
        insertIn (Arg ArgInfo
    info Maybe (Arg a)
    nm : [Arg (Maybe (Arg a))]
    ps) (Arg a
    w : [Arg a]
    wps) | ArgInfo -> Bool
    forall a. LensHiding a => a -> Bool
    visible ArgInfo
    info =
          Arg a
    w Arg a -> [Arg a] -> [Arg a]
    forall a. a -> [a] -> [a]
    : Maybe (Arg a) -> [Arg a]
    forall a. Maybe a -> [a]
    maybeToList Maybe (Arg a)
    nm [Arg a] -> [Arg a] -> [Arg a]
    forall a. [a] -> [a] -> [a]
    ++ [Arg (Maybe (Arg a))] -> [Arg a] -> [Arg a]
    forall a. [Arg (Maybe (Arg a))] -> [Arg a] -> [Arg a]
    insertIn [Arg (Maybe (Arg a))]
    ps [Arg a]
    wps
        insertIn (Arg ArgInfo
    info Maybe (Arg a)
    nm : [Arg (Maybe (Arg a))]
    ps) [Arg a]
    wps       | ArgInfo -> Bool
    forall a. LensHiding a => a -> Bool
    notVisible ArgInfo
    info =
              Maybe (Arg a) -> [Arg a]
    forall a. Maybe a -> [a]
    maybeToList Maybe (Arg a)
    nm [Arg a] -> [Arg a] -> [Arg a]
    forall a. [a] -> [a] -> [a]
    ++ [Arg (Maybe (Arg a))] -> [Arg a] -> [Arg a]
    forall a. [Arg (Maybe (Arg a))] -> [Arg a] -> [Arg a]
    insertIn [Arg (Maybe (Arg a))]
    ps [Arg a]
    wps
        insertIn [Arg (Maybe (Arg a))]
    _ [Arg a]
    _ = [Arg a]
    forall a. HasCallStack => a
    __IMPOSSIBLE__

    -- | Insert some with-patterns into the with-clauses LHS of the given RHS.
    -- (Used for @rewrite@)
    insertPatterns :: List1 (Arg A.Pattern) -> A.RHS -> A.RHS
    insertPatterns :: List1 (Arg (Pattern' Expr)) -> RHS -> RHS
    insertPatterns List1 (Arg (Pattern' Expr))
    pats = (LHSCore' Expr -> LHSCore' Expr) -> RHS -> RHS
    mapLHSCores (List1 (Arg (Pattern' Expr)) -> LHSCore' Expr -> LHSCore' Expr
    insertPatternsLHSCore List1 (Arg (Pattern' Expr))
    pats)

    -- | Insert with-patterns before the trailing with patterns.
    -- If there are none, append the with-patterns.
    insertPatternsLHSCore :: List1 (Arg A.Pattern) -> A.LHSCore -> A.LHSCore
    insertPatternsLHSCore :: List1 (Arg (Pattern' Expr)) -> LHSCore' Expr -> LHSCore' Expr
    insertPatternsLHSCore List1 (Arg (Pattern' Expr))
    pats = \case
      A.LHSWith LHSCore' Expr
    core List1 (Arg (Pattern' Expr))
    wps [] -> LHSCore' Expr
    -> List1 (Arg (Pattern' Expr))
    -> [NamedArg (Pattern' Expr)]
    -> LHSCore' Expr
    forall e.
    LHSCore' e
    -> List1 (Arg (Pattern' e))
    -> [NamedArg (Pattern' e)]
    -> LHSCore' e
    A.LHSWith LHSCore' Expr
    core (List1 (Arg (Pattern' Expr))
    pats List1 (Arg (Pattern' Expr))
    -> List1 (Arg (Pattern' Expr)) -> List1 (Arg (Pattern' Expr))
    forall a. Semigroup a => a -> a -> a
    <> List1 (Arg (Pattern' Expr))
    wps) []
      LHSCore' Expr
    core                  -> LHSCore' Expr
    -> List1 (Arg (Pattern' Expr))
    -> [NamedArg (Pattern' Expr)]
    -> LHSCore' Expr
    forall e.
    LHSCore' e
    -> List1 (Arg (Pattern' e))
    -> [NamedArg (Pattern' e)]
    -> LHSCore' e
    A.LHSWith LHSCore' Expr
    core List1 (Arg (Pattern' Expr))
    pats []

    -- | Parameters for creating a @with@-function.
    data WithFunctionProblem
      = NoWithFunction
      | WithFunction
        { WithFunctionProblem -> QName
    wfParentName   :: QName                            -- ^ Parent function name.
        , WithFunctionProblem -> QName
    wfName         :: QName                            -- ^ With function name.
        , WithFunctionProblem -> Type
    wfParentType   :: Type                             -- ^ Type of the parent function.
        , WithFunctionProblem -> Tele (Dom Type)
    wfParentTel    :: Telescope                        -- ^ Context of the parent patterns.
        , WithFunctionProblem -> Tele (Dom Type)
    wfBeforeTel    :: Telescope                        -- ^ Types of arguments to the with function before the with expressions (needed vars).
        , WithFunctionProblem -> Tele (Dom Type)
    wfAfterTel     :: Telescope                        -- ^ Types of arguments to the with function after the with expressions (unneeded vars).
        , WithFunctionProblem -> List1 (Arg (Term, EqualityView))
    wfExprs        :: List1 (Arg (Term, EqualityView)) -- ^ With and rewrite expressions and their types.
        , WithFunctionProblem -> Type
    wfRHSType      :: Type                             -- ^ Type of the right hand side.
        , WithFunctionProblem -> [NamedArg DeBruijnPattern]
    wfParentPats   :: [NamedArg DeBruijnPattern]       -- ^ Parent patterns.
        , WithFunctionProblem -> Int
    wfParentParams :: Nat                              -- ^ Number of module parameters in parent patterns
        , WithFunctionProblem -> Permutation
    wfPermSplit    :: Permutation                      -- ^ Permutation resulting from splitting the telescope into needed and unneeded vars.
        , WithFunctionProblem -> Permutation
    wfPermParent   :: Permutation                      -- ^ Permutation reordering the variables in the parent pattern.
        , WithFunctionProblem -> Permutation
    wfPermFinal    :: Permutation                      -- ^ Final permutation (including permutation for the parent clause).
        , WithFunctionProblem -> List1 (Clause' LHS)
    wfClauses      :: List1 A.Clause                   -- ^ The given clauses for the with function
        , WithFunctionProblem -> Substitution
    wfCallSubst    :: Substitution                     -- ^ Substitution to generate call for the parent.
        , WithFunctionProblem -> Map Name LetBinding
    wfLetBindings  :: Map Name LetBinding              -- ^ The let-bindings in scope of the parent (in the parent context).
        }

    checkSystemCoverage
      :: QName
      -> [Int]
      -> Type
      -> [Clause]
      -> TCM System
    checkSystemCoverage :: QName -> [Int] -> Type -> [Clause] -> TCMT IO System
    checkSystemCoverage QName
    f [Int
    n] Type
    t [Clause]
    cs = do
      [Char] -> Int -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "tc.sys.cover" Int
    10 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ [Char] -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => [Char] -> m Doc
    text ((Int, Int) -> [Char]
    forall a. Show a => a -> [Char]
    show (Int
    n , [Clause] -> Int
    forall a. [a] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length [Clause]
    cs)) TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Type -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => Type -> m Doc
    prettyTCM Type
    t
      TelV gamma t <- Int -> Type -> TCMT IO (TelV Type)
    forall (m :: * -> *).
    (MonadReduce m, MonadAddContext m) =>
    Int -> Type -> m (TelV Type)
    telViewUpTo Int
    n Type
    t
      addContext gamma $ do
      TelV (ExtendTel a _) _ <- telViewUpTo 1 t
      a <- reduce $ unEl $ unDom a

      case a of
        Def QName
    q [Apply Arg Term
    phi] -> do
          [iz,io] <- (BuiltinId -> TCMT IO (Maybe QName))
    -> [BuiltinId] -> 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 BuiltinId -> TCMT IO (Maybe QName)
    forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe QName)
    getBuiltinName' [BuiltinId
    builtinIZero, BuiltinId
    builtinIOne]
          ineg <- primINeg
          imin <- primIMin
          imax <- primIMax
          i0 <- primIZero
          i1 <- primIOne
          let
            isDir (ConP ConHead
    q ConPatternInfo
    _ []) | QName -> Maybe QName
    forall a. a -> Maybe a
    Just (ConHead -> QName
    conName ConHead
    q) Maybe QName -> Maybe QName -> Bool
    forall a. Eq a => a -> a -> Bool
    == Maybe QName
    iz = Bool -> Maybe Bool
    forall a. a -> Maybe a
    Just Bool
    False
            isDir (ConP ConHead
    q ConPatternInfo
    _ []) | QName -> Maybe QName
    forall a. a -> Maybe a
    Just (ConHead -> QName
    conName ConHead
    q) Maybe QName -> Maybe QName -> Bool
    forall a. Eq a => a -> a -> Bool
    == Maybe QName
    io = Bool -> Maybe Bool
    forall a. a -> Maybe a
    Just Bool
    True
            isDir DeBruijnPattern
    _ = Maybe Bool
    forall a. Maybe a
    Nothing

            collectDirs :: [Int] -> [DeBruijnPattern] -> [(Int,Bool)]
            collectDirs [] [] = []
            collectDirs (Int
    i : [Int]
    is) (DeBruijnPattern
    p : [DeBruijnPattern]
    ps) | Just Bool
    d <- DeBruijnPattern -> Maybe Bool
    isDir DeBruijnPattern
    p = (Int
    i,Bool
    d) (Int, Bool) -> [(Int, Bool)] -> [(Int, Bool)]
    forall a. a -> [a] -> [a]
    : [Int] -> [DeBruijnPattern] -> [(Int, Bool)]
    collectDirs [Int]
    is [DeBruijnPattern]
    ps
                                          | Bool
    otherwise         = [Int] -> [DeBruijnPattern] -> [(Int, Bool)]
    collectDirs [Int]
    is [DeBruijnPattern]
    ps
            collectDirs [Int]
    _ [DeBruijnPattern]
    _ = [(Int, Bool)]
    forall a. HasCallStack => a
    __IMPOSSIBLE__

            dir :: (Int,Bool) -> Term
            dir (Int
    i,Bool
    False) = Term
    ineg Term -> [Arg Term] -> Term
    forall t. Apply t => t -> [Arg Term] -> t
    `apply` [Term -> Arg Term
    forall a. a -> Arg a
    argN (Term -> Arg Term) -> Term -> Arg Term
    forall a b. (a -> b) -> a -> b
    $ Int -> Term
    var Int
    i]
            dir (Int
    i,Bool
    True) = Int -> Term
    var Int
    i

            -- andI and orI have cases for singletons to improve error messages.
            andI, orI :: [Term] -> Term
            andI [] = Term
    i1
            andI [Term
    t] = Term
    t
            andI (Term
    t:[Term]
    ts) = (\ Term
    x -> Term
    imin Term -> [Arg Term] -> Term
    forall t. Apply t => t -> [Arg Term] -> t
    `apply` [Term -> Arg Term
    forall a. a -> Arg a
    argN Term
    t, Term -> Arg Term
    forall a. a -> Arg a
    argN Term
    x]) (Term -> Term) -> Term -> Term
    forall a b. (a -> b) -> a -> b
    $ [Term] -> Term
    andI [Term]
    ts

            orI [] = Term
    i0
            orI [Term
    t] = Term
    t
            orI (Term
    t:[Term]
    ts) = Term
    imax Term -> [Arg Term] -> Term
    forall t. Apply t => t -> [Arg Term] -> t
    `apply` [Term -> Arg Term
    forall a. a -> Arg a
    argN Term
    t, Term -> Arg Term
    forall a. a -> Arg a
    argN ([Term] -> Term
    orI [Term]
    ts)]

          let
            pats = (Clause -> [DeBruijnPattern]) -> [Clause] -> [[DeBruijnPattern]]
    forall a b. (a -> b) -> [a] -> [b]
    map (Int -> [DeBruijnPattern] -> [DeBruijnPattern]
    forall a. Int -> [a] -> [a]
    take Int
    n ([DeBruijnPattern] -> [DeBruijnPattern])
    -> (Clause -> [DeBruijnPattern]) -> Clause -> [DeBruijnPattern]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (NamedArg DeBruijnPattern -> DeBruijnPattern)
    -> [NamedArg DeBruijnPattern] -> [DeBruijnPattern]
    forall a b. (a -> b) -> [a] -> [b]
    map (Named NamedName DeBruijnPattern -> DeBruijnPattern
    forall name a. Named name a -> a
    namedThing (Named NamedName DeBruijnPattern -> DeBruijnPattern)
    -> (NamedArg DeBruijnPattern -> Named NamedName DeBruijnPattern)
    -> NamedArg DeBruijnPattern
    -> DeBruijnPattern
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . NamedArg DeBruijnPattern -> Named NamedName DeBruijnPattern
    forall e. Arg e -> e
    unArg) ([NamedArg DeBruijnPattern] -> [DeBruijnPattern])
    -> (Clause -> [NamedArg DeBruijnPattern])
    -> Clause
    -> [DeBruijnPattern]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Clause -> [NamedArg DeBruijnPattern]
    namedClausePats) [Clause]
    cs
            alphas :: [[(Int,Bool)]] -- the face maps corresponding to each clause
            alphas = ([DeBruijnPattern] -> [(Int, Bool)])
    -> [[DeBruijnPattern]] -> [[(Int, Bool)]]
    forall a b. (a -> b) -> [a] -> [b]
    map ([Int] -> [DeBruijnPattern] -> [(Int, Bool)]
    collectDirs (Int -> [Int]
    forall a. Integral a => a -> [a]
    downFrom Int
    n)) [[DeBruijnPattern]]
    pats
            phis :: [Term] -- the φ terms for each clause (i.e. the alphas as terms)
            phis = ([(Int, Bool)] -> Term) -> [[(Int, Bool)]] -> [Term]
    forall a b. (a -> b) -> [a] -> [b]
    map ([Term] -> Term
    andI ([Term] -> Term)
    -> ([(Int, Bool)] -> [Term]) -> [(Int, Bool)] -> Term
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (((Int, Bool) -> Term) -> [(Int, Bool)] -> [Term]
    forall a b. (a -> b) -> [a] -> [b]
    map (Int, Bool) -> Term
    dir)) [[(Int, Bool)]]
    alphas
            psi = [Term] -> Term
    orI ([Term] -> Term) -> [Term] -> Term
    forall a b. (a -> b) -> a -> b
    $ [Term]
    phis
            pcs = [Term] -> [Clause] -> [(Term, Clause)]
    forall a b. [a] -> [b] -> [(a, b)]
    zip [Term]
    phis [Clause]
    cs

          reportSDoc "tc.sys.cover" 20 $ fsep $ map prettyTCM pats
          interval <- primIntervalType
          reportSDoc "tc.sys.cover" 10 $ "equalTerm " <+> prettyTCM (unArg phi) <+> prettyTCM psi
          equalTerm interval (unArg phi) psi

          forM_ (initWithDefault __IMPOSSIBLE__ $
                 initWithDefault __IMPOSSIBLE__ $ List.tails pcs) $ \ ((Term
    phi1,Clause
    cl1):[(Term, Clause)]
    pcs') -> do
            [(Term, Clause)] -> ((Term, Clause) -> TCMT IO [()]) -> TCM ()
    forall (t :: * -> *) (m :: * -> *) a b.
    (Foldable t, Monad m) =>
    t a -> (a -> m b) -> m ()
    forM_ [(Term, Clause)]
    pcs' (((Term, Clause) -> TCMT IO [()]) -> TCM ())
    -> ((Term, Clause) -> TCMT IO [()]) -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ \ (Term
    phi2,Clause
    cl2) -> do
              phi12 <- Term -> TCMT IO Term
    forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
    reduce (Term
    imin Term -> [Arg Term] -> Term
    forall t. Apply t => t -> [Arg Term] -> t
    `apply` [Term -> Arg Term
    forall a. a -> Arg a
    argN Term
    phi1, Term -> Arg Term
    forall a. a -> Arg a
    argN Term
    phi2])
              forallFaceMaps phi12 (\ IntMap Bool
    _ Blocker
    _ -> Term -> TCM ()
    forall a. HasCallStack => a
    __IMPOSSIBLE__) $ \IntMap Bool
    _ Substitution
    sigma -> do
                let args :: [Arg Term]
    args = Substitution
    Substitution' (SubstArg [Arg Term])
    sigma Substitution' (SubstArg [Arg Term]) -> [Arg Term] -> [Arg Term]
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    `applySubst` Tele (Dom Type) -> [Arg Term]
    forall a t. DeBruijn a => Tele (Dom t) -> [Arg a]
    teleArgs Tele (Dom Type)
    gamma
                    t' :: Type
    t' = Substitution
    Substitution' (SubstArg Type)
    sigma Substitution' (SubstArg Type) -> Type -> Type
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    `applySubst` Type
    t
                    fromReduced :: Reduced (Blocked' t yes) yes -> yes
    fromReduced (YesReduction Simplification
    _ yes
    x) = yes
    x
                    fromReduced (NoReduction Blocked' t yes
    x) = Blocked' t yes -> yes
    forall t a. Blocked' t a -> a
    ignoreBlocking Blocked' t yes
    x
                    body :: Clause -> TCMT IO Term
    body Clause
    cl = do
                      let extra :: Int
    extra = [NamedArg DeBruijnPattern] -> Int
    forall a. [a] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length (Int -> [NamedArg DeBruijnPattern] -> [NamedArg DeBruijnPattern]
    forall a. Int -> [a] -> [a]
    drop Int
    n ([NamedArg DeBruijnPattern] -> [NamedArg DeBruijnPattern])
    -> [NamedArg DeBruijnPattern] -> [NamedArg DeBruijnPattern]
    forall a b. (a -> b) -> a -> b
    $ Clause -> [NamedArg DeBruijnPattern]
    namedClausePats Clause
    cl)
                      TelV delta _ <- Int -> Type -> TCMT IO (TelV Type)
    forall (m :: * -> *).
    (MonadReduce m, MonadAddContext m) =>
    Int -> Type -> m (TelV Type)
    telViewUpTo Int
    extra Type
    t'
                      fmap (abstract delta) $ addContext delta $ do
                        fmap fromReduced $ runReduceM $
                          appDef' f (Def f []) [cl] [] (map notReduced $ raise (size delta) args ++ teleArgs delta)
                v1 <- Clause -> TCMT IO Term
    body Clause
    cl1
                v2 <- body cl2
                equalTerm t' v1 v2

          sys <- forM (zip alphas cs) $ \ ([(Int, Bool)]
    alpha,Clause
    cl) -> do

                let
                    -- Δ = Γ_α , Δ'α
                    delta :: Tele (Dom Type)
    delta = Clause -> Tele (Dom Type)
    clauseTel Clause
    cl
                    -- Δ ⊢ b
                    Just Term
    b = Clause -> Maybe Term
    clauseBody Clause
    cl
                    -- Δ ⊢ ps : Γ , o : [φ] , Δ'
                    -- we assume that there's no pattern matching other
                    -- than from the system
                    ps :: [NamedArg DeBruijnPattern]
    ps = Clause -> [NamedArg DeBruijnPattern]
    namedClausePats Clause
    cl
                    extra :: Int
    extra = [NamedArg DeBruijnPattern] -> Int
    forall a. [a] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length (Int -> [NamedArg DeBruijnPattern] -> [NamedArg DeBruijnPattern]
    forall a. Int -> [a] -> [a]
    drop (Tele (Dom Type) -> Int
    forall a. Sized a => a -> Int
    size Tele (Dom Type)
    gamma Int -> Int -> Int
    forall a. Num a => a -> a -> a
    + Int
    1) [NamedArg DeBruijnPattern]
    ps)
                    -- size Δ'α = size Δ' = extra
                    -- Γ , α ⊢ u
                    takeLast :: Int -> [a] -> [a]
    takeLast Int
    n [a]
    xs = Int -> [a] -> [a]
    forall a. Int -> [a] -> [a]
    drop ([a] -> Int
    forall a. [a] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length [a]
    xs Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - Int
    n) [a]
    xs
                    weak :: [Int] -> Substitution' a
    weak [] = Substitution' a
    forall a. Substitution' a
    idS
                    weak (Int
    i:[Int]
    is) = [Int] -> Substitution' a
    weak [Int]
    is Substitution' a -> Substitution' a -> Substitution' a
    forall a.
    EndoSubst a =>
    Substitution' a -> Substitution' a -> Substitution' a
    `composeS` Int -> Substitution' a -> Substitution' a
    forall a. Int -> Substitution' a -> Substitution' a
    liftS Int
    i (Int -> Substitution' a
    forall a. Int -> Substitution' a
    raiseS Int
    1)
                    tel :: Tele (Dom Type)
    tel = [Dom ([Char], Type)] -> Tele (Dom Type)
    telFromList (Int -> [Dom ([Char], Type)] -> [Dom ([Char], Type)]
    forall a. Int -> [a] -> [a]
    takeLast Int
    extra (Tele (Dom Type) -> [Dom ([Char], Type)]
    forall t. Tele (Dom t) -> [Dom ([Char], t)]
    telToList Tele (Dom Type)
    delta))
                    u :: Term
    u = Tele (Dom Type) -> Term -> Term
    forall t. Abstract t => Tele (Dom Type) -> t -> t
    abstract Tele (Dom Type)
    tel (Int -> Substitution -> Substitution
    forall a. Int -> Substitution' a -> Substitution' a
    liftS Int
    extra ([Int] -> Substitution
    forall {a}.
    (SubstArg a ~ a, Subst a, DeBruijn a) =>
    [Int] -> Substitution' a
    weak ([Int] -> Substitution) -> [Int] -> Substitution
    forall a b. (a -> b) -> a -> b
    $ [Int] -> [Int]
    forall a. Ord a => [a] -> [a]
    List.sort ([Int] -> [Int]) -> [Int] -> [Int]
    forall a b. (a -> b) -> a -> b
    $ ((Int, Bool) -> Int) -> [(Int, Bool)] -> [Int]
    forall a b. (a -> b) -> [a] -> [b]
    map (Int, Bool) -> Int
    forall a b. (a, b) -> a
    fst [(Int, Bool)]
    alpha) Substitution' (SubstArg Term) -> Term -> Term
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    `applySubst` Term
    b)
                ([(Term, Bool)], Term) -> TCMT IO ([(Term, Bool)], Term)
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (((Int, Bool) -> (Term, Bool)) -> [(Int, Bool)] -> [(Term, Bool)]
    forall a b. (a -> b) -> [a] -> [b]
    map ((Int -> Term) -> (Int, Bool) -> (Term, Bool)
    forall a b c. (a -> b) -> (a, c) -> (b, c)
    forall (p :: * -> * -> *) a b c.
    Bifunctor p =>
    (a -> b) -> p a c -> p b c
    first Int -> Term
    var) [(Int, Bool)]
    alpha,Term
    u)

          reportSDoc "tc.sys.cover.sys" 20 $ fsep $ prettyTCM gamma : map prettyTCM sys
          reportSDoc "tc.sys.cover.sys" 40 $ fsep $ (text . show) gamma : map (text . show) sys
          return (System gamma sys) -- gamma uses names from the type, not the patterns, could we do better?
        Term
    _ -> TCMT IO System
    forall a. HasCallStack => a
    __IMPOSSIBLE__
    checkSystemCoverage QName
    _ [Int]
    _ Type
    t [Clause]
    cs = TCMT IO System
    forall a. HasCallStack => a
    __IMPOSSIBLE__

    -- * Info that is needed after all clauses have been processed.

    data ClausesPostChecks = CPC
        { ClausesPostChecks -> IntSet
    cpcPartialSplits :: IntSet
          -- ^ Which argument indexes have a partial split.
        }

    instance Semigroup ClausesPostChecks where
      CPC IntSet
    xs <> :: ClausesPostChecks -> ClausesPostChecks -> ClausesPostChecks
    <> CPC IntSet
    xs' = IntSet -> ClausesPostChecks
    CPC (IntSet -> IntSet -> IntSet
    IntSet.union IntSet
    xs IntSet
    xs')

    instance Monoid ClausesPostChecks where
      mempty :: ClausesPostChecks
    mempty  = IntSet -> ClausesPostChecks
    CPC IntSet
    forall a. Null a => a
    empty
      mappend :: ClausesPostChecks -> ClausesPostChecks -> ClausesPostChecks
    mappend = ClausesPostChecks -> ClausesPostChecks -> ClausesPostChecks
    forall a. Semigroup a => a -> a -> a
    (<>)

    -- | The LHS part of checkClause.
    checkClauseLHS :: Type -> Maybe Substitution -> A.SpineClause -> (LHSResult -> TCM a) -> TCM a
    checkClauseLHS :: forall a.
    Type
    -> Maybe Substitution
    -> SpineClause
    -> (LHSResult -> TCM a)
    -> TCM a
    checkClauseLHS Type
    t Maybe Substitution
    withSub c :: SpineClause
    c@(A.Clause lhs :: SpineLHS
    lhs@(A.SpineLHS LHSInfo
    i QName
    x [NamedArg (Pattern' Expr)]
    aps) [ProblemEq]
    strippedPats RHS
    rhs0 WhereDeclarations
    wh Catchall
    catchall) LHSResult -> TCM a
    ret = do
        [Char] -> Int -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "tc.lhs.top" Int
    30 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Doc
    "Checking clause" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    $$ SpineClause -> TCMT IO Doc
    forall a (m :: * -> *).
    (ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
    a -> m Doc
    prettyA SpineClause
    c
        () <- [NamedArg (Pattern' Expr)]
    -> (List1 (NamedArg (Pattern' Expr)) -> TCM ()) -> TCM ()
    forall (m :: * -> *) a.
    Applicative m =>
    [a] -> (List1 a -> m ()) -> m ()
    List1.unlessNull ([NamedArg (Pattern' Expr)] -> [NamedArg (Pattern' Expr)]
    trailingWithPatterns [NamedArg (Pattern' Expr)]
    aps) ((List1 (NamedArg (Pattern' Expr)) -> TCM ()) -> TCM ())
    -> (List1 (NamedArg (Pattern' Expr)) -> TCM ()) -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ \ List1 (NamedArg (Pattern' Expr))
    withPats -> do
          TypeError -> TCM ()
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    TypeError -> m a
    typeError (TypeError -> TCM ()) -> TypeError -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ NonEmpty (Pattern' Expr) -> TypeError
    UnexpectedWithPatterns (NonEmpty (Pattern' Expr) -> TypeError)
    -> NonEmpty (Pattern' Expr) -> TypeError
    forall a b. (a -> b) -> a -> b
    $ (NamedArg (Pattern' Expr) -> Pattern' Expr)
    -> List1 (NamedArg (Pattern' Expr)) -> NonEmpty (Pattern' Expr)
    forall a b. (a -> b) -> NonEmpty a -> NonEmpty b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap NamedArg (Pattern' Expr) -> Pattern' Expr
    forall a. NamedArg a -> a
    namedArg List1 (NamedArg (Pattern' Expr))
    withPats
        traceCall (CheckClause t c) $ do
          aps <- expandPatternSynonyms aps
          unless (null strippedPats) $ reportSDoc "tc.lhs.top" 50 $
            "strippedPats:" <+> vcat [ prettyA p <+> "=" <+> prettyTCM v <+> ":" <+> prettyTCM a | A.ProblemEq p v a <- strippedPats ]
          closed_t <- flip abstract t <$> getContextTelescope
          checkLeftHandSide (CheckLHS lhs) (getRange lhs) (Just x) aps t withSub strippedPats ret

    -- | Type check a function clause.

    checkClause
      :: Type          -- ^ Type of function defined by this clause.
      -> Maybe (Substitution, Map Name LetBinding)  -- ^ Module parameter substitution arising from with-abstraction, and inherited let-bindings.
      -> A.SpineClause -- ^ Clause.
      -> TCM (Clause, ClausesPostChecks)  -- ^ Type-checked clause

    checkClause :: Type
    -> Maybe (Substitution, Map Name LetBinding)
    -> SpineClause
    -> TCMT IO (Clause, ClausesPostChecks)
    checkClause Type
    t Maybe (Substitution, Map Name LetBinding)
    withSubAndLets c :: SpineClause
    c@(A.Clause lhs :: SpineLHS
    lhs@(A.SpineLHS LHSInfo
    i QName
    x [NamedArg (Pattern' Expr)]
    aps) [ProblemEq]
    strippedPats RHS
    rhs0 WhereDeclarations
    wh Catchall
    catchall) = do
      let withSub :: Maybe Substitution
    withSub       = (Substitution, Map Name LetBinding) -> Substitution
    forall a b. (a, b) -> a
    fst ((Substitution, Map Name LetBinding) -> Substitution)
    -> Maybe (Substitution, Map Name LetBinding) -> Maybe Substitution
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Maybe (Substitution, Map Name LetBinding)
    withSubAndLets
      cxtNames <- TCMT IO [Name]
    forall (m :: * -> *). MonadTCEnv m => m [Name]
    getContextNames
      checkClauseLHS t withSub c $ \ lhsResult :: LHSResult
    lhsResult@(LHSResult Int
    npars Tele (Dom Type)
    delta [NamedArg DeBruijnPattern]
    ps Bool
    absurdPat Arg Type
    trhs Substitution
    patSubst [AsBinding]
    asb IntSet
    psplit Bool
    ixsplit) -> do

        let installInheritedLets :: TCMT IO (Clause, ClausesPostChecks)
    -> TCMT IO (Clause, ClausesPostChecks)
    installInheritedLets TCMT IO (Clause, ClausesPostChecks)
    k
              | Just (Substitution
    withSub, Map Name LetBinding
    lets) <- Maybe (Substitution, Map Name LetBinding)
    withSubAndLets = do
                lets' <- (LetBinding -> TCMT IO (Open LetBinding))
    -> Map Name LetBinding -> TCMT IO (Map Name (Open LetBinding))
    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) -> Map Name a -> f (Map Name b)
    traverse LetBinding -> TCMT IO (Open LetBinding)
    forall (m :: * -> *) a.
    (ReadTCState m, MonadTCEnv m) =>
    a -> m (Open a)
    makeOpen (Map Name LetBinding -> TCMT IO (Map Name (Open LetBinding)))
    -> Map Name LetBinding -> TCMT IO (Map Name (Open LetBinding))
    forall a b. (a -> b) -> a -> b
    $ Substitution' (SubstArg (Map Name LetBinding))
    -> Map Name LetBinding -> Map Name LetBinding
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    applySubst (Substitution
    patSubst Substitution -> Substitution -> Substitution
    forall a.
    EndoSubst a =>
    Substitution' a -> Substitution' a -> Substitution' a
    `composeS` Substitution
    withSub) Map Name LetBinding
    lets
                locallyTC eLetBindings (lets' <>) k
              | Bool
    otherwise = TCMT IO (Clause, ClausesPostChecks)
    k

        TCMT IO (Clause, ClausesPostChecks)
    -> TCMT IO (Clause, ClausesPostChecks)
    installInheritedLets (TCMT IO (Clause, ClausesPostChecks)
     -> TCMT IO (Clause, ClausesPostChecks))
    -> TCMT IO (Clause, ClausesPostChecks)
    -> TCMT IO (Clause, ClausesPostChecks)
    forall a b. (a -> b) -> a -> b
    $ do
            -- Note that we might now be in irrelevant context,
            -- in case checkLeftHandSide walked over an irrelevant projection pattern.

            -- Subtle: checkRHS expects the function type to be the lambda lifted
            -- type. If we're checking a with-function that's already the case,
            -- otherwise we need to abstract over the module telescope.
            t' <- case Maybe Substitution
    withSub of
                    Just{}  -> Type -> TCMT IO Type
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Type
    t
                    Maybe Substitution
    Nothing -> do
                      theta <- ModuleName -> TCMT IO (Tele (Dom Type))
    forall (m :: * -> *).
    (Functor m, ReadTCState m) =>
    ModuleName -> m (Tele (Dom Type))
    lookupSection (QName -> ModuleName
    qnameModule QName
    x)
                      return $ abstract theta t

            -- At this point we should update the named dots potential with-clauses
            -- in the right-hand side. When checking a clause we expect the named
            -- dots to live in the context of the closest parent lhs, but the named
            -- dots added by buildWithFunction live in the context of the
            -- with-function arguments before pattern matching. That's what we need
            -- patSubst for.
            let rhs = RHS -> RHS
    updateRHS RHS
    rhs0
                updateRHS rhs :: RHS
    rhs@A.RHS{}               = RHS
    rhs
                updateRHS rhs :: RHS
    rhs@A.AbsurdRHS{}         = RHS
    rhs
                updateRHS (A.WithRHS QName
    q List1 WithExpr
    es List1 (Clause' LHS)
    cs)       = QName -> List1 WithExpr -> List1 (Clause' LHS) -> RHS
    A.WithRHS QName
    q List1 WithExpr
    es (List1 (Clause' LHS) -> RHS) -> List1 (Clause' LHS) -> RHS
    forall a b. (a -> b) -> a -> b
    $ (Clause' LHS -> Clause' LHS)
    -> List1 (Clause' LHS) -> List1 (Clause' LHS)
    forall a b. (a -> b) -> NonEmpty a -> NonEmpty b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap Clause' LHS -> Clause' LHS
    updateClause List1 (Clause' LHS)
    cs
                updateRHS (A.RewriteRHS [RewriteEqn]
    qes [ProblemEq]
    spats RHS
    rhs WhereDeclarations
    wh) =
                  [RewriteEqn] -> [ProblemEq] -> RHS -> WhereDeclarations -> RHS
    A.RewriteRHS [RewriteEqn]
    qes (Substitution' (SubstArg [ProblemEq]) -> [ProblemEq] -> [ProblemEq]
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    applySubst Substitution
    Substitution' (SubstArg [ProblemEq])
    patSubst [ProblemEq]
    spats) (RHS -> RHS
    updateRHS RHS
    rhs) WhereDeclarations
    wh

                updateClause (A.Clause LHS
    f [ProblemEq]
    spats RHS
    rhs WhereDeclarations
    wh Catchall
    ca) =
                  LHS
    -> [ProblemEq]
    -> RHS
    -> WhereDeclarations
    -> Catchall
    -> Clause' LHS
    forall lhs.
    lhs
    -> [ProblemEq]
    -> RHS
    -> WhereDeclarations
    -> Catchall
    -> Clause' lhs
    A.Clause LHS
    f (Substitution' (SubstArg [ProblemEq]) -> [ProblemEq] -> [ProblemEq]
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    applySubst Substitution
    Substitution' (SubstArg [ProblemEq])
    patSubst [ProblemEq]
    spats) (RHS -> RHS
    updateRHS RHS
    rhs) WhereDeclarations
    wh Catchall
    ca

            (body, with) <- bindAsPatterns asb $ checkWhere wh $ checkRHS i x aps t' lhsResult rhs

            -- Note that the with function doesn't necessarily share any part of
            -- the context with the parent (but withSub will take you from parent
            -- to child).

            wbody <- unsafeInTopContext $ Bench.billTo [Bench.Typing, Bench.With] $ checkWithFunction cxtNames with

            body <- return $ body `mplus` wbody

            whenM (optDoubleCheck <$> pragmaOptions) $ case body of
              Just Term
    v  -> do
                [Char] -> Int -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "tc.lhs.top" Int
    30 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ [TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    vcat
                  [ TCMT IO Doc
    "double checking rhs"
                  , Int -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
    nest Int
    2 (Term -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => Term -> m Doc
    prettyTCM Term
    v TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> TCMT IO Doc
    " : " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Type -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => Type -> m Doc
    prettyTCM (Arg Type -> Type
    forall e. Arg e -> e
    unArg Arg Type
    trhs))
                  ]
                TCM () -> TCM ()
    forall (m :: * -> *) a.
    (MonadConstraint m, MonadWarning m, MonadError TCErr m,
     MonadFresh ProblemId m) =>
    m a -> m a
    noConstraints (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ TCM () -> TCM ()
    forall (m :: * -> *) a.
    (MonadMetaSolver m, MonadTCState m) =>
    m a -> m a
    withFrozenMetas (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ Term -> Comparison -> TypeOf Term -> TCM ()
    forall a (m :: * -> *).
    (CheckInternal a, MonadCheckInternal m) =>
    a -> Comparison -> TypeOf a -> m ()
    forall (m :: * -> *).
    MonadCheckInternal m =>
    Term -> Comparison -> TypeOf Term -> m ()
    checkInternal Term
    v Comparison
    CmpLeq (TypeOf Term -> TCM ()) -> TypeOf Term -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ Arg Type -> Type
    forall e. Arg e -> e
    unArg Arg Type
    trhs
              Maybe Term
    Nothing -> () -> TCM ()
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()

            reportSDoc "tc.lhs.top" 10 $ vcat
              [ "Clause before translation:"
              , nest 2 $ vcat
                [ "delta =" <+> do escapeContext impossible (size delta) $ prettyTCM delta
                , "ps    =" <+> do P.fsep <$> prettyTCMPatterns ps
                , "body  =" <+> maybe "_|_" prettyTCM body
                , "type  =" <+> prettyTCM t
                ]
              ]

            reportSDoc "tc.lhs.top" 60 $ escapeContext impossible (size delta) $ vcat
              [ "Clause before translation (raw):"
              , nest 2 $ vcat
                [ "ps    =" <+> text (show ps)
                , "body  =" <+> text (show body)
                , "type  =" <+> text (show t)
                ]
              ]

            -- compute body modification for irrelevant definitions, see issue 610
            rel <- viewTC eRelevance
            let bodyMod = Bool -> (Maybe Term -> Maybe Term) -> Maybe Term -> Maybe Term
    forall b a. IsBool b => b -> (a -> a) -> a -> a
    applyWhen (Relevance -> Bool
    forall a. LensRelevance a => a -> Bool
    isIrrelevant Relevance
    rel) ((Term -> Term) -> Maybe Term -> Maybe Term
    forall a b. (a -> b) -> Maybe a -> Maybe b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap Term -> Term
    dontCare)

            -- absurd clauses don't define computational behaviour, so it's fine to
            -- treat them as catchalls.
            let catchall' = if Maybe Term -> Bool
    forall a. Maybe a -> Bool
    isNothing Maybe Term
    body then Range -> Catchall
    YesCatchall Range
    forall a. Null a => a
    empty else Catchall
    catchall

            return $ (, CPC psplit)
              Clause { clauseLHSRange  = getRange i
                     , clauseFullRange = getRange c
                     , clauseTel       = killRange delta
                     , namedClausePats = ps
                     , clauseBody      = bodyMod body
                     , clauseType      = Just trhs
                     , clauseCatchall  = catchall'
                     , clauseRecursive   = Nothing -- we don't know yet
                     , clauseUnreachable = Nothing -- we don't know yet
                     , clauseEllipsis    = lhsEllipsis i
                     , clauseWhereModule = A.whereModule wh
                     }

    -- | Generate the abstract pattern corresponding to Refl
    getReflPattern :: TCM A.Pattern
    getReflPattern :: TCM (Pattern' Expr)
    getReflPattern = do
      -- Get the name of builtin REFL.
      Con reflCon _ [] <- TCMT IO Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primRefl

      reflInfo <- fmap (setOrigin Inserted) <$> getReflArgInfo reflCon
      let patInfo = ConInfo -> PatInfo -> ConPatLazy -> ConPatInfo
    ConPatInfo ConInfo
    ConOCon PatInfo
    patNoRange ConPatLazy
    ConPatEager
      -- The REFL constructor might have an argument
      let reflArg = Maybe (NamedArg (Pattern' Expr)) -> [NamedArg (Pattern' Expr)]
    forall a. Maybe a -> [a]
    maybeToList (Maybe (NamedArg (Pattern' Expr)) -> [NamedArg (Pattern' Expr)])
    -> Maybe (NamedArg (Pattern' Expr)) -> [NamedArg (Pattern' Expr)]
    forall a b. (a -> b) -> a -> b
    $ (ArgInfo -> NamedArg (Pattern' Expr))
    -> Maybe ArgInfo -> Maybe (NamedArg (Pattern' Expr))
    forall a b. (a -> b) -> Maybe a -> Maybe b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (\ ArgInfo
    ai -> ArgInfo
    -> Named NamedName (Pattern' Expr) -> NamedArg (Pattern' Expr)
    forall e. ArgInfo -> e -> Arg e
    Arg ArgInfo
    ai (Named NamedName (Pattern' Expr) -> NamedArg (Pattern' Expr))
    -> Named NamedName (Pattern' Expr) -> NamedArg (Pattern' Expr)
    forall a b. (a -> b) -> a -> b
    $ Pattern' Expr -> Named NamedName (Pattern' Expr)
    forall a name. a -> Named name a
    unnamed (Pattern' Expr -> Named NamedName (Pattern' Expr))
    -> Pattern' Expr -> Named NamedName (Pattern' Expr)
    forall a b. (a -> b) -> a -> b
    $ PatInfo -> Pattern' Expr
    forall e. PatInfo -> Pattern' e
    A.WildP PatInfo
    patNoRange) Maybe ArgInfo
    reflInfo

      pure $ A.ConP patInfo (unambiguous $ conName reflCon) reflArg

    -- | Type check the @with@ and @rewrite@ lhss and/or the rhs.
    checkRHS
      :: LHSInfo                 -- ^ Range of lhs.
      -> QName                   -- ^ Name of function.
      -> [NamedArg A.Pattern]    -- ^ Patterns in lhs.
      -> Type                    -- ^ Top-level type of function.
      -> LHSResult               -- ^ Result of type-checking patterns
      -> A.RHS                   -- ^ Rhs to check.
      -> TCM (Maybe Term, WithFunctionProblem)
                                                  -- Note: the as-bindings are already bound (in checkClause)
    checkRHS :: LHSInfo
    -> QName
    -> [NamedArg (Pattern' Expr)]
    -> Type
    -> LHSResult
    -> RHS
    -> TCM (Maybe Term, WithFunctionProblem)
    checkRHS LHSInfo
    i QName
    x [NamedArg (Pattern' Expr)]
    aps Type
    t lhsResult :: LHSResult
    lhsResult@(LHSResult Int
    _ Tele (Dom Type)
    delta [NamedArg DeBruijnPattern]
    ps Bool
    absurdPat Arg Type
    trhs Substitution
    _ [AsBinding]
    _asb IntSet
    _ Bool
    _) RHS
    rhs0 =
      RHS -> TCM (Maybe Term, WithFunctionProblem)
    handleRHS RHS
    rhs0 where

      handleRHS :: A.RHS -> TCM (Maybe Term, WithFunctionProblem)
      handleRHS :: RHS -> TCM (Maybe Term, WithFunctionProblem)
    handleRHS RHS
    rhs = case RHS
    rhs of
        A.RHS Expr
    e Maybe Expr
    _                  -> Expr -> TCM (Maybe Term, WithFunctionProblem)
    ordinaryRHS Expr
    e
        RHS
    A.AbsurdRHS                -> TCM (Maybe Term, WithFunctionProblem)
    noRHS
        A.RewriteRHS [RewriteEqn]
    eqs [ProblemEq]
    ps RHS
    rhs WhereDeclarations
    wh -> [RewriteEqn]
    -> [ProblemEq]
    -> RHS
    -> WhereDeclarations
    -> TCM (Maybe Term, WithFunctionProblem)
    rewriteEqnsRHS [RewriteEqn]
    eqs [ProblemEq]
    ps RHS
    rhs WhereDeclarations
    wh
        A.WithRHS QName
    aux List1 WithExpr
    es List1 (Clause' LHS)
    cs        -> QName
    -> List1 WithExpr
    -> List1 (Clause' LHS)
    -> TCM (Maybe Term, WithFunctionProblem)
    withRHS QName
    aux List1 WithExpr
    es List1 (Clause' LHS)
    cs

      -- Ordinary case: f xs = e
      ordinaryRHS :: A.Expr -> TCM (Maybe Term, WithFunctionProblem)
      ordinaryRHS :: Expr -> TCM (Maybe Term, WithFunctionProblem)
    ordinaryRHS Expr
    e = Account (BenchPhase (TCMT IO))
    -> TCM (Maybe Term, WithFunctionProblem)
    -> TCM (Maybe Term, WithFunctionProblem)
    forall (m :: * -> *) c.
    MonadBench m =>
    Account (BenchPhase m) -> m c -> m c
    Bench.billTo [BenchPhase (TCMT IO)
    Phase
    Bench.Typing, BenchPhase (TCMT IO)
    Phase
    Bench.CheckRHS] (TCM (Maybe Term, WithFunctionProblem)
     -> TCM (Maybe Term, WithFunctionProblem))
    -> TCM (Maybe Term, WithFunctionProblem)
    -> TCM (Maybe Term, WithFunctionProblem)
    forall a b. (a -> b) -> a -> b
    $ do
        -- If there is an absurd pattern, we do not need a RHS. If we have
        -- one we complain, ignore it and return the same @(Nothing, NoWithFunction)@
        -- as the case dealing with @A.AbsurdRHS@.
        mv <- if Bool
    absurdPat
              then Maybe Term
    forall a. Maybe a
    Nothing Maybe Term -> TCM () -> TCMT IO (Maybe Term)
    forall a b. a -> TCMT IO b -> TCMT IO a
    forall (f :: * -> *) a b. Functor f => a -> f b -> f a
    <$ do Expr -> TCM () -> TCM ()
    forall (m :: * -> *) x a.
    (MonadTrace m, HasRange x) =>
    x -> m a -> m a
    setCurrentRange Expr
    e (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ Warning -> TCM ()
    forall (m :: * -> *).
    (HasCallStack, MonadWarning m) =>
    Warning -> m ()
    warning Warning
    AbsurdPatternRequiresAbsentRHS
              else Term -> Maybe Term
    forall a. a -> Maybe a
    Just (Term -> Maybe Term) -> TCMT IO Term -> TCMT IO (Maybe Term)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Expr -> Type -> TCMT IO Term
    checkExpr Expr
    e (Arg Type -> Type
    forall e. Arg e -> e
    unArg Arg Type
    trhs)
        return (mv, NoWithFunction)

      -- Absurd case: no right hand side
      noRHS :: TCM (Maybe Term, WithFunctionProblem)
      noRHS :: TCM (Maybe Term, WithFunctionProblem)
    noRHS = do
        Bool -> TCM () -> TCM ()
    forall b (m :: * -> *). (IsBool b, Monad m) => b -> m () -> m ()
    unless Bool
    absurdPat (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ TypeError -> TCM ()
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    TypeError -> m a
    typeError TypeError
    AbsentRHSRequiresAbsurdPattern
        (Maybe Term, WithFunctionProblem)
    -> TCM (Maybe Term, WithFunctionProblem)
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Maybe Term
    forall a. Maybe a
    Nothing, WithFunctionProblem
    NoWithFunction)

      -- With case: @f xs with {a} in eqa | b in eqb | {{c}} | ...; ... | ps1 = rhs1; ... | ps2 = rhs2; ...@
      -- We need to modify the patterns `ps1, ps2, ...` in the user-provided clauses
      -- to insert the {eqb} names so that the equality proofs are available on the various RHS.
      withRHS ::
           QName             -- name of the with-function
        -> List1 A.WithExpr  -- @[{a} in eqa, b in eqb, {{c}}, ...]@
        -> List1 A.Clause    -- @[(ps1 = rhs1), (ps2 = rhs), ...]@
        -> TCM (Maybe Term, WithFunctionProblem)
      withRHS :: QName
    -> List1 WithExpr
    -> List1 (Clause' LHS)
    -> TCM (Maybe Term, WithFunctionProblem)
    withRHS QName
    aux List1 WithExpr
    es List1 (Clause' LHS)
    cs = do

        [Char] -> Int -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "tc.with.top" Int
    15 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ [TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    vcat
          [ TCMT IO Doc
    "TC.Rules.Def.checkclause reached A.WithRHS"
          , NonEmpty (TCMT IO Doc) -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    sep (NonEmpty (TCMT IO Doc) -> TCMT IO Doc)
    -> NonEmpty (TCMT IO Doc) -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ QName -> TCMT IO Doc
    forall a (m :: * -> *).
    (ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
    a -> m Doc
    prettyA QName
    aux TCMT IO Doc -> NonEmpty (TCMT IO Doc) -> NonEmpty (TCMT IO Doc)
    forall a. a -> NonEmpty a -> NonEmpty a
    <| (WithExpr -> TCMT IO Doc)
    -> List1 WithExpr -> NonEmpty (TCMT IO Doc)
    forall a b. (a -> b) -> NonEmpty a -> NonEmpty b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Functor m => m Doc -> m Doc
    parens (TCMT IO Doc -> TCMT IO Doc)
    -> (WithExpr -> TCMT IO Doc) -> WithExpr -> TCMT IO Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Arg Expr -> TCMT IO Doc
    forall a (m :: * -> *).
    (ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
    a -> m Doc
    prettyA (Arg Expr -> TCMT IO Doc)
    -> (WithExpr -> Arg Expr) -> WithExpr -> TCMT IO Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . WithExpr -> Arg Expr
    forall name a. Named name a -> a
    namedThing) List1 WithExpr
    es
          ]
        [Char] -> Int -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "tc.with.top" Int
    20 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ do
          nfv <- TCM Int
    getCurrentModuleFreeVars
          m   <- currentModule
          sep [ "with function module:" <+>
                 prettyList (map prettyTCM $ mnameToList m)
              ,  text $ "free variables: " ++ show nfv
              ]

        -- Infer the types of the with expressions

        vtys <- List1 WithExpr
    -> (WithExpr -> TCMT IO (Arg (Term, EqualityView)))
    -> TCMT IO (List1 (Arg (Term, EqualityView)))
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    t a -> (a -> m b) -> m (t b)
    forM List1 WithExpr
    es ((WithExpr -> TCMT IO (Arg (Term, EqualityView)))
     -> TCMT IO (List1 (Arg (Term, EqualityView))))
    -> (WithExpr -> TCMT IO (Arg (Term, EqualityView)))
    -> TCMT IO (List1 (Arg (Term, EqualityView)))
    forall a b. (a -> b) -> a -> b
    $ \ (Named Maybe BindName
    nm Arg Expr
    we) -> do
                  (e, ty) <- Arg Expr -> TCM (Term, Type)
    inferExprForWith Arg Expr
    we
                  pure $ (<$ we) . (e,) $ case nm of
                    Maybe BindName
    Nothing -> Type -> EqualityView
    OtherType Type
    ty
                    Just{}  -> Type -> EqualityView
    IdiomType Type
    ty

        let names = (WithExpr -> Arg (Maybe BindName))
    -> List1 WithExpr -> List1 (Arg (Maybe BindName))
    forall a b. (a -> b) -> NonEmpty a -> NonEmpty b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (\ (Named Maybe BindName
    nm Arg Expr
    e) -> Maybe BindName
    nm Maybe BindName -> Arg Expr -> Arg (Maybe BindName)
    forall a b. a -> Arg b -> Arg a
    forall (f :: * -> *) a b. Functor f => a -> f b -> f a
    <$ Arg Expr
    e) List1 WithExpr
    es
        cs <- forM cs $ \ c :: Clause' LHS
    c@(A.Clause (A.LHS LHSInfo
    i LHSCore' Expr
    core) [ProblemEq]
    eqs RHS
    rhs WhereDeclarations
    wh Catchall
    b) -> do
          let rhs' :: RHS
    rhs'  = List1 (Arg (Maybe BindName)) -> RHS -> RHS
    insertNames    List1 (Arg (Maybe BindName))
    names RHS
    rhs
          let core' :: LHSCore' Expr
    core' = List1 (Arg (Maybe BindName)) -> LHSCore' Expr -> LHSCore' Expr
    insertInspects List1 (Arg (Maybe BindName))
    names LHSCore' Expr
    core
          Clause' LHS -> TCMT IO (Clause' LHS)
    forall a. a -> TCMT IO a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Clause' LHS -> TCMT IO (Clause' LHS))
    -> Clause' LHS -> TCMT IO (Clause' LHS)
    forall a b. (a -> b) -> a -> b
    $ LHS
    -> [ProblemEq]
    -> RHS
    -> WhereDeclarations
    -> Catchall
    -> Clause' LHS
    forall lhs.
    lhs
    -> [ProblemEq]
    -> RHS
    -> WhereDeclarations
    -> Catchall
    -> Clause' lhs
    A.Clause (LHSInfo -> LHSCore' Expr -> LHS
    A.LHS LHSInfo
    i LHSCore' Expr
    core') [ProblemEq]
    eqs RHS
    rhs' WhereDeclarations
    wh Catchall
    b

        -- Andreas, 2016-01-23, Issue #1796
        -- Run the size constraint solver to improve with-abstraction
        -- in case the with-expression contains size metas.
        solveSizeConstraints DefaultToInfty

        checkWithRHS x aux t lhsResult vtys cs

      -- Rewrite case: f xs (rewrite / invert) a | b | c | ...
      rewriteEqnsRHS
        :: [A.RewriteEqn]
        -> [A.ProblemEq]
        -> A.RHS
        -> A.WhereDeclarations
        -> TCM (Maybe Term, WithFunctionProblem)

      rewriteEqnsRHS :: [RewriteEqn]
    -> [ProblemEq]
    -> RHS
    -> WhereDeclarations
    -> TCM (Maybe Term, WithFunctionProblem)
    rewriteEqnsRHS [] [ProblemEq]
    strippedPats RHS
    rhs WhereDeclarations
    wh = WhereDeclarations
    -> TCM (Maybe Term, WithFunctionProblem)
    -> TCM (Maybe Term, WithFunctionProblem)
    forall a. WhereDeclarations -> TCM a -> TCM a
    checkWhere WhereDeclarations
    wh (TCM (Maybe Term, WithFunctionProblem)
     -> TCM (Maybe Term, WithFunctionProblem))
    -> TCM (Maybe Term, WithFunctionProblem)
    -> TCM (Maybe Term, WithFunctionProblem)
    forall a b. (a -> b) -> a -> b
    $ RHS -> TCM (Maybe Term, WithFunctionProblem)
    handleRHS RHS
    rhs
          -- Case: @rewrite@
          -- Andreas, 2014-01-17, Issue 1402:
          -- If the rewrites are discarded since lhs=rhs, then
          -- we can actually have where clauses.
      rewriteEqnsRHS (RewriteEqn
    r:[RewriteEqn]
    rs) [ProblemEq]
    strippedPats RHS
    rhs WhereDeclarations
    wh = case RewriteEqn
    r of
        Rewrite ((QName
    qname, Expr
    eq) :| [(QName, Expr)]
    qes) ->
          QName
    -> Expr -> [RewriteEqn] -> TCM (Maybe Term, WithFunctionProblem)
    rewriteEqnRHS QName
    qname Expr
    eq ([RewriteEqn] -> TCM (Maybe Term, WithFunctionProblem))
    -> [RewriteEqn] -> TCM (Maybe Term, WithFunctionProblem)
    forall a b. (a -> b) -> a -> b
    $
            [(QName, Expr)]
    -> [RewriteEqn]
    -> (NonEmpty (QName, Expr) -> [RewriteEqn])
    -> [RewriteEqn]
    forall a b. [a] -> b -> (List1 a -> b) -> b
    List1.ifNull [(QName, Expr)]
    qes {-then-} [RewriteEqn]
    rs {-else-} ((NonEmpty (QName, Expr) -> [RewriteEqn]) -> [RewriteEqn])
    -> (NonEmpty (QName, Expr) -> [RewriteEqn]) -> [RewriteEqn]
    forall a b. (a -> b) -> a -> b
    $ \ NonEmpty (QName, Expr)
    qes -> NonEmpty (QName, Expr) -> RewriteEqn
    forall qn nm p e. List1 (qn, e) -> RewriteEqn' qn nm p e
    Rewrite NonEmpty (QName, Expr)
    qes RewriteEqn -> [RewriteEqn] -> [RewriteEqn]
    forall a. a -> [a] -> [a]
    : [RewriteEqn]
    rs
        Invert QName
    qname List1 (Named BindName (Pattern' Expr, Expr))
    pes -> QName
    -> List1 (Named BindName (Pattern' Expr, Expr))
    -> [RewriteEqn]
    -> TCM (Maybe Term, WithFunctionProblem)
    invertEqnRHS QName
    qname List1 (Named BindName (Pattern' Expr, Expr))
    pes [RewriteEqn]
    rs
        LeftLet List1 (Pattern' Expr, Expr)
    pes -> List1 (Pattern' Expr, Expr)
    -> [RewriteEqn] -> TCM (Maybe Term, WithFunctionProblem)
    usingEqnRHS List1 (Pattern' Expr, Expr)
    pes [RewriteEqn]
    rs

        where

        -- @using@ clauses
        usingEqnRHS :: List1 (A.Pattern, A.Expr) -> [A.RewriteEqn] -> TCM (Maybe Term, WithFunctionProblem)
        usingEqnRHS :: List1 (Pattern' Expr, Expr)
    -> [RewriteEqn] -> TCM (Maybe Term, WithFunctionProblem)
    usingEqnRHS List1 (Pattern' Expr, Expr)
    pes [RewriteEqn]
    rs = do
          let letBindings :: [LetBinding]
    letBindings = [(Pattern' Expr, Expr)]
    -> ((Pattern' Expr, Expr) -> LetBinding) -> [LetBinding]
    forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
    for (List1 (Pattern' Expr, Expr) -> [Item (List1 (Pattern' Expr, Expr))]
    forall l. IsList l => l -> [Item l]
    List1.toList List1 (Pattern' Expr, Expr)
    pes) (((Pattern' Expr, Expr) -> LetBinding) -> [LetBinding])
    -> ((Pattern' Expr, Expr) -> LetBinding) -> [LetBinding]
    forall a b. (a -> b) -> a -> b
    $ \(Pattern' Expr
    p, Expr
    e) -> LetInfo -> Pattern' Expr -> Expr -> LetBinding
    A.LetPatBind (Range -> LetInfo
    LetRange (Expr -> Range
    forall a. HasRange a => a -> Range
    getRange Expr
    e)) Pattern' Expr
    p Expr
    e
          [LetBinding]
    -> TCM (Maybe Term, WithFunctionProblem)
    -> TCM (Maybe Term, WithFunctionProblem)
    forall (t :: * -> *) a.
    Foldable t =>
    t LetBinding -> TCM a -> TCM a
    checkLetBindings' [LetBinding]
    letBindings (TCM (Maybe Term, WithFunctionProblem)
     -> TCM (Maybe Term, WithFunctionProblem))
    -> TCM (Maybe Term, WithFunctionProblem)
    -> TCM (Maybe Term, WithFunctionProblem)
    forall a b. (a -> b) -> a -> b
    $ [RewriteEqn]
    -> [ProblemEq]
    -> RHS
    -> WhereDeclarations
    -> TCM (Maybe Term, WithFunctionProblem)
    rewriteEqnsRHS [RewriteEqn]
    rs [ProblemEq]
    strippedPats RHS
    rhs WhereDeclarations
    wh

        -- @invert@ clauses
        invertEqnRHS :: QName -> List1 (Named A.BindName (A.Pattern,A.Expr)) -> [A.RewriteEqn] -> TCM (Maybe Term, WithFunctionProblem)
        invertEqnRHS :: QName
    -> List1 (Named BindName (Pattern' Expr, Expr))
    -> [RewriteEqn]
    -> TCM (Maybe Term, WithFunctionProblem)
    invertEqnRHS QName
    qname List1 (Named BindName (Pattern' Expr, Expr))
    pes [RewriteEqn]
    rs = do

          let (List1 (Named BindName (Pattern' Expr))
    npats, List1 (Named BindName Expr)
    es) = (Named BindName (Pattern' Expr, Expr)
     -> (Named BindName (Pattern' Expr), Named BindName Expr))
    -> List1 (Named BindName (Pattern' Expr, Expr))
    -> (List1 (Named BindName (Pattern' Expr)),
        List1 (Named BindName Expr))
    forall a b c. (a -> (b, c)) -> List1 a -> (List1 b, List1 c)
    List1.unzipWith (\ (Named Maybe BindName
    nm (Pattern' Expr
    p , Expr
    e)) -> (Maybe BindName -> Pattern' Expr -> Named BindName (Pattern' Expr)
    forall name a. Maybe name -> a -> Named name a
    Named Maybe BindName
    nm Pattern' Expr
    p, Maybe BindName -> Expr -> Named BindName Expr
    forall name a. Maybe name -> a -> Named name a
    Named Maybe BindName
    nm Expr
    e)) List1 (Named BindName (Pattern' Expr, Expr))
    pes
          -- Infer the types of the with expressions
          vtys <- List1 (Named BindName Expr)
    -> (Named BindName Expr -> TCMT IO (Arg (Term, EqualityView)))
    -> TCMT IO (List1 (Arg (Term, EqualityView)))
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    t a -> (a -> m b) -> m (t b)
    forM List1 (Named BindName Expr)
    es ((Named BindName Expr -> TCMT IO (Arg (Term, EqualityView)))
     -> TCMT IO (List1 (Arg (Term, EqualityView))))
    -> (Named BindName Expr -> TCMT IO (Arg (Term, EqualityView)))
    -> TCMT IO (List1 (Arg (Term, EqualityView)))
    forall a b. (a -> b) -> a -> b
    $ \ (Named Maybe BindName
    nm Expr
    we) -> do
            (e, ty) <- Arg Expr -> TCM (Term, Type)
    inferExprForWith (Expr -> Arg Expr
    forall a. a -> Arg a
    defaultArg Expr
    we)
            pure $ defaultArg . (e,) $ case nm of
              Maybe BindName
    Nothing -> Type -> EqualityView
    OtherType Type
    ty
              Just{}  -> Type -> EqualityView
    IdiomType Type
    ty

          let pats = (Pattern' Expr -> Arg (Pattern' Expr))
    -> NonEmpty (Pattern' Expr) -> List1 (Arg (Pattern' Expr))
    forall a b. (a -> b) -> NonEmpty a -> NonEmpty b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap Pattern' Expr -> Arg (Pattern' Expr)
    forall a. a -> Arg a
    defaultArg (NonEmpty (Pattern' Expr) -> List1 (Arg (Pattern' Expr)))
    -> NonEmpty (Pattern' Expr) -> List1 (Arg (Pattern' Expr))
    forall a b. (a -> b) -> a -> b
    $ NonEmpty (NonEmpty (Pattern' Expr)) -> NonEmpty (Pattern' Expr)
    forall a. Semigroup a => NonEmpty a -> a
    sconcat (NonEmpty (NonEmpty (Pattern' Expr)) -> NonEmpty (Pattern' Expr))
    -> NonEmpty (NonEmpty (Pattern' Expr)) -> NonEmpty (Pattern' Expr)
    forall a b. (a -> b) -> a -> b
    $
                List1 (Named BindName (Pattern' Expr))
    -> (Named BindName (Pattern' Expr) -> NonEmpty (Pattern' Expr))
    -> NonEmpty (NonEmpty (Pattern' Expr))
    forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
    for List1 (Named BindName (Pattern' Expr))
    npats ((Named BindName (Pattern' Expr) -> NonEmpty (Pattern' Expr))
     -> NonEmpty (NonEmpty (Pattern' Expr)))
    -> (Named BindName (Pattern' Expr) -> NonEmpty (Pattern' Expr))
    -> NonEmpty (NonEmpty (Pattern' Expr))
    forall a b. (a -> b) -> a -> b
    $ \ (Named Maybe BindName
    nm Pattern' Expr
    p) -> Pattern' Expr
    p Pattern' Expr -> [Pattern' Expr] -> NonEmpty (Pattern' Expr)
    forall a. a -> [a] -> NonEmpty a
    :| [Pattern' Expr]
    -> (BindName -> [Pattern' Expr])
    -> Maybe BindName
    -> [Pattern' Expr]
    forall b a. b -> (a -> b) -> Maybe a -> b
    maybe [] (\ BindName
    n -> [BindName -> Pattern' Expr
    forall e. BindName -> Pattern' e
    A.VarP BindName
    n]) Maybe BindName
    nm

          -- Andreas, 2016-04-14, see also Issue #1796
          -- Run the size constraint solver to improve with-abstraction
          -- in case the with-expression contains size metas.
          solveSizeConstraints DefaultToInfty

          let rhs' = List1 (Arg (Pattern' Expr)) -> RHS -> RHS
    insertPatterns List1 (Arg (Pattern' Expr))
    pats RHS
    rhs
              (rhs'', outerWhere) -- the where clauses should go on the inner-most with
                | null rs  = (rhs', wh)
                | otherwise = (A.RewriteRHS rs strippedPats rhs' wh, A.noWhereDecls)
              -- Andreas, 2014-03-05 kill range of copied patterns
              -- since they really do not have a source location.
              cl = LHS
    -> [ProblemEq]
    -> RHS
    -> WhereDeclarations
    -> Catchall
    -> Clause' LHS
    forall lhs.
    lhs
    -> [ProblemEq]
    -> RHS
    -> WhereDeclarations
    -> Catchall
    -> Clause' lhs
    A.Clause (LHSInfo -> LHSCore' Expr -> LHS
    A.LHS LHSInfo
    i (LHSCore' Expr -> LHS) -> LHSCore' Expr -> LHS
    forall a b. (a -> b) -> a -> b
    $ List1 (Arg (Pattern' Expr)) -> LHSCore' Expr -> LHSCore' Expr
    insertPatternsLHSCore List1 (Arg (Pattern' Expr))
    pats (LHSCore' Expr -> LHSCore' Expr) -> LHSCore' Expr -> LHSCore' Expr
    forall a b. (a -> b) -> a -> b
    $ QName -> [NamedArg (Pattern' Expr)] -> LHSCore' Expr
    forall e. QName -> [NamedArg (Pattern' e)] -> LHSCore' e
    A.LHSHead QName
    x ([NamedArg (Pattern' Expr)] -> LHSCore' Expr)
    -> [NamedArg (Pattern' Expr)] -> LHSCore' Expr
    forall a b. (a -> b) -> a -> b
    $ [NamedArg (Pattern' Expr)] -> [NamedArg (Pattern' Expr)]
    forall a. KillRange a => KillRangeT a
    killRange [NamedArg (Pattern' Expr)]
    aps)
                     [ProblemEq]
    strippedPats RHS
    rhs'' WhereDeclarations
    outerWhere Catchall
    forall a. Null a => a
    empty

          reportSDoc "tc.invert" 60 $ vcat
            [ text "invert"
            , "  rhs' = " <> (text . show) rhs'
            ]
          checkWithRHS x qname t lhsResult vtys $ singleton cl

        -- @rewrite@ clauses
        rewriteEqnRHS
          :: QName
          -> A.Expr
          -> [A.RewriteEqn]
          -> TCM (Maybe Term, WithFunctionProblem)
        rewriteEqnRHS :: QName
    -> Expr -> [RewriteEqn] -> TCM (Maybe Term, WithFunctionProblem)
    rewriteEqnRHS QName
    qname Expr
    eq [RewriteEqn]
    rs = do

          -- Action for skipping this rewrite.
          -- We do not want to create unsolved metas in case of
          -- a futile rewrite with a reflexive equation.
          -- Thus, we restore the state in this case,
          -- unless the rewrite expression contains questionmarks.
          st <- TCMT IO TCState
    forall (m :: * -> *). MonadTCState m => m TCState
    getTC
          -- TODO:: recurse defined but not used
          let recurse = do
               st' <- TCMT IO TCState
    forall (m :: * -> *). MonadTCState m => m TCState
    getTC
               -- Comparing the whole stInteractionPoints maps is a bit
               -- wasteful, but we assume
               -- 1. rewriting with a reflexive equality to happen rarely,
               -- 2. especially with ?-holes in the rewrite expression
               -- 3. and a large overall number of ?s.
               let sameIP = InteractionPoints -> InteractionPoints -> Bool
    forall a. Eq a => a -> a -> Bool
    (==) (InteractionPoints -> InteractionPoints -> Bool)
    -> (TCState -> InteractionPoints) -> TCState -> TCState -> Bool
    forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
    `on` (TCState -> Lens' TCState InteractionPoints -> InteractionPoints
    forall o i. o -> Lens' o i -> i
    ^. (InteractionPoints -> f InteractionPoints) -> TCState -> f TCState
    Lens' TCState InteractionPoints
    stInteractionPoints)
               when (sameIP st st') $ putTC st
               handleRHS $ A.RewriteRHS rs strippedPats rhs wh

          -- Get value and type of rewrite-expression.

          (proof, eqt) <- inferExpr eq

          -- Andreas, 2024-02-27, issue #7150
          -- trigger instance search to resolve instances in rewrite-expression
          solveAwakeConstraints

          -- Andreas, 2016-04-14, see also Issue #1796
          -- Run the size constraint solver to improve with-abstraction
          -- in case the with-expression contains size metas.
          solveSizeConstraints DefaultToInfty

          -- Check that the type is actually an equality (lhs ≡ rhs)
          -- and extract lhs, rhs, and their type.

          t' <- reduce =<< instantiateFull eqt
          (eqt, rewriteType, rewriteFrom, rewriteTo) <- equalityView (getRange eq) t' >>= \case
            eqt :: EqualityView
    eqt@(EqualityType Range
    _r Sort
    _s QName
    _eq [Arg Term]
    _params (Arg ArgInfo
    _ Term
    dom) Arg Term
    a Arg Term
    b) -> do
              s <- Term -> TCMT IO Sort
    forall (m :: * -> *).
    (PureTCM m, MonadBlock m, MonadConstraint m) =>
    Term -> m Sort
    sortOf Term
    dom
              return (eqt, El s dom, unArg a, unArg b)
              -- Note: the sort _s of the equality need not be the sort of the type @dom@!
            OtherType{} -> TypeError -> TCMT IO (EqualityView, Type, Term, Term)
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    TypeError -> m a
    typeError (TypeError -> TCMT IO (EqualityView, Type, Term, Term))
    -> TypeError -> TCMT IO (EqualityView, Type, Term, Term)
    forall a b. (a -> b) -> a -> b
    $ Type -> TypeError
    CannotRewriteByNonEquation Type
    t'
            IdiomType{} -> TypeError -> TCMT IO (EqualityView, Type, Term, Term)
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    TypeError -> m a
    typeError (TypeError -> TCMT IO (EqualityView, Type, Term, Term))
    -> TypeError -> TCMT IO (EqualityView, Type, Term, Term)
    forall a b. (a -> b) -> a -> b
    $ Type -> TypeError
    CannotRewriteByNonEquation Type
    t'

          reflPat <- getReflPattern

          -- Andreas, 2015-12-25  Issue #1740:
          -- After the fix of #520, rewriting with a reflexive equation
          -- has to be desugared as matching against refl.
          let isReflexive = TCM () -> TCMT IO Bool
    forall (m :: * -> *).
    (MonadConstraint m, MonadWarning m, MonadError TCErr m,
     MonadFresh ProblemId m) =>
    m () -> m Bool
    tryConversion (TCM () -> TCMT IO Bool) -> TCM () -> TCMT IO Bool
    forall a b. (a -> b) -> a -> b
    $ TCM () -> TCM ()
    forall (m :: * -> *) a.
    (MonadTCEnv m, HasOptions m, MonadDebug m) =>
    m a -> m a
    dontAssignMetas (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $
               Type -> Term -> Term -> TCM ()
    forall (m :: * -> *).
    MonadConversion m =>
    Type -> Term -> Term -> m ()
    equalTerm Type
    rewriteType Term
    rewriteFrom Term
    rewriteTo

          (pats', withExpr, withType) <- do
            ifM isReflexive
              {-then-} (return (                      reflPat :| [], proof, OtherType t'))
              {-else-} (return (A.WildP patNoRange <| reflPat :| [], proof, eqt))
          let pats = Pattern' Expr -> Arg (Pattern' Expr)
    forall a. a -> Arg a
    defaultArg (Pattern' Expr -> Arg (Pattern' Expr))
    -> NonEmpty (Pattern' Expr) -> List1 (Arg (Pattern' Expr))
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> NonEmpty (Pattern' Expr)
    pats'

          let rhs' = List1 (Arg (Pattern' Expr)) -> RHS -> RHS
    insertPatterns List1 (Arg (Pattern' Expr))
    pats RHS
    rhs
              (rhs'', outerWhere) -- the where clauses should go on the inner-most with
                | null rs  = (rhs', wh)
                | otherwise = (A.RewriteRHS rs strippedPats rhs' wh, A.noWhereDecls)
              -- Andreas, 2014-03-05 kill range of copied patterns
              -- since they really do not have a source location.
              cl = LHS
    -> [ProblemEq]
    -> RHS
    -> WhereDeclarations
    -> Catchall
    -> Clause' LHS
    forall lhs.
    lhs
    -> [ProblemEq]
    -> RHS
    -> WhereDeclarations
    -> Catchall
    -> Clause' lhs
    A.Clause (LHSInfo -> LHSCore' Expr -> LHS
    A.LHS LHSInfo
    i (LHSCore' Expr -> LHS) -> LHSCore' Expr -> LHS
    forall a b. (a -> b) -> a -> b
    $ List1 (Arg (Pattern' Expr)) -> LHSCore' Expr -> LHSCore' Expr
    insertPatternsLHSCore List1 (Arg (Pattern' Expr))
    pats (LHSCore' Expr -> LHSCore' Expr) -> LHSCore' Expr -> LHSCore' Expr
    forall a b. (a -> b) -> a -> b
    $ QName -> [NamedArg (Pattern' Expr)] -> LHSCore' Expr
    forall e. QName -> [NamedArg (Pattern' e)] -> LHSCore' e
    A.LHSHead QName
    x ([NamedArg (Pattern' Expr)] -> LHSCore' Expr)
    -> [NamedArg (Pattern' Expr)] -> LHSCore' Expr
    forall a b. (a -> b) -> a -> b
    $ [NamedArg (Pattern' Expr)] -> [NamedArg (Pattern' Expr)]
    forall a. KillRange a => KillRangeT a
    killRange [NamedArg (Pattern' Expr)]
    aps)
                     [ProblemEq]
    strippedPats RHS
    rhs'' WhereDeclarations
    outerWhere Catchall
    forall a. Null a => a
    empty

          reportSDoc "tc.rewrite" 60 $ vcat
            [ text "rewrite"
            , "  rhs' = " <> (text . show) rhs'
            ]
          checkWithRHS x qname t lhsResult (singleton $ defaultArg (withExpr, withType)) $ singleton cl

    checkWithRHS
      :: QName                             -- ^ Name of function.
      -> QName                             -- ^ Name of the with-function.
      -> Type                              -- ^ Type of function.
      -> LHSResult                         -- ^ Result of type-checking patterns
      -> List1 (Arg (Term, EqualityView))  -- ^ Expressions and types of with-expressions.
      -> List1 A.Clause                    -- ^ With-clauses to check.
      -> TCM (Maybe Term, WithFunctionProblem)
                                    -- Note: as-bindings already bound (in checkClause)
    checkWithRHS :: QName
    -> QName
    -> Type
    -> LHSResult
    -> List1 (Arg (Term, EqualityView))
    -> List1 (Clause' LHS)
    -> TCM (Maybe Term, WithFunctionProblem)
    checkWithRHS QName
    x QName
    aux Type
    t (LHSResult Int
    npars Tele (Dom Type)
    delta [NamedArg DeBruijnPattern]
    ps Bool
    _absurdPat Arg Type
    trhs Substitution
    _ [AsBinding]
    _asb IntSet
    _ Bool
    _) List1 (Arg (Term, EqualityView))
    vtys0 List1 (Clause' LHS)
    cs =
      [Char]
    -> Int
    -> [Char]
    -> TCM (Maybe Term, WithFunctionProblem)
    -> TCM (Maybe Term, WithFunctionProblem)
    forall a. [Char] -> Int -> [Char] -> TCMT IO a -> TCMT IO a
    forall (m :: * -> *) a.
    MonadDebug m =>
    [Char] -> Int -> [Char] -> m a -> m a
    verboseBracket [Char]
    "tc.with.top" Int
    25 [Char]
    "checkWithRHS" (TCM (Maybe Term, WithFunctionProblem)
     -> TCM (Maybe Term, WithFunctionProblem))
    -> TCM (Maybe Term, WithFunctionProblem)
    -> TCM (Maybe Term, WithFunctionProblem)
    forall a b. (a -> b) -> a -> b
    $ do
        Account (BenchPhase (TCMT IO))
    -> TCM (Maybe Term, WithFunctionProblem)
    -> TCM (Maybe Term, WithFunctionProblem)
    forall (m :: * -> *) c.
    MonadBench m =>
    Account (BenchPhase m) -> m c -> m c
    Bench.billTo [BenchPhase (TCMT IO)
    Phase
    Bench.Typing, BenchPhase (TCMT IO)
    Phase
    Bench.With] (TCM (Maybe Term, WithFunctionProblem)
     -> TCM (Maybe Term, WithFunctionProblem))
    -> TCM (Maybe Term, WithFunctionProblem)
    -> TCM (Maybe Term, WithFunctionProblem)
    forall a b. (a -> b) -> a -> b
    $ do
            withArgs <- List1 (Arg (Term, EqualityView)) -> TCM (List1 (Arg Term))
    withArguments List1 (Arg (Term, EqualityView))
    vtys0
            let perm = Permutation -> Maybe Permutation -> Permutation
    forall a. a -> Maybe a -> a
    fromMaybe Permutation
    forall a. HasCallStack => a
    __IMPOSSIBLE__ (Maybe Permutation -> Permutation)
    -> Maybe Permutation -> Permutation
    forall a b. (a -> b) -> a -> b
    $ [NamedArg DeBruijnPattern] -> Maybe Permutation
    dbPatPerm [NamedArg DeBruijnPattern]
    ps

            reportSDoc "tc.with.top" 30 $ vcat $
              -- declared locally because we do not want to use the unzip'd thing!
              let (vs, as) = List1.unzipWith unArg vtys0 in
              [ "vs (before normalization) =" <+> prettyTCM vs
              , "as (before normalization) =" <+> prettyTCM as
              ]
            reportSDoc "tc.with.top" 45 $ vcat $
              -- declared locally because we do not want to use the unzip'd thing!
              let (vs, as) = List1.unzipWith unArg vtys0 in
              [ "vs (before norm., raw) =" <+> pretty vs
              ]
            vtys0 <- normalise vtys0

            -- Andreas, 2012-09-17: for printing delta,
            -- we should remove it from the context first
            reportSDoc "tc.with.top" 25 $ escapeContext impossible (size delta) $ vcat
              [ "delta  =" <+> prettyTCM delta
              ]
            reportSDoc "tc.with.top" 25 $ vcat $
              -- declared locally because we do not want to use the unzip'd thing!
              let (vs, as) = List1.unzipWith unArg vtys0 in
              [ "vs     =" <+> prettyTCM vs
              , "as     =" <+> prettyTCM as
              , "perm   =" <+> text (show perm)
              ]

            -- Split the telescope into the part needed to type the with arguments
            -- and all the other stuff
            let (delta1, delta2, perm', t', vtys) = splitTelForWith delta (unArg trhs) vtys0
            let finalPerm = Permutation -> Permutation -> Permutation
    composeP Permutation
    perm' Permutation
    perm

            reportSLn "tc.with.top" 75 $ "delta  = " ++ show delta

            -- Andreas, 2012-09-17: for printing delta,
            -- we should remove it from the context first
            reportSDoc "tc.with.top" 25 $ escapeContext impossible (size delta) $ vcat
              [ "delta1 =" <+> prettyTCM delta1
              , "delta2 =" <+> addContext delta1 (prettyTCM delta2)
              ]
            reportSDoc "tc.with.top" 25 $ vcat
              [ "perm'  =" <+> text (show perm')
              , "fPerm  =" <+> text (show finalPerm)
              ]

            -- Create the body of the original function

            -- All the context variables
            us <- getContextTerms
            let n = [Term] -> Int
    forall a. Sized a => a -> Int
    size [Term]
    us
                m = Tele (Dom Type) -> Int
    forall a. Sized a => a -> Int
    size Tele (Dom Type)
    delta
                -- First the variables bound outside this definition
                (us0, us1') = splitAt (n - m) us
                -- Then permute the rest and grab those needed to for the with arguments
                (us1, us2)  = splitAt (size delta1) $ permute perm' us1'
                -- Now stuff the with arguments in between and finish with the remaining variables
                argsS = [Term] -> Substitution
    forall a. DeBruijn a => [a] -> Substitution' a
    parallelS ([Term] -> Substitution) -> [Term] -> Substitution
    forall a b. (a -> b) -> a -> b
    $ [Term] -> [Term]
    forall a. [a] -> [a]
    reverse ([Term] -> [Term]) -> [Term] -> [Term]
    forall a b. (a -> b) -> a -> b
    $ [Term]
    us0 [Term] -> [Term] -> [Term]
    forall a. [a] -> [a] -> [a]
    ++ [Term]
    us1 [Term] -> [Term] -> [Term]
    forall a. [a] -> [a] -> [a]
    ++ (Arg Term -> Term) -> [Arg Term] -> [Term]
    forall a b. (a -> b) -> [a] -> [b]
    map Arg Term -> Term
    forall e. Arg e -> e
    unArg (List1 (Arg Term) -> [Item (List1 (Arg Term))]
    forall l. IsList l => l -> [Item l]
    List1.toList List1 (Arg Term)
    withArgs) [Term] -> [Term] -> [Term]
    forall a. [a] -> [a] -> [a]
    ++ [Term]
    us2
                v         = Maybe a
    forall a. Maybe a
    Nothing -- generated by checkWithFunction
            -- Andreas, 2013-02-26 add with-name to signature for printing purposes
            addConstant aux =<< do
              lang <- getLanguage
              useTerPragma =<<
                defaultDefn defaultArgInfo aux __DUMMY_TYPE__ lang <$>
                  emptyFunction

            reportSDoc "tc.with.top" 20 $ vcat $
              let (vs, as) = List1.unzipWith unArg vtys in
              -- Andreas, 2025-04-07, escapeContext impossible Δ leads to crash if e.g. vs has metas defined in Δ.
              -- Thus, we use unsafeEscapeContext instead.
              [ "    with arguments" <+> do unsafeEscapeContext (size delta) $ addContext delta1 $ prettyList (fmap prettyTCM vs)
              , "             types" <+> do unsafeEscapeContext (size delta) $ addContext delta1 $ prettyList (fmap prettyTCM as)
              , "           context" <+> (prettyTCM =<< getContextTelescope)
              , "             delta" <+> do escapeContext impossible (size delta) $ prettyTCM delta
              , "            delta1" <+> do escapeContext impossible (size delta) $ prettyTCM delta1
              , "            delta2" <+> do escapeContext impossible (size delta) $ addContext delta1 $ prettyTCM delta2
              ]

            -- Only inherit user-written let bindings from parent clauses. Others, like @-patterns,
            -- should not be carried over.
            lets <- Map.filter ((== UserWritten) . letOrigin) <$> (traverse getOpen =<< viewTC eLetBindings)

            return (v, WithFunction x aux t delta delta1 delta2 vtys t' ps npars perm' perm finalPerm cs argsS lets)

    -- | Invoked in empty context.
    checkWithFunction :: [Name] -> WithFunctionProblem -> TCM (Maybe Term)
    checkWithFunction :: [Name] -> WithFunctionProblem -> TCMT IO (Maybe Term)
    checkWithFunction [Name]
    _ WithFunctionProblem
    NoWithFunction = Maybe Term -> TCMT IO (Maybe Term)
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Maybe Term
    forall a. Maybe a
    Nothing
    checkWithFunction [Name]
    cxtNames (WithFunction QName
    f QName
    aux Type
    t Tele (Dom Type)
    delta Tele (Dom Type)
    delta1 Tele (Dom Type)
    delta2 List1 (Arg (Term, EqualityView))
    vtys Type
    b [NamedArg DeBruijnPattern]
    qs Int
    npars Permutation
    perm' Permutation
    perm Permutation
    finalPerm List1 (Clause' LHS)
    cs Substitution
    argsS Map Name LetBinding
    lets) = do
      let -- Δ₁ ws Δ₂ ⊢ withSub : Δ′    (where Δ′ is the context of the parent lhs)
          withSub :: Substitution
          withSub :: Substitution
    withSub = let as :: List1 EqualityView
    as = (Arg (Term, EqualityView) -> EqualityView)
    -> List1 (Arg (Term, EqualityView)) -> List1 EqualityView
    forall a b. (a -> b) -> NonEmpty a -> NonEmpty b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap ((Term, EqualityView) -> EqualityView
    forall a b. (a, b) -> b
    snd ((Term, EqualityView) -> EqualityView)
    -> (Arg (Term, EqualityView) -> (Term, EqualityView))
    -> Arg (Term, EqualityView)
    -> EqualityView
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Arg (Term, EqualityView) -> (Term, EqualityView)
    forall e. Arg e -> e
    unArg) List1 (Arg (Term, EqualityView))
    vtys in
                    Int -> Substitution -> Substitution
    forall a. Int -> Substitution' a -> Substitution' a
    liftS (Tele (Dom Type) -> Int
    forall a. Sized a => a -> Int
    size Tele (Dom Type)
    delta2) (Int -> Substitution -> Substitution
    forall a. Int -> Substitution' a -> Substitution' a
    wkS (List1 EqualityView -> Int
    forall (f :: * -> *).
    (Functor f, Foldable f) =>
    f EqualityView -> Int
    countWithArgs List1 EqualityView
    as) Substitution
    forall a. Substitution' a
    idS)
                    Substitution -> Substitution -> Substitution
    forall a.
    EndoSubst a =>
    Substitution' a -> Substitution' a -> Substitution' a
    `composeS` Impossible -> Permutation -> Substitution
    forall a.
    DeBruijn a =>
    Impossible -> Permutation -> Substitution' a
    renaming Impossible
    HasCallStack => Impossible
    impossible (Permutation -> Permutation
    reverseP Permutation
    perm')

      [Char] -> Int -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "tc.with.top" 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
    "checkWithFunction"
        , 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] -> TCMT IO Doc) -> [TCMT IO Doc] -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $
          let (List1 Term
    vs, List1 EqualityView
    as) = (Arg (Term, EqualityView) -> (Term, EqualityView))
    -> List1 (Arg (Term, EqualityView))
    -> (List1 Term, List1 EqualityView)
    forall a b c. (a -> (b, c)) -> List1 a -> (List1 b, List1 c)
    List1.unzipWith Arg (Term, EqualityView) -> (Term, EqualityView)
    forall e. Arg e -> e
    unArg List1 (Arg (Term, EqualityView))
    vtys in
          [ TCMT IO Doc
    "delta1 =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Tele (Dom Type) -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => Tele (Dom Type) -> m Doc
    prettyTCM Tele (Dom Type)
    delta1
          , TCMT IO Doc
    "delta2 =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Tele (Dom Type) -> TCMT IO Doc -> TCMT IO Doc
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    forall (m :: * -> *) a.
    MonadAddContext m =>
    Tele (Dom Type) -> m a -> m a
    addContext Tele (Dom Type)
    delta1 (Tele (Dom Type) -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => Tele (Dom Type) -> m Doc
    prettyTCM Tele (Dom Type)
    delta2)
          , TCMT IO Doc
    "t      =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Type -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => Type -> m Doc
    prettyTCM Type
    t
          , TCMT IO Doc
    "as     =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Tele (Dom Type) -> TCMT IO Doc -> TCMT IO Doc
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    forall (m :: * -> *) a.
    MonadAddContext m =>
    Tele (Dom Type) -> m a -> m a
    addContext Tele (Dom Type)
    delta1 (List1 EqualityView -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => List1 EqualityView -> m Doc
    prettyTCM List1 EqualityView
    as)
          , TCMT IO Doc
    "vs     =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> do Tele (Dom Type) -> TCMT IO Doc -> TCMT IO Doc
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    forall (m :: * -> *) a.
    MonadAddContext m =>
    Tele (Dom Type) -> m a -> m a
    addContext Tele (Dom Type)
    delta1 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ List1 Term -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => List1 Term -> m Doc
    prettyTCM List1 Term
    vs
          , TCMT IO Doc
    "b      =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> do Tele (Dom Type) -> TCMT IO Doc -> TCMT IO Doc
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    forall (m :: * -> *) a.
    MonadAddContext m =>
    Tele (Dom Type) -> m a -> m a
    addContext Tele (Dom Type)
    delta1 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ Tele (Dom Type) -> TCMT IO Doc -> TCMT IO Doc
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    forall (m :: * -> *) a.
    MonadAddContext m =>
    Tele (Dom Type) -> m a -> m a
    addContext Tele (Dom Type)
    delta2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ Type -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => Type -> m Doc
    prettyTCM Type
    b
          , TCMT IO Doc
    "qs     =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> do Tele (Dom Type) -> TCMT IO Doc -> TCMT IO Doc
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    forall (m :: * -> *) a.
    MonadAddContext m =>
    Tele (Dom Type) -> m a -> m a
    addContext Tele (Dom Type)
    delta (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ [NamedArg DeBruijnPattern] -> TCMT IO Doc
    forall (m :: * -> *).
    MonadPretty m =>
    [NamedArg DeBruijnPattern] -> m Doc
    prettyTCMPatternList [NamedArg DeBruijnPattern]
    qs
          , TCMT IO Doc
    "perm'  =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> [Char] -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => [Char] -> m Doc
    text (Permutation -> [Char]
    forall a. Show a => a -> [Char]
    show Permutation
    perm')
          , TCMT IO Doc
    "perm   =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> [Char] -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => [Char] -> m Doc
    text (Permutation -> [Char]
    forall a. Show a => a -> [Char]
    show Permutation
    perm)
          , TCMT IO Doc
    "fperm  =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> [Char] -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => [Char] -> m Doc
    text (Permutation -> [Char]
    forall a. Show a => a -> [Char]
    show Permutation
    finalPerm)
          , TCMT IO Doc
    "withSub=" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> [Char] -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => [Char] -> m Doc
    text (Substitution -> [Char]
    forall a. Show a => a -> [Char]
    show Substitution
    withSub)
          ]
        ]

      -- Add the type of the auxiliary function to the signature

      -- Jesper, 2020-04-05: Currently variable generalization inserts
      -- dummy terms, we have to reduce projections to get rid of them.
      -- (see also #1332).
      let reds :: SmallSet AllowedReduction
    reds = [AllowedReduction] -> SmallSet AllowedReduction
    forall a. SmallSetElement a => [a] -> SmallSet a
    SmallSet.fromList [AllowedReduction
    ProjectionReductions]
      delta1 <- (SmallSet AllowedReduction -> SmallSet AllowedReduction)
    -> TCMT IO (Tele (Dom Type)) -> TCMT IO (Tele (Dom Type))
    forall (m :: * -> *) a.
    MonadTCEnv m =>
    (SmallSet AllowedReduction -> SmallSet AllowedReduction)
    -> m a -> m a
    modifyAllowedReductions (SmallSet AllowedReduction
    -> SmallSet AllowedReduction -> SmallSet AllowedReduction
    forall a b. a -> b -> a
    const SmallSet AllowedReduction
    reds) (TCMT IO (Tele (Dom Type)) -> TCMT IO (Tele (Dom Type)))
    -> TCMT IO (Tele (Dom Type)) -> TCMT IO (Tele (Dom Type))
    forall a b. (a -> b) -> a -> b
    $ Tele (Dom Type) -> TCMT IO (Tele (Dom Type))
    forall a (m :: * -> *). (Normalise a, MonadReduce m) => a -> m a
    normalise Tele (Dom Type)
    delta1

      -- Amy, 2025-05-14: (InstanceHack) we have to flush instances that may
      -- come from previous clauses, see #7882.
      flushInstanceConstraints

      -- Generate the type of the with function
      (withFunType, (nwithargs, nwithpats)) <- do
        let ps = Impossible -> Permutation -> Substitution' DeBruijnPattern
    forall a.
    DeBruijn a =>
    Impossible -> Permutation -> Substitution' a
    renaming Impossible
    HasCallStack => Impossible
    impossible (Permutation -> Permutation
    reverseP Permutation
    perm') Substitution' (SubstArg [NamedArg DeBruijnPattern])
    -> [NamedArg DeBruijnPattern] -> [NamedArg DeBruijnPattern]
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    `applySubst` [NamedArg DeBruijnPattern]
    qs
        reportSDoc "tc.with.bndry" 40 $ addContext delta1 $ addContext delta2
                                      $ text "ps =" <+> pretty ps
        let vs = [NamedArg DeBruijnPattern] -> [Int]
    forall p. IApplyVars p => p -> [Int]
    iApplyVars [NamedArg DeBruijnPattern]
    ps
        bndry <- if null vs then return empty else do
          iz <- primIZero
          io <- primIOne
          let tm = QName -> Elims -> Term
    Def QName
    f ([NamedArg DeBruijnPattern] -> Elims
    patternsToElims [NamedArg DeBruijnPattern]
    ps)
          return $ Boundary [(i,(inplaceS i iz `applySubst` tm, inplaceS i io `applySubst` tm)) | i <- vs]
        reportSDoc "tc.with.bndry" 40 $ addContext delta1 $ addContext delta2
                                      $ text "bndry =" <+> pretty bndry
        withFunctionType delta1 vtys delta2 b bndry
      reportSDoc "tc.with.type" 10 $ sep [ "with-function type:", nest 2 $ prettyTCM withFunType ]
      reportSDoc "tc.with.type" 50 $ sep [ "with-function type:", nest 2 $ pretty withFunType ]

      call_in_parent <- do
        (TelV tel _,bs) <- telViewUpToPathBoundary' (nwithargs + size delta) withFunType
        return $ argsS `applySubst` Def aux (teleElims tel bs)

      reportSDoc "tc.with.top" 20 $ addContext delta $ "with function call" <+> prettyTCM call_in_parent

      -- Andreas, 2013-10-21
      -- Check generated type directly in internal syntax.
      setCurrentRange cs $
        traceCall NoHighlighting $   -- To avoid flicker.
        traceCall (CheckWithFunctionType withFunType) $
        -- Jesper, 2024-07-10, issue #6841:
        -- Having an ill-typed type can lead to problems in the
        -- coverage checker, so we ensure there are no constraints here.
        noConstraints $ checkType withFunType

      reportSLn "tc.with.top" 20 "creating with display form..."

      -- With display forms are closed
      df <- inTopContext $ makeOpen =<< withDisplayForm f aux delta1 delta2 nwithargs qs perm' perm

      reportSLn "tc.with.top" 20 "created with display form"

      case dget df of
        Display Int
    n Elims
    ts DisplayTerm
    dt ->
          [Char] -> Int -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "tc.with.top" Int
    20 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Doc
    "Display" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> [TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    fsep
            [ [Char] -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => [Char] -> m Doc
    text (Int -> [Char]
    forall a. Show a => a -> [Char]
    show Int
    n)
            , [TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    prettyList ([TCMT IO Doc] -> TCMT IO Doc) -> [TCMT IO Doc] -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ (Elim -> TCMT IO Doc) -> Elims -> [TCMT IO Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map Elim -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => Elim -> m Doc
    prettyTCM Elims
    ts
            , DisplayTerm -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => DisplayTerm -> m Doc
    prettyTCM DisplayTerm
    dt
            ]
      addConstant aux =<< do
        lang <- getLanguage
        fun  <- emptyFunction
        useTerPragma $
          (defaultDefn defaultArgInfo aux withFunType lang fun)
            { defDisplay = [df] }
      -- solveSizeConstraints -- Andreas, 2012-10-16 does not seem necessary

      reportSDoc "tc.with.top" 10 $ sep
        [ "added with function" <+> (prettyTCM aux) <+> "of type"
        , nest 2 $ prettyTCM withFunType
        , nest 2 $ "-|" <+> (prettyTCM =<< getContextTelescope)
        ]
      reportSDoc "tc.with.top" 70 $ vcat
        [ nest 2 $ text $ "raw with func. type = " ++ show withFunType
        ]

      -- Construct the body for the with function
      cs <- return $ fmap (A.lhsToSpine) cs
      cs <- buildWithFunction cxtNames f aux t delta qs npars withSub finalPerm (size delta1) nwithpats cs
      cs <- return $ fmap (A.spineToLhs) cs

      -- #4833: inherit abstract mode from parent
      abstr <- defAbstract <$> ignoreAbstractMode (getConstInfo f)

      -- Check the with function
      let info = Name -> Fixity' -> Access -> IsAbstract -> Range -> DefInfo
    forall t.
    Name -> Fixity' -> Access -> IsAbstract -> Range -> DefInfo' t
    Info.mkDefInfo (Name -> Name
    nameConcrete (Name -> Name) -> Name -> Name
    forall a b. (a -> b) -> a -> b
    $ QName -> Name
    qnameName QName
    aux) Fixity'
    noFixity' Access
    PublicAccess IsAbstract
    abstr (List1 (Clause' LHS) -> Range
    forall a. HasRange a => a -> Range
    getRange List1 (Clause' LHS)
    cs)
      ai <- defArgInfo <$> getConstInfo f
      checkFunDefS withFunType ai Nothing (Just f) info aux (Just (withSub, lets)) $ List1.toList cs
      return $ Just $ call_in_parent

    -- | Type check a where clause.
    checkWhere
      :: A.WhereDeclarations -- ^ Where-declarations to check.
      -> TCM a               -- ^ Continuation.
      -> TCM a
    checkWhere :: forall a. WhereDeclarations -> TCM a -> TCM a
    checkWhere wh :: WhereDeclarations
    wh@(A.WhereDecls Maybe ModuleName
    whmod Bool
    whNamed Maybe Declaration
    mds) TCM a
    ret = do
      Bool -> TCM () -> TCM ()
    forall b (m :: * -> *). (IsBool b, Monad m) => b -> m () -> m ()
    when (Bool -> Bool
    not Bool
    whNamed) (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ Maybe ModuleName -> TCM ()
    forall {m :: * -> *}.
    (MonadTrace m, HasOptions m, MonadDebug m, MonadError TCErr m) =>
    Maybe ModuleName -> m ()
    ensureNoNamedWhereInRefinedContext Maybe ModuleName
    whmod
      case Maybe Declaration
    mds of
          Maybe Declaration
    Nothing -> TCM a
    ret
          Just (A.Section Range
    _ Erased
    e ModuleName
    m GeneralizeTelescope
    tel [Declaration]
    ds) -> do

            -- Andreas, 2025-06-14, issue #7943.
            -- If we are in erased context, mark the module as erased.
            e <- case Erased
    e of
              NotErased QωOrigin
    oo -> do
                (TCEnv -> Quantity) -> TCMT IO Quantity
    forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
    asksTC TCEnv -> Quantity
    envQuantity TCMT IO Quantity -> (Quantity -> TCMT IO Erased) -> TCMT IO Erased
    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
                  Quantity0 Q0Origin
    o -> do
                    Bool -> TCM () -> TCM ()
    forall b (m :: * -> *). (IsBool b, Monad m) => b -> m () -> m ()
    unless (QωOrigin
    oo QωOrigin -> QωOrigin -> Bool
    forall a. Eq a => a -> a -> Bool
    == QωOrigin
    QωInferred) (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $
                      QωOrigin -> TCM () -> TCM ()
    forall (m :: * -> *) x a.
    (MonadTrace m, HasRange x) =>
    x -> m a -> m a
    setCurrentRange QωOrigin
    oo (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ 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
    oo
                    Erased -> TCMT IO Erased
    forall a. a -> TCMT IO a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Erased -> TCMT IO Erased) -> Erased -> TCMT IO Erased
    forall a b. (a -> b) -> a -> b
    $ Q0Origin -> Erased
    Erased Q0Origin
    o
                  Quantityω{} -> Erased -> TCMT IO Erased
    forall a. a -> TCMT IO a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Erased
    e
                  Quantity1{} -> TCMT IO Erased
    forall a. HasCallStack => a
    __IMPOSSIBLE__
              Erased{}      -> Erased -> TCMT IO Erased
    forall a. a -> TCMT IO a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Erased
    e

            localTC whereEnv $ newSection e m tel $ checkDecls ds
            -- Andreas, 2025-06-14, issue #7944
            -- We need to check the body in its original erasure status.
            withCurrentModule m ret
          Maybe Declaration
    _ -> TCM a
    forall a. HasCallStack => a
    __IMPOSSIBLE__
      where
        whereEnv :: TCEnv -> TCEnv
    whereEnv TCEnv
    e = TCEnv
    e
          { envCheckingWhere       = if whNamed then C.SomeWhere_ else C.AnyWhere_
          }
        -- #2897: We can't handle named where-modules in refined contexts.
        ensureNoNamedWhereInRefinedContext :: Maybe ModuleName -> m ()
    ensureNoNamedWhereInRefinedContext Maybe ModuleName
    Nothing = () -> m ()
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
        ensureNoNamedWhereInRefinedContext (Just ModuleName
    m) = Call -> m () -> m ()
    forall a. Call -> m a -> m a
    forall (m :: * -> *) a. MonadTrace m => Call -> m a -> m a
    traceCall (ModuleName -> Call
    CheckNamedWhere ModuleName
    m) (m () -> m ()) -> m () -> m ()
    forall a b. (a -> b) -> a -> b
    $ do
          args <- (Arg Term -> Term) -> [Arg Term] -> [Term]
    forall a b. (a -> b) -> [a] -> [b]
    map Arg Term -> Term
    forall e. Arg e -> e
    unArg ([Arg Term] -> [Term]) -> m [Arg Term] -> m [Term]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (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]) -> m ModuleName -> m [Arg Term]
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< m ModuleName
    forall (m :: * -> *). MonadTCEnv m => m ModuleName
    currentModule)
          unless (isWeakening args) $ do -- weakened contexts are fine
            names <- map (argNameToString . fst . unDom) . telToList <$>
                    (lookupSection =<< currentModule)
            typeError $ NamedWhereModuleInRefinedContext args names
          where
            isWeakening :: [Term] -> Bool
    isWeakening [] = Bool
    True
            isWeakening (Var Int
    i [] : [Term]
    args) = Int -> [Term] -> Bool
    isWk (Int
    i Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - Int
    1) [Term]
    args
              where
                isWk :: Int -> [Term] -> Bool
    isWk Int
    i []                = Bool
    True
                isWk Int
    i (Var Int
    j [] : [Term]
    args) = Int
    i Int -> Int -> Bool
    forall a. Eq a => a -> a -> Bool
    == Int
    j Bool -> Bool -> Bool
    && Int -> [Term] -> Bool
    isWk (Int
    i Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - Int
    1) [Term]
    args
                isWk Int
    _ [Term]
    _ = Bool
    False
            isWeakening [Term]
    _ = Bool
    False

    -- | Enter a new section during type-checking.

    newSection ::
      Erased -> ModuleName -> A.GeneralizeTelescope -> TCM a -> TCM a
    newSection :: forall a.
    Erased -> ModuleName -> GeneralizeTelescope -> TCM a -> TCM a
    newSection Erased
    e ModuleName
    m gtel :: GeneralizeTelescope
    gtel@(A.GeneralizeTel Map QName Name
    _ Telescope
    tel) TCM a
    cont = do
      -- If the section is erased, then hard compile-time mode is entered.
      Erased -> TCM ()
    warnForPlentyInHardCompileTimeMode Erased
    e
      Erased -> TCM a -> TCM a
    forall a. Erased -> TCM a -> TCM a
    setHardCompileTimeModeIfErased Erased
    e (TCM a -> TCM a) -> TCM a -> TCM a
    forall a b. (a -> b) -> a -> b
    $ do
      [Char] -> Int -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "tc.section" Int
    10 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    forall a b. (a -> b) -> a -> b
    $
        TCMT IO Doc
    "checking section" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> (Erased -> Doc -> Doc
    prettyErased Erased
    e (Doc -> Doc) -> TCMT IO Doc -> TCMT IO Doc
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> ModuleName -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => ModuleName -> m Doc
    prettyTCM ModuleName
    m) TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+>
        [TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    fsep ((TypedBinding -> TCMT IO Doc) -> Telescope -> [TCMT IO Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map TypedBinding -> TCMT IO Doc
    forall a (m :: * -> *).
    (ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
    a -> m Doc
    prettyA Telescope
    tel)

      Maybe ModuleName
    -> GeneralizeTelescope
    -> ([Maybe Name] -> Tele (Dom Type) -> TCM a)
    -> TCM a
    forall a.
    Maybe ModuleName
    -> GeneralizeTelescope
    -> ([Maybe Name] -> Tele (Dom Type) -> TCM a)
    -> TCM a
    checkGeneralizeTelescope (ModuleName -> Maybe ModuleName
    forall a. a -> Maybe a
    Just ModuleName
    m) GeneralizeTelescope
    gtel (([Maybe Name] -> Tele (Dom Type) -> TCM a) -> TCM a)
    -> ([Maybe Name] -> Tele (Dom Type) -> TCM a) -> TCM a
    forall a b. (a -> b) -> a -> b
    $ \ [Maybe Name]
    _ Tele (Dom Type)
    tel' -> do
        [Char] -> Int -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "tc.section" Int
    10 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    forall a b. (a -> b) -> a -> b
    $
          TCMT IO Doc
    "adding section:" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> ModuleName -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => ModuleName -> m Doc
    prettyTCM ModuleName
    m TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> [Char] -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => [Char] -> m Doc
    text (Int -> [Char]
    forall a. Show a => a -> [Char]
    show (Tele (Dom Type) -> Int
    forall a. Sized a => a -> Int
    size Tele (Dom Type)
    tel'))

        ModuleName -> TCM ()
    addSection ModuleName
    m

        [Char] -> Int -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "tc.section" Int
    10 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Doc -> TCMT IO Doc
    forall (tcm :: * -> *) a.
    (MonadTCEnv tcm, ReadTCState tcm) =>
    tcm a -> tcm a
    inTopContext (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
    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
    4 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Doc
    "actual tele:" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> do Tele (Dom Type) -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => Tele (Dom Type) -> m Doc
    prettyTCM (Tele (Dom Type) -> TCMT IO Doc)
    -> TCMT IO (Tele (Dom Type)) -> TCMT IO Doc
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< ModuleName -> TCMT IO (Tele (Dom Type))
    forall (m :: * -> *).
    (Functor m, ReadTCState m) =>
    ModuleName -> m (Tele (Dom Type))
    lookupSection ModuleName
    m

        ModuleName -> TCM a -> TCM a
    forall (m :: * -> *) a. MonadTCEnv m => ModuleName -> m a -> m a
    withCurrentModule ModuleName
    m TCM a
    cont

    -- | Set the current clause number.

    atClause :: QName -> Int -> Type -> Maybe Substitution -> A.SpineClause -> TCM a -> TCM a
    atClause :: forall a.
    QName
    -> Int
    -> Type
    -> Maybe Substitution
    -> SpineClause
    -> TCM a
    -> TCM a
    atClause QName
    name Int
    i Type
    t Maybe Substitution
    sub SpineClause
    cl TCM a
    ret = do
      clo <- () -> TCMT IO (Closure ())
    forall (m :: * -> *) a.
    (MonadTCEnv m, ReadTCState m) =>
    a -> m (Closure a)
    buildClosure ()
      localTC (\ TCEnv
    e -> TCEnv
    e { envClause = IPClause name i t sub cl clo }) ret