    {-# 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
    import Data.IntSet (IntSet)
    import qualified Data.IntSet as IntSet
    import qualified Data.List as List
    import Data.Maybe
    import Data.Semigroup (Semigroup((<>)))

    import Agda.Interaction.Options

    import Agda.Syntax.Common
    import qualified Agda.Syntax.Concrete 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, genericWarning )

    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.Irrelevance
    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.Sort

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

    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.Utils.Pretty ( prettyShow )
    import qualified Agda.Utils.Pretty as P
    import Agda.Utils.Size
    import qualified Agda.Utils.SmallSet as SmallSet

    import Agda.Utils.Impossible

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

    checkFunDef :: Delayed -> A.DefInfo -> QName -> [A.Clause] -> TCM ()
    checkFunDef :: Delayed -> DefInfo -> QName -> [Clause] -> TCM ()
    checkFunDef Delayed
    delayed DefInfo
    i QName
    name [Clause]
    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 NotBlocked' Term
    forall t. NotBlocked' t
    MissingClauses ()
            -- Get the type and relevance of the function
            Definition
    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 :: Type
    t    = Definition -> Type
    defType Definition
    def
            let info :: ArgInfo
    info = Definition -> ArgInfo
    forall a. LensArgInfo a => a -> ArgInfo
    getArgInfo Definition
    def
            case [Clause] -> Type -> Maybe (Expr, Maybe Expr, MetaId)
    isAlias [Clause]
    cs Type
    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
    AbstractDef ->
                  Call -> TCM () -> TCM ()
    forall (m :: * -> *) a. MonadTrace m => Call -> m a -> m a
    traceCall (Range -> QName -> [Clause] -> Bool -> Call
    CheckFunDefCall (DefInfo -> Range
    forall a. HasRange a => a -> Range
    getRange DefInfo
    i) QName
    name [Clause]
    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 :: * -> *).
    (MonadFail m, ReadTCState m) =>
    MetaId -> m Bool
    isFrozen MetaId
    x) (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ do
                      [MetaId]
    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 :: * -> *).
    (MonadFail m, ReadTCState m) =>
    MetaId -> m MetaVariable
    lookupMeta MetaId
    x
                      (MetaId -> TCM ()) -> [MetaId] -> TCM ()
    forall (t :: * -> *) (m :: * -> *) a b.
    (Foldable t, Monad m) =>
    (a -> m b) -> t a -> m ()
    mapM_ MetaId -> TCM ()
    forall a (m :: * -> *).
    (UnFreezeMeta a, MonadMetaSolver m) =>
    a -> m ()
    unfreezeMeta (MetaId
    x MetaId -> [MetaId] -> [MetaId]
    forall a. a -> [a] -> [a]
    : [MetaId]
    xs)
                    Type
    -> ArgInfo
    -> Delayed
    -> DefInfo
    -> QName
    -> Expr
    -> Maybe Expr
    -> TCM ()
    checkAlias Type
    t ArgInfo
    info Delayed
    delayed 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)
    -> (MetaVariable -> MetaInstantiation) -> MetaVariable -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . MetaVariable -> MetaInstantiation
    mvInstantiation (MetaVariable -> Bool) -> TCMT IO MetaVariable -> TCMT IO Bool
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> MetaId -> TCMT IO MetaVariable
    forall (m :: * -> *).
    (MonadFail m, ReadTCState m) =>
    MetaId -> m MetaVariable
    lookupMeta 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
    $ Doc -> TCM ()
    forall (m :: * -> *). MonadWarning m => Doc -> m ()
    genericWarning (Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<<
                      TCMT IO Doc
    "Missing type signature for abstract definition" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> (QName -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM QName
    name TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall a. Semigroup a => a -> a -> a
    <> TCMT IO Doc
    ".") TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    $$
                      [TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    fsep ([Char] -> [TCMT IO Doc]
    forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
    pwords [Char]
    "Types of abstract definitions are never inferred since this would leak" [TCMT IO Doc] -> [TCMT IO Doc] -> [TCMT IO Doc]
    forall a. [a] -> [a] -> [a]
    ++
                            [Char] -> [TCMT IO Doc]
    forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
    pwords [Char]
    "information that should be abstract.")
                  Type
    -> ArgInfo
    -> Delayed
    -> Maybe ExtLamInfo
    -> Maybe QName
    -> DefInfo
    -> QName
    -> [Clause]
    -> TCM ()
    checkFunDef' Type
    t ArgInfo
    info Delayed
    delayed Maybe ExtLamInfo
    forall a. Maybe a
    Nothing Maybe QName
    forall a. Maybe a
    Nothing DefInfo
    i QName
    name [Clause]
    cs
              Maybe (Expr, Maybe Expr, MetaId)
    _ -> Type
    -> ArgInfo
    -> Delayed
    -> Maybe ExtLamInfo
    -> Maybe QName
    -> DefInfo
    -> QName
    -> [Clause]
    -> TCM ()
    checkFunDef' Type
    t ArgInfo
    info Delayed
    delayed Maybe ExtLamInfo
    forall a. Maybe a
    Nothing Maybe QName
    forall a. Maybe a
    Nothing DefInfo
    i QName
    name [Clause]
    cs

            -- If it's a macro check that it ends in Term → TC ⊤
            let ismacro :: Bool
    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
            Bool -> TCM () -> TCM ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    when (Bool
    ismacro Bool -> Bool -> Bool
    || DefInfo -> IsMacro
    forall t. DefInfo' t -> IsMacro
    Info.defMacro DefInfo
    i IsMacro -> IsMacro -> Bool
    forall a. Eq a => a -> a -> Bool
    == IsMacro
    MacroDef) (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ Type -> TCM ()
    checkMacroType Type
    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
    $ Delayed -> DefInfo -> QName -> [Clause] -> TCErr -> Constraint
    CheckFunDef Delayed
    delayed DefInfo
    i QName
    name [Clause]
    cs TCErr
    err

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

      let telList :: [Dom ([Char], Type)]
    telList = Tele (Dom Type) -> [Dom ([Char], Type)]
    forall t. Tele (Dom t) -> [Dom ([Char], t)]
    telToList Tele (Dom Type)
    tel
          resType :: Type
    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 (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
      Type
    expectedType <- TCMT IO Term -> TCMT IO Type
    forall (m :: * -> *). Functor m => m Term -> m Type
    el TCMT IO Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primAgdaTerm TCMT IO Type -> TCMT IO Type -> TCMT IO Type
    forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
    --> TCMT IO Term -> TCMT IO Type
    forall (m :: * -> *). Functor m => m Term -> m Type
    el (TCMT IO Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primAgdaTCM TCMT IO Term -> TCMT IO Term -> TCMT IO Term
    forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
    <#> TCMT IO Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primLevelZero TCMT IO Term -> TCMT IO Term -> TCMT IO Term
    forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
    <@> TCMT IO Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primUnit)
      Type -> Type -> TCM ()
    forall (m :: * -> *). MonadConversion m => Type -> Type -> m ()
    equalType Type
    resType Type
    expectedType
        TCM () -> (TCErr -> TCM ()) -> TCM ()
    forall e (m :: * -> *) a.
    MonadError e m =>
    m a -> (e -> m a) -> m a
    `catchError` \ TCErr
    _ -> TypeError -> TCM ()
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    TypeError -> m a
    typeError (TypeError -> TCM ()) -> (Doc -> TypeError) -> Doc -> TCM ()
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Doc -> TypeError
    GenericDocError (Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< [TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    sep [ TCMT IO Doc
    "Result type of a macro must be"
                                                                , Int -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
    nest Int
    2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ Type -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Type
    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] -> Type -> Maybe (Expr, Maybe Expr, MetaId)
    isAlias [Clause]
    cs Type
    t =
            case [Clause] -> Maybe (Expr, Maybe Expr)
    trivialClause [Clause]
    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] -> 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 Bool
    _]
          | 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]
    _ = Maybe (Expr, Maybe Expr)
    forall a. Maybe a
    Nothing

    -- | Check a trivial definition of the form @f = e@
    checkAlias :: Type -> ArgInfo -> Delayed -> A.DefInfo -> QName -> A.Expr -> Maybe C.Expr -> TCM ()
    checkAlias :: Type
    -> ArgInfo
    -> Delayed
    -> DefInfo
    -> QName
    -> Expr
    -> Maybe Expr
    -> TCM ()
    checkAlias Type
    t ArgInfo
    ai Delayed
    delayed DefInfo
    i QName
    name Expr
    e Maybe Expr
    mc =
      let clause :: SpineClause
    clause = Clause :: forall lhs.
    lhs
    -> [ProblemEq] -> RHS -> WhereDeclarations -> Bool -> Clause' lhs
    A.Clause { clauseLHS :: SpineLHS
    clauseLHS          = LHSInfo -> QName -> [NamedArg Pattern] -> 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 :: Bool
    clauseCatchall     = Bool
    False } 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
    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
    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.
      Term
    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

      [Char] -> Int -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "tc.def.alias" Int
    20 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Doc
    "checkAlias: finished checking"

      DefaultToInfty -> TCM ()
    solveSizeConstraints DefaultToInfty
    DontDefaultToInfty

      Term
    v <- Term -> TCMT IO Term
    forall a (m :: * -> *).
    (InstantiateFull a, MonadReduce m) =>
    a -> m a
    instantiateFull Term
    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 :: Term -> Term
    bodyMod = case ArgInfo -> Relevance
    forall a. LensRelevance a => a -> Relevance
    getRelevance ArgInfo
    ai of
            Relevance
    Irrelevant -> Term -> Term
    dontCare
            Relevance
    _          -> Term -> Term
    forall a. a -> a
    id

      -- Add the definition
      QName -> ArgInfo -> QName -> Type -> Defn -> TCM ()
    addConstant' QName
    name ArgInfo
    ai QName
    name Type
    t
                       (Defn -> TCM ()) -> Defn -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ Lens' Bool Defn -> LensSet Bool Defn
    forall i o. Lens' i o -> LensSet i o
    set Lens' Bool Defn
    funMacro (DefInfo -> IsMacro
    forall t. DefInfo' t -> IsMacro
    Info.defMacro DefInfo
    i IsMacro -> IsMacro -> Bool
    forall a. Eq a => a -> a -> Bool
    == IsMacro
    MacroDef) (Defn -> Defn) -> Defn -> Defn
    forall a b. (a -> b) -> a -> b
    $
                         Defn
    emptyFunction
                          { funClauses :: [Clause]
    funClauses = [ Clause :: Range
    -> Range
    -> Tele (Dom Type)
    -> [NamedArg DeBruijnPattern]
    -> Maybe Term
    -> Maybe (Arg Type)
    -> Bool
    -> Maybe Bool
    -> Maybe Bool
    -> Maybe Bool
    -> ExpandedEllipsis
    -> Clause
    Clause  -- trivial clause @name = v@
                              { clauseLHSRange :: Range
    clauseLHSRange  = DefInfo -> Range
    forall a. HasRange a => a -> Range
    getRange DefInfo
    i
                              , clauseFullRange :: Range
    clauseFullRange = DefInfo -> Range
    forall a. HasRange a => a -> Range
    getRange DefInfo
    i
                              , clauseTel :: Tele (Dom Type)
    clauseTel       = Tele (Dom Type)
    forall a. Tele a
    EmptyTel
                              , namedClausePats :: [NamedArg DeBruijnPattern]
    namedClausePats = []
                              , clauseBody :: Maybe Term
    clauseBody      = Term -> Maybe Term
    forall a. a -> Maybe a
    Just (Term -> Maybe Term) -> Term -> Maybe Term
    forall a b. (a -> b) -> a -> b
    $ Term -> Term
    bodyMod Term
    v
                              , clauseType :: Maybe (Arg Type)
    clauseType      = Arg Type -> Maybe (Arg Type)
    forall a. a -> Maybe a
    Just (Arg Type -> Maybe (Arg Type)) -> Arg Type -> Maybe (Arg Type)
    forall a b. (a -> b) -> a -> b
    $ ArgInfo -> Type -> Arg Type
    forall e. ArgInfo -> e -> Arg e
    Arg ArgInfo
    ai Type
    t
                              , clauseCatchall :: Bool
    clauseCatchall  = Bool
    False
                              , clauseExact :: Maybe Bool
    clauseExact     = Bool -> Maybe Bool
    forall a. a -> Maybe a
    Just Bool
    True
                              , clauseRecursive :: Maybe Bool
    clauseRecursive = Maybe Bool
    forall a. Maybe a
    Nothing   -- we don't know yet
                              , clauseUnreachable :: Maybe Bool
    clauseUnreachable = Bool -> Maybe Bool
    forall a. a -> Maybe a
    Just Bool
    False
                              , clauseEllipsis :: ExpandedEllipsis
    clauseEllipsis = ExpandedEllipsis
    NoEllipsis
                              } ]
                          , funCompiled :: Maybe CompiledClauses
    funCompiled = CompiledClauses -> Maybe CompiledClauses
    forall a. a -> Maybe a
    Just (CompiledClauses -> Maybe CompiledClauses)
    -> CompiledClauses -> Maybe CompiledClauses
    forall a b. (a -> b) -> a -> b
    $ [Arg [Char]] -> Term -> CompiledClauses
    forall a. [Arg [Char]] -> a -> CompiledClauses' a
    Done [] (Term -> CompiledClauses) -> Term -> CompiledClauses
    forall a b. (a -> b) -> a -> b
    $ Term -> Term
    bodyMod Term
    v
                          , funSplitTree :: Maybe SplitTree
    funSplitTree = SplitTree -> Maybe SplitTree
    forall a. a -> Maybe a
    Just (SplitTree -> Maybe SplitTree) -> SplitTree -> Maybe SplitTree
    forall a b. (a -> b) -> a -> b
    $ Int -> SplitTree
    forall a. Int -> SplitTree' a
    SplittingDone Int
    0
                          , funDelayed :: Delayed
    funDelayed  = Delayed
    delayed
                          , funAbstr :: IsAbstract
    funAbstr    = DefInfo -> IsAbstract
    forall t. DefInfo' t -> IsAbstract
    Info.defAbstract DefInfo
    i
                          }

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

      [Char] -> Int -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "tc.def.alias" Int
    20 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Doc
    "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)
                 -> Delayed          -- ^ are the clauses delayed (not unfolded willy-nilly)
                 -> 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
    -> Delayed
    -> Maybe ExtLamInfo
    -> Maybe QName
    -> DefInfo
    -> QName
    -> [Clause]
    -> TCM ()
    checkFunDef' Type
    t ArgInfo
    ai Delayed
    delayed Maybe ExtLamInfo
    extlam Maybe QName
    with DefInfo
    i QName
    name [Clause]
    cs =
      Type
    -> ArgInfo
    -> Delayed
    -> Maybe ExtLamInfo
    -> Maybe QName
    -> DefInfo
    -> QName
    -> Maybe Substitution
    -> [Clause]
    -> TCM ()
    checkFunDefS Type
    t ArgInfo
    ai Delayed
    delayed Maybe ExtLamInfo
    extlam Maybe QName
    with DefInfo
    i QName
    name Maybe Substitution
    forall a. Maybe a
    Nothing [Clause]
    cs

    -- | Type check a definition by pattern matching.
    checkFunDefS :: Type             -- ^ the type we expect the function to have
                 -> ArgInfo          -- ^ is it irrelevant (for instance)
                 -> Delayed          -- ^ are the clauses delayed (not unfolded willy-nilly)
                 -> 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 -- ^ substitution (from with abstraction) that needs to be applied to module parameters
                 -> [A.Clause]       -- ^ the clauses to check
                 -> TCM ()
    checkFunDefS :: Type
    -> ArgInfo
    -> Delayed
    -> Maybe ExtLamInfo
    -> Maybe QName
    -> DefInfo
    -> QName
    -> Maybe Substitution
    -> [Clause]
    -> TCM ()
    checkFunDefS Type
    t ArgInfo
    ai Delayed
    delayed Maybe ExtLamInfo
    extlam Maybe QName
    with DefInfo
    i QName
    name Maybe Substitution
    withSub [Clause]
    cs = do

        Call -> TCM () -> TCM ()
    forall (m :: * -> *) a. MonadTrace m => Call -> m a -> m a
    traceCall (Range -> QName -> [Clause] -> Bool -> Call
    CheckFunDefCall (DefInfo -> Range
    forall a. HasRange a => a -> Range
    getRange DefInfo
    i) QName
    name [Clause]
    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
    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
    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
    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 -> TCMT IO Doc) -> [Clause] -> [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 -> TCMT IO Doc) -> Clause -> 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 -> [Char]) -> Clause -> TCMT IO Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Clause -> [Char]
    forall a. Show a => a -> [Char]
    show (Clause -> [Char]) -> (Clause -> Clause) -> Clause -> [Char]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Clause -> Clause
    forall a. ExprLike a => a -> a
    A.deepUnscope) [Clause]
    cs

            [SpineClause]
    cs <- [SpineClause] -> TCMT IO [SpineClause]
    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 -> SpineClause) -> [Clause] -> [SpineClause]
    forall a b. (a -> b) -> [a] -> [b]
    map Clause -> SpineClause
    forall a b. LHSToSpine a b => a -> b
    A.lhsToSpine [Clause]
    cs

            [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
    "spine clauses:" TCMT IO Doc -> [TCMT IO Doc] -> [TCMT IO Doc]
    forall a. a -> [a] -> [a]
    : (SpineClause -> TCMT IO Doc) -> [SpineClause] -> [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)
    -> (SpineClause -> TCMT IO Doc) -> SpineClause -> 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)
    -> (SpineClause -> [Char]) -> SpineClause -> TCMT IO Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . SpineClause -> [Char]
    forall a. Show a => a -> [Char]
    show (SpineClause -> [Char])
    -> (SpineClause -> SpineClause) -> SpineClause -> [Char]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . SpineClause -> SpineClause
    forall a. ExprLike a => a -> a
    A.deepUnscope) [SpineClause]
    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
            [(Clause, ClausesPostChecks)]
    cs <- Call
    -> TCMT IO [(Clause, ClausesPostChecks)]
    -> TCMT IO [(Clause, ClausesPostChecks)]
    forall (m :: * -> *) a. MonadTrace m => Call -> m a -> m a
    traceCall Call
    NoHighlighting (TCMT IO [(Clause, ClausesPostChecks)]
     -> TCMT IO [(Clause, ClausesPostChecks)])
    -> TCMT IO [(Clause, ClausesPostChecks)]
    -> TCMT IO [(Clause, ClausesPostChecks)]
    forall a b. (a -> b) -> a -> b
    $ do -- To avoid flicker.
              [(SpineClause, Int)]
    -> ((SpineClause, Int) -> TCMT IO (Clause, ClausesPostChecks))
    -> TCMT IO [(Clause, ClausesPostChecks)]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    t a -> (a -> m b) -> m (t b)
    forM ([SpineClause] -> [Int] -> [(SpineClause, Int)]
    forall a b. [a] -> [b] -> [(a, b)]
    zip [SpineClause]
    cs [Int
    0..]) (((SpineClause, Int) -> TCMT IO (Clause, ClausesPostChecks))
     -> TCMT IO [(Clause, ClausesPostChecks)])
    -> ((SpineClause, Int) -> TCMT IO (Clause, ClausesPostChecks))
    -> TCMT IO [(Clause, ClausesPostChecks)]
    forall a b. (a -> b) -> a -> b
    $ \ (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 Maybe Substitution
    withSub 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
                  (Clause
    c,ClausesPostChecks
    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
    -> SpineClause
    -> TCMT IO (Clause, ClausesPostChecks)
    checkClause Type
    t Maybe Substitution
    withSub 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.
                  Maybe ExtLamInfo -> TCM () -> TCM ()
    forall m a. Monoid m => Maybe a -> m -> m
    whenNothing Maybe ExtLamInfo
    extlam (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ DefaultToInfty -> TCM ()
    solveSizeConstraints DefaultToInfty
    DontDefaultToInfty
                  -- Andreas, 2013-10-27 add clause as soon it is type-checked
                  -- TODO: instantiateFull?
                  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
    $ QName -> [Clause] -> TCM ()
    addClauses QName
    name [Clause
    c]
                  (Clause, ClausesPostChecks) -> TCMT IO (Clause, ClausesPostChecks)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Clause
    c,ClausesPostChecks
    b)

            ([Clause]
    cs, CPC IntSet
    isOneIxs) <- ([Clause], ClausesPostChecks)
    -> TCMT IO ([Clause], ClausesPostChecks)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (([Clause], ClausesPostChecks)
     -> TCMT IO ([Clause], ClausesPostChecks))
    -> ([Clause], ClausesPostChecks)
    -> TCMT IO ([Clause], ClausesPostChecks)
    forall a b. (a -> b) -> a -> b
    $ (([ClausesPostChecks] -> ClausesPostChecks)
    -> ([Clause], [ClausesPostChecks]) -> ([Clause], ClausesPostChecks)
    forall (p :: * -> * -> *) b c a.
    Bifunctor p =>
    (b -> c) -> p a b -> p a c
    second [ClausesPostChecks] -> ClausesPostChecks
    forall a. Monoid a => [a] -> a
    mconcat (([Clause], [ClausesPostChecks]) -> ([Clause], ClausesPostChecks))
    -> ([(Clause, ClausesPostChecks)]
        -> ([Clause], [ClausesPostChecks]))
    -> [(Clause, ClausesPostChecks)]
    -> ([Clause], ClausesPostChecks)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [(Clause, ClausesPostChecks)] -> ([Clause], [ClausesPostChecks])
    forall a b. [(a, b)] -> ([a], [b])
    unzip) [(Clause, ClausesPostChecks)]
    cs

            let isSystem :: Bool
    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

            Bool
    canBeSystem <- do
              -- allow VarP and ConP i0/i1 fallThrough = yes, DotP
              let pss :: [[NamedArg DeBruijnPattern]]
    pss = (Clause -> [NamedArg DeBruijnPattern])
    -> [Clause] -> [[NamedArg DeBruijnPattern]]
    forall a b. (a -> b) -> [a] -> [b]
    map Clause -> [NamedArg DeBruijnPattern]
    namedClausePats [Clause]
    cs
                  allowed :: Pattern' x -> Bool
    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
              Bool -> TCMT IO Bool
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Bool -> TCMT IO Bool) -> Bool -> TCMT IO Bool
    forall a b. (a -> b) -> a -> b
    $! (NamedArg DeBruijnPattern -> Bool)
    -> [NamedArg DeBruijnPattern] -> Bool
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
    all (DeBruijnPattern -> Bool
    forall {x}. Pattern' x -> Bool
    allowed (DeBruijnPattern -> Bool)
    -> (NamedArg DeBruijnPattern -> DeBruijnPattern)
    -> NamedArg DeBruijnPattern
    -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . NamedArg DeBruijnPattern -> DeBruijnPattern
    forall a. NamedArg a -> a
    namedArg) ([[NamedArg DeBruijnPattern]] -> [NamedArg DeBruijnPattern]
    forall (t :: * -> *) a. Foldable t => t [a] -> [a]
    concat [[NamedArg DeBruijnPattern]]
    pss)
            Bool -> TCM () -> TCM ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    when Bool
    isSystem (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ Bool -> TCM () -> TCM ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    unless Bool
    canBeSystem (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $
              TypeError -> TCM ()
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    TypeError -> m a
    typeError (TypeError -> TCM ()) -> TypeError -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ [Char] -> TypeError
    GenericError [Char]
    "no pattern matching or path copatterns in systems!"

            [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 (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
    $ do
              [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
    "checked clauses:" TCMT IO Doc -> [TCMT IO Doc] -> [TCMT IO Doc]
    forall a. a -> [a] -> [a]
    : (Clause -> TCMT IO Doc) -> [Clause] -> [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 -> TCMT IO Doc) -> Clause -> 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 -> [Char]) -> Clause -> TCMT IO Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Clause -> [Char]
    forall a. Show a => a -> [Char]
    show) [Clause]
    cs

            -- After checking, remove the clauses again.
            -- (Otherwise, @checkInjectivity@ loops for issue 801).
            QName -> ([Clause] -> [Clause]) -> TCM ()
    modifyFunClauses QName
    name ([Clause] -> [Clause] -> [Clause]
    forall a b. a -> b -> a
    const [])

            [Char] -> Int -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "tc.cc" Int
    25 (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
    $ do
              [TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    sep [ TCMT IO Doc
    "clauses before injectivity test"
                  , 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
    $ [QNamed Clause] -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM ([QNamed Clause] -> TCMT IO Doc) -> [QNamed Clause] -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ (Clause -> QNamed Clause) -> [Clause] -> [QNamed Clause]
    forall a b. (a -> b) -> [a] -> [b]
    map (QName -> Clause -> QNamed Clause
    forall a. QName -> a -> QNamed a
    QNamed QName
    name) [Clause]
    cs  -- broken, reify (QNamed n cl) expect cl to live at top level
                  ]
            [Char] -> Int -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "tc.cc" Int
    60 (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
    $ do
              [TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    sep [ TCMT IO Doc
    "raw clauses: "
                  , 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
    sep ([TCMT IO Doc] -> TCMT IO Doc) -> [TCMT IO Doc] -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ (Clause -> TCMT IO Doc) -> [Clause] -> [TCMT IO Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map ([Char] -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => [Char] -> m Doc
    text ([Char] -> TCMT IO Doc)
    -> (Clause -> [Char]) -> Clause -> TCMT IO Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . QNamed Clause -> [Char]
    forall a. Show a => a -> [Char]
    show (QNamed Clause -> [Char])
    -> (Clause -> QNamed Clause) -> Clause -> [Char]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . QName -> Clause -> QNamed Clause
    forall a. QName -> a -> QNamed a
    QNamed QName
    name) [Clause]
    cs
                  ]

            -- Needed to calculate the proper fullType below.
            -- Also: issue #4173, allow splitting on erased arguments in erased definitions
            -- in the coverage checker.
            ArgInfo -> TCM () -> TCM ()
    forall (tcm :: * -> *) m a.
    (MonadTCEnv tcm, LensCohesion m) =>
    m -> tcm a -> tcm a
    applyCohesionToContext ArgInfo
    ai (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ ArgInfo -> TCM () -> TCM ()
    forall (tcm :: * -> *) q a.
    (MonadTCEnv tcm, LensQuantity q) =>
    q -> tcm a -> tcm a
    applyQuantityToContext ArgInfo
    ai (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ do

            -- Systems have their own coverage and "coherence" check, we
            -- also add an absurd clause for the cases not needed.
            ([Clause]
    cs,Maybe System
    sys) <- if Bool -> Bool
    not Bool
    isSystem then ([Clause], Maybe System) -> TCMT IO ([Clause], Maybe System)
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([Clause]
    cs, Maybe System
    forall a. Null a => a
    empty) else do
                     Type
    fullType <- (Tele (Dom Type) -> Type -> Type)
    -> Type -> Tele (Dom Type) -> Type
    forall a b c. (a -> b -> c) -> b -> a -> c
    flip Tele (Dom Type) -> Type -> Type
    forall t. Abstract t => Tele (Dom Type) -> t -> t
    abstract Type
    t (Tele (Dom Type) -> Type)
    -> TCMT IO (Tele (Dom Type)) -> TCMT IO Type
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> TCMT IO (Tele (Dom Type))
    forall (m :: * -> *).
    (Applicative m, MonadTCEnv m) =>
    m (Tele (Dom Type))
    getContextTelescope
                     System
    sys <- TCMT IO System -> TCMT IO System
    forall (tcm :: * -> *) a.
    (MonadTCEnv tcm, ReadTCState tcm) =>
    tcm a -> tcm a
    inTopContext (TCMT IO System -> TCMT IO System)
    -> TCMT IO System -> TCMT IO System
    forall a b. (a -> b) -> a -> b
    $ QName -> [Int] -> Type -> [Clause] -> TCMT IO System
    checkSystemCoverage QName
    name (IntSet -> [Int]
    IntSet.toList IntSet
    isOneIxs) Type
    fullType [Clause]
    cs
                     Tele (Dom Type)
    tel <- TCMT IO (Tele (Dom Type))
    forall (m :: * -> *).
    (Applicative m, MonadTCEnv m) =>
    m (Tele (Dom Type))
    getContextTelescope
                     let c :: Clause
    c = Clause :: Range
    -> Range
    -> Tele (Dom Type)
    -> [NamedArg DeBruijnPattern]
    -> Maybe Term
    -> Maybe (Arg Type)
    -> Bool
    -> Maybe Bool
    -> Maybe Bool
    -> Maybe Bool
    -> ExpandedEllipsis
    -> Clause
    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. DeBruijn a => Tele (Dom Type) -> [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 :: Bool
    clauseCatchall = Bool
    False
                           , clauseExact :: Maybe Bool
    clauseExact     = Bool -> Maybe Bool
    forall a. a -> Maybe a
    Just Bool
    True
                           , clauseRecursive :: Maybe Bool
    clauseRecursive = Bool -> Maybe Bool
    forall a. a -> Maybe a
    Just Bool
    False
                           , clauseUnreachable :: Maybe Bool
    clauseUnreachable = Bool -> Maybe Bool
    forall a. a -> Maybe a
    Just Bool
    False
                           , clauseEllipsis :: ExpandedEllipsis
    clauseEllipsis = ExpandedEllipsis
    NoEllipsis
                           }
                     ([Clause], Maybe System) -> TCMT IO ([Clause], Maybe System)
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([Clause]
    cs [Clause] -> [Clause] -> [Clause]
    forall a. [a] -> [a] -> [a]
    ++ [Clause
    c], System -> Maybe System
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure System
    sys)

            -- Annotate the clauses with which arguments are actually used.
            [Clause]
    cs <- [Clause] -> TCMT IO [Clause]
    forall a (m :: * -> *).
    (InstantiateFull a, MonadReduce m) =>
    a -> m a
    instantiateFull {- =<< mapM rebindClause -} [Clause]
    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!?

            -- 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.
            [Char] -> Int -> [Char] -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> [Char] -> m ()
    reportSLn [Char]
    "tc.inj.def" Int
    20 ([Char] -> TCM ()) -> [Char] -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ [Char]
    "checkFunDef': checking injectivity..."
            FunctionInverse
    inv <- Account (BenchPhase (TCMT IO))
    -> TCMT IO FunctionInverse -> TCMT IO FunctionInverse
    forall (m :: * -> *) c.
    MonadBench m =>
    Account (BenchPhase m) -> m c -> m c
    Bench.billTo [BenchPhase (TCMT IO)
    Phase
    Bench.Injectivity] (TCMT IO FunctionInverse -> TCMT IO FunctionInverse)
    -> TCMT IO FunctionInverse -> TCMT IO FunctionInverse
    forall a b. (a -> b) -> a -> b
    $
              QName -> [Clause] -> TCMT IO FunctionInverse
    checkInjectivity QName
    name [Clause]
    cs

            [Char] -> Int -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "tc.cc" Int
    15 (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
    $ do
              [TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    sep [ TCMT IO Doc
    "clauses before compilation"
                  , 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
    sep ([TCMT IO Doc] -> TCMT IO Doc) -> [TCMT IO Doc] -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ (Clause -> TCMT IO Doc) -> [Clause] -> [TCMT IO Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map (QNamed Clause -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM (QNamed Clause -> TCMT IO Doc)
    -> (Clause -> QNamed Clause) -> Clause -> TCMT IO Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . QName -> Clause -> QNamed Clause
    forall a. QName -> a -> QNamed a
    QNamed QName
    name) [Clause]
    cs
                  ]

            [Char] -> Int -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "tc.cc.raw" Int
    65 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ do
              [TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    sep [ TCMT IO Doc
    "clauses before compilation"
                  , 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
    sep ([TCMT IO Doc] -> TCMT IO Doc) -> [TCMT IO Doc] -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ (Clause -> TCMT IO Doc) -> [Clause] -> [TCMT IO Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map ([Char] -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => [Char] -> m Doc
    text ([Char] -> TCMT IO Doc)
    -> (Clause -> [Char]) -> Clause -> TCMT IO Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Clause -> [Char]
    forall a. Show a => a -> [Char]
    show) [Clause]
    cs
                  ]

            -- add clauses for the coverage (& confluence) checker (needs to reduce)
            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
    $ QName -> [Clause] -> TCM ()
    addClauses QName
    name [Clause]
    cs

            [Char] -> Int -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "tc.cc.type" Int
    60 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Doc
    "  type   : " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> ([Char] -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => [Char] -> m Doc
    text ([Char] -> TCMT IO Doc) -> (Type -> [Char]) -> Type -> TCMT IO Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Type -> [Char]
    forall a. Pretty a => a -> [Char]
    prettyShow) Type
    t
            [Char] -> Int -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "tc.cc.type" Int
    60 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Doc
    "  context: " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> ([Char] -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => [Char] -> m Doc
    text ([Char] -> TCMT IO Doc)
    -> (Tele (Dom Type) -> [Char]) -> Tele (Dom Type) -> TCMT IO Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Tele (Dom Type) -> [Char]
    forall a. Pretty a => a -> [Char]
    prettyShow (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
    =<< TCMT IO (Tele (Dom Type))
    forall (m :: * -> *).
    (Applicative m, MonadTCEnv m) =>
    m (Tele (Dom Type))
    getContextTelescope)

            Type
    fullType <- (Tele (Dom Type) -> Type -> Type)
    -> Type -> Tele (Dom Type) -> Type
    forall a b c. (a -> b -> c) -> b -> a -> c
    flip Tele (Dom Type) -> Type -> Type
    telePi Type
    t (Tele (Dom Type) -> Type)
    -> TCMT IO (Tele (Dom Type)) -> TCMT IO Type
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> TCMT IO (Tele (Dom Type))
    forall (m :: * -> *).
    (Applicative m, MonadTCEnv m) =>
    m (Tele (Dom Type))
    getContextTelescope

            [Char] -> Int -> [Char] -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> [Char] -> m ()
    reportSLn  [Char]
    "tc.cc.type" Int
    80 ([Char] -> TCM ()) -> [Char] -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ Type -> [Char]
    forall a. Show a => a -> [Char]
    show Type
    fullType

            -- Coverage check and compile the clauses
            (Maybe SplitTree
    mst, Bool
    _recordExpressionBecameCopatternLHS, CompiledClauses
    cc) <- Account (BenchPhase (TCMT IO))
    -> TCMT IO (Maybe SplitTree, Bool, CompiledClauses)
    -> TCMT IO (Maybe SplitTree, Bool, CompiledClauses)
    forall (m :: * -> *) c.
    MonadBench m =>
    Account (BenchPhase m) -> m c -> m c
    Bench.billTo [BenchPhase (TCMT IO)
    Phase
    Bench.Coverage] (TCMT IO (Maybe SplitTree, Bool, CompiledClauses)
     -> TCMT IO (Maybe SplitTree, Bool, CompiledClauses))
    -> TCMT IO (Maybe SplitTree, Bool, CompiledClauses)
    -> TCMT IO (Maybe SplitTree, Bool, CompiledClauses)
    forall a b. (a -> b) -> a -> b
    $
              TCMT IO (Maybe SplitTree, Bool, CompiledClauses)
    -> TCMT IO (Maybe SplitTree, Bool, CompiledClauses)
    forall (tcm :: * -> *) a.
    (MonadTCEnv tcm, ReadTCState tcm) =>
    tcm a -> tcm a
    unsafeInTopContext (TCMT IO (Maybe SplitTree, Bool, CompiledClauses)
     -> TCMT IO (Maybe SplitTree, Bool, CompiledClauses))
    -> TCMT IO (Maybe SplitTree, Bool, CompiledClauses)
    -> TCMT IO (Maybe SplitTree, Bool, CompiledClauses)
    forall a b. (a -> b) -> a -> b
    $ Maybe (QName, Type)
    -> [Clause] -> TCMT IO (Maybe SplitTree, Bool, CompiledClauses)
    compileClauses (if Bool
    isSystem then Maybe (QName, Type)
    forall a. Maybe a
    Nothing else ((QName, Type) -> Maybe (QName, Type)
    forall a. a -> Maybe a
    Just (QName
    name, Type
    fullType)))
                                            [Clause]
    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.
            [Clause]
    cs <- Definition -> [Clause]
    defClauses (Definition -> [Clause]) -> TCMT IO Definition -> TCMT IO [Clause]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> QName -> TCMT IO Definition
    forall (m :: * -> *). HasConstInfo m => QName -> m Definition
    getConstInfo QName
    name

            [Char] -> Int -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "tc.cc" Int
    60 (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
    $ do
              [TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    sep [ TCMT IO Doc
    "compiled clauses 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
    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
    $ CompiledClauses -> TCMT IO Doc
    forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
    pretty CompiledClauses
    cc
                  ]

            -- The macro tag might be on the type signature
            Bool
    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) -> TCMT IO Definition -> TCMT IO Bool
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> QName -> TCMT IO Definition
    forall (m :: * -> *). HasConstInfo m => QName -> m Definition
    getConstInfo QName
    name

            [Clause]
    covering <- Defn -> [Clause]
    funCovering (Defn -> [Clause])
    -> (Definition -> Defn) -> Definition -> [Clause]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Definition -> Defn
    theDef (Definition -> [Clause]) -> TCMT IO Definition -> TCMT IO [Clause]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> QName -> TCMT IO Definition
    forall (m :: * -> *). HasConstInfo m => QName -> m Definition
    getConstInfo QName
    name

            -- Add the definition
            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
    $ QName -> Definition -> TCM ()
    addConstant QName
    name (Definition -> TCM ()) -> TCMT IO Definition -> TCM ()
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< do
              -- If there was a pragma for this definition, we can set the
              -- funTerminates field directly.
              Defn
    defn <- Defn -> TCM Defn
    autoInline (Defn -> TCM Defn) -> Defn -> TCM Defn
    forall a b. (a -> b) -> a -> b
    $
                 Lens' Bool Defn -> LensSet Bool Defn
    forall i o. Lens' i o -> LensSet i o
    set Lens' Bool Defn
    funMacro (Bool
    ismacro Bool -> Bool -> Bool
    || DefInfo -> IsMacro
    forall t. DefInfo' t -> IsMacro
    Info.defMacro DefInfo
    i IsMacro -> IsMacro -> Bool
    forall a. Eq a => a -> a -> Bool
    == IsMacro
    MacroDef) (Defn -> Defn) -> Defn -> Defn
    forall a b. (a -> b) -> a -> b
    $
                 Defn
    emptyFunction
                 { funClauses :: [Clause]
    funClauses        = [Clause]
    cs
                 , funCompiled :: Maybe CompiledClauses
    funCompiled       = CompiledClauses -> Maybe CompiledClauses
    forall a. a -> Maybe a
    Just CompiledClauses
    cc
                 , funSplitTree :: Maybe SplitTree
    funSplitTree      = Maybe SplitTree
    mst
                 , funDelayed :: Delayed
    funDelayed        = Delayed
    delayed
                 , funInv :: FunctionInverse
    funInv            = FunctionInverse
    inv
                 , funAbstr :: IsAbstract
    funAbstr          = DefInfo -> IsAbstract
    forall t. DefInfo' t -> IsAbstract
    Info.defAbstract DefInfo
    i
                 , funExtLam :: Maybe ExtLamInfo
    funExtLam         = (\ ExtLamInfo
    e -> ExtLamInfo
    e { extLamSys :: Maybe System
    extLamSys = Maybe System
    sys }) (ExtLamInfo -> ExtLamInfo) -> Maybe ExtLamInfo -> Maybe ExtLamInfo
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Maybe ExtLamInfo
    extlam
                 , funWith :: Maybe QName
    funWith           = Maybe QName
    with
                 , funCovering :: [Clause]
    funCovering       = [Clause]
    covering
                 }
              Language
    lang <- TCMT IO Language
    forall (m :: * -> *). HasOptions m => m Language
    getLanguage
              Definition -> TCMT IO Definition
    useTerPragma (Definition -> TCMT IO Definition)
    -> Definition -> TCMT IO Definition
    forall a b. (a -> b) -> a -> b
    $
                (Bool -> Bool) -> Definition -> Definition
    updateDefCopatternLHS (Bool -> Bool -> Bool
    forall a b. a -> b -> a
    const (Bool -> Bool -> Bool) -> Bool -> Bool -> Bool
    forall a b. (a -> b) -> a -> b
    $ CompiledClauses -> Bool
    hasProjectionPatterns CompiledClauses
    cc) (Definition -> Definition) -> Definition -> Definition
    forall a b. (a -> b) -> a -> b
    $
                ArgInfo -> QName -> Type -> Language -> Defn -> Definition
    defaultDefn ArgInfo
    ai QName
    name Type
    fullType Language
    lang Defn
    defn

            [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
    $ do
              [TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    sep [ TCMT IO Doc
    "added " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> QName -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM QName
    name TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> TCMT IO Doc
    ":"
                  , Int -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
    nest Int
    2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ Type -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM (Type -> 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
                  ]

            -- Jesper, 2019-05-30: if the constructors used in the
            -- lhs of a clause have rewrite rules, we need to check
            -- confluence here
            TCMT IO (Maybe ConfluenceCheck)
    -> (ConfluenceCheck -> TCM ()) -> TCM ()
    forall (m :: * -> *) a.
    Monad m =>
    m (Maybe a) -> (a -> m ()) -> m ()
    whenJustM (PragmaOptions -> Maybe ConfluenceCheck
    optConfluenceCheck (PragmaOptions -> Maybe ConfluenceCheck)
    -> TCMT IO PragmaOptions -> TCMT IO (Maybe ConfluenceCheck)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> TCMT IO PragmaOptions
    forall (m :: * -> *). HasOptions m => m PragmaOptions
    pragmaOptions) ((ConfluenceCheck -> TCM ()) -> TCM ())
    -> (ConfluenceCheck -> TCM ()) -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ \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
      TerminationCheck ()
    tc <- Lens' (TerminationCheck ()) TCEnv -> TCMT IO (TerminationCheck ())
    forall (m :: * -> *) a. MonadTCEnv m => Lens' a TCEnv -> m a
    viewTC Lens' (TerminationCheck ()) TCEnv
    eTerminationCheck
      let terminates :: Maybe Bool
    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
      [Char] -> Int -> [[Char]] -> TCM ()
    forall a (m :: * -> *).
    (ReportS a, MonadDebug m) =>
    [Char] -> Int -> a -> m ()
    reportS [Char]
    "tc.fundef" Int
    30 ([[Char]] -> TCM ()) -> [[Char]] -> TCM ()
    forall a b. (a -> b) -> a -> b
    $
        [ [Char]
    "funTerminates of " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ QName -> [Char]
    forall a. Pretty a => a -> [Char]
    prettyShow QName
    name [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    " set to " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ Maybe Bool -> [Char]
    forall a. Show a => a -> [Char]
    show Maybe Bool
    terminates
        , [Char]
    "  tc = " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ TerminationCheck () -> [Char]
    forall a. Show a => a -> [Char]
    show TerminationCheck ()
    tc
        ]
      Definition -> TCMT IO Definition
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Definition -> TCMT IO Definition)
    -> Definition -> TCMT IO Definition
    forall a b. (a -> b) -> a -> b
    $ Definition
    def { theDef :: Defn
    theDef = Defn
    fun { funTerminates :: Maybe Bool
    funTerminates = Maybe Bool
    terminates }}
    useTerPragma Definition
    def = Definition -> TCMT IO Definition
    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 [WithExpr]
    es [Clause]
    cs -> QName -> [WithExpr] -> [Clause] -> RHS
    A.WithRHS QName
    aux [WithExpr]
    es ([Clause] -> RHS) -> [Clause] -> RHS
    forall a b. (a -> b) -> a -> b
    $ [Clause] -> (Clause -> Clause) -> [Clause]
    forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
    for [Clause]
    cs ((Clause -> Clause) -> [Clause]) -> (Clause -> Clause) -> [Clause]
    forall a b. (a -> b) -> a -> b
    $
        \ (A.Clause (A.LHS LHSInfo
    info LHSCore' Expr
    core)     [ProblemEq]
    spats RHS
    rhs                 WhereDeclarations
    ds Bool
    catchall) ->
           LHS -> [ProblemEq] -> RHS -> WhereDeclarations -> Bool -> Clause
    forall lhs.
    lhs
    -> [ProblemEq] -> RHS -> WhereDeclarations -> Bool -> 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 Bool
    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 :: [Arg (Maybe A.BindName)] -> A.RHS -> A.RHS
    insertNames :: [Arg (Maybe BindName)] -> RHS -> RHS
    insertNames = (LHSCore' Expr -> LHSCore' Expr) -> RHS -> RHS
    mapLHSCores ((LHSCore' Expr -> LHSCore' Expr) -> RHS -> RHS)
    -> ([Arg (Maybe BindName)] -> LHSCore' Expr -> LHSCore' Expr)
    -> [Arg (Maybe BindName)]
    -> RHS
    -> RHS
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [Arg (Maybe BindName)] -> LHSCore' Expr -> LHSCore' Expr
    insertInspects

    insertInspects :: [Arg (Maybe A.BindName)] -> A.LHSCore -> A.LHSCore
    insertInspects :: [Arg (Maybe BindName)] -> LHSCore' Expr -> LHSCore' Expr
    insertInspects [Arg (Maybe BindName)]
    ps = \case
      A.LHSWith LHSCore' Expr
    core [Arg Pattern]
    wps [] ->
        let ps' :: [Arg (Maybe (Arg Pattern))]
    ps' = (Arg (Maybe BindName) -> Arg (Maybe (Arg Pattern)))
    -> [Arg (Maybe BindName)] -> [Arg (Maybe (Arg Pattern))]
    forall a b. (a -> b) -> [a] -> [b]
    map ((Maybe BindName -> Maybe (Arg Pattern))
    -> Arg (Maybe BindName) -> Arg (Maybe (Arg Pattern))
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap ((Maybe BindName -> Maybe (Arg Pattern))
     -> Arg (Maybe BindName) -> Arg (Maybe (Arg Pattern)))
    -> (Maybe BindName -> Maybe (Arg Pattern))
    -> Arg (Maybe BindName)
    -> Arg (Maybe (Arg Pattern))
    forall a b. (a -> b) -> a -> b
    $ (BindName -> Arg Pattern) -> Maybe BindName -> Maybe (Arg Pattern)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap BindName -> Arg Pattern
    patOfName) [Arg (Maybe BindName)]
    ps in
        LHSCore' Expr
    -> [Arg Pattern] -> [NamedArg Pattern] -> LHSCore' Expr
    forall e.
    LHSCore' e
    -> [Arg (Pattern' e)] -> [NamedArg (Pattern' e)] -> LHSCore' e
    A.LHSWith LHSCore' Expr
    core ([Arg (Maybe (Arg Pattern))] -> [Arg Pattern] -> [Arg Pattern]
    forall a. [Arg (Maybe (Arg a))] -> [Arg a] -> [Arg a]
    insertIn [Arg (Maybe (Arg Pattern))]
    ps' [Arg Pattern]
    wps) []
      LHSCore' Expr
    _ -> LHSCore' Expr
    forall a. HasCallStack => a
    __IMPOSSIBLE__

      where

        patOfName :: A.BindName -> Arg A.Pattern
        patOfName :: BindName -> Arg Pattern
    patOfName = Pattern -> Arg Pattern
    forall a. a -> Arg a
    defaultArg (Pattern -> Arg Pattern)
    -> (BindName -> Pattern) -> BindName -> Arg Pattern
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . BindName -> Pattern
    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]
    : ([Arg a] -> (Arg a -> [Arg a]) -> Maybe (Arg a) -> [Arg a]
    forall b a. b -> (a -> b) -> Maybe a -> b
    maybe [] Arg a -> [Arg a]
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure 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 =
              ([Arg a] -> (Arg a -> [Arg a]) -> Maybe (Arg a) -> [Arg a]
    forall b a. b -> (a -> b) -> Maybe a -> b
    maybe [] Arg a -> [Arg a]
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure 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 :: [Arg A.Pattern] -> A.RHS -> A.RHS
    insertPatterns :: [Arg Pattern] -> RHS -> RHS
    insertPatterns [Arg Pattern]
    pats = (LHSCore' Expr -> LHSCore' Expr) -> RHS -> RHS
    mapLHSCores ([Arg Pattern] -> LHSCore' Expr -> LHSCore' Expr
    insertPatternsLHSCore [Arg Pattern]
    pats)

    -- | Insert with-patterns before the trailing with patterns.
    -- If there are none, append the with-patterns.
    insertPatternsLHSCore :: [Arg A.Pattern] -> A.LHSCore -> A.LHSCore
    insertPatternsLHSCore :: [Arg Pattern] -> LHSCore' Expr -> LHSCore' Expr
    insertPatternsLHSCore [Arg Pattern]
    pats = \case
      A.LHSWith LHSCore' Expr
    core [Arg Pattern]
    wps [] -> LHSCore' Expr
    -> [Arg Pattern] -> [NamedArg Pattern] -> LHSCore' Expr
    forall e.
    LHSCore' e
    -> [Arg (Pattern' e)] -> [NamedArg (Pattern' e)] -> LHSCore' e
    A.LHSWith LHSCore' Expr
    core ([Arg Pattern]
    pats [Arg Pattern] -> [Arg Pattern] -> [Arg Pattern]
    forall a. [a] -> [a] -> [a]
    ++ [Arg Pattern]
    wps) []
      LHSCore' Expr
    core                  -> LHSCore' Expr
    -> [Arg Pattern] -> [NamedArg Pattern] -> LHSCore' Expr
    forall e.
    LHSCore' e
    -> [Arg (Pattern' e)] -> [NamedArg (Pattern' e)] -> LHSCore' e
    A.LHSWith LHSCore' Expr
    core [Arg Pattern]
    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 -> [Arg (Term, EqualityView)]
    wfExprs      :: [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 -> [Clause]
    wfClauses    :: [A.Clause]                        -- ^ The given clauses for the with function
        , WithFunctionProblem -> Substitution
    wfCallSubst :: Substitution                       -- ^ Subtsitution to generate call for the parent.
        }

    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 (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
    prettyTCM Type
    t
      TelV Tele (Dom Type)
    gamma Type
    t <- Int -> Type -> TCMT IO (TelV Type)
    forall (m :: * -> *).
    (MonadReduce m, MonadAddContext m) =>
    Int -> Type -> m (TelV Type)
    telViewUpTo Int
    n Type
    t
      Tele (Dom Type) -> TCMT IO System -> TCMT IO System
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    addContext Tele (Dom Type)
    gamma (TCMT IO System -> TCMT IO System)
    -> TCMT IO System -> TCMT IO System
    forall a b. (a -> b) -> a -> b
    $ do
      TelV (ExtendTel Dom Type
    a Abs (Tele (Dom Type))
    _) Type
    _ <- Int -> Type -> TCMT IO (TelV Type)
    forall (m :: * -> *).
    (MonadReduce m, MonadAddContext m) =>
    Int -> Type -> m (TelV Type)
    telViewUpTo Int
    1 Type
    t
      Term
    a <- Term -> TCMT IO Term
    forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
    reduce (Term -> TCMT IO Term) -> Term -> TCMT IO Term
    forall a b. (a -> b) -> a -> b
    $ Type -> Term
    forall t a. Type'' t a -> a
    unEl (Type -> Term) -> Type -> Term
    forall a b. (a -> b) -> a -> b
    $ Dom Type -> Type
    forall t e. Dom' t e -> e
    unDom Dom Type
    a

      case Term
    a of
        Def QName
    q [Apply Arg Term
    phi] -> do
          [Maybe QName
    iz,Maybe QName
    io] <- ([Char] -> TCMT IO (Maybe QName))
    -> [[Char]] -> TCMT IO [Maybe QName]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    mapM [Char] -> TCMT IO (Maybe QName)
    forall (m :: * -> *). HasBuiltins m => [Char] -> m (Maybe QName)
    getBuiltinName' [[Char]
    builtinIZero, [Char]
    builtinIOne]
          Term
    ineg <- TCMT IO Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primINeg
          Term
    imin <- TCMT IO Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primIMin
          Term
    imax <- TCMT IO Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primIMax
          Term
    i0 <- TCMT IO Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primIZero
          Term
    i1 <- TCMT IO Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primIOne
          let
            isDir :: DeBruijnPattern -> Maybe Bool
    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 :: [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, 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] -> 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] -> Term
    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 :: [[DeBruijnPattern]]
    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 :: [[(Int, Bool)]]
    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 :: [Term]
    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
    psi = [Term] -> Term
    orI ([Term] -> Term) -> [Term] -> Term
    forall a b. (a -> b) -> a -> b
    $ [Term]
    phis
            pcs :: [(Term, Clause)]
    pcs = [Term] -> [Clause] -> [(Term, Clause)]
    forall a b. [a] -> [b] -> [(a, b)]
    zip [Term]
    phis [Clause]
    cs

          [Char] -> Int -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "tc.sys.cover" 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
    fsep ([TCMT IO Doc] -> TCMT IO Doc) -> [TCMT IO Doc] -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ ([DeBruijnPattern] -> TCMT IO Doc)
    -> [[DeBruijnPattern]] -> [TCMT IO Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map [DeBruijnPattern] -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM [[DeBruijnPattern]]
    pats
          Type
    interval <- TCMT IO Type
    forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Type
    primIntervalType
          [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
    $ TCMT IO Doc
    "equalTerm " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Term -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM (Arg Term -> Term
    forall e. Arg e -> e
    unArg Arg Term
    phi) TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Term -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Term
    psi
          Type -> Term -> Term -> TCM ()
    forall (m :: * -> *).
    MonadConversion m =>
    Type -> Term -> Term -> m ()
    equalTerm Type
    interval (Arg Term -> Term
    forall e. Arg e -> e
    unArg Arg Term
    phi) Term
    psi

          [[(Term, Clause)]] -> ([(Term, Clause)] -> TCM ()) -> TCM ()
    forall (t :: * -> *) (m :: * -> *) a b.
    (Foldable t, Monad m) =>
    t a -> (a -> m b) -> m ()
    forM_ ([[(Term, Clause)]] -> [[(Term, Clause)]] -> [[(Term, Clause)]]
    forall a. [a] -> [a] -> [a]
    initWithDefault [[(Term, Clause)]]
    forall a. HasCallStack => a
    __IMPOSSIBLE__ ([[(Term, Clause)]] -> [[(Term, Clause)]])
    -> [[(Term, Clause)]] -> [[(Term, Clause)]]
    forall a b. (a -> b) -> a -> b
    $
                 [[(Term, Clause)]] -> [[(Term, Clause)]] -> [[(Term, Clause)]]
    forall a. [a] -> [a] -> [a]
    initWithDefault [[(Term, Clause)]]
    forall a. HasCallStack => a
    __IMPOSSIBLE__ ([[(Term, Clause)]] -> [[(Term, Clause)]])
    -> [[(Term, Clause)]] -> [[(Term, Clause)]]
    forall a b. (a -> b) -> a -> b
    $ [(Term, Clause)] -> [[(Term, Clause)]]
    forall a. [a] -> [[a]]
    List.tails [(Term, Clause)]
    pcs) (([(Term, Clause)] -> TCM ()) -> TCM ())
    -> ([(Term, Clause)] -> TCM ()) -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ \ ((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
              Term
    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])
              Term
    -> (Map Int Bool -> Blocker -> Term -> TCM ())
    -> (Substitution -> TCM ())
    -> TCMT IO [()]
    forall (m :: * -> *) a.
    MonadConversion m =>
    Term
    -> (Map Int Bool -> Blocker -> Term -> m a)
    -> (Substitution -> m a)
    -> m [a]
    forallFaceMaps Term
    phi12 (\ Map Int Bool
    _ Blocker
    _ -> Term -> TCM ()
    forall a. HasCallStack => a
    __IMPOSSIBLE__) ((Substitution -> TCM ()) -> TCMT IO [()])
    -> (Substitution -> TCM ()) -> TCMT IO [()]
    forall a b. (a -> b) -> a -> b
    $ \ 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 (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 Tele (Dom Type)
    delta Type
    _ <- Int -> Type -> TCMT IO (TelV Type)
    forall (m :: * -> *).
    (MonadReduce m, MonadAddContext m) =>
    Int -> Type -> m (TelV Type)
    telViewUpTo Int
    extra Type
    t'
                      (Term -> Term) -> TCMT IO Term -> TCMT IO Term
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (Tele (Dom Type) -> Term -> Term
    forall t. Abstract t => Tele (Dom Type) -> t -> t
    abstract Tele (Dom Type)
    delta) (TCMT IO Term -> TCMT IO Term) -> TCMT IO Term -> TCMT IO Term
    forall a b. (a -> b) -> a -> b
    $ Tele (Dom Type) -> TCMT IO Term -> TCMT IO Term
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    addContext Tele (Dom Type)
    delta (TCMT IO Term -> TCMT IO Term) -> TCMT IO Term -> TCMT IO Term
    forall a b. (a -> b) -> a -> b
    $ do
                        (Reduced (Blocked' Term Term) Term -> Term)
    -> TCMT IO (Reduced (Blocked' Term Term) Term) -> TCMT IO Term
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap Reduced (Blocked' Term Term) Term -> Term
    forall {t} {yes}. Reduced (Blocked' t yes) yes -> yes
    fromReduced (TCMT IO (Reduced (Blocked' Term Term) Term) -> TCMT IO Term)
    -> TCMT IO (Reduced (Blocked' Term Term) Term) -> TCMT IO Term
    forall a b. (a -> b) -> a -> b
    $ ReduceM (Reduced (Blocked' Term Term) Term)
    -> TCMT IO (Reduced (Blocked' Term Term) Term)
    forall a. ReduceM a -> TCM a
    runReduceM (ReduceM (Reduced (Blocked' Term Term) Term)
     -> TCMT IO (Reduced (Blocked' Term Term) Term))
    -> ReduceM (Reduced (Blocked' Term Term) Term)
    -> TCMT IO (Reduced (Blocked' Term Term) Term)
    forall a b. (a -> b) -> a -> b
    $
                          Term
    -> [Clause]
    -> RewriteRules
    -> MaybeReducedArgs
    -> ReduceM (Reduced (Blocked' Term Term) Term)
    appDef' (QName -> Elims -> Term
    Def QName
    f []) [Clause
    cl] [] ((Arg Term -> MaybeReduced (Arg Term))
    -> [Arg Term] -> MaybeReducedArgs
    forall a b. (a -> b) -> [a] -> [b]
    map Arg Term -> MaybeReduced (Arg Term)
    forall a. a -> MaybeReduced a
    notReduced ([Arg Term] -> MaybeReducedArgs) -> [Arg Term] -> MaybeReducedArgs
    forall a b. (a -> b) -> a -> b
    $ Int -> [Arg Term] -> [Arg Term]
    forall a. Subst a => Int -> a -> a
    raise (Tele (Dom Type) -> Int
    forall a. Sized a => a -> Int
    size Tele (Dom Type)
    delta) [Arg Term]
    args [Arg Term] -> [Arg Term] -> [Arg Term]
    forall a. [a] -> [a] -> [a]
    ++ Tele (Dom Type) -> [Arg Term]
    forall a t. DeBruijn a => Tele (Dom t) -> [Arg a]
    teleArgs Tele (Dom Type)
    delta)
                Term
    v1 <- Clause -> TCMT IO Term
    body Clause
    cl1
                Term
    v2 <- Clause -> TCMT IO Term
    body Clause
    cl2
                Type -> Term -> Term -> TCM ()
    forall (m :: * -> *).
    MonadConversion m =>
    Type -> Term -> Term -> m ()
    equalTerm Type
    t' Term
    v1 Term
    v2

          [([(Term, Bool)], Term)]
    sys <- [([(Int, Bool)], Clause)]
    -> (([(Int, Bool)], Clause) -> TCMT IO ([(Term, Bool)], Term))
    -> TCMT IO [([(Term, Bool)], Term)]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    t a -> (a -> m b) -> m (t b)
    forM ([[(Int, Bool)]] -> [Clause] -> [([(Int, Bool)], Clause)]
    forall a b. [a] -> [b] -> [(a, b)]
    zip [[(Int, Bool)]]
    alphas [Clause]
    cs) ((([(Int, Bool)], Clause) -> TCMT IO ([(Term, Bool)], Term))
     -> TCMT IO [([(Term, Bool)], Term)])
    -> (([(Int, Bool)], Clause) -> TCMT IO ([(Term, Bool)], Term))
    -> TCMT IO [([(Term, Bool)], Term)]
    forall a b. (a -> b) -> a -> b
    $ \ ([(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 (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 (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}. (Subst a, SubstArg a ~ 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 (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 (p :: * -> * -> *) a b c.
    Bifunctor p =>
    (a -> b) -> p a c -> p b c
    first Int -> Term
    var) [(Int, Bool)]
    alpha,Term
    u)

          [Char] -> Int -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "tc.sys.cover.sys" 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
    fsep ([TCMT IO Doc] -> TCMT IO Doc) -> [TCMT IO Doc] -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ Tele (Dom Type) -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Tele (Dom Type)
    gamma TCMT IO Doc -> [TCMT IO Doc] -> [TCMT IO Doc]
    forall a. a -> [a] -> [a]
    : (([(Term, Bool)], Term) -> TCMT IO Doc)
    -> [([(Term, Bool)], Term)] -> [TCMT IO Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map ([(Term, Bool)], Term) -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM [([(Term, Bool)], Term)]
    sys
          [Char] -> Int -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "tc.sys.cover.sys" Int
    40 (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
    fsep ([TCMT IO Doc] -> TCMT IO Doc) -> [TCMT IO Doc] -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ ([Char] -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => [Char] -> m Doc
    text ([Char] -> TCMT IO Doc)
    -> (Tele (Dom Type) -> [Char]) -> Tele (Dom Type) -> TCMT IO Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Tele (Dom Type) -> [Char]
    forall a. Show a => a -> [Char]
    show) Tele (Dom Type)
    gamma TCMT IO Doc -> [TCMT IO Doc] -> [TCMT IO Doc]
    forall a. a -> [a] -> [a]
    : (([(Term, Bool)], Term) -> TCMT IO Doc)
    -> [([(Term, Bool)], Term)] -> [TCMT IO Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map ([Char] -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => [Char] -> m Doc
    text ([Char] -> TCMT IO Doc)
    -> (([(Term, Bool)], Term) -> [Char])
    -> ([(Term, Bool)], Term)
    -> TCMT IO Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ([(Term, Bool)], Term) -> [Char]
    forall a. Show a => a -> [Char]
    show) [([(Term, Bool)], Term)]
    sys
          System -> TCMT IO System
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Tele (Dom Type) -> [([(Term, Bool)], Term)] -> System
    System Tele (Dom Type)
    gamma [([(Term, Bool)], Term)]
    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]
    aps) [ProblemEq]
    strippedPats RHS
    rhs0 WhereDeclarations
    wh Bool
    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] -> ([NamedArg Pattern] -> TCM ()) -> TCM ()
    forall (m :: * -> *) a.
    (Monad m, Null a) =>
    a -> (a -> m ()) -> m ()
    unlessNull ([NamedArg Pattern] -> [NamedArg Pattern]
    trailingWithPatterns [NamedArg Pattern]
    aps) (([NamedArg Pattern] -> TCM ()) -> TCM ())
    -> ([NamedArg Pattern] -> TCM ()) -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ \ [NamedArg Pattern]
    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
    $ [Pattern] -> TypeError
    UnexpectedWithPatterns ([Pattern] -> TypeError) -> [Pattern] -> TypeError
    forall a b. (a -> b) -> a -> b
    $ (NamedArg Pattern -> Pattern) -> [NamedArg Pattern] -> [Pattern]
    forall a b. (a -> b) -> [a] -> [b]
    map NamedArg Pattern -> Pattern
    forall a. NamedArg a -> a
    namedArg [NamedArg Pattern]
    withPats
        Call -> TCM a -> TCM a
    forall (m :: * -> *) a. MonadTrace m => Call -> m a -> m a
    traceCall (Type -> SpineClause -> Call
    CheckClause Type
    t SpineClause
    c) (TCM a -> TCM a) -> TCM a -> TCM a
    forall a b. (a -> b) -> a -> b
    $ do
          [NamedArg Pattern]
    aps <- [NamedArg Pattern] -> TCM [NamedArg Pattern]
    forall a. ExpandPatternSynonyms a => a -> TCM a
    expandPatternSynonyms [NamedArg Pattern]
    aps
          Bool -> TCM () -> TCM ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    unless ([ProblemEq] -> Bool
    forall a. Null a => a -> Bool
    null [ProblemEq]
    strippedPats) (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ [Char] -> Int -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "tc.lhs.top" Int
    50 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    forall a b. (a -> b) -> a -> b
    $
            TCMT IO Doc
    "strippedPats:" 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 [ Pattern -> TCMT IO Doc
    forall a (m :: * -> *).
    (ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
    a -> m Doc
    prettyA Pattern
    p 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
    <+> Term -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> 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
    <+> Dom Type -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Dom Type
    a | A.ProblemEq Pattern
    p Term
    v Dom Type
    a <- [ProblemEq]
    strippedPats ]
          Type
    closed_t <- (Tele (Dom Type) -> Type -> Type)
    -> Type -> Tele (Dom Type) -> Type
    forall a b c. (a -> b -> c) -> b -> a -> c
    flip Tele (Dom Type) -> Type -> Type
    forall t. Abstract t => Tele (Dom Type) -> t -> t
    abstract Type
    t (Tele (Dom Type) -> Type)
    -> TCMT IO (Tele (Dom Type)) -> TCMT IO Type
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> TCMT IO (Tele (Dom Type))
    forall (m :: * -> *).
    (Applicative m, MonadTCEnv m) =>
    m (Tele (Dom Type))
    getContextTelescope
          Call
    -> Maybe QName
    -> [NamedArg Pattern]
    -> Type
    -> Maybe Substitution
    -> [ProblemEq]
    -> (LHSResult -> TCM a)
    -> TCM a
    forall a.
    Call
    -> Maybe QName
    -> [NamedArg Pattern]
    -> Type
    -> Maybe Substitution
    -> [ProblemEq]
    -> (LHSResult -> TCM a)
    -> TCM a
    checkLeftHandSide (SpineLHS -> Call
    CheckLHS SpineLHS
    lhs) (QName -> Maybe QName
    forall a. a -> Maybe a
    Just QName
    x) [NamedArg Pattern]
    aps Type
    t Maybe Substitution
    withSub [ProblemEq]
    strippedPats LHSResult -> TCM a
    ret

    -- | Type check a function clause.

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

    checkClause :: Type
    -> Maybe Substitution
    -> SpineClause
    -> TCMT IO (Clause, ClausesPostChecks)
    checkClause Type
    t Maybe Substitution
    withSub c :: SpineClause
    c@(A.Clause lhs :: SpineLHS
    lhs@(A.SpineLHS LHSInfo
    i QName
    x [NamedArg Pattern]
    aps) [ProblemEq]
    strippedPats RHS
    rhs0 WhereDeclarations
    wh Bool
    catchall) = do
      [Name]
    cxtNames <- [Name] -> [Name]
    forall a. [a] -> [a]
    reverse ([Name] -> [Name])
    -> ([Dom' Term (Name, Type)] -> [Name])
    -> [Dom' Term (Name, Type)]
    -> [Name]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Dom' Term (Name, Type) -> Name)
    -> [Dom' Term (Name, Type)] -> [Name]
    forall a b. (a -> b) -> [a] -> [b]
    map ((Name, Type) -> Name
    forall a b. (a, b) -> a
    fst ((Name, Type) -> Name)
    -> (Dom' Term (Name, Type) -> (Name, Type))
    -> Dom' Term (Name, Type)
    -> Name
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Dom' Term (Name, Type) -> (Name, Type)
    forall t e. Dom' t e -> e
    unDom) ([Dom' Term (Name, Type)] -> [Name])
    -> TCMT IO [Dom' Term (Name, Type)] -> TCMT IO [Name]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> TCMT IO [Dom' Term (Name, Type)]
    forall (m :: * -> *). MonadTCEnv m => m [Dom' Term (Name, Type)]
    getContext
      Type
    -> Maybe Substitution
    -> SpineClause
    -> (LHSResult -> TCMT IO (Clause, ClausesPostChecks))
    -> TCMT IO (Clause, ClausesPostChecks)
    forall a.
    Type
    -> Maybe Substitution
    -> SpineClause
    -> (LHSResult -> TCM a)
    -> TCM a
    checkClauseLHS Type
    t Maybe Substitution
    withSub SpineClause
    c ((LHSResult -> TCMT IO (Clause, ClausesPostChecks))
     -> TCMT IO (Clause, ClausesPostChecks))
    -> (LHSResult -> TCMT IO (Clause, ClausesPostChecks))
    -> TCMT IO (Clause, ClausesPostChecks)
    forall a b. (a -> b) -> a -> b
    $ \ lhsResult :: LHSResult
    lhsResult@(LHSResult Int
    npars Tele (Dom Type)
    delta [NamedArg DeBruijnPattern]
    ps Bool
    absurdPat Arg Type
    trhs Substitution
    patSubst [AsBinding]
    asb IntSet
    psplit) -> 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.
            Type
    t' <- case Maybe Substitution
    withSub of
                    Just{}  -> Type -> TCMT IO Type
    forall (m :: * -> *) a. Monad m => a -> m a
    return Type
    t
                    Maybe Substitution
    Nothing -> do
                      Tele (Dom Type)
    theta <- ModuleName -> TCMT IO (Tele (Dom Type))
    forall (m :: * -> *).
    (Functor m, ReadTCState m) =>
    ModuleName -> m (Tele (Dom Type))
    lookupSection (QName -> ModuleName
    qnameModule QName
    x)
                      Type -> TCMT IO Type
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Type -> TCMT IO Type) -> Type -> TCMT IO Type
    forall a b. (a -> b) -> a -> b
    $ Tele (Dom Type) -> Type -> Type
    forall t. Abstract t => Tele (Dom Type) -> t -> t
    abstract Tele (Dom Type)
    theta Type
    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 = RHS -> RHS
    updateRHS RHS
    rhs0
                updateRHS :: RHS -> RHS
    updateRHS rhs :: RHS
    rhs@A.RHS{}               = RHS
    rhs
                updateRHS rhs :: RHS
    rhs@A.AbsurdRHS{}         = RHS
    rhs
                updateRHS (A.WithRHS QName
    q [WithExpr]
    es [Clause]
    cs)       = QName -> [WithExpr] -> [Clause] -> RHS
    A.WithRHS QName
    q [WithExpr]
    es ((Clause -> Clause) -> [Clause] -> [Clause]
    forall a b. (a -> b) -> [a] -> [b]
    map Clause -> Clause
    updateClause [Clause]
    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 :: Clause -> Clause
    updateClause (A.Clause LHS
    f [ProblemEq]
    spats RHS
    rhs WhereDeclarations
    wh Bool
    ca) =
                  LHS -> [ProblemEq] -> RHS -> WhereDeclarations -> Bool -> Clause
    forall lhs.
    lhs
    -> [ProblemEq] -> RHS -> WhereDeclarations -> Bool -> 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 Bool
    ca

            (Maybe Term
    body, WithFunctionProblem
    with) <- [AsBinding]
    -> TCM (Maybe Term, WithFunctionProblem)
    -> TCM (Maybe Term, WithFunctionProblem)
    forall a. [AsBinding] -> TCM a -> TCM a
    bindAsPatterns [AsBinding]
    asb (TCM (Maybe Term, WithFunctionProblem)
     -> TCM (Maybe Term, WithFunctionProblem))
    -> TCM (Maybe Term, WithFunctionProblem)
    -> TCM (Maybe Term, WithFunctionProblem)
    forall a b. (a -> b) -> a -> b
    $ 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
    $ LHSInfo
    -> QName
    -> [NamedArg Pattern]
    -> Type
    -> LHSResult
    -> RHS
    -> TCM (Maybe Term, WithFunctionProblem)
    checkRHS LHSInfo
    i QName
    x [NamedArg Pattern]
    aps Type
    t' LHSResult
    lhsResult RHS
    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).

            Maybe Term
    wbody <- TCMT IO (Maybe Term) -> TCMT IO (Maybe Term)
    forall (tcm :: * -> *) a.
    (MonadTCEnv tcm, ReadTCState tcm) =>
    tcm a -> tcm a
    unsafeInTopContext (TCMT IO (Maybe Term) -> TCMT IO (Maybe Term))
    -> TCMT IO (Maybe Term) -> TCMT IO (Maybe Term)
    forall a b. (a -> b) -> a -> b
    $ Account (BenchPhase (TCMT IO))
    -> TCMT IO (Maybe Term) -> TCMT IO (Maybe Term)
    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] (TCMT IO (Maybe Term) -> TCMT IO (Maybe Term))
    -> TCMT IO (Maybe Term) -> TCMT IO (Maybe Term)
    forall a b. (a -> b) -> a -> b
    $ [Name] -> WithFunctionProblem -> TCMT IO (Maybe Term)
    checkWithFunction [Name]
    cxtNames WithFunctionProblem
    with

            Maybe Term
    body <- Maybe Term -> TCMT IO (Maybe Term)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Maybe Term -> TCMT IO (Maybe Term))
    -> Maybe Term -> TCMT IO (Maybe Term)
    forall a b. (a -> b) -> a -> b
    $ Maybe Term
    body Maybe Term -> Maybe Term -> Maybe Term
    forall (m :: * -> *) a. MonadPlus m => m a -> m a -> m a
    `mplus` Maybe Term
    wbody

            TCMT IO Bool -> TCM () -> TCM ()
    forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
    whenM (PragmaOptions -> Bool
    optDoubleCheck (PragmaOptions -> Bool) -> TCMT IO PragmaOptions -> TCMT IO Bool
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> TCMT IO PragmaOptions
    forall (m :: * -> *). HasOptions m => m PragmaOptions
    pragmaOptions) (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ case Maybe Term
    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
    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
    prettyTCM (Arg Type -> Type
    forall e. Arg e -> e
    unArg Arg Type
    trhs))
                  ]
                TCM () -> TCM ()
    forall (m :: * -> *) a.
    (HasOptions m, MonadConstraint m, MonadDebug m, MonadError TCErr m,
     MonadFresh ProblemId m, MonadTCEnv m, MonadWarning m) =>
    m a -> m a
    nonConstraining (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ Term -> Comparison -> Type -> TCM ()
    forall (m :: * -> *).
    MonadCheckInternal m =>
    Term -> Comparison -> Type -> m ()
    checkInternal Term
    v Comparison
    CmpLeq (Type -> TCM ()) -> Type -> 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 (m :: * -> *) a. Monad m => a -> m a
    return ()

            [Char] -> Int -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "tc.lhs.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
    "Clause before translation:"
              , 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
    "delta =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> do Impossible -> Int -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *) a.
    MonadAddContext m =>
    Impossible -> Int -> m a -> m a
    escapeContext Impossible
    HasCallStack => Impossible
    impossible (Tele (Dom Type) -> Int
    forall a. Sized a => a -> Int
    size Tele (Dom Type)
    delta) (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ Tele (Dom Type) -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Tele (Dom Type)
    delta
                , TCMT IO Doc
    "ps    =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> do [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    P.fsep ([Doc] -> Doc) -> TCMT IO [Doc] -> TCMT IO Doc
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> [NamedArg DeBruijnPattern] -> TCMT IO [Doc]
    forall (m :: * -> *).
    MonadPretty m =>
    [NamedArg DeBruijnPattern] -> m [Doc]
    prettyTCMPatterns [NamedArg DeBruijnPattern]
    ps
                , TCMT IO Doc
    "body  =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> TCMT IO Doc -> (Term -> TCMT IO Doc) -> Maybe Term -> TCMT IO Doc
    forall b a. b -> (a -> b) -> Maybe a -> b
    maybe TCMT IO Doc
    "_|_" Term -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Maybe Term
    body
                , TCMT IO Doc
    "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
    prettyTCM Type
    t
                ]
              ]

            [Char] -> Int -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "tc.lhs.top" Int
    60 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ Impossible -> Int -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *) a.
    MonadAddContext m =>
    Impossible -> Int -> m a -> m a
    escapeContext Impossible
    HasCallStack => Impossible
    impossible (Tele (Dom Type) -> Int
    forall a. Sized a => a -> Int
    size Tele (Dom Type)
    delta) (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
    "Clause before translation (raw):"
              , 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
    "ps    =" 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 ([NamedArg DeBruijnPattern] -> [Char]
    forall a. Show a => a -> [Char]
    show [NamedArg DeBruijnPattern]
    ps)
                , TCMT IO Doc
    "body  =" 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 (Maybe Term -> [Char]
    forall a. Show a => a -> [Char]
    show Maybe Term
    body)
                , TCMT IO Doc
    "type  =" 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 (Type -> [Char]
    forall a. Show a => a -> [Char]
    show Type
    t)
                ]
              ]

            -- check naturality wrt the interval.
            let
              -- TODO:: Defined but not used
              iApplyVars :: [NamedArg DeBruijnPattern] -> [(Int, (Term,Term))]
              iApplyVars :: [NamedArg DeBruijnPattern] -> [(Int, (Term, Term))]
    iApplyVars [NamedArg DeBruijnPattern]
    ps = ((DeBruijnPattern -> [(Int, (Term, Term))])
     -> [DeBruijnPattern] -> [(Int, (Term, Term))])
    -> [DeBruijnPattern]
    -> (DeBruijnPattern -> [(Int, (Term, Term))])
    -> [(Int, (Term, Term))]
    forall a b c. (a -> b -> c) -> b -> a -> c
    flip (DeBruijnPattern -> [(Int, (Term, Term))])
    -> [DeBruijnPattern] -> [(Int, (Term, Term))]
    forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
    concatMap ((NamedArg DeBruijnPattern -> DeBruijnPattern)
    -> [NamedArg DeBruijnPattern] -> [DeBruijnPattern]
    forall a b. (a -> b) -> [a] -> [b]
    map NamedArg DeBruijnPattern -> DeBruijnPattern
    forall a. NamedArg a -> a
    namedArg [NamedArg DeBruijnPattern]
    ps) ((DeBruijnPattern -> [(Int, (Term, Term))])
     -> [(Int, (Term, Term))])
    -> (DeBruijnPattern -> [(Int, (Term, Term))])
    -> [(Int, (Term, Term))]
    forall a b. (a -> b) -> a -> b
    $ \case
                                 IApplyP PatternInfo
    _ Term
    t Term
    u DBPatVar
    x -> [(DBPatVar -> Int
    dbPatVarIndex DBPatVar
    x,(Term
    t,Term
    u))]
                                 VarP{} -> []
                                 ProjP{}-> []
                                 LitP{} -> []
                                 DotP{} -> []
                                 DefP PatternInfo
    _ QName
    _ [NamedArg DeBruijnPattern]
    ps -> [NamedArg DeBruijnPattern] -> [(Int, (Term, Term))]
    iApplyVars [NamedArg DeBruijnPattern]
    ps
                                 ConP ConHead
    _ ConPatternInfo
    _ [NamedArg DeBruijnPattern]
    ps -> [NamedArg DeBruijnPattern] -> [(Int, (Term, Term))]
    iApplyVars [NamedArg DeBruijnPattern]
    ps

            -- compute body modification for irrelevant definitions, see issue 610
            Relevance
    rel <- (TCEnv -> Relevance) -> TCMT IO Relevance
    forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
    asksTC TCEnv -> Relevance
    forall a. LensRelevance a => a -> Relevance
    getRelevance
            let bodyMod :: Maybe Term -> Maybe Term
    bodyMod Maybe Term
    body = case Relevance
    rel of
                  Relevance
    Irrelevant -> Term -> Term
    dontCare (Term -> Term) -> Maybe Term -> Maybe Term
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Maybe Term
    body
                  Relevance
    _          -> Maybe Term
    body

            -- absurd clauses don't define computational behaviour, so it's fine to
            -- treat them as catchalls.
            let catchall' :: Bool
    catchall' = Bool
    catchall Bool -> Bool -> Bool
    || Maybe Term -> Bool
    forall a. Maybe a -> Bool
    isNothing Maybe Term
    body

            -- absurd clauses are not exact
            let exact :: Maybe Bool
    exact = if Maybe Term -> Bool
    forall a. Maybe a -> Bool
    isNothing Maybe Term
    body then Bool -> Maybe Bool
    forall a. a -> Maybe a
    Just Bool
    False else Maybe Bool
    forall a. Maybe a
    Nothing -- we don't know yet

            (Clause, ClausesPostChecks) -> TCMT IO (Clause, ClausesPostChecks)
    forall (m :: * -> *) a. Monad m => a -> m a
    return ((Clause, ClausesPostChecks)
     -> TCMT IO (Clause, ClausesPostChecks))
    -> (Clause, ClausesPostChecks)
    -> TCMT IO (Clause, ClausesPostChecks)
    forall a b. (a -> b) -> a -> b
    $ (, IntSet -> ClausesPostChecks
    CPC IntSet
    psplit)
              Clause :: Range
    -> Range
    -> Tele (Dom Type)
    -> [NamedArg DeBruijnPattern]
    -> Maybe Term
    -> Maybe (Arg Type)
    -> Bool
    -> Maybe Bool
    -> Maybe Bool
    -> Maybe Bool
    -> ExpandedEllipsis
    -> Clause
    Clause { clauseLHSRange :: Range
    clauseLHSRange  = LHSInfo -> Range
    forall a. HasRange a => a -> Range
    getRange LHSInfo
    i
                     , clauseFullRange :: Range
    clauseFullRange = SpineClause -> Range
    forall a. HasRange a => a -> Range
    getRange SpineClause
    c
                     , clauseTel :: Tele (Dom Type)
    clauseTel       = KillRangeT (Tele (Dom Type))
    forall a. KillRange a => KillRangeT a
    killRange Tele (Dom Type)
    delta
                     , namedClausePats :: [NamedArg DeBruijnPattern]
    namedClausePats = [NamedArg DeBruijnPattern]
    ps
                     , clauseBody :: Maybe Term
    clauseBody      = Maybe Term -> Maybe Term
    bodyMod Maybe Term
    body
                     , clauseType :: Maybe (Arg Type)
    clauseType      = Arg Type -> Maybe (Arg Type)
    forall a. a -> Maybe a
    Just Arg Type
    trhs
                     , clauseCatchall :: Bool
    clauseCatchall  = Bool
    catchall'
                     , clauseExact :: Maybe Bool
    clauseExact       = Maybe Bool
    exact
                     , clauseRecursive :: Maybe Bool
    clauseRecursive   = Maybe Bool
    forall a. Maybe a
    Nothing -- we don't know yet
                     , clauseUnreachable :: Maybe Bool
    clauseUnreachable = Maybe Bool
    forall a. Maybe a
    Nothing -- we don't know yet
                     , clauseEllipsis :: ExpandedEllipsis
    clauseEllipsis  = LHSInfo -> ExpandedEllipsis
    lhsEllipsis LHSInfo
    i
                     }

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

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

      Pattern -> TCM Pattern
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Pattern -> TCM Pattern) -> Pattern -> TCM Pattern
    forall a b. (a -> b) -> a -> b
    $ ConPatInfo -> AmbiguousQName -> [NamedArg Pattern] -> Pattern
    forall e. ConPatInfo -> AmbiguousQName -> NAPs e -> Pattern' e
    A.ConP ConPatInfo
    patInfo (QName -> AmbiguousQName
    unambiguous (QName -> AmbiguousQName) -> QName -> AmbiguousQName
    forall a b. (a -> b) -> a -> b
    $ ConHead -> QName
    conName ConHead
    reflCon) [NamedArg Pattern]
    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]
    -> Type
    -> LHSResult
    -> RHS
    -> TCM (Maybe Term, WithFunctionProblem)
    checkRHS LHSInfo
    i QName
    x [NamedArg Pattern]
    aps Type
    t lhsResult :: LHSResult
    lhsResult@(LHSResult Int
    _ Tele (Dom Type)
    delta [NamedArg DeBruijnPattern]
    ps Bool
    absurdPat Arg Type
    trhs Substitution
    _ [AsBinding]
    _asb IntSet
    _) 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 [WithExpr]
    es [Clause]
    cs        -> QName
    -> [WithExpr] -> [Clause] -> TCM (Maybe Term, WithFunctionProblem)
    withRHS QName
    aux [WithExpr]
    es [Clause]
    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@.
        Maybe Term
    mv <- if Bool
    absurdPat
              then do
                [NamedArg DeBruijnPattern]
    ps <- [NamedArg DeBruijnPattern] -> TCMT IO [NamedArg DeBruijnPattern]
    forall a (m :: * -> *).
    (InstantiateFull a, MonadReduce m) =>
    a -> m a
    instantiateFull [NamedArg DeBruijnPattern]
    ps
                Maybe Term
    forall a. Maybe a
    Nothing Maybe Term -> TCM () -> TCMT IO (Maybe Term)
    forall (f :: * -> *) a b. Functor f => a -> f b -> f a
    <$ Expr -> TCM () -> TCM ()
    forall (m :: * -> *) x a.
    (MonadTrace m, HasRange x) =>
    x -> m a -> m a
    setCurrentRange Expr
    e (Warning -> TCM ()
    forall (m :: * -> *).
    (HasCallStack, MonadWarning m) =>
    Warning -> m ()
    warning (Warning -> TCM ()) -> Warning -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ [NamedArg DeBruijnPattern] -> Warning
    AbsurdPatternRequiresNoRHS [NamedArg DeBruijnPattern]
    ps)
              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)
        (Maybe Term, WithFunctionProblem)
    -> TCM (Maybe Term, WithFunctionProblem)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Maybe Term
    mv, WithFunctionProblem
    NoWithFunction)

      -- Absurd case: no right hand side
      noRHS :: TCM (Maybe Term, WithFunctionProblem)
      noRHS :: TCM (Maybe Term, WithFunctionProblem)
    noRHS = do
        Bool -> TCM () -> TCM ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    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 -> TCM ()) -> TypeError -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ [NamedArg Pattern] -> TypeError
    NoRHSRequiresAbsurdPattern [NamedArg Pattern]
    aps
        (Maybe Term, WithFunctionProblem)
    -> TCM (Maybe Term, WithFunctionProblem)
    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
              -> [A.WithExpr]  -- @[{a} in eqa, b in eqb, {{c}}, ...]@
              -> [A.Clause]    -- @[(ps1 = rhs1), (ps2 = rhs), ...]@
              -> TCM (Maybe Term, WithFunctionProblem)
      withRHS :: QName
    -> [WithExpr] -> [Clause] -> TCM (Maybe Term, WithFunctionProblem)
    withRHS QName
    aux [WithExpr]
    es [Clause]
    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"
          , [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
    $ QName -> TCMT IO Doc
    forall a (m :: * -> *).
    (ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
    a -> m Doc
    prettyA QName
    aux TCMT IO Doc -> [TCMT IO Doc] -> [TCMT IO Doc]
    forall a. a -> [a] -> [a]
    : (WithExpr -> TCMT IO Doc) -> [WithExpr] -> [TCMT IO Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map (TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Functor m => m Doc -> m Doc
    parens (TCMT IO Doc -> TCMT IO Doc)
    -> (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) [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
          Int
    nfv <- TCM Int
    getCurrentModuleFreeVars
          ModuleName
    m   <- TCMT IO ModuleName
    forall (m :: * -> *). MonadTCEnv m => m ModuleName
    currentModule
          [TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    sep [ TCMT IO Doc
    "with function module:" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+>
                 [TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Semigroup (m Doc), Foldable t) =>
    t (m Doc) -> m Doc
    prettyList ((Name -> TCMT IO Doc) -> [Name] -> [TCMT IO Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map Name -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM ([Name] -> [TCMT IO Doc]) -> [Name] -> [TCMT IO Doc]
    forall a b. (a -> b) -> a -> b
    $ ModuleName -> [Name]
    mnameToList ModuleName
    m)
              ,  [Char] -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => [Char] -> m Doc
    text ([Char] -> TCMT IO Doc) -> [Char] -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ [Char]
    "free variables: " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ Int -> [Char]
    forall a. Show a => a -> [Char]
    show Int
    nfv
              ]

        -- Infer the types of the with expressions

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

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

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

        QName
    -> QName
    -> Type
    -> LHSResult
    -> [Arg (Term, EqualityView)]
    -> [Clause]
    -> TCM (Maybe Term, WithFunctionProblem)
    checkWithRHS QName
    x QName
    aux Type
    t LHSResult
    lhsResult [Arg (Term, EqualityView)]
    vtys [Clause]
    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))
    pes -> QName
    -> [Named BindName (Pattern, Expr)]
    -> [RewriteEqn]
    -> TCM (Maybe Term, WithFunctionProblem)
    invertEqnRHS QName
    qname (List1 (Named BindName (Pattern, Expr))
    -> [Named BindName (Pattern, Expr)]
    forall a. NonEmpty a -> [a]
    List1.toList List1 (Named BindName (Pattern, Expr))
    pes) [RewriteEqn]
    rs

        where

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

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

          let pats :: [Arg Pattern]
    pats = ([Pattern] -> [Arg Pattern]) -> [[Pattern]] -> [Arg Pattern]
    forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
    concatMap ((Pattern -> Arg Pattern) -> [Pattern] -> [Arg Pattern]
    forall a b. (a -> b) -> [a] -> [b]
    map Pattern -> Arg Pattern
    forall a. a -> Arg a
    defaultArg) ([[Pattern]] -> [Arg Pattern]) -> [[Pattern]] -> [Arg Pattern]
    forall a b. (a -> b) -> a -> b
    $
                [Named BindName Pattern]
    -> (Named BindName Pattern -> [Pattern]) -> [[Pattern]]
    forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
    for [Named BindName Pattern]
    npats ((Named BindName Pattern -> [Pattern]) -> [[Pattern]])
    -> (Named BindName Pattern -> [Pattern]) -> [[Pattern]]
    forall a b. (a -> b) -> a -> b
    $ \ (Named Maybe BindName
    nm Pattern
    p) -> case Maybe BindName
    nm of
                  Maybe BindName
    Nothing -> [Pattern
    p]
                  Just BindName
    n  -> [Pattern
    p, BindName -> Pattern
    forall e. BindName -> Pattern' e
    A.VarP BindName
    n]

          -- 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.
          DefaultToInfty -> TCM ()
    solveSizeConstraints DefaultToInfty
    DefaultToInfty

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

          [Char] -> Int -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "tc.invert" Int
    60 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ [TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    vcat
            [ [Char] -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => [Char] -> m Doc
    text [Char]
    "invert"
            , TCMT IO Doc
    "  rhs' = " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall a. Semigroup a => a -> a -> a
    <> ([Char] -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => [Char] -> m Doc
    text ([Char] -> TCMT IO Doc) -> (RHS -> [Char]) -> RHS -> TCMT IO Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . RHS -> [Char]
    forall a. Show a => a -> [Char]
    show) RHS
    rhs'
            ]
          QName
    -> QName
    -> Type
    -> LHSResult
    -> [Arg (Term, EqualityView)]
    -> [Clause]
    -> TCM (Maybe Term, WithFunctionProblem)
    checkWithRHS QName
    x QName
    qname Type
    t LHSResult
    lhsResult [Arg (Term, EqualityView)]
    vtys [Clause
    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.
          TCState
    st <- TCMT IO TCState
    forall (m :: * -> *). MonadTCState m => m TCState
    getTC
          -- TODO:: recurse defined but not used
          let recurse :: TCM (Maybe Term, WithFunctionProblem)
    recurse = do
               TCState
    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 :: TCState -> TCState -> Bool
    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' InteractionPoints TCState -> InteractionPoints
    forall o i. o -> Lens' i o -> i
    ^.Lens' InteractionPoints TCState
    stInteractionPoints)
               Bool -> TCM () -> TCM ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    when (TCState -> TCState -> Bool
    sameIP TCState
    st TCState
    st') (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ TCState -> TCM ()
    forall (m :: * -> *). MonadTCState m => TCState -> m ()
    putTC TCState
    st
               RHS -> TCM (Maybe Term, WithFunctionProblem)
    handleRHS (RHS -> TCM (Maybe Term, WithFunctionProblem))
    -> RHS -> TCM (Maybe Term, WithFunctionProblem)
    forall a b. (a -> b) -> a -> b
    $ [RewriteEqn] -> [ProblemEq] -> RHS -> WhereDeclarations -> RHS
    A.RewriteRHS [RewriteEqn]
    rs [ProblemEq]
    strippedPats RHS
    rhs WhereDeclarations
    wh

          -- Get value and type of rewrite-expression.

          (Term
    proof, Type
    eqt) <- Expr -> TCM (Term, Type)
    inferExpr Expr
    eq

          -- 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.
          DefaultToInfty -> TCM ()
    solveSizeConstraints DefaultToInfty
    DefaultToInfty

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

          Type
    t' <- Type -> TCMT IO Type
    forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
    reduce (Type -> TCMT IO Type) -> TCMT IO Type -> TCMT IO Type
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< Type -> TCMT IO Type
    forall a (m :: * -> *).
    (InstantiateFull a, MonadReduce m) =>
    a -> m a
    instantiateFull Type
    eqt
          (EqualityView
    eqt,Type
    rewriteType,Term
    rewriteFrom,Term
    rewriteTo) <- Type -> TCM EqualityView
    equalityView Type
    t' TCM EqualityView
    -> (EqualityView -> TCMT IO (EqualityView, Type, Term, Term))
    -> TCMT IO (EqualityView, Type, Term, Term)
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \case
            eqt :: EqualityView
    eqt@(EqualityType Sort
    _s QName
    _eq [Arg Term]
    _params (Arg ArgInfo
    _ Term
    dom) Arg Term
    a Arg Term
    b) -> do
              Sort
    s <- Term -> TCMT IO Sort
    forall (m :: * -> *). (PureTCM m, MonadBlock m) => Term -> m Sort
    sortOf Term
    dom
              (EqualityView, Type, Term, Term)
    -> TCMT IO (EqualityView, Type, Term, Term)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (EqualityView
    eqt, Sort -> Term -> Type
    forall t a. Sort' t -> a -> Type'' t a
    El Sort
    s Term
    dom, Arg Term -> Term
    forall e. Arg e -> e
    unArg Arg Term
    a, Arg Term -> Term
    forall e. Arg e -> e
    unArg Arg Term
    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))
    -> (Doc -> TypeError)
    -> Doc
    -> TCMT IO (EqualityView, Type, Term, Term)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Doc -> TypeError
    GenericDocError (Doc -> TCMT IO (EqualityView, Type, Term, Term))
    -> TCMT IO Doc -> TCMT IO (EqualityView, Type, Term, Term)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< do
              TCMT IO Doc
    "Cannot rewrite by equation of 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
    prettyTCM 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))
    -> (Doc -> TypeError)
    -> Doc
    -> TCMT IO (EqualityView, Type, Term, Term)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Doc -> TypeError
    GenericDocError (Doc -> TCMT IO (EqualityView, Type, Term, Term))
    -> TCMT IO Doc -> TCMT IO (EqualityView, Type, Term, Term)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< do
              TCMT IO Doc
    "Cannot rewrite by equation of 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
    prettyTCM Type
    t'

          Pattern
    reflPat <- TCM Pattern
    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 :: TCMT IO Bool
    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

          ([Pattern]
    pats', Term
    withExpr, EqualityView
    withType) <- do
            TCMT IO Bool
    -> TCMT IO ([Pattern], Term, EqualityView)
    -> TCMT IO ([Pattern], Term, EqualityView)
    -> TCMT IO ([Pattern], Term, EqualityView)
    forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
    ifM TCMT IO Bool
    isReflexive
              {-then-} (([Pattern], Term, EqualityView)
    -> TCMT IO ([Pattern], Term, EqualityView)
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([ Pattern
    reflPat ]                    , Term
    proof, Type -> EqualityView
    OtherType Type
    t'))
              {-else-} (([Pattern], Term, EqualityView)
    -> TCMT IO ([Pattern], Term, EqualityView)
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([ PatInfo -> Pattern
    forall e. PatInfo -> Pattern' e
    A.WildP PatInfo
    patNoRange, Pattern
    reflPat ], Term
    proof, EqualityView
    eqt))
          let pats :: [Arg Pattern]
    pats = Pattern -> Arg Pattern
    forall a. a -> Arg a
    defaultArg (Pattern -> Arg Pattern) -> [Pattern] -> [Arg Pattern]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> [Pattern]
    pats'

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

          [Char] -> Int -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "tc.rewrite" Int
    60 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ [TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    vcat
            [ [Char] -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => [Char] -> m Doc
    text [Char]
    "rewrite"
            , TCMT IO Doc
    "  rhs' = " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall a. Semigroup a => a -> a -> a
    <> ([Char] -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => [Char] -> m Doc
    text ([Char] -> TCMT IO Doc) -> (RHS -> [Char]) -> RHS -> TCMT IO Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . RHS -> [Char]
    forall a. Show a => a -> [Char]
    show) RHS
    rhs'
            ]
          QName
    -> QName
    -> Type
    -> LHSResult
    -> [Arg (Term, EqualityView)]
    -> [Clause]
    -> TCM (Maybe Term, WithFunctionProblem)
    checkWithRHS QName
    x QName
    qname Type
    t LHSResult
    lhsResult [(Term, EqualityView) -> Arg (Term, EqualityView)
    forall a. a -> Arg a
    defaultArg (Term
    withExpr, EqualityView
    withType)] [Clause
    cl]

    checkWithRHS
      :: QName                             -- ^ Name of function.
      -> QName                             -- ^ Name of the with-function.
      -> Type                              -- ^ Type of function.
      -> LHSResult                         -- ^ Result of type-checking patterns
      -> [Arg (Term, EqualityView)]        -- ^ Expressions and types of with-expressions.
      -> [A.Clause]                        -- ^ With-clauses to check.
      -> TCM (Maybe Term, WithFunctionProblem)
                                    -- Note: as-bindings already bound (in checkClause)
    checkWithRHS :: QName
    -> QName
    -> Type
    -> LHSResult
    -> [Arg (Term, EqualityView)]
    -> [Clause]
    -> 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
    _) [Arg (Term, EqualityView)]
    vtys0 [Clause]
    cs =
      [Char]
    -> Int
    -> [Char]
    -> TCM (Maybe Term, WithFunctionProblem)
    -> TCM (Maybe Term, WithFunctionProblem)
    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
            [Arg Term]
    withArgs <- [Arg (Term, EqualityView)] -> TCM [Arg Term]
    withArguments [Arg (Term, EqualityView)]
    vtys0
            let perm :: Permutation
    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

            [Char] -> Int -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "tc.with.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] -> TCMT IO Doc) -> [TCMT IO Doc] -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $
              -- declared locally because we do not want to use the unzip'd thing!
              let ([Term]
    vs, [EqualityView]
    as) = (Arg (Term, EqualityView) -> (Term, EqualityView))
    -> [Arg (Term, EqualityView)] -> ([Term], [EqualityView])
    forall a b c. (a -> (b, c)) -> [a] -> ([b], [c])
    unzipWith Arg (Term, EqualityView) -> (Term, EqualityView)
    forall e. Arg e -> e
    unArg [Arg (Term, EqualityView)]
    vtys0 in
              [ TCMT IO Doc
    "vs (before normalization) =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> [Term] -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM [Term]
    vs
              , TCMT IO Doc
    "as (before normalization) =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> [EqualityView] -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM [EqualityView]
    as
              ]
            [Char] -> Int -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "tc.with.top" Int
    45 (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
    $
              -- declared locally because we do not want to use the unzip'd thing!
              let ([Term]
    vs, [EqualityView]
    as) = (Arg (Term, EqualityView) -> (Term, EqualityView))
    -> [Arg (Term, EqualityView)] -> ([Term], [EqualityView])
    forall a b c. (a -> (b, c)) -> [a] -> ([b], [c])
    unzipWith Arg (Term, EqualityView) -> (Term, EqualityView)
    forall e. Arg e -> e
    unArg [Arg (Term, EqualityView)]
    vtys0 in
              [ TCMT IO Doc
    "vs (before norm., raw) =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> [Term] -> TCMT IO Doc
    forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
    pretty [Term]
    vs
              ]
            [Arg (Term, EqualityView)]
    vtys0 <- [Arg (Term, EqualityView)] -> TCMT IO [Arg (Term, EqualityView)]
    forall a (m :: * -> *). (Normalise a, MonadReduce m) => a -> m a
    normalise [Arg (Term, EqualityView)]
    vtys0

            -- Andreas, 2012-09-17: for printing delta,
            -- we should remove it from the context first
            [Char] -> Int -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "tc.with.top" Int
    25 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ Impossible -> Int -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *) a.
    MonadAddContext m =>
    Impossible -> Int -> m a -> m a
    escapeContext Impossible
    HasCallStack => Impossible
    impossible (Tele (Dom Type) -> Int
    forall a. Sized a => a -> Int
    size Tele (Dom Type)
    delta) (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
    "delta  =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Tele (Dom Type) -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Tele (Dom Type)
    delta
              ]
            [Char] -> Int -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "tc.with.top" Int
    25 (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
    $
              -- declared locally because we do not want to use the unzip'd thing!
              let ([Term]
    vs, [EqualityView]
    as) = (Arg (Term, EqualityView) -> (Term, EqualityView))
    -> [Arg (Term, EqualityView)] -> ([Term], [EqualityView])
    forall a b c. (a -> (b, c)) -> [a] -> ([b], [c])
    unzipWith Arg (Term, EqualityView) -> (Term, EqualityView)
    forall e. Arg e -> e
    unArg [Arg (Term, EqualityView)]
    vtys0 in
              [ TCMT IO Doc
    "vs     =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> [Term] -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM [Term]
    vs
              , TCMT IO Doc
    "as     =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> [EqualityView] -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM [EqualityView]
    as
              , 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)
              ]

            -- Split the telescope into the part needed to type the with arguments
            -- and all the other stuff
            let (Tele (Dom Type)
    delta1, Tele (Dom Type)
    delta2, Permutation
    perm', Type
    t', [Arg (Term, EqualityView)]
    vtys) = Tele (Dom Type)
    -> Type
    -> [Arg (Term, EqualityView)]
    -> (Tele (Dom Type), Tele (Dom Type), Permutation, Type,
        [Arg (Term, EqualityView)])
    splitTelForWith Tele (Dom Type)
    delta (Arg Type -> Type
    forall e. Arg e -> e
    unArg Arg Type
    trhs) [Arg (Term, EqualityView)]
    vtys0
            let finalPerm :: Permutation
    finalPerm = Permutation -> Permutation -> Permutation
    composeP Permutation
    perm' Permutation
    perm

            [Char] -> Int -> [Char] -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> [Char] -> m ()
    reportSLn [Char]
    "tc.with.top" Int
    75 ([Char] -> TCM ()) -> [Char] -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ [Char]
    "delta  = " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ Tele (Dom Type) -> [Char]
    forall a. Show a => a -> [Char]
    show Tele (Dom Type)
    delta

            -- Andreas, 2012-09-17: for printing delta,
            -- we should remove it from the context first
            [Char] -> Int -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "tc.with.top" Int
    25 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ Impossible -> Int -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *) a.
    MonadAddContext m =>
    Impossible -> Int -> m a -> m a
    escapeContext Impossible
    HasCallStack => Impossible
    impossible (Tele (Dom Type) -> Int
    forall a. Sized a => a -> Int
    size Tele (Dom Type)
    delta) (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
    "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
    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
    addContext Tele (Dom Type)
    delta1 (Tele (Dom Type) -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Tele (Dom Type)
    delta2)
              ]
            [Char] -> Int -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "tc.with.top" Int
    25 (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
    "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)
              ]

            -- Create the body of the original function

            -- All the context variables
            [Term]
    us <- TCMT IO [Term]
    forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m [Term]
    getContextTerms
            let n :: Int
    n = [Term] -> Int
    forall a. Sized a => a -> Int
    size [Term]
    us
                m :: Int
    m = Tele (Dom Type) -> Int
    forall a. Sized a => a -> Int
    size Tele (Dom Type)
    delta
                -- First the variables bound outside this definition
                ([Term]
    us0, [Term]
    us1') = Int -> [Term] -> ([Term], [Term])
    forall a. Int -> [a] -> ([a], [a])
    splitAt (Int
    n Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - Int
    m) [Term]
    us
                -- Then permute the rest and grab those needed to for the with arguments
                ([Term]
    us1, [Term]
    us2)  = Int -> [Term] -> ([Term], [Term])
    forall a. Int -> [a] -> ([a], [a])
    splitAt (Tele (Dom Type) -> Int
    forall a. Sized a => a -> Int
    size Tele (Dom Type)
    delta1) ([Term] -> ([Term], [Term])) -> [Term] -> ([Term], [Term])
    forall a b. (a -> b) -> a -> b
    $ Permutation -> [Term] -> [Term]
    forall a. Permutation -> [a] -> [a]
    permute Permutation
    perm' [Term]
    us1'
                -- Now stuff the with arguments in between and finish with the remaining variables
                argsS :: Substitution
    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 [Arg Term]
    withArgs [Term] -> [Term] -> [Term]
    forall a. [a] -> [a] -> [a]
    ++ [Term]
    us2
                v :: Maybe a
    v         = Maybe a
    forall a. Maybe a
    Nothing -- generated by checkWithFunction
            -- Andreas, 2013-02-26 add with-name to signature for printing purposes
            QName -> Definition -> TCM ()
    addConstant QName
    aux (Definition -> TCM ()) -> TCMT IO Definition -> TCM ()
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< do
              Language
    lang <- TCMT IO Language
    forall (m :: * -> *). HasOptions m => m Language
    getLanguage
              Definition -> TCMT IO Definition
    useTerPragma (Definition -> TCMT IO Definition)
    -> Definition -> TCMT IO Definition
    forall a b. (a -> b) -> a -> b
    $
                ArgInfo -> QName -> Type -> Language -> Defn -> Definition
    defaultDefn ArgInfo
    defaultArgInfo QName
    aux Type
    HasCallStack => Type
    __DUMMY_TYPE__ Language
    lang
                  Defn
    emptyFunction

            [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] -> 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 ([Term]
    vs, [EqualityView]
    as) = (Arg (Term, EqualityView) -> (Term, EqualityView))
    -> [Arg (Term, EqualityView)] -> ([Term], [EqualityView])
    forall a b c. (a -> (b, c)) -> [a] -> ([b], [c])
    unzipWith Arg (Term, EqualityView) -> (Term, EqualityView)
    forall e. Arg e -> e
    unArg [Arg (Term, EqualityView)]
    vtys in
              [ TCMT IO Doc
    "    with arguments" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> do Impossible -> Int -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *) a.
    MonadAddContext m =>
    Impossible -> Int -> m a -> m a
    escapeContext Impossible
    HasCallStack => Impossible
    impossible (Tele (Dom Type) -> Int
    forall a. Sized a => a -> Int
    size Tele (Dom Type)
    delta) (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
    addContext Tele (Dom Type)
    delta1 (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, Semigroup (m Doc), Foldable t) =>
    t (m Doc) -> m Doc
    prettyList ((Term -> TCMT IO Doc) -> [Term] -> [TCMT IO Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map Term -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM [Term]
    vs)
              , TCMT IO Doc
    "             types" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> do Impossible -> Int -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *) a.
    MonadAddContext m =>
    Impossible -> Int -> m a -> m a
    escapeContext Impossible
    HasCallStack => Impossible
    impossible (Tele (Dom Type) -> Int
    forall a. Sized a => a -> Int
    size Tele (Dom Type)
    delta) (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
    addContext Tele (Dom Type)
    delta1 (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, Semigroup (m Doc), Foldable t) =>
    t (m Doc) -> m Doc
    prettyList ((EqualityView -> TCMT IO Doc) -> [EqualityView] -> [TCMT IO Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map EqualityView -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM [EqualityView]
    as)
              , TCMT IO Doc
    "           context" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> (Tele (Dom Type) -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM (Tele (Dom Type) -> TCMT IO Doc)
    -> TCMT IO (Tele (Dom Type)) -> TCMT IO Doc
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< TCMT IO (Tele (Dom Type))
    forall (m :: * -> *).
    (Applicative m, MonadTCEnv m) =>
    m (Tele (Dom Type))
    getContextTelescope)
              , TCMT IO Doc
    "             delta" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> do Impossible -> Int -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *) a.
    MonadAddContext m =>
    Impossible -> Int -> m a -> m a
    escapeContext Impossible
    HasCallStack => Impossible
    impossible (Tele (Dom Type) -> Int
    forall a. Sized a => a -> Int
    size Tele (Dom Type)
    delta) (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ Tele (Dom Type) -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Tele (Dom Type)
    delta
              , TCMT IO Doc
    "            delta1" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> do Impossible -> Int -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *) a.
    MonadAddContext m =>
    Impossible -> Int -> m a -> m a
    escapeContext Impossible
    HasCallStack => Impossible
    impossible (Tele (Dom Type) -> Int
    forall a. Sized a => a -> Int
    size Tele (Dom Type)
    delta) (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ Tele (Dom Type) -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Tele (Dom Type)
    delta1
              , TCMT IO Doc
    "            delta2" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> do Impossible -> Int -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *) a.
    MonadAddContext m =>
    Impossible -> Int -> m a -> m a
    escapeContext Impossible
    HasCallStack => Impossible
    impossible (Tele (Dom Type) -> Int
    forall a. Sized a => a -> Int
    size Tele (Dom Type)
    delta) (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
    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
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Tele (Dom Type)
    delta2
              ]

            (Maybe Term, WithFunctionProblem)
    -> TCM (Maybe Term, WithFunctionProblem)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Maybe Term
    forall a. Maybe a
    v, QName
    -> QName
    -> Type
    -> Tele (Dom Type)
    -> Tele (Dom Type)
    -> Tele (Dom Type)
    -> [Arg (Term, EqualityView)]
    -> Type
    -> [NamedArg DeBruijnPattern]
    -> Int
    -> Permutation
    -> Permutation
    -> Permutation
    -> [Clause]
    -> Substitution
    -> WithFunctionProblem
    WithFunction QName
    x QName
    aux Type
    t Tele (Dom Type)
    delta Tele (Dom Type)
    delta1 Tele (Dom Type)
    delta2 [Arg (Term, EqualityView)]
    vtys Type
    t' [NamedArg DeBruijnPattern]
    ps Int
    npars Permutation
    perm' Permutation
    perm Permutation
    finalPerm [Clause]
    cs Substitution
    argsS)

    -- | 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 (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 [Arg (Term, EqualityView)]
    vtys Type
    b [NamedArg DeBruijnPattern]
    qs Int
    npars Permutation
    perm' Permutation
    perm Permutation
    finalPerm [Clause]
    cs Substitution
    argsS) = do

      let -- Δ₁ ws Δ₂ ⊢ withSub : Δ′    (where Δ′ is the context of the parent lhs)
          withSub :: Substitution
          withSub :: Substitution
    withSub = let as :: [EqualityView]
    as = (Arg (Term, EqualityView) -> EqualityView)
    -> [Arg (Term, EqualityView)] -> [EqualityView]
    forall a b. (a -> b) -> [a] -> [b]
    map ((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) [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 ([EqualityView] -> Int
    countWithArgs [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 ([Term]
    vs, [EqualityView]
    as) = (Arg (Term, EqualityView) -> (Term, EqualityView))
    -> [Arg (Term, EqualityView)] -> ([Term], [EqualityView])
    forall a b c. (a -> (b, c)) -> [a] -> ([b], [c])
    unzipWith Arg (Term, EqualityView) -> (Term, EqualityView)
    forall e. Arg e -> e
    unArg [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
    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
    addContext Tele (Dom Type)
    delta1 (Tele (Dom Type) -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> 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
    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
    addContext Tele (Dom Type)
    delta1 ([EqualityView] -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM [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
    addContext Tele (Dom Type)
    delta1 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ [Term] -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM [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
    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
    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
    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
    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]
      Tele (Dom Type)
    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

      -- Generate the type of the with function
      (Type
    withFunType, Int
    n) <- do
        let ps :: [NamedArg DeBruijnPattern]
    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
        [Char] -> Int -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "tc.with.bndry" Int
    40 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    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
    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
    addContext Tele (Dom Type)
    delta2
                                      (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ [Char] -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => [Char] -> m Doc
    text [Char]
    "ps =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> [NamedArg DeBruijnPattern] -> TCMT IO Doc
    forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
    pretty [NamedArg DeBruijnPattern]
    ps
        let vs :: [Int]
    vs = [NamedArg DeBruijnPattern] -> [Int]
    forall a. DeBruijn a => [NamedArg (Pattern' a)] -> [Int]
    iApplyVars [NamedArg DeBruijnPattern]
    ps
        [(Int, (Term, Term))]
    bndry <- if [Int] -> Bool
    forall a. Null a => a -> Bool
    null [Int]
    vs then [(Int, (Term, Term))] -> TCMT IO [(Int, (Term, Term))]
    forall (m :: * -> *) a. Monad m => a -> m a
    return [] else do
          Term
    iz <- TCMT IO Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primIZero
          Term
    io <- TCMT IO Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primIOne
          let tm :: Term
    tm = QName -> Elims -> Term
    Def QName
    f ([NamedArg DeBruijnPattern] -> Elims
    patternsToElims [NamedArg DeBruijnPattern]
    ps)
          [(Int, (Term, Term))] -> TCMT IO [(Int, (Term, Term))]
    forall (m :: * -> *) a. Monad m => a -> m a
    return [(Int
    i,(Int -> Term -> Substitution
    forall a. EndoSubst a => Int -> a -> Substitution' a
    inplaceS Int
    i Term
    iz Substitution' (SubstArg Term) -> Term -> Term
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    `applySubst` Term
    tm, Int -> Term -> Substitution
    forall a. EndoSubst a => Int -> a -> Substitution' a
    inplaceS Int
    i Term
    io Substitution' (SubstArg Term) -> Term -> Term
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    `applySubst` Term
    tm)) | Int
    i <- [Int]
    vs]
        [Char] -> Int -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "tc.with.bndry" Int
    40 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    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
    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
    addContext Tele (Dom Type)
    delta2
                                      (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ [Char] -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => [Char] -> m Doc
    text [Char]
    "bndry =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> [(Int, (Term, Term))] -> TCMT IO Doc
    forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
    pretty [(Int, (Term, Term))]
    bndry
        Tele (Dom Type)
    -> [Arg (Term, EqualityView)]
    -> Tele (Dom Type)
    -> Type
    -> [(Int, (Term, Term))]
    -> TCMT IO (Type, Int)
    withFunctionType Tele (Dom Type)
    delta1 [Arg (Term, EqualityView)]
    vtys Tele (Dom Type)
    delta2 Type
    b [(Int, (Term, Term))]
    bndry
      [Char] -> Int -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "tc.with.type" 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
    "with-function type:", Int -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
    nest Int
    2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ Type -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Type
    withFunType ]
      [Char] -> Int -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "tc.with.type" Int
    50 (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
    "with-function type:", Int -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
    nest Int
    2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ Type -> TCMT IO Doc
    forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
    pretty Type
    withFunType ]

      Term
    call_in_parent <- do
        (TelV Tele (Dom Type)
    tel Type
    _,Boundary
    bs) <- Int -> Type -> TCMT IO (TelV Type, Boundary)
    forall (m :: * -> *).
    PureTCM m =>
    Int -> Type -> m (TelV Type, Boundary)
    telViewUpToPathBoundaryP (Int
    n Int -> Int -> Int
    forall a. Num a => a -> a -> a
    + Tele (Dom Type) -> Int
    forall a. Sized a => a -> Int
    size Tele (Dom Type)
    delta) Type
    withFunType
        Term -> TCMT IO Term
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Term -> TCMT IO Term) -> Term -> TCMT IO Term
    forall a b. (a -> b) -> a -> b
    $ Substitution
    Substitution' (SubstArg Term)
    argsS Substitution' (SubstArg Term) -> Term -> Term
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    `applySubst` QName -> Elims -> Term
    Def QName
    aux (Tele (Dom Type) -> Boundary -> Elims
    forall a.
    DeBruijn a =>
    Tele (Dom Type) -> Boundary' (a, a) -> [Elim' a]
    teleElims Tele (Dom Type)
    tel Boundary
    bs)

      [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
    $ Tele (Dom Type) -> TCMT IO Doc -> TCMT IO Doc
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    addContext Tele (Dom Type)
    delta (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Doc
    "with function call" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Term -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Term
    call_in_parent

      -- Andreas, 2013-10-21
      -- Check generated type directly in internal syntax.
      [Clause] -> TCM () -> TCM ()
    forall (m :: * -> *) x a.
    (MonadTrace m, HasRange x) =>
    x -> m a -> m a
    setCurrentRange [Clause]
    cs (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $
        Call -> TCM () -> TCM ()
    forall (m :: * -> *) a. MonadTrace m => Call -> m a -> m a
    traceCall Call
    NoHighlighting (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $   -- To avoid flicker.
        Call -> TCM () -> TCM ()
    forall (m :: * -> *) a. MonadTrace m => Call -> m a -> m a
    traceCall (Type -> Call
    CheckWithFunctionType Type
    withFunType) (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $
        Type -> TCM ()
    forall (m :: * -> *). MonadCheckInternal m => Type -> m ()
    checkType Type
    withFunType

      -- With display forms are closed
      Open DisplayForm
    df <- TCMT IO (Open DisplayForm) -> TCMT IO (Open DisplayForm)
    forall (tcm :: * -> *) a.
    (MonadTCEnv tcm, ReadTCState tcm) =>
    tcm a -> tcm a
    inTopContext (TCMT IO (Open DisplayForm) -> TCMT IO (Open DisplayForm))
    -> TCMT IO (Open DisplayForm) -> TCMT IO (Open DisplayForm)
    forall a b. (a -> b) -> a -> b
    $ DisplayForm -> TCMT IO (Open DisplayForm)
    forall (m :: * -> *) a.
    (ReadTCState m, MonadTCEnv m) =>
    a -> m (Open a)
    makeOpen (DisplayForm -> TCMT IO (Open DisplayForm))
    -> TCMT IO DisplayForm -> TCMT IO (Open DisplayForm)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< QName
    -> QName
    -> Tele (Dom Type)
    -> Tele (Dom Type)
    -> Int
    -> [NamedArg DeBruijnPattern]
    -> Permutation
    -> Permutation
    -> TCMT IO DisplayForm
    withDisplayForm QName
    f QName
    aux Tele (Dom Type)
    delta1 Tele (Dom Type)
    delta2 Int
    n [NamedArg DeBruijnPattern]
    qs Permutation
    perm' Permutation
    perm

      [Char] -> Int -> [Char] -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> [Char] -> m ()
    reportSLn [Char]
    "tc.with.top" Int
    20 [Char]
    "created with display form"

      case Open DisplayForm -> DisplayForm
    forall (t :: * -> *) a. Decoration t => t a -> a
    dget Open DisplayForm
    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, Semigroup (m Doc), 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
    prettyTCM Elims
    ts
            , DisplayTerm -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM DisplayTerm
    dt
            ]
      QName -> Definition -> TCM ()
    addConstant QName
    aux (Definition -> TCM ()) -> TCMT IO Definition -> TCM ()
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< do
        Language
    lang <- TCMT IO Language
    forall (m :: * -> *). HasOptions m => m Language
    getLanguage
        Definition -> TCMT IO Definition
    useTerPragma (Definition -> TCMT IO Definition)
    -> Definition -> TCMT IO Definition
    forall a b. (a -> b) -> a -> b
    $
          (ArgInfo -> QName -> Type -> Language -> Defn -> Definition
    defaultDefn ArgInfo
    defaultArgInfo QName
    aux Type
    withFunType Language
    lang Defn
    emptyFunction)
            { defDisplay :: [Open DisplayForm]
    defDisplay = [Open DisplayForm
    df] }
      -- solveSizeConstraints -- Andreas, 2012-10-16 does not seem necessary

      [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
    sep
        [ TCMT IO Doc
    "added with function" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> (QName -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM QName
    aux) TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> TCMT IO Doc
    "of type"
        , Int -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
    nest Int
    2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ Type -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Type
    withFunType
        , 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
    <+> (Tele (Dom Type) -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> 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
    =<< TCMT IO (Tele (Dom Type))
    forall (m :: * -> *).
    (Applicative m, MonadTCEnv m) =>
    m (Tele (Dom Type))
    getContextTelescope)
        ]
      [Char] -> Int -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "tc.with.top" 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
    vcat
        [ Int -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
    nest Int
    2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ [Char] -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => [Char] -> m Doc
    text ([Char] -> TCMT IO Doc) -> [Char] -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ [Char]
    "raw with func. type = " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ Type -> [Char]
    forall a. Show a => a -> [Char]
    show Type
    withFunType
        ]

      -- Construct the body for the with function
      [SpineClause]
    cs <- [SpineClause] -> TCMT IO [SpineClause]
    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 -> SpineClause) -> [Clause] -> [SpineClause]
    forall a b. (a -> b) -> [a] -> [b]
    map (Clause -> SpineClause
    forall a b. LHSToSpine a b => a -> b
    A.lhsToSpine) [Clause]
    cs
      [SpineClause]
    cs <- [Name]
    -> QName
    -> QName
    -> Type
    -> Tele (Dom Type)
    -> [NamedArg DeBruijnPattern]
    -> Int
    -> Substitution
    -> Permutation
    -> Int
    -> Int
    -> [SpineClause]
    -> TCMT IO [SpineClause]
    buildWithFunction [Name]
    cxtNames QName
    f QName
    aux Type
    t Tele (Dom Type)
    delta [NamedArg DeBruijnPattern]
    qs Int
    npars Substitution
    withSub Permutation
    finalPerm (Tele (Dom Type) -> Int
    forall a. Sized a => a -> Int
    size Tele (Dom Type)
    delta1) Int
    n [SpineClause]
    cs
      [Clause]
    cs <- [Clause] -> TCMT IO [Clause]
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([Clause] -> TCMT IO [Clause]) -> [Clause] -> TCMT IO [Clause]
    forall a b. (a -> b) -> a -> b
    $ (SpineClause -> Clause) -> [SpineClause] -> [Clause]
    forall a b. (a -> b) -> [a] -> [b]
    map (SpineClause -> Clause
    forall a b. LHSToSpine a b => b -> a
    A.spineToLhs) [SpineClause]
    cs

      -- #4833: inherit abstract mode from parent
      IsAbstract
    abstr <- Definition -> IsAbstract
    defAbstract (Definition -> IsAbstract)
    -> TCMT IO Definition -> TCMT IO IsAbstract
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> TCMT IO Definition -> TCMT IO Definition
    forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
    ignoreAbstractMode (QName -> TCMT IO Definition
    forall (m :: * -> *). HasConstInfo m => QName -> m Definition
    getConstInfo QName
    f)

      -- Check the with function
      let info :: DefInfo
    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 ([Clause] -> Range
    forall a. HasRange a => a -> Range
    getRange [Clause]
    cs)
      Type
    -> ArgInfo
    -> Delayed
    -> Maybe ExtLamInfo
    -> Maybe QName
    -> DefInfo
    -> QName
    -> Maybe Substitution
    -> [Clause]
    -> TCM ()
    checkFunDefS Type
    withFunType ArgInfo
    defaultArgInfo Delayed
    NotDelayed Maybe ExtLamInfo
    forall a. Maybe a
    Nothing (QName -> Maybe QName
    forall a. a -> Maybe a
    Just QName
    f) DefInfo
    info QName
    aux (Substitution -> Maybe Substitution
    forall a. a -> Maybe a
    Just Substitution
    withSub) [Clause]
    cs
      Maybe Term -> TCMT IO (Maybe Term)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Maybe Term -> TCMT IO (Maybe Term))
    -> Maybe Term -> TCMT IO (Maybe Term)
    forall a b. (a -> b) -> a -> b
    $ Term -> Maybe Term
    forall a. a -> Maybe a
    Just (Term -> Maybe Term) -> Term -> Maybe Term
    forall a b. (a -> b) -> a -> b
    $ Term
    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 Maybe Declaration
    ds) TCM a
    ret = do
      Maybe ModuleName -> TCM ()
    forall {m :: * -> *}.
    (MonadTrace m, MonadError TCErr m, PureTCM m,
     MonadInteractionPoints m, MonadFresh NameId m,
     MonadStConcreteNames m, IsString (m Doc), Null (m Doc),
     Semigroup (m Doc)) =>
    Maybe ModuleName -> m ()
    ensureNoNamedWhereInRefinedContext Maybe ModuleName
    whmod
      Maybe Declaration -> TCM a
    loop Maybe Declaration
    ds
      where
        loop :: Maybe Declaration -> TCM a
    loop = \case
          Maybe Declaration
    Nothing -> TCM a
    ret
          -- [A.ScopedDecl scope ds] -> withScope_ scope $ loop ds  -- IMPOSSIBLE
          Just (A.Section Range
    _ ModuleName
    m GeneralizeTelescope
    tel [Declaration]
    ds) -> ModuleName -> GeneralizeTelescope -> TCM a -> TCM a
    forall a. ModuleName -> GeneralizeTelescope -> TCM a -> TCM a
    newSection ModuleName
    m GeneralizeTelescope
    tel (TCM a -> TCM a) -> TCM a -> TCM a
    forall a b. (a -> b) -> a -> b
    $ do
              (TCEnv -> TCEnv) -> TCM a -> TCM a
    forall (m :: * -> *) a.
    MonadTCEnv m =>
    (TCEnv -> TCEnv) -> m a -> m a
    localTC (\ TCEnv
    e -> TCEnv
    e { envCheckingWhere :: Bool
    envCheckingWhere = Bool
    True }) (TCM a -> TCM a) -> TCM a -> TCM a
    forall a b. (a -> b) -> a -> b
    $ do
                [Declaration] -> TCM ()
    checkDecls [Declaration]
    ds
                TCM a
    ret
          Maybe Declaration
    _ -> TCM a
    forall a. HasCallStack => a
    __IMPOSSIBLE__

        -- #2897: We can't handle named where-modules in refined contexts.
        ensureNoNamedWhereInRefinedContext :: Maybe ModuleName -> m ()
    ensureNoNamedWhereInRefinedContext Maybe ModuleName
    Nothing = () -> m ()
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
        ensureNoNamedWhereInRefinedContext (Just ModuleName
    m) = Call -> m () -> m ()
    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
          [Term]
    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)
          Bool -> m () -> m ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    unless ([Term] -> Bool
    isWeakening [Term]
    args) (m () -> m ()) -> m () -> m ()
    forall a b. (a -> b) -> a -> b
    $ -- weakened contexts are fine
            Doc -> m ()
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    Doc -> m a
    genericDocError (Doc -> m ()) -> m Doc -> m ()
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< do
              [[Char]]
    names <- (Dom ([Char], Type) -> [Char]) -> [Dom ([Char], Type)] -> [[Char]]
    forall a b. (a -> b) -> [a] -> [b]
    map ([Char] -> [Char]
    argNameToString ([Char] -> [Char])
    -> (Dom ([Char], Type) -> [Char]) -> Dom ([Char], Type) -> [Char]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ([Char], Type) -> [Char]
    forall a b. (a, b) -> a
    fst (([Char], Type) -> [Char])
    -> (Dom ([Char], Type) -> ([Char], Type))
    -> Dom ([Char], Type)
    -> [Char]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Dom ([Char], Type) -> ([Char], Type)
    forall t e. Dom' t e -> e
    unDom) ([Dom ([Char], Type)] -> [[Char]])
    -> (Tele (Dom Type) -> [Dom ([Char], Type)])
    -> Tele (Dom Type)
    -> [[Char]]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Tele (Dom Type) -> [Dom ([Char], Type)]
    forall t. Tele (Dom t) -> [Dom ([Char], t)]
    telToList (Tele (Dom Type) -> [[Char]]) -> m (Tele (Dom Type)) -> m [[Char]]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$>
                        (ModuleName -> m (Tele (Dom Type))
    forall (m :: * -> *).
    (Functor m, ReadTCState m) =>
    ModuleName -> m (Tele (Dom Type))
    lookupSection (ModuleName -> m (Tele (Dom Type)))
    -> m ModuleName -> m (Tele (Dom Type))
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< m ModuleName
    forall (m :: * -> *). MonadTCEnv m => m ModuleName
    currentModule)
              let pr :: [Char] -> a -> m Doc
    pr [Char]
    x a
    v = [Char] -> m Doc
    forall (m :: * -> *). Applicative m => [Char] -> m Doc
    text ([Char]
    x [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    " =") m Doc -> m Doc -> m Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> a -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM a
    v
              [m Doc] -> m Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    vcat
                [ [m Doc] -> m Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    fsep ([Char] -> [m Doc]
    forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
    pwords ([Char] -> [m Doc]) -> [Char] -> [m Doc]
    forall a b. (a -> b) -> a -> b
    $ [Char]
    "Named where-modules are not allowed when module parameters have been refined by pattern matching. " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++
                                 [Char]
    "See https://github.com/agda/agda/issues/2897.")
                , [Char] -> m Doc
    forall (m :: * -> *). Applicative m => [Char] -> m Doc
    text ([Char] -> m Doc) -> [Char] -> m Doc
    forall a b. (a -> b) -> a -> b
    $ [Char]
    "In this case the module parameter" [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++
                         (if Bool -> Bool
    not ([Term] -> Bool
    forall a. Null a => a -> Bool
    null [Term]
    args) then [Char]
    "s have" else [Char]
    " has") [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++
                         [Char]
    " been refined to"
                , Int -> m Doc -> m Doc
    forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
    nest Int
    2 (m Doc -> m Doc) -> m Doc -> m Doc
    forall a b. (a -> b) -> a -> b
    $ [m Doc] -> m Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    vcat (([Char] -> Term -> m Doc) -> [[Char]] -> [Term] -> [m Doc]
    forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
    zipWith [Char] -> Term -> m Doc
    forall {m :: * -> *} {a}.
    (PrettyTCM a, PureTCM m, MonadInteractionPoints m,
     MonadFresh NameId m, MonadStConcreteNames m, IsString (m Doc),
     Null (m Doc), Semigroup (m Doc)) =>
    [Char] -> a -> m Doc
    pr [[Char]]
    names [Term]
    args) ]
          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 :: ModuleName -> A.GeneralizeTelescope -> TCM a -> TCM a
    newSection :: forall a. ModuleName -> GeneralizeTelescope -> TCM a -> TCM a
    newSection ModuleName
    m gtel :: GeneralizeTelescope
    gtel@(A.GeneralizeTel Map QName Name
    _ Telescope
    tel) TCM a
    cont = 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
    <+> ModuleName -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> 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)

      GeneralizeTelescope
    -> ([Maybe Name] -> Tele (Dom Type) -> TCM a) -> TCM a
    forall a.
    GeneralizeTelescope
    -> ([Maybe Name] -> Tele (Dom Type) -> TCM a) -> TCM a
    checkGeneralizeTelescope 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
    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
    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
      Closure ()
    clo <- () -> TCMT IO (Closure ())
    forall (m :: * -> *) a.
    (MonadTCEnv m, ReadTCState m) =>
    a -> m (Closure a)
    buildClosure ()
      (TCEnv -> TCEnv) -> TCM a -> TCM a
    forall (m :: * -> *) a.
    MonadTCEnv m =>
    (TCEnv -> TCEnv) -> m a -> m a
    localTC (\ TCEnv
    e -> TCEnv
    e { envClause :: IPClause
    envClause = QName
    -> Int
    -> Type
    -> Maybe Substitution
    -> SpineClause
    -> Closure ()
    -> [Closure IPBoundary]
    -> IPClause
    IPClause QName
    name Int
    i Type
    t Maybe Substitution
    sub SpineClause
    cl Closure ()
    clo [] }) TCM a
    ret