    {-# OPTIONS_GHC -Wunused-imports #-}

    {-# LANGUAGE NondecreasingIndentation #-}

    module Agda.TypeChecking.With where

    import Prelude hiding ((!!))

    import Control.Monad.Writer (WriterT, runWriterT, tell)

    import qualified Data.List as List
    import Data.Maybe
    import Data.Foldable ( foldrM )
    import Data.Semigroup ( sconcat )

    import Agda.Syntax.Common
    import Agda.Syntax.Internal as I
    import Agda.Syntax.Internal.Pattern
    import qualified Agda.Syntax.Abstract as A
    import Agda.Syntax.Abstract.Pattern as A
    import Agda.Syntax.Abstract.Views
    import Agda.Syntax.Info
    import Agda.Syntax.Position

    import Agda.TypeChecking.Abstract
    import Agda.TypeChecking.Datatypes
    import Agda.TypeChecking.EtaContract
    import Agda.TypeChecking.Free
    import Agda.TypeChecking.Monad
    import Agda.TypeChecking.Patterns.Abstract
    import Agda.TypeChecking.Pretty
    import Agda.TypeChecking.Primitive ( getRefl )
    import Agda.TypeChecking.Records
    import Agda.TypeChecking.Reduce
    import Agda.TypeChecking.Rules.LHS.Implicit
    import Agda.TypeChecking.Rules.LHS.Problem (ProblemEq(..))
    import Agda.TypeChecking.Substitute
    import Agda.TypeChecking.Telescope
    import Agda.TypeChecking.Telescope.Path
    import Agda.TypeChecking.Warnings ( warning )

    import Agda.Utils.Functor
    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 (empty)
    import Agda.Utils.Permutation
    import Agda.Syntax.Common.Pretty (prettyShow)
    import Agda.Utils.Singleton
    import Agda.Utils.Size

    import Agda.Utils.Impossible

    -- | Split pattern variables according to with-expressions.

    --   Input:
    --
    --   [@Δ@]         context of types and with-arguments.
    --
    --   [@Δ ⊢ t@]     type of rhs.
    --
    --   [@Δ ⊢ vs : as@]    with arguments and their types
    --
    --   Output:
    --
    --   [@Δ₁@]              part of context needed for with arguments and their types.
    --
    --   [@Δ₂@]              part of context not needed for with arguments and their types.
    --
    --   [@π@]               permutation from Δ to Δ₁Δ₂ as returned by 'splitTelescope'.
    --
    --   [@Δ₁Δ₂ ⊢ t'@]       type of rhs under @π@
    --
    --   [@Δ₁ ⊢ vs' : as'@]  with-arguments and their types depending only on @Δ₁@.

    splitTelForWith
      -- Input:
      :: Telescope                         -- ^ __@Δ@__             context of types and with-arguments.
      -> Type                              -- ^ __@Δ ⊢ t@__         type of rhs.
      -> List1 (Arg (Term, EqualityView))  -- ^ __@Δ ⊢ vs : as@__   with arguments and their types.
      -- Output:
      -> ( Telescope                         -- @Δ₁@             part of context needed for with arguments and their types.
         , Telescope                         -- @Δ₂@             part of context not needed for with arguments and their types.
         , Permutation                       -- @π@              permutation from Δ to Δ₁Δ₂ as returned by 'splitTelescope'.
         , Type                              -- @Δ₁Δ₂ ⊢ t'@      type of rhs under @π@
         , List1 (Arg (Term, EqualityView))  -- @Δ₁ ⊢ vs' : as'@ with- and rewrite-arguments and types under @π@.
         )              -- ^ (__@Δ₁@__,__@Δ₂@__,__@π@__,__@t'@__,__@vtys'@__) where
    --
    --   [@Δ₁@]        part of context needed for with arguments and their types.
    --
    --   [@Δ₂@]        part of context not needed for with arguments and their types.
    --
    --   [@π@]         permutation from Δ to Δ₁Δ₂ as returned by 'splitTelescope'.
    --
    --   [@Δ₁Δ₂ ⊢ t'@] type of rhs under @π@
    --
    --   [@Δ₁ ⊢ vtys'@]  with-arguments and their types under @π@.

    splitTelForWith :: Telescope
    -> Type
    -> List1 (Arg (Term, EqualityView))
    -> (Telescope, Telescope, Permutation, Type,
        List1 (Arg (Term, EqualityView)))
    splitTelForWith Telescope
    delta Type
    t List1 (Arg (Term, EqualityView))
    vtys = let
        -- Split the telescope into the part needed to type the with arguments
        -- and all the other stuff.
        fv :: VarSet
    fv = List1 (Arg (Term, EqualityView)) -> VarSet
    forall t. Free t => t -> VarSet
    allFreeVars List1 (Arg (Term, EqualityView))
    vtys
        SplitTel Telescope
    delta1 Telescope
    delta2 Permutation
    perm = VarSet -> Telescope -> SplitTel
    splitTelescope VarSet
    fv Telescope
    delta

        -- Δ₁Δ₂ ⊢ π : Δ
        pi :: Substitution' Term
    pi = Impossible -> Permutation -> Substitution' Term
    forall a.
    DeBruijn a =>
    Impossible -> Permutation -> Substitution' a
    renaming Impossible
    HasCallStack => Impossible
    impossible (Permutation -> Permutation
    reverseP Permutation
    perm)
        -- Δ₁ ⊢ ρ : Δ₁Δ₂  (We know that as does not depend on Δ₂.)
        rho :: Substitution' Term
    rho = Impossible -> Int -> Substitution' Term
    forall a. Impossible -> Int -> Substitution' a
    strengthenS Impossible
    HasCallStack => Impossible
    impossible (Int -> Substitution' Term) -> Int -> Substitution' Term
    forall a b. (a -> b) -> a -> b
    $ Telescope -> Int
    forall a. Sized a => a -> Int
    size Telescope
    delta2
        -- Δ₁ ⊢ ρ ∘ π : Δ
        rhopi :: Substitution' Term
    rhopi = Substitution' Term -> Substitution' Term -> Substitution' Term
    forall a.
    EndoSubst a =>
    Substitution' a -> Substitution' a -> Substitution' a
    composeS Substitution' Term
    rho Substitution' Term
    pi

        -- We need Δ₁Δ₂ ⊢ t'
        t' :: Type
    t' = Substitution' (SubstArg Type) -> Type -> Type
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    applySubst Substitution' Term
    Substitution' (SubstArg Type)
    pi Type
    t
        -- and Δ₁ ⊢ vtys'
        vtys' :: List1 (Arg (Term, EqualityView))
    vtys' = Substitution' (SubstArg (List1 (Arg (Term, EqualityView))))
    -> List1 (Arg (Term, EqualityView))
    -> List1 (Arg (Term, EqualityView))
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    applySubst Substitution' Term
    Substitution' (SubstArg (List1 (Arg (Term, EqualityView))))
    rhopi List1 (Arg (Term, EqualityView))
    vtys

      in (Telescope
    delta1, Telescope
    delta2, Permutation
    perm, Type
    t', List1 (Arg (Term, EqualityView))
    vtys')

    -- | Abstract with-expressions @vs@ to generate type for with-helper function.
    --
    -- Each @EqualityType@, coming from a @rewrite@, will turn into 2 abstractions.

    withFunctionType
      :: Telescope                          -- ^ @Δ₁@                        context for types of with-expressions.
      -> List1 (Arg (Term, EqualityView))   -- ^ @Δ₁,Δ₂ ⊢ vs : raise Δ₂ as@  with and rewrite-expressions and their type.
      -> Telescope                          -- ^ @Δ₁ ⊢ Δ₂@                   context extension to type with-expressions.
      -> Type                               -- ^ @Δ₁,Δ₂ ⊢ b@                 type of rhs.
      -> Boundary                           -- ^ @Δ₁,Δ₂ ⊢ [(i,(u0,u1))] : b@ boundary of rhs.
      -> TCM (Type, (Nat1, Nat))
        -- ^ @Δ₁ → wtel → Δ₂′ → b′@ such that
        --     @[vs/wtel]wtel = as@ and
        --     @[vs/wtel]Δ₂′ = Δ₂@ and
        --     @[vs/wtel]b′ = b@.
        -- Plus the final number of with-arguments and the number of visible ones.
    withFunctionType :: Telescope
    -> List1 (Arg (Term, EqualityView))
    -> Telescope
    -> Type
    -> Boundary
    -> TCM (Type, (Int, Int))
    withFunctionType Telescope
    delta1 List1 (Arg (Term, EqualityView))
    vtys Telescope
    delta2 Type
    b Boundary
    bndry = Telescope -> TCM (Type, (Int, Int)) -> TCM (Type, (Int, Int))
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    forall (m :: * -> *) a.
    MonadAddContext m =>
    Telescope -> m a -> m a
    addContext Telescope
    delta1 (TCM (Type, (Int, Int)) -> TCM (Type, (Int, Int)))
    -> TCM (Type, (Int, Int)) -> TCM (Type, (Int, Int))
    forall a b. (a -> b) -> a -> b
    $ do

      [Char] -> Int -> [Char] -> TCMT IO ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> [Char] -> m ()
    reportSLn [Char]
    "tc.with.abstract" Int
    20 ([Char] -> TCMT IO ()) -> [Char] -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $ [Char]
    "preparing for with-abstraction"

      -- Normalize and η-contract the type @b@ of the rhs and the types @delta2@
      -- of the pattern variables not mentioned in @vs : as@.
      let dbg :: Int -> [Char] -> a -> m ()
    dbg Int
    n [Char]
    s a
    x = [Char] -> Int -> TCMT IO Doc -> m ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "tc.with.abstract" Int
    n (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
    forall a b. (a -> b) -> a -> b
    $ Int -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
    nest Int
    2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ [Char] -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => [Char] -> m Doc
    text ([Char]
    s [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    " =") TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> a -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => a -> m Doc
    prettyTCM a
    x

      d2b <- Telescope -> Type -> Boundary -> TCM Type
    telePiPath_ Telescope
    delta2 Type
    b Boundary
    bndry
      dbg 30 "Δ₂ → B" d2b
      d2b  <- normalise d2b
      dbg 30 "normal Δ₂ → B" d2b
      d2b  <- etaContract d2b
      dbg 30 "eta-contracted Δ₂ → B" d2b

      vtys <- etaContract =<< normalise vtys

      -- wd2b = wtel → [vs : as] (Δ₂ → B)
      wd2b <- foldrM piAbstract d2b vtys
      dbg 30 "wΓ → Δ₂ → B" wd2b

      let nwithargs = NonEmpty EqualityView -> Int
    forall (f :: * -> *).
    (Functor f, Foldable f) =>
    f EqualityView -> Int
    countWithArgs (NonEmpty EqualityView -> Int) -> NonEmpty EqualityView -> Int
    forall a b. (a -> b) -> a -> b
    $ (Arg (Term, EqualityView) -> EqualityView)
    -> List1 (Arg (Term, EqualityView)) -> NonEmpty EqualityView
    forall a b. (a -> b) -> NonEmpty a -> NonEmpty b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap ((Term, EqualityView) -> EqualityView
    forall a b. (a, b) -> b
    snd ((Term, EqualityView) -> EqualityView)
    -> (Arg (Term, EqualityView) -> (Term, EqualityView))
    -> Arg (Term, EqualityView)
    -> EqualityView
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Arg (Term, EqualityView) -> (Term, EqualityView)
    forall e. Arg e -> e
    unArg) List1 (Arg (Term, EqualityView))
    vtys
      let nwithpats = List1 (Arg (Term, EqualityView)) -> Int
    forall (f :: * -> *).
    (Functor f, Foldable f) =>
    f (Arg (Term, EqualityView)) -> Int
    countWithPats List1 (Arg (Term, EqualityView))
    vtys

      TelV wtel _ <- telViewUpTo nwithargs wd2b

      -- select the boundary for "Δ₁" abstracting over "wΓ.Δ₂"
      let bndry' = [(Int, (Term, Term))] -> Boundary
    forall x a. [(x, (a, a))] -> Boundary' x a
    Boundary [(Int
    i Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - Int
    sd2,(Term -> Term
    lams Term
    u0, Term -> Term
    lams Term
    u1)) | (Int
    i,(Term
    u0,Term
    u1)) <- Boundary -> [(Int, (Term, Term))]
    forall x a. Boundary' x a -> [(x, (a, a))]
    theBoundary Boundary
    bndry, Int
    i Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    >= Int
    sd2]
            where sd2 :: Int
    sd2 = Telescope -> Int
    forall a. Sized a => a -> Int
    size Telescope
    delta2
                  lams :: Term -> Term
    lams = Telescope -> Term -> Term
    forall a. TeleNoAbs a => a -> Term -> Term
    teleNoAbs Telescope
    wtel (Term -> Term) -> (Term -> Term) -> Term -> Term
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Telescope -> Term -> Term
    forall t. Abstract t => Telescope -> t -> t
    abstract Telescope
    delta2

      d1wd2b <- telePiPath_ delta1 wd2b bndry'

      dbg 30 "Δ₁ → wΓ → Δ₂ → B" d1wd2b

      return (d1wd2b, (nwithargs, nwithpats))

    -- | Count the number of arguments introduced into the type of the with-function.
    countWithArgs :: (Functor f, Foldable f) => f EqualityView -> Nat1
    countWithArgs :: forall (f :: * -> *).
    (Functor f, Foldable f) =>
    f EqualityView -> Int
    countWithArgs = f Int -> Int
    forall a. Num a => f a -> a
    forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
    sum (f Int -> Int)
    -> (f EqualityView -> f Int) -> f EqualityView -> Int
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (EqualityView -> Int) -> f EqualityView -> f Int
    forall a b. (a -> b) -> f a -> f b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap EqualityView -> Int
    forall {a}. Num a => EqualityView -> a
    countArgs
      where
        countArgs :: EqualityView -> a
    countArgs OtherType{}    = a
    1
        countArgs IdiomType{}    = a
    2
        countArgs EqualityType{} = a
    2

    -- | Count the number of with-patterns in the with-clause
    --   that need to be transformed to regular patterns
    --   in the **current round** of with-abstraction
    --   (important for nested with).
    countWithPats :: (Functor f, Foldable f) => f (Arg (Term, EqualityView)) -> Nat1
    countWithPats :: forall (f :: * -> *).
    (Functor f, Foldable f) =>
    f (Arg (Term, EqualityView)) -> Int
    countWithPats = f Int -> Int
    forall a. Num a => f a -> a
    forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
    sum (f Int -> Int)
    -> (f (Arg (Term, EqualityView)) -> f Int)
    -> f (Arg (Term, EqualityView))
    -> Int
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Arg (Term, EqualityView) -> Int)
    -> f (Arg (Term, EqualityView)) -> f Int
    forall a b. (a -> b) -> f a -> f b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap \case
        -- Andreas, 2025-04-08, see issue #7788.
        Arg ArgInfo
    ai (Term
    _, OtherType   {}) -> if ArgInfo -> Bool
    forall a. LensHiding a => a -> Bool
    visible ArgInfo
    ai then Int
    1 else Int
    0
          -- A hidden @with@ (issue #500) does not have a with-pattern in the abstract syntax.
        Arg ArgInfo
    ai (Term
    _, IdiomType   {}) -> if ArgInfo -> Bool
    forall a. LensHiding a => a -> Bool
    visible ArgInfo
    ai then Int
    2 else Int
    1
          -- The hidden version of the inspect idiom has just one with-pattern in the abstract syntax.
        Arg ArgInfo
    ai (Term
    _, EqualityType{}) -> if ArgInfo -> Bool
    forall a. LensHiding a => a -> Bool
    visible ArgInfo
    ai then Int
    2 else Int
    forall a. HasCallStack => a
    __IMPOSSIBLE__
          -- The desugaring of @rewrite@ produces two new with-patterns in the abstract syntax.
          -- They are always @NotHidden@.

    -- | From a list of @with@ and @rewrite@ expressions and their types,
    --   compute the list of final @with@ expressions (after expanding the @rewrite@s).
    withArguments :: List1 (Arg (Term, EqualityView)) ->
                     TCM (List1 (Arg Term))
    withArguments :: List1 (Arg (Term, EqualityView)) -> TCM (List1 (Arg Term))
    withArguments List1 (Arg (Term, EqualityView))
    vtys = do
      NonEmpty (List1 (Arg Term)) -> List1 (Arg Term)
    forall a. Semigroup a => NonEmpty a -> a
    sconcat (NonEmpty (List1 (Arg Term)) -> List1 (Arg Term))
    -> TCMT IO (NonEmpty (List1 (Arg Term))) -> TCM (List1 (Arg Term))
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> do
        List1 (Arg (Term, EqualityView))
    -> (Arg (Term, EqualityView) -> TCM (List1 (Arg Term)))
    -> TCMT IO (NonEmpty (List1 (Arg Term)))
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    t a -> (a -> m b) -> m (t b)
    forM List1 (Arg (Term, EqualityView))
    vtys ((Arg (Term, EqualityView) -> TCM (List1 (Arg Term)))
     -> TCMT IO (NonEmpty (List1 (Arg Term))))
    -> (Arg (Term, EqualityView) -> TCM (List1 (Arg Term)))
    -> TCMT IO (NonEmpty (List1 (Arg Term)))
    forall a b. (a -> b) -> a -> b
    $ \ (Arg ArgInfo
    info (Term, EqualityView)
    ts) -> do
          (Term -> Arg Term) -> NonEmpty Term -> List1 (Arg Term)
    forall a b. (a -> b) -> NonEmpty a -> NonEmpty b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (ArgInfo -> Term -> Arg Term
    forall e. ArgInfo -> e -> Arg e
    Arg ArgInfo
    info) (NonEmpty Term -> List1 (Arg Term))
    -> TCMT IO (NonEmpty Term) -> TCM (List1 (Arg Term))
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> do
            case (Term, EqualityView)
    ts of
              (Term
    v, OtherType Type
    a) -> do
                NonEmpty Term -> TCMT IO (NonEmpty Term)
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (NonEmpty Term -> TCMT IO (NonEmpty Term))
    -> NonEmpty Term -> TCMT IO (NonEmpty Term)
    forall a b. (a -> b) -> a -> b
    $ Term -> NonEmpty Term
    forall el coll. Singleton el coll => el -> coll
    singleton Term
    v
              (Term
    prf, eqt :: EqualityView
    eqt@(EqualityType Range
    _r Sort
    _s QName
    _eq Args
    _pars Arg Term
    _t Arg Term
    v Arg Term
    _v')) -> do
                NonEmpty Term -> TCMT IO (NonEmpty Term)
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (NonEmpty Term -> TCMT IO (NonEmpty Term))
    -> NonEmpty Term -> TCMT IO (NonEmpty Term)
    forall a b. (a -> b) -> a -> b
    $ Arg Term -> Term
    forall e. Arg e -> e
    unArg Arg Term
    v Term -> [Term] -> NonEmpty Term
    forall a. a -> [a] -> NonEmpty a
    :| Term
    prf Term -> [Term] -> [Term]
    forall a. a -> [a] -> [a]
    : []
              (Term
    v, IdiomType Type
    t) -> do
                mkRefl <- TCM (Arg Term -> Term)
    getRefl
                return $ v :| mkRefl (defaultArg v) : []

    -- | Compute the clauses for the with-function given the original patterns.
    buildWithFunction
      :: [Name]               -- ^ Names of the module parameters of the parent function.
      -> QName                -- ^ Name of the parent function.
      -> QName                -- ^ Name of the with-function.
      -> Type                 -- ^ Types of the parent function.
      -> Telescope            -- ^ Context of parent patterns.
      -> [NamedArg DeBruijnPattern] -- ^ Parent patterns.
      -> Nat                  -- ^ Number of module parameters in parent patterns
      -> Substitution         -- ^ Substitution from parent lhs to with function lhs
      -> Permutation          -- ^ Final permutation.
      -> Nat                  -- ^ Number of needed vars.
      -> Nat                  -- ^ Number of with expressions.
      -> List1 A.SpineClause  -- ^ With-clauses.
      -> TCM (List1 A.SpineClause) -- ^ With-clauses flattened wrt. parent patterns.
    buildWithFunction :: [Name]
    -> QName
    -> QName
    -> Type
    -> Telescope
    -> [NamedArg DeBruijnPattern]
    -> Int
    -> Substitution' Term
    -> Permutation
    -> Int
    -> Int
    -> List1 (Clause' SpineLHS)
    -> TCM (List1 (Clause' SpineLHS))
    buildWithFunction [Name]
    cxtNames QName
    f QName
    aux Type
    t Telescope
    delta [NamedArg DeBruijnPattern]
    qs Int
    npars Substitution' Term
    withSub Permutation
    perm Int
    n1 Int
    n List1 (Clause' SpineLHS)
    cs = (Clause' SpineLHS -> TCMT IO (Clause' SpineLHS))
    -> List1 (Clause' SpineLHS) -> TCM (List1 (Clause' SpineLHS))
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> NonEmpty a -> m (NonEmpty b)
    mapM Clause' SpineLHS -> TCMT IO (Clause' SpineLHS)
    buildWithClause List1 (Clause' SpineLHS)
    cs
      where
        -- Nested with-functions will iterate this function once for each parent clause.
        buildWithClause :: Clause' SpineLHS -> TCMT IO (Clause' SpineLHS)
    buildWithClause (A.Clause lhs :: SpineLHS
    lhs@(A.SpineLHS LHSInfo
    i QName
    _ [NamedArg Pattern]
    allPs) [ProblemEq]
    inheritedPats RHS
    rhs WhereDeclarations
    wh Catchall
    catchall) = do
          let ([NamedArg Pattern]
    ps, [NamedArg Pattern]
    wps)    = [NamedArg Pattern] -> ([NamedArg Pattern], [NamedArg Pattern])
    splitOffTrailingWithPatterns [NamedArg Pattern]
    allPs
              ([NamedArg Pattern]
    wps0, [NamedArg Pattern]
    wps1) = Int
    -> [NamedArg Pattern] -> ([NamedArg Pattern], [NamedArg Pattern])
    forall a. Int -> [a] -> ([a], [a])
    splitAt Int
    n [NamedArg Pattern]
    wps
              ps0 :: [NamedArg Pattern]
    ps0          = (NamedArg Pattern -> NamedArg Pattern)
    -> [NamedArg Pattern] -> [NamedArg Pattern]
    forall a b. (a -> b) -> [a] -> [b]
    map ((Pattern -> Pattern) -> NamedArg Pattern -> NamedArg Pattern
    forall a b. (a -> b) -> NamedArg a -> NamedArg b
    updateNamedArg Pattern -> Pattern
    forall {e}. Pattern' e -> Pattern' e
    fromWithP) [NamedArg Pattern]
    wps0
                where
                fromWithP :: Pattern' e -> Pattern' e
    fromWithP (A.WithP PatInfo
    _ Pattern' e
    p) = Pattern' e
    p
                fromWithP Pattern' e
    _ = Pattern' e
    forall a. HasCallStack => a
    __IMPOSSIBLE__

          [Char] -> Int -> TCMT IO Doc -> TCMT IO ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "tc.with.split" Int
    40 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
    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
    "buildWithClause"
            , Int -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
    nest Int
    2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Doc
    "n    =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Int -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => Int -> m Doc
    prettyTCM Int
    n
            , 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
    "wps  =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> [NamedArg Pattern] -> TCMT IO Doc
    forall a (m :: * -> *).
    (ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
    a -> m Doc
    prettyA [NamedArg Pattern]
    wps
            , 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
    "wps0 =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> [NamedArg Pattern] -> TCMT IO Doc
    forall a (m :: * -> *).
    (ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
    a -> m Doc
    prettyA [NamedArg Pattern]
    wps0
            , 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
    "wps1 =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> [NamedArg Pattern] -> TCMT IO Doc
    forall a (m :: * -> *).
    (ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
    a -> m Doc
    prettyA [NamedArg Pattern]
    wps1
            ]

          -- Andreas, 2025-04-07, issue #7759
          -- Usually the following is impossible because the with-clause collection
          -- already looks for the correct number of with-patterns.
          -- However, if the lhs is just an ellipsis, we can slip through the cracks.
          -- Thus, we install another check here to enforce the correct number of with-patterns.
          Bool -> TCMT IO () -> TCMT IO ()
    forall b (m :: * -> *). (IsBool b, Monad m) => b -> m () -> m ()
    when ([NamedArg Pattern] -> Int
    forall a. [a] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length [NamedArg Pattern]
    wps0 Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    < Int
    n) (TCMT IO () -> TCMT IO ()) -> TCMT IO () -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $
            SpineLHS -> TCMT IO () -> TCMT IO ()
    forall (m :: * -> *) x a.
    (MonadTrace m, HasRange x) =>
    x -> m a -> m a
    setCurrentRange SpineLHS
    lhs (TCMT IO () -> TCMT IO ()) -> TCMT IO () -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $ TypeError -> TCMT IO ()
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    TypeError -> m a
    typeError TypeError
    TooFewPatternsInWithClause

          [Char] -> Int -> TCMT IO Doc -> TCMT IO ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "tc.with" Int
    50 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Doc
    "inheritedPats:" 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
    forall (m :: * -> *). MonadPretty m => Term -> m Doc
    prettyTCM Term
    v TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> TCMT IO Doc
    ":" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Dom Type -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => Dom Type -> m Doc
    prettyTCM Dom Type
    a
            | A.ProblemEq Pattern
    p Term
    v Dom Type
    a <- [ProblemEq]
    inheritedPats
            ]
          (strippedPats, ps') <- [Name]
    -> QName
    -> QName
    -> Type
    -> Telescope
    -> [NamedArg DeBruijnPattern]
    -> Int
    -> Permutation
    -> [NamedArg Pattern]
    -> TCM ([ProblemEq], [NamedArg Pattern])
    stripWithClausePatterns [Name]
    cxtNames QName
    f QName
    aux Type
    t Telescope
    delta [NamedArg DeBruijnPattern]
    qs Int
    npars Permutation
    perm [NamedArg Pattern]
    ps
          reportSDoc "tc.with" 50 $ hang "strippedPats:" 2 $
                                      vcat [ prettyA p <+> "==" <+> prettyTCM v <+> (":" <+> prettyTCM t)
                                           | A.ProblemEq p v t <- strippedPats ]
          rhs <- buildRHS strippedPats rhs
          let (ps1, ps2) = splitAt n1 ps'
          let result = SpineLHS
    -> [ProblemEq]
    -> RHS
    -> WhereDeclarations
    -> Catchall
    -> Clause' SpineLHS
    forall lhs.
    lhs
    -> [ProblemEq]
    -> RHS
    -> WhereDeclarations
    -> Catchall
    -> Clause' lhs
    A.Clause (LHSInfo -> QName -> [NamedArg Pattern] -> SpineLHS
    A.SpineLHS LHSInfo
    i QName
    aux ([NamedArg Pattern] -> SpineLHS) -> [NamedArg Pattern] -> SpineLHS
    forall a b. (a -> b) -> a -> b
    $ [NamedArg Pattern]
    ps1 [NamedArg Pattern] -> [NamedArg Pattern] -> [NamedArg Pattern]
    forall a. [a] -> [a] -> [a]
    ++ [NamedArg Pattern]
    ps0 [NamedArg Pattern] -> [NamedArg Pattern] -> [NamedArg Pattern]
    forall a. [a] -> [a] -> [a]
    ++ [NamedArg Pattern]
    ps2 [NamedArg Pattern] -> [NamedArg Pattern] -> [NamedArg Pattern]
    forall a. [a] -> [a] -> [a]
    ++ [NamedArg Pattern]
    wps1)
                         ([ProblemEq]
    inheritedPats [ProblemEq] -> [ProblemEq] -> [ProblemEq]
    forall a. [a] -> [a] -> [a]
    ++ [ProblemEq]
    strippedPats)
                         RHS
    rhs WhereDeclarations
    wh Catchall
    catchall
          reportSDoc "tc.with" 20 $ vcat
            [ "buildWithClause returns" <+> prettyA result
            ]
          return result

        buildRHS :: [ProblemEq] -> RHS -> TCMT IO RHS
    buildRHS [ProblemEq]
    _ rhs :: RHS
    rhs@A.RHS{}                 = RHS -> TCMT IO RHS
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return RHS
    rhs
        buildRHS [ProblemEq]
    _ rhs :: RHS
    rhs@RHS
    A.AbsurdRHS             = RHS -> TCMT IO RHS
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return RHS
    rhs
        buildRHS [ProblemEq]
    _ (A.WithRHS QName
    q List1 WithExpr
    es List1 Clause
    cs)         = QName -> List1 WithExpr -> List1 Clause -> RHS
    A.WithRHS QName
    q List1 WithExpr
    es (List1 Clause -> RHS) -> TCMT IO (List1 Clause) -> TCMT IO RHS
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$>
          (Clause -> TCMT IO Clause)
    -> List1 Clause -> TCMT IO (List1 Clause)
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> NonEmpty a -> m (NonEmpty b)
    mapM ((Clause' SpineLHS -> Clause
    forall a b. LHSToSpine a b => b -> a
    A.spineToLhs (Clause' SpineLHS -> Clause)
    -> (Clause' SpineLHS -> Clause' SpineLHS)
    -> Clause' SpineLHS
    -> Clause
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Clause' SpineLHS -> Clause' SpineLHS
    permuteNamedDots) (Clause' SpineLHS -> Clause)
    -> (Clause -> TCMT IO (Clause' SpineLHS))
    -> Clause
    -> TCMT IO Clause
    forall (m :: * -> *) b c a.
    Functor m =>
    (b -> c) -> (a -> m b) -> a -> m c
    <.> Clause' SpineLHS -> TCMT IO (Clause' SpineLHS)
    buildWithClause (Clause' SpineLHS -> TCMT IO (Clause' SpineLHS))
    -> (Clause -> Clause' SpineLHS)
    -> Clause
    -> TCMT IO (Clause' SpineLHS)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Clause -> Clause' SpineLHS
    forall a b. LHSToSpine a b => a -> b
    A.lhsToSpine) List1 Clause
    cs
        buildRHS [ProblemEq]
    strippedPats1 (A.RewriteRHS [RewriteEqn]
    qes [ProblemEq]
    strippedPats2 RHS
    rhs WhereDeclarations
    wh) =
          (RHS -> WhereDeclarations -> RHS)
    -> WhereDeclarations -> RHS -> RHS
    forall a b c. (a -> b -> c) -> b -> a -> c
    flip ([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' Term
    Substitution' (SubstArg [ProblemEq])
    withSub ([ProblemEq] -> [ProblemEq]) -> [ProblemEq] -> [ProblemEq]
    forall a b. (a -> b) -> a -> b
    $ [ProblemEq]
    strippedPats1 [ProblemEq] -> [ProblemEq] -> [ProblemEq]
    forall a. [a] -> [a] -> [a]
    ++ [ProblemEq]
    strippedPats2)) WhereDeclarations
    wh (RHS -> RHS) -> TCMT IO RHS -> TCMT IO RHS
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> [ProblemEq] -> RHS -> TCMT IO RHS
    buildRHS [] RHS
    rhs

        -- The stripped patterns computed by buildWithClause lives in the context
        -- of the top with-clause (of the current call to buildWithFunction). When
        -- we recurse we expect inherited patterns to live in the context
        -- of the innermost parent clause. Note that this makes them live in the
        -- context of the with-function arguments before any pattern matching. We
        -- need to update again once the with-clause patterns have been checked.
        -- This happens in Rules.Def.checkClause before calling checkRHS.
        permuteNamedDots :: A.SpineClause -> A.SpineClause
        permuteNamedDots :: Clause' SpineLHS -> Clause' SpineLHS
    permuteNamedDots (A.Clause SpineLHS
    lhs [ProblemEq]
    strippedPats RHS
    rhs WhereDeclarations
    wh Catchall
    catchall) =
          SpineLHS
    -> [ProblemEq]
    -> RHS
    -> WhereDeclarations
    -> Catchall
    -> Clause' SpineLHS
    forall lhs.
    lhs
    -> [ProblemEq]
    -> RHS
    -> WhereDeclarations
    -> Catchall
    -> Clause' lhs
    A.Clause SpineLHS
    lhs (Substitution' (SubstArg [ProblemEq]) -> [ProblemEq] -> [ProblemEq]
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    applySubst Substitution' Term
    Substitution' (SubstArg [ProblemEq])
    withSub [ProblemEq]
    strippedPats) RHS
    rhs WhereDeclarations
    wh Catchall
    catchall

    -- The arguments of @stripWithClausePatterns@ are documented
    -- at its type signature.
    -- The following is duplicate information, but may help reading the examples below.
    --
    -- [@Δ@]   context bound by lhs of original function.
    -- [@f@]   name of @with@-function.
    -- [@t@]   type of the original function.
    -- [@qs@]  internal patterns for original function.
    -- [@np@]  number of module parameters in @qs@
    -- [@π@]   permutation taking @vars(qs)@ to @support(Δ)@.
    -- [@ps@]  patterns in with clause (eliminating type @t@).
    -- [@ps'@] patterns for with function (presumably of type @Δ@).

    {-| @stripWithClausePatterns cxtNames parent f t Δ qs np π ps = ps'@

    Example:

    @
      record Stream (A : Set) : Set where
        coinductive
        constructor delay
        field       force : A × Stream A

      record SEq (s t : Stream A) : Set where
        coinductive
        field
          ~force : let a , as = force s
                       b , bs = force t
                   in  a ≡ b × SEq as bs

      test : (s : Nat × Stream Nat) (t : Stream Nat) → SEq (delay s) t → SEq t (delay s)
      ~force (test (a     , as) t p) with force t
      ~force (test (suc n , as) t p) | b , bs = ?
    @

    With function:

    @
      f : (t : Stream Nat) (w : Nat × Stream Nat) (a : Nat) (as : Stream Nat)
          (p : SEq (delay (a , as)) t) → (fst w ≡ a) × SEq (snd w) as

      Δ  = t a as p   -- reorder to bring with-relevant (= needed) vars first
      π  = a as t p → Δ
      qs = (a     , as) t p ~force
      ps = (suc n , as) t p ~force
      ps' = (suc n) as t p
    @

    Resulting with-function clause is:

    @
      f t (b , bs) (suc n) as t p
    @

    Note: stripWithClausePatterns factors __@ps@__ through __@qs@__, thus

    @
      ps = qs[ps']
    @

    where @[..]@ is to be understood as substitution.
    The projection patterns have vanished from __@ps'@__ (as they are already in __@qs@__).
    -}

    stripWithClausePatterns
      :: [Name]                   -- ^ __@cxtNames@__ names of the module parameters of the parent function
      -> QName                    -- ^ __@parent@__ name of the parent function.
      -> QName                    -- ^ __@f@__   name of with-function.
      -> Type                     -- ^ __@t@__   top-level type of the original function.
      -> Telescope                -- ^ __@Δ@__   context of patterns of parent function.
      -> [NamedArg DeBruijnPattern] -- ^ __@qs@__  internal patterns for original function.
      -> Nat                      -- ^ __@npars@__ number of module parameters in @qs@.
      -> Permutation              -- ^ __@π@__   permutation taking @vars(qs)@ to @support(Δ)@.
      -> [NamedArg A.Pattern]     -- ^ __@ps@__  patterns in with clause (eliminating type @t@).
      -> TCM ([A.ProblemEq], [NamedArg A.Pattern]) -- ^ __@ps'@__ patterns for with function (presumably of type @Δ@).
    stripWithClausePatterns :: [Name]
    -> QName
    -> QName
    -> Type
    -> Telescope
    -> [NamedArg DeBruijnPattern]
    -> Int
    -> Permutation
    -> [NamedArg Pattern]
    -> TCM ([ProblemEq], [NamedArg Pattern])
    stripWithClausePatterns [Name]
    cxtNames QName
    parent QName
    f Type
    t Telescope
    delta [NamedArg DeBruijnPattern]
    qs Int
    npars Permutation
    perm [NamedArg Pattern]
    ps = do
      -- Andreas, 2014-03-05 expand away pattern synoyms (issue 1074)
      ps <- [NamedArg Pattern] -> TCM [NamedArg Pattern]
    forall a. ExpandPatternSynonyms a => a -> TCM a
    expandPatternSynonyms [NamedArg Pattern]
    ps
      -- Ulf, 2016-11-16 Issue 2303: We need the module parameter
      -- instantiations from qs, so we make sure
      -- that t is the top-level type of the parent function and add patterns for
      -- the module parameters to ps before stripping.
      let paramPat Int
    i DeBruijnPattern
    _ = BindName -> Pattern
    forall e. BindName -> Pattern' e
    A.VarP (BindName -> Pattern) -> BindName -> Pattern
    forall a b. (a -> b) -> a -> b
    $ Name -> BindName
    A.mkBindName (Name -> BindName) -> Name -> BindName
    forall a b. (a -> b) -> a -> b
    $ Name -> [Name] -> Int -> Name
    forall a. a -> [a] -> Int -> a
    indexWithDefault Name
    forall a. HasCallStack => a
    __IMPOSSIBLE__ [Name]
    cxtNames Int
    i
          ps' = (Int -> NamedArg DeBruijnPattern -> NamedArg Pattern)
    -> [Int] -> [NamedArg DeBruijnPattern] -> [NamedArg Pattern]
    forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
    zipWith ((Named NamedName DeBruijnPattern -> Named NamedName Pattern)
    -> NamedArg DeBruijnPattern -> NamedArg Pattern
    forall a b. (a -> b) -> Arg a -> Arg b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap ((Named NamedName DeBruijnPattern -> Named NamedName Pattern)
     -> NamedArg DeBruijnPattern -> NamedArg Pattern)
    -> (Int
        -> Named NamedName DeBruijnPattern -> Named NamedName Pattern)
    -> Int
    -> NamedArg DeBruijnPattern
    -> NamedArg Pattern
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (DeBruijnPattern -> Pattern)
    -> Named NamedName DeBruijnPattern -> Named NamedName Pattern
    forall a b. (a -> b) -> Named NamedName a -> Named NamedName b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap ((DeBruijnPattern -> Pattern)
     -> Named NamedName DeBruijnPattern -> Named NamedName Pattern)
    -> (Int -> DeBruijnPattern -> Pattern)
    -> Int
    -> Named NamedName DeBruijnPattern
    -> Named NamedName Pattern
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Int -> DeBruijnPattern -> Pattern
    paramPat) [Int
    0..] (Int -> [NamedArg DeBruijnPattern] -> [NamedArg DeBruijnPattern]
    forall a. Int -> [a] -> [a]
    take Int
    npars [NamedArg DeBruijnPattern]
    qs) [NamedArg Pattern] -> [NamedArg Pattern] -> [NamedArg Pattern]
    forall a. [a] -> [a] -> [a]
    ++ [NamedArg Pattern]
    ps
      psi <- insertImplicitPatternsT ExpandLast ps' t
      reportSDoc "tc.with.strip" 10 $ vcat
        [ "stripping patterns"
        , nest 2 $ "t   = " <+> prettyTCM t
        , nest 2 $ "ps  = " <+> fsep (punctuate comma $ map prettyA ps)
        , nest 2 $ "ps' = " <+> fsep (punctuate comma $ map prettyA ps')
        , nest 2 $ "psi = " <+> fsep (punctuate comma $ map prettyA psi)
        , nest 2 $ addContext delta $
                   "qs  = " <+> fsep (punctuate comma $ map (prettyTCM . namedArg) qs)
        , nest 2 $ "perm= " <+> text (show perm)
        ]

      -- Andreas, 2015-11-09 Issue 1710: self starts with parent-function, not with-function!
      (ps', strippedPats) <- runWriterT $ strip (Def parent []) t psi qs
      unless (null strippedPats) $ reportSDoc "tc.with.strip" 50 $ nest 2 $
        "strippedPats:" <+> vcat [ prettyA p <+> "=" <+> prettyTCM v <+> ":" <+> prettyTCM a | A.ProblemEq p v a <- strippedPats ]
      let psp = Permutation -> [NamedArg Pattern] -> [NamedArg Pattern]
    forall a. Permutation -> [a] -> [a]
    permute Permutation
    perm [NamedArg Pattern]
    ps'
      reportSDoc "tc.with.strip" 10 $ vcat
        [ nest 2 $ "ps' = " <+> fsep (punctuate comma $ map prettyA ps')
        , nest 2 $ "psp = " <+> fsep (punctuate comma $ map prettyA $ psp)
        ]
      return (strippedPats, psp)
      where

        -- We need to get the correct hiding from the lhs context. The unifier may have moved bindings
        -- sites around so we can't trust the hiding of the parent pattern variables. We should preserve
        -- the origin though.
        varArgInfo :: DBPatVar -> ArgInfo
    varArgInfo = \ DBPatVar
    x -> let n :: Int
    n = DBPatVar -> Int
    dbPatVarIndex DBPatVar
    x in
                            if Int
    n Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    < [ArgInfo] -> Int
    forall a. [a] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length [ArgInfo]
    infos then [ArgInfo]
    infos [ArgInfo] -> Int -> ArgInfo
    forall a. HasCallStack => [a] -> Int -> a
    !! Int
    n else ArgInfo
    forall a. HasCallStack => a
    __IMPOSSIBLE__
          where infos :: [ArgInfo]
    infos = [ArgInfo] -> [ArgInfo]
    forall a. [a] -> [a]
    reverse ([ArgInfo] -> [ArgInfo]) -> [ArgInfo] -> [ArgInfo]
    forall a b. (a -> b) -> a -> b
    $ (Dom ([Char], Type) -> ArgInfo)
    -> [Dom ([Char], Type)] -> [ArgInfo]
    forall a b. (a -> b) -> [a] -> [b]
    map Dom ([Char], Type) -> ArgInfo
    forall a. LensArgInfo a => a -> ArgInfo
    getArgInfo ([Dom ([Char], Type)] -> [ArgInfo])
    -> [Dom ([Char], Type)] -> [ArgInfo]
    forall a b. (a -> b) -> a -> b
    $ Telescope -> [Dom ([Char], Type)]
    forall t. Tele (Dom t) -> [Dom ([Char], t)]
    telToList Telescope
    delta

        setVarArgInfo :: DBPatVar -> NamedArg Pattern -> NamedArg Pattern
    setVarArgInfo DBPatVar
    x NamedArg Pattern
    p = Origin -> NamedArg Pattern -> NamedArg Pattern
    forall a. LensOrigin a => Origin -> a -> a
    setOrigin (NamedArg Pattern -> Origin
    forall a. LensOrigin a => a -> Origin
    getOrigin NamedArg Pattern
    p) (NamedArg Pattern -> NamedArg Pattern)
    -> NamedArg Pattern -> NamedArg Pattern
    forall a b. (a -> b) -> a -> b
    $ ArgInfo -> NamedArg Pattern -> NamedArg Pattern
    forall a. LensArgInfo a => ArgInfo -> a -> a
    setArgInfo (DBPatVar -> ArgInfo
    varArgInfo DBPatVar
    x) NamedArg Pattern
    p

        strip
          :: Term                         -- Self.
          -> Type                         -- The type to be eliminated.
          -> [NamedArg A.Pattern]         -- With-clause patterns.
          -> [NamedArg DeBruijnPattern]   -- Parent-clause patterns with de Bruijn indices relative to Δ.
          -> WriterT [ProblemEq] TCM [NamedArg A.Pattern]
                -- With-clause patterns decomposed by parent-clause patterns.
                -- Also outputs named dot patterns from the parent clause that
                -- we need to add let-bindings for.

        -- Case: out of with-clause patterns.
        strip :: Term
    -> Type
    -> [NamedArg Pattern]
    -> [NamedArg DeBruijnPattern]
    -> WriterT [ProblemEq] (TCMT IO) [NamedArg Pattern]
    strip Term
    self Type
    t [] qs :: [NamedArg DeBruijnPattern]
    qs@(NamedArg DeBruijnPattern
    _ : [NamedArg DeBruijnPattern]
    _) = do
          [Char] -> Int -> TCMT IO Doc -> WriterT [ProblemEq] (TCMT IO) ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "tc.with.strip" Int
    15 (TCMT IO Doc -> WriterT [ProblemEq] (TCMT IO) ())
    -> TCMT IO Doc -> WriterT [ProblemEq] (TCMT IO) ()
    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
    "strip (out of A.Patterns)"
            , 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
    "qs  =" 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 (TCMT IO Doc -> [TCMT IO Doc] -> [TCMT IO Doc]
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Semigroup (m Doc), Foldable t) =>
    m Doc -> t (m Doc) -> [m Doc]
    punctuate TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc
    comma ([TCMT IO Doc] -> [TCMT IO Doc]) -> [TCMT IO Doc] -> [TCMT IO Doc]
    forall a b. (a -> b) -> a -> b
    $ (NamedArg DeBruijnPattern -> TCMT IO Doc)
    -> [NamedArg 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
    forall (m :: * -> *). MonadPretty m => DeBruijnPattern -> m Doc
    prettyTCM (DeBruijnPattern -> TCMT IO Doc)
    -> (NamedArg DeBruijnPattern -> DeBruijnPattern)
    -> NamedArg DeBruijnPattern
    -> TCMT IO Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . NamedArg DeBruijnPattern -> DeBruijnPattern
    forall a. NamedArg a -> a
    namedArg) [NamedArg DeBruijnPattern]
    qs)
            , 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
    "self=" 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
    forall (m :: * -> *). MonadPretty m => Term -> m Doc
    prettyTCM Term
    self
            , 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
    "t   =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Type -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => Type -> m Doc
    prettyTCM Type
    t
            ]
          -- Andreas, 2015-06-11, issue 1551:
          -- As the type t develops, we need to insert more implicit patterns,
          -- due to copatterns / flexible arity.
          ps <- TCM [NamedArg Pattern]
    -> WriterT [ProblemEq] (TCMT IO) [NamedArg Pattern]
    forall a. TCM a -> WriterT [ProblemEq] (TCMT IO) a
    forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
    liftTCM (TCM [NamedArg Pattern]
     -> WriterT [ProblemEq] (TCMT IO) [NamedArg Pattern])
    -> TCM [NamedArg Pattern]
    -> WriterT [ProblemEq] (TCMT IO) [NamedArg Pattern]
    forall a b. (a -> b) -> a -> b
    $ ExpandHidden
    -> [NamedArg Pattern] -> Type -> TCM [NamedArg Pattern]
    forall (m :: * -> *).
    (PureTCM m, MonadError TCErr m, MonadFresh NameId m,
     MonadTrace m) =>
    ExpandHidden -> [NamedArg Pattern] -> Type -> m [NamedArg Pattern]
    insertImplicitPatternsT ExpandHidden
    ExpandLast [] Type
    t
          if null ps then typeError TooFewPatternsInWithClause
           else strip self t ps qs

        -- Case: out of parent-clause patterns.
        -- This is only ok if all remaining with-clause patterns
        -- are implicit patterns (we inserted too many).
        strip Term
    _ Type
    _ [NamedArg Pattern]
    ps      []      = do
          let implicit :: Pattern' e -> Bool
    implicit (A.WildP{})     = Bool
    True
              implicit (A.ConP ConPatInfo
    ci AmbiguousQName
    _ NAPs e
    _) = ConPatInfo -> ConOrigin
    conPatOrigin ConPatInfo
    ci ConOrigin -> ConOrigin -> Bool
    forall a. Eq a => a -> a -> Bool
    == ConOrigin
    ConOSystem
              implicit Pattern' e
    _               = Bool
    False
          Bool
    -> WriterT [ProblemEq] (TCMT IO) ()
    -> WriterT [ProblemEq] (TCMT IO) ()
    forall b (m :: * -> *). (IsBool b, Monad m) => b -> m () -> m ()
    unless ((NamedArg Pattern -> Bool) -> [NamedArg Pattern] -> Bool
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
    all (Pattern -> Bool
    forall {e}. Pattern' e -> Bool
    implicit (Pattern -> Bool)
    -> (NamedArg Pattern -> Pattern) -> NamedArg Pattern -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . NamedArg Pattern -> Pattern
    forall a. NamedArg a -> a
    namedArg) [NamedArg Pattern]
    ps) (WriterT [ProblemEq] (TCMT IO) ()
     -> WriterT [ProblemEq] (TCMT IO) ())
    -> WriterT [ProblemEq] (TCMT IO) ()
    -> WriterT [ProblemEq] (TCMT IO) ()
    forall a b. (a -> b) -> a -> b
    $ TypeError -> WriterT [ProblemEq] (TCMT IO) ()
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    TypeError -> m a
    typeError TypeError
    TooManyPatternsInWithClause
          [NamedArg Pattern]
    -> WriterT [ProblemEq] (TCMT IO) [NamedArg Pattern]
    forall a. a -> WriterT [ProblemEq] (TCMT IO) a
    forall (m :: * -> *) a. Monad m => a -> m a
    return []

        -- Case: both parent-clause pattern and with-clause pattern present.
        -- Make sure they match, and decompose into subpatterns.
        strip Term
    self Type
    t (NamedArg Pattern
    p0 : [NamedArg Pattern]
    ps) qs :: [NamedArg DeBruijnPattern]
    qs@(NamedArg DeBruijnPattern
    q : [NamedArg DeBruijnPattern]
    _)
          | A.AsP PatInfo
    _ BindName
    x Pattern
    p <- NamedArg Pattern -> Pattern
    forall a. NamedArg a -> a
    namedArg NamedArg Pattern
    p0 = do
            (a, _) <- Type -> WriterT [ProblemEq] (TCMT IO) (Dom Type, Abs Type)
    forall (m :: * -> *).
    MonadReduce m =>
    Type -> m (Dom Type, Abs Type)
    mustBePi Type
    t
            let v = DeBruijnPattern -> Term
    patternToTerm (NamedArg DeBruijnPattern -> DeBruijnPattern
    forall a. NamedArg a -> a
    namedArg NamedArg DeBruijnPattern
    q)
            tell [ProblemEq (A.VarP x) v a]
            strip self t (fmap (p <$) p0 : ps) qs
        strip Term
    self Type
    t ps0 :: [NamedArg Pattern]
    ps0@(NamedArg Pattern
    p0 : [NamedArg Pattern]
    ps) qs0 :: [NamedArg DeBruijnPattern]
    qs0@(NamedArg DeBruijnPattern
    q : [NamedArg DeBruijnPattern]
    qs) = do
          p <- ((Named NamedName Pattern
     -> WriterT [ProblemEq] (TCMT IO) (Named NamedName Pattern))
    -> NamedArg Pattern
    -> WriterT [ProblemEq] (TCMT IO) (NamedArg Pattern)
    forall (t :: * -> *) (f :: * -> *) a b.
    (Traversable t, Applicative f) =>
    (a -> f b) -> t a -> f (t b)
    forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> Arg a -> f (Arg b)
    traverse ((Named NamedName Pattern
      -> WriterT [ProblemEq] (TCMT IO) (Named NamedName Pattern))
     -> NamedArg Pattern
     -> WriterT [ProblemEq] (TCMT IO) (NamedArg Pattern))
    -> ((Pattern -> WriterT [ProblemEq] (TCMT IO) Pattern)
        -> Named NamedName Pattern
        -> WriterT [ProblemEq] (TCMT IO) (Named NamedName Pattern))
    -> (Pattern -> WriterT [ProblemEq] (TCMT IO) Pattern)
    -> NamedArg Pattern
    -> WriterT [ProblemEq] (TCMT IO) (NamedArg Pattern)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Pattern -> WriterT [ProblemEq] (TCMT IO) Pattern)
    -> Named NamedName Pattern
    -> WriterT [ProblemEq] (TCMT IO) (Named NamedName Pattern)
    forall (t :: * -> *) (f :: * -> *) a b.
    (Traversable t, Applicative f) =>
    (a -> f b) -> t a -> f (t b)
    forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> Named NamedName a -> f (Named NamedName b)
    traverse) Pattern -> WriterT [ProblemEq] (TCMT IO) Pattern
    forall (m :: * -> *).
    (MonadError TCErr m, MonadTCEnv m, ReadTCState m, HasBuiltins m) =>
    Pattern -> m Pattern
    expandLitPattern NamedArg Pattern
    p0
          reportSDoc "tc.with.strip" 15 $ vcat
            [ "strip"
            , nest 2 $ "ps0 =" <+> fsep (punctuate comma $ map prettyA ps0)
            , nest 2 $ "exp =" <+> prettyA p
            , nest 2 $ "qs0 =" <+> fsep (punctuate comma $ map (prettyTCM . namedArg) qs0)
            , nest 2 $ "self=" <+> prettyTCM self
            , nest 2 $ "t   =" <+> prettyTCM t
            ]
          case namedArg q of
            ProjP ProjOrigin
    o QName
    d -> case NamedArg Pattern -> Maybe (ProjOrigin, AmbiguousQName)
    forall a. IsProjP a => a -> Maybe (ProjOrigin, AmbiguousQName)
    A.isProjP NamedArg Pattern
    p of
              Just (ProjOrigin
    o', AmbQ List1 QName
    ds) -> do
                -- We assume here that neither @o@ nor @o'@ can be @ProjSystem@.
                Bool
    -> WriterT [ProblemEq] (TCMT IO) ()
    -> WriterT [ProblemEq] (TCMT IO) ()
    forall b (m :: * -> *). (IsBool b, Monad m) => b -> m () -> m ()
    when (ProjOrigin
    o ProjOrigin -> ProjOrigin -> Bool
    forall a. Eq a => a -> a -> Bool
    /= ProjOrigin
    o') (WriterT [ProblemEq] (TCMT IO) ()
     -> WriterT [ProblemEq] (TCMT IO) ())
    -> WriterT [ProblemEq] (TCMT IO) ()
    -> WriterT [ProblemEq] (TCMT IO) ()
    forall a b. (a -> b) -> a -> b
    $ NamedArg Pattern
    -> WriterT [ProblemEq] (TCMT IO) ()
    -> WriterT [ProblemEq] (TCMT IO) ()
    forall (m :: * -> *) x a.
    (MonadTrace m, HasRange x) =>
    x -> m a -> m a
    setCurrentRange NamedArg Pattern
    p0 (WriterT [ProblemEq] (TCMT IO) ()
     -> WriterT [ProblemEq] (TCMT IO) ())
    -> WriterT [ProblemEq] (TCMT IO) ()
    -> WriterT [ProblemEq] (TCMT IO) ()
    forall a b. (a -> b) -> a -> b
    $ Telescope
    -> WriterT [ProblemEq] (TCMT IO) ()
    -> WriterT [ProblemEq] (TCMT IO) ()
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    forall (m :: * -> *) a.
    MonadAddContext m =>
    Telescope -> m a -> m a
    addContext Telescope
    delta do
                  [Char] -> Int -> [Char] -> WriterT [ProblemEq] (TCMT IO) ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> [Char] -> m ()
    reportSLn [Char]
    "tc.with.strip" Int
    90 ([Char] -> WriterT [ProblemEq] (TCMT IO) ())
    -> [Char] -> WriterT [ProblemEq] (TCMT IO) ()
    forall a b. (a -> b) -> a -> b
    $ [Char]
    "p0 = " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ NamedArg Pattern -> [Char]
    forall a. Show a => a -> [Char]
    show NamedArg Pattern
    p0
                  [Char] -> Int -> [Char] -> WriterT [ProblemEq] (TCMT IO) ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> [Char] -> m ()
    reportSLn [Char]
    "tc.with.strip" Int
    80 ([Char] -> WriterT [ProblemEq] (TCMT IO) ())
    -> [Char] -> WriterT [ProblemEq] (TCMT IO) ()
    forall a b. (a -> b) -> a -> b
    $ [Char]
    "getRange p0 = " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ Range -> [Char]
    forall a. Pretty a => a -> [Char]
    prettyShow (NamedArg Pattern -> Range
    forall a. HasRange a => a -> Range
    getRange NamedArg Pattern
    p0)
                  Warning -> WriterT [ProblemEq] (TCMT IO) ()
    forall (m :: * -> *).
    (HasCallStack, MonadWarning m) =>
    Warning -> m ()
    warning (Warning -> WriterT [ProblemEq] (TCMT IO) ())
    -> Warning -> WriterT [ProblemEq] (TCMT IO) ()
    forall a b. (a -> b) -> a -> b
    $ NamedArg Pattern
    -> ProjOrigin -> NamedArg DeBruijnPattern -> ProjOrigin -> Warning
    WithClauseProjectionFixityMismatch NamedArg Pattern
    p0 ProjOrigin
    o' NamedArg DeBruijnPattern
    q ProjOrigin
    o
                -- Andreas, 2016-12-28, issue #2360:
                -- We disambiguate the projection in the with clause
                -- to the projection in the parent clause.
                d  <- TCM QName -> WriterT [ProblemEq] (TCMT IO) QName
    forall a. TCM a -> WriterT [ProblemEq] (TCMT IO) a
    forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
    liftTCM (TCM QName -> WriterT [ProblemEq] (TCMT IO) QName)
    -> TCM QName -> WriterT [ProblemEq] (TCMT IO) QName
    forall a b. (a -> b) -> a -> b
    $ QName -> TCM QName
    forall (m :: * -> *). HasConstInfo m => QName -> m QName
    getOriginalProjection QName
    d
                found <- existsM ds $ \ QName
    d' -> TCM Bool -> WriterT [ProblemEq] (TCMT IO) Bool
    forall a. TCM a -> WriterT [ProblemEq] (TCMT IO) a
    forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
    liftTCM (TCM Bool -> WriterT [ProblemEq] (TCMT IO) Bool)
    -> TCM Bool -> WriterT [ProblemEq] (TCMT IO) Bool
    forall a b. (a -> b) -> a -> b
    $ (QName -> Maybe QName
    forall a. a -> Maybe a
    Just QName
    d Maybe QName -> Maybe QName -> Bool
    forall a. Eq a => a -> a -> Bool
    ==) (Maybe QName -> Bool)
    -> (Maybe Projection -> Maybe QName) -> Maybe Projection -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Projection -> QName) -> Maybe Projection -> Maybe QName
    forall a b. (a -> b) -> Maybe a -> Maybe b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap Projection -> QName
    projOrig (Maybe Projection -> Bool)
    -> TCMT IO (Maybe Projection) -> TCM Bool
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> QName -> TCMT IO (Maybe Projection)
    forall (m :: * -> *).
    HasConstInfo m =>
    QName -> m (Maybe Projection)
    isProjection QName
    d'
                if not found then mismatch else do
                  (self1, t1, ps) <- liftTCM $ do
                    t <- reduce t
                    (_, self1, t1) <- fromMaybe __IMPOSSIBLE__ <$> projectTyped self t o d
                    -- Andreas, 2016-01-21, issue #1791
                    -- The type of a field might start with hidden quantifiers.
                    -- So we may have to insert more implicit patterns here.
                    ps <- insertImplicitPatternsT ExpandLast ps t1
                    return (self1, t1, ps)
                  strip self1 t1 ps qs
              Maybe (ProjOrigin, AmbiguousQName)
    Nothing -> WriterT [ProblemEq] (TCMT IO) [NamedArg Pattern]
    forall (m :: * -> *) a. (MonadAddContext m, MonadTCError m) => m a
    mismatch

            -- We can safely strip dots from variables. The unifier will put them back when required.
            VarP PatternInfo
    _ DBPatVar
    x | A.DotP PatInfo
    _ Expr
    u <- NamedArg Pattern -> Pattern
    forall a. NamedArg a -> a
    namedArg NamedArg Pattern
    p
                     , A.Var Name
    y <- Expr -> Expr
    unScope Expr
    u -> do
              (DBPatVar -> NamedArg Pattern -> NamedArg Pattern
    setVarArgInfo DBPatVar
    x (NamedArg Pattern -> Pattern -> NamedArg Pattern
    forall a b. NamedArg a -> b -> NamedArg b
    setNamedArg NamedArg Pattern
    p (Pattern -> NamedArg Pattern) -> Pattern -> NamedArg Pattern
    forall a b. (a -> b) -> a -> b
    $ BindName -> Pattern
    forall e. BindName -> Pattern' e
    A.VarP (BindName -> Pattern) -> BindName -> Pattern
    forall a b. (a -> b) -> a -> b
    $ Name -> BindName
    A.mkBindName Name
    y) NamedArg Pattern -> [NamedArg Pattern] -> [NamedArg Pattern]
    forall a. a -> [a] -> [a]
    :) ([NamedArg Pattern] -> [NamedArg Pattern])
    -> WriterT [ProblemEq] (TCMT IO) [NamedArg Pattern]
    -> WriterT [ProblemEq] (TCMT IO) [NamedArg Pattern]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$>
                Term -> WriterT [ProblemEq] (TCMT IO) [NamedArg Pattern]
    recurse (Int -> Term
    var (DBPatVar -> Int
    dbPatVarIndex DBPatVar
    x))

            VarP PatternInfo
    _ DBPatVar
    x  ->
              (DBPatVar -> NamedArg Pattern -> NamedArg Pattern
    setVarArgInfo DBPatVar
    x NamedArg Pattern
    p NamedArg Pattern -> [NamedArg Pattern] -> [NamedArg Pattern]
    forall a. a -> [a] -> [a]
    :) ([NamedArg Pattern] -> [NamedArg Pattern])
    -> WriterT [ProblemEq] (TCMT IO) [NamedArg Pattern]
    -> WriterT [ProblemEq] (TCMT IO) [NamedArg Pattern]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Term -> WriterT [ProblemEq] (TCMT IO) [NamedArg Pattern]
    recurse (Int -> Term
    var (DBPatVar -> Int
    dbPatVarIndex DBPatVar
    x))

            IApplyP PatternInfo
    _ Term
    _ Term
    _ DBPatVar
    x  ->
              (DBPatVar -> NamedArg Pattern -> NamedArg Pattern
    setVarArgInfo DBPatVar
    x NamedArg Pattern
    p NamedArg Pattern -> [NamedArg Pattern] -> [NamedArg Pattern]
    forall a. a -> [a] -> [a]
    :) ([NamedArg Pattern] -> [NamedArg Pattern])
    -> WriterT [ProblemEq] (TCMT IO) [NamedArg Pattern]
    -> WriterT [ProblemEq] (TCMT IO) [NamedArg Pattern]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Term -> WriterT [ProblemEq] (TCMT IO) [NamedArg Pattern]
    recurse (Int -> Term
    var (DBPatVar -> Int
    dbPatVarIndex DBPatVar
    x))

            DefP{}  -> WriterT [ProblemEq] (TCMT IO) [NamedArg Pattern]
    forall a. HasCallStack => a
    __IMPOSSIBLE__

            DotP PatternInfo
    i Term
    v  -> do
              (a, _) <- Type -> WriterT [ProblemEq] (TCMT IO) (Dom Type, Abs Type)
    forall (m :: * -> *).
    MonadReduce m =>
    Type -> m (Dom Type, Abs Type)
    mustBePi Type
    t
              tell [ProblemEq (namedArg p) v a]
              case v of
                Var Int
    x [] | PatOVar{} <- PatternInfo -> PatOrigin
    patOrigin PatternInfo
    i
                   -> (NamedArg Pattern
    p NamedArg Pattern -> [NamedArg Pattern] -> [NamedArg Pattern]
    forall a. a -> [a] -> [a]
    :) ([NamedArg Pattern] -> [NamedArg Pattern])
    -> WriterT [ProblemEq] (TCMT IO) [NamedArg Pattern]
    -> WriterT [ProblemEq] (TCMT IO) [NamedArg Pattern]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Term -> WriterT [ProblemEq] (TCMT IO) [NamedArg Pattern]
    recurse (Int -> Term
    var Int
    x)
                Term
    _  -> (NamedArg Pattern -> NamedArg Pattern
    makeWildP NamedArg Pattern
    p NamedArg Pattern -> [NamedArg Pattern] -> [NamedArg Pattern]
    forall a. a -> [a] -> [a]
    :) ([NamedArg Pattern] -> [NamedArg Pattern])
    -> WriterT [ProblemEq] (TCMT IO) [NamedArg Pattern]
    -> WriterT [ProblemEq] (TCMT IO) [NamedArg Pattern]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Term -> WriterT [ProblemEq] (TCMT IO) [NamedArg Pattern]
    recurse Term
    v

            q' :: DeBruijnPattern
    q'@(ConP ConHead
    c ConPatternInfo
    ci [NamedArg DeBruijnPattern]
    qs') -> do
             [Char] -> Int -> TCMT IO Doc -> WriterT [ProblemEq] (TCMT IO) ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "tc.with.strip" Int
    60 (TCMT IO Doc -> WriterT [ProblemEq] (TCMT IO) ())
    -> TCMT IO Doc -> WriterT [ProblemEq] (TCMT IO) ()
    forall a b. (a -> b) -> a -> b
    $
               TCMT IO Doc
    "parent pattern is constructor " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> ConHead -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => ConHead -> m Doc
    prettyTCM ConHead
    c
             (a, b) <- Type -> WriterT [ProblemEq] (TCMT IO) (Dom Type, Abs Type)
    forall (m :: * -> *).
    MonadReduce m =>
    Type -> m (Dom Type, Abs Type)
    mustBePi Type
    t
             -- The type of the current pattern is a datatype.
             Def d es <- liftTCM $ reduce (unEl $ unDom a)
             let us = Args -> Maybe Args -> Args
    forall a. a -> Maybe a -> a
    fromMaybe Args
    forall a. HasCallStack => a
    __IMPOSSIBLE__ (Maybe Args -> Args) -> Maybe Args -> Args
    forall a b. (a -> b) -> a -> b
    $ Elims -> Maybe Args
    forall a. [Elim' a] -> Maybe [Arg a]
    allApplyElims Elims
    es
             -- Get the original constructor and field names.
             c <- either __IMPOSSIBLE__ (`withRangeOf` c) <$> do liftTCM $ getConForm $ conName c

             case namedArg p of

              -- Andreas, 2015-07-07 Issue 1606.
              -- Agda sometimes changes a record of dot patterns into a dot pattern,
              -- so the user should be allowed to do likewise.
              -- Jesper, 2017-11-16. This is now also allowed for data constructors.
              A.DotP PatInfo
    r Expr
    e -> do
                [ProblemEq] -> WriterT [ProblemEq] (TCMT IO) ()
    forall w (m :: * -> *). MonadWriter w m => w -> m ()
    tell [Pattern -> Term -> Dom Type -> ProblemEq
    ProblemEq (PatInfo -> Expr -> Pattern
    forall e. PatInfo -> e -> Pattern' e
    A.DotP PatInfo
    r Expr
    e) (DeBruijnPattern -> Term
    patternToTerm DeBruijnPattern
    q') Dom Type
    a]
                ps' <-
                  case Expr -> AppView
    appView Expr
    e of
                    -- If dot-pattern is an application of the constructor, try to preserve the
                    -- arguments.
                    Application (A.Con (A.AmbQ List1 QName
    cs')) [NamedArg Expr]
    es -> do
                      cs' <- TCM [ConHead] -> WriterT [ProblemEq] (TCMT IO) [ConHead]
    forall a. TCM a -> WriterT [ProblemEq] (TCMT IO) a
    forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
    liftTCM (TCM [ConHead] -> WriterT [ProblemEq] (TCMT IO) [ConHead])
    -> TCM [ConHead] -> WriterT [ProblemEq] (TCMT IO) [ConHead]
    forall a b. (a -> b) -> a -> b
    $ List1 (Either SigError ConHead) -> [ConHead]
    forall a b. List1 (Either a b) -> [b]
    List1.rights (List1 (Either SigError ConHead) -> [ConHead])
    -> TCMT IO (List1 (Either SigError ConHead)) -> TCM [ConHead]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (QName -> TCM (Either SigError ConHead))
    -> List1 QName -> TCMT IO (List1 (Either SigError ConHead))
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> NonEmpty a -> m (NonEmpty b)
    mapM QName -> TCM (Either SigError ConHead)
    getConForm List1 QName
    cs'
                      unless (c `elem` cs') mismatch
                      return $ (map . fmap . fmap) (A.DotP r) es
                    AppView
    _  -> [NamedArg Pattern]
    -> WriterT [ProblemEq] (TCMT IO) [NamedArg Pattern]
    forall a. a -> WriterT [ProblemEq] (TCMT IO) a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([NamedArg Pattern]
     -> WriterT [ProblemEq] (TCMT IO) [NamedArg Pattern])
    -> [NamedArg Pattern]
    -> WriterT [ProblemEq] (TCMT IO) [NamedArg Pattern]
    forall a b. (a -> b) -> a -> b
    $ (NamedArg DeBruijnPattern -> NamedArg Pattern)
    -> [NamedArg DeBruijnPattern] -> [NamedArg Pattern]
    forall a b. (a -> b) -> [a] -> [b]
    map (Pattern -> Named NamedName Pattern
    forall a name. a -> Named name a
    unnamed (PatInfo -> Pattern
    forall e. PatInfo -> Pattern' e
    A.WildP PatInfo
    forall a. Null a => a
    empty) Named NamedName Pattern
    -> NamedArg DeBruijnPattern -> NamedArg Pattern
    forall a b. a -> Arg b -> Arg a
    forall (f :: * -> *) a b. Functor f => a -> f b -> f a
    <$) [NamedArg DeBruijnPattern]
    qs'
                stripConP d us b c ConOCon qs' ps'

              -- Andreas, 2016-12-29, issue #2363.
              -- Allow _ to stand for the corresponding parent pattern.
              A.WildP{} -> do
                -- Andreas, 2017-10-13, issue #2803:
                -- Delete the name, since it can confuse insertImplicitPattern.
                let ps' :: [NamedArg Pattern]
    ps' = (NamedArg DeBruijnPattern -> NamedArg Pattern)
    -> [NamedArg DeBruijnPattern] -> [NamedArg Pattern]
    forall a b. (a -> b) -> [a] -> [b]
    map (Pattern -> Named NamedName Pattern
    forall a name. a -> Named name a
    unnamed (PatInfo -> Pattern
    forall e. PatInfo -> Pattern' e
    A.WildP PatInfo
    forall a. Null a => a
    empty) Named NamedName Pattern
    -> NamedArg DeBruijnPattern -> NamedArg Pattern
    forall a b. a -> Arg b -> Arg a
    forall (f :: * -> *) a b. Functor f => a -> f b -> f a
    <$) [NamedArg DeBruijnPattern]
    qs'
                QName
    -> Args
    -> Abs Type
    -> ConHead
    -> ConOrigin
    -> [NamedArg DeBruijnPattern]
    -> [NamedArg Pattern]
    -> WriterT [ProblemEq] (TCMT IO) [NamedArg Pattern]
    stripConP QName
    d Args
    us Abs Type
    b ConHead
    c ConOrigin
    ConOCon [NamedArg DeBruijnPattern]
    qs' [NamedArg Pattern]
    ps'

              -- Jesper, 2018-05-13, issue #2998.
              -- We also allow turning a constructor pattern into a variable.
              -- In general this is not type-safe since the types of some variables
              -- in the constructor pattern may have changed, so we have to
              -- re-check these solutions when checking the with clause (see LHS.hs)
              A.VarP BindName
    x -> do
                [ProblemEq] -> WriterT [ProblemEq] (TCMT IO) ()
    forall w (m :: * -> *). MonadWriter w m => w -> m ()
    tell [Pattern -> Term -> Dom Type -> ProblemEq
    ProblemEq (BindName -> Pattern
    forall e. BindName -> Pattern' e
    A.VarP BindName
    x) (DeBruijnPattern -> Term
    patternToTerm DeBruijnPattern
    q') Dom Type
    a]
                let ps' :: [NamedArg Pattern]
    ps' = (NamedArg DeBruijnPattern -> NamedArg Pattern)
    -> [NamedArg DeBruijnPattern] -> [NamedArg Pattern]
    forall a b. (a -> b) -> [a] -> [b]
    map (Pattern -> Named NamedName Pattern
    forall a name. a -> Named name a
    unnamed (PatInfo -> Pattern
    forall e. PatInfo -> Pattern' e
    A.WildP PatInfo
    forall a. Null a => a
    empty) Named NamedName Pattern
    -> NamedArg DeBruijnPattern -> NamedArg Pattern
    forall a b. a -> Arg b -> Arg a
    forall (f :: * -> *) a b. Functor f => a -> f b -> f a
    <$) [NamedArg DeBruijnPattern]
    qs'
                QName
    -> Args
    -> Abs Type
    -> ConHead
    -> ConOrigin
    -> [NamedArg DeBruijnPattern]
    -> [NamedArg Pattern]
    -> WriterT [ProblemEq] (TCMT IO) [NamedArg Pattern]
    stripConP QName
    d Args
    us Abs Type
    b ConHead
    c ConOrigin
    ConOCon [NamedArg DeBruijnPattern]
    qs' [NamedArg Pattern]
    ps'

              A.ConP ConPatInfo
    _ (A.AmbQ List1 QName
    cs') [NamedArg Pattern]
    ps' -> do
                -- Check whether the with-clause constructor can be (possibly trivially)
                -- disambiguated to be equal to the parent-clause constructor.
                -- Andreas, 2017-08-13, herein, ignore abstract constructors.
                cs' <- TCM [ConHead] -> WriterT [ProblemEq] (TCMT IO) [ConHead]
    forall a. TCM a -> WriterT [ProblemEq] (TCMT IO) a
    forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
    liftTCM (TCM [ConHead] -> WriterT [ProblemEq] (TCMT IO) [ConHead])
    -> TCM [ConHead] -> WriterT [ProblemEq] (TCMT IO) [ConHead]
    forall a b. (a -> b) -> a -> b
    $ List1 (Either SigError ConHead) -> [ConHead]
    forall a b. List1 (Either a b) -> [b]
    List1.rights (List1 (Either SigError ConHead) -> [ConHead])
    -> TCMT IO (List1 (Either SigError ConHead)) -> TCM [ConHead]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (QName -> TCM (Either SigError ConHead))
    -> List1 QName -> TCMT IO (List1 (Either SigError ConHead))
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> NonEmpty a -> m (NonEmpty b)
    mapM QName -> TCM (Either SigError ConHead)
    getConForm List1 QName
    cs'
                unless (c `elem` cs') mismatch
                -- Strip the subpatterns ps' and then continue.
                stripConP d us b c ConOCon qs' ps'

              A.RecP KwRange
    _ ConPatInfo
    _ [FieldAssignment' Pattern]
    fs -> WriterT [ProblemEq] (TCMT IO) (Maybe RecordData)
    -> WriterT [ProblemEq] (TCMT IO) [NamedArg Pattern]
    -> (RecordData -> WriterT [ProblemEq] (TCMT IO) [NamedArg Pattern])
    -> WriterT [ProblemEq] (TCMT IO) [NamedArg Pattern]
    forall (m :: * -> *) a b.
    Monad m =>
    m (Maybe a) -> m b -> (a -> m b) -> m b
    caseMaybeM (TCM (Maybe RecordData)
    -> WriterT [ProblemEq] (TCMT IO) (Maybe RecordData)
    forall a. TCM a -> WriterT [ProblemEq] (TCMT IO) a
    forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
    liftTCM (TCM (Maybe RecordData)
     -> WriterT [ProblemEq] (TCMT IO) (Maybe RecordData))
    -> TCM (Maybe RecordData)
    -> WriterT [ProblemEq] (TCMT IO) (Maybe RecordData)
    forall a b. (a -> b) -> a -> b
    $ QName -> TCM (Maybe RecordData)
    forall (m :: * -> *).
    HasConstInfo m =>
    QName -> m (Maybe RecordData)
    isRecord QName
    d) WriterT [ProblemEq] (TCMT IO) [NamedArg Pattern]
    forall (m :: * -> *) a. (MonadAddContext m, MonadTCError m) => m a
    mismatch ((RecordData -> WriterT [ProblemEq] (TCMT IO) [NamedArg Pattern])
     -> WriterT [ProblemEq] (TCMT IO) [NamedArg Pattern])
    -> (RecordData -> WriterT [ProblemEq] (TCMT IO) [NamedArg Pattern])
    -> WriterT [ProblemEq] (TCMT IO) [NamedArg Pattern]
    forall a b. (a -> b) -> a -> b
    $ \ RecordData
    def -> do
                ps' <- TCM [NamedArg Pattern]
    -> WriterT [ProblemEq] (TCMT IO) [NamedArg Pattern]
    forall a. TCM a -> WriterT [ProblemEq] (TCMT IO) a
    forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
    liftTCM (TCM [NamedArg Pattern]
     -> WriterT [ProblemEq] (TCMT IO) [NamedArg Pattern])
    -> TCM [NamedArg Pattern]
    -> WriterT [ProblemEq] (TCMT IO) [NamedArg Pattern]
    forall a b. (a -> b) -> a -> b
    $ QName
    -> (Name -> Pattern)
    -> [FieldAssignment' Pattern]
    -> [Arg Name]
    -> TCM [NamedArg Pattern]
    forall a.
    HasRange a =>
    QName
    -> (Name -> a)
    -> [FieldAssignment' a]
    -> [Arg Name]
    -> TCM [NamedArg a]
    insertMissingFieldsFail QName
    d (Pattern -> Name -> Pattern
    forall a b. a -> b -> a
    const (Pattern -> Name -> Pattern) -> Pattern -> Name -> Pattern
    forall a b. (a -> b) -> a -> b
    $ PatInfo -> Pattern
    forall e. PatInfo -> Pattern' e
    A.WildP PatInfo
    forall a. Null a => a
    empty) [FieldAssignment' Pattern]
    fs
                                                     ((Dom Name -> Arg Name) -> [Dom Name] -> [Arg Name]
    forall a b. (a -> b) -> [a] -> [b]
    map Dom Name -> Arg Name
    forall t a. Dom' t a -> Arg a
    argFromDom ([Dom Name] -> [Arg Name]) -> [Dom Name] -> [Arg Name]
    forall a b. (a -> b) -> a -> b
    $ RecordData -> [Dom Name]
    recordFieldNames RecordData
    def)
                stripConP d us b c ConORec qs' ps'

              p :: Pattern
    p@(A.PatternSynP PatInfo
    pi' AmbiguousQName
    c' [NamedArg Pattern]
    ps') -> do
                 [Char] -> Int -> TCMT IO Doc -> WriterT [ProblemEq] (TCMT IO) ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "impossible" Int
    10 (TCMT IO Doc -> WriterT [ProblemEq] (TCMT IO) ())
    -> TCMT IO Doc -> WriterT [ProblemEq] (TCMT IO) ()
    forall a b. (a -> b) -> a -> b
    $
                   TCMT IO Doc
    "stripWithClausePatterns: encountered pattern synonym " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Pattern -> TCMT IO Doc
    forall a (m :: * -> *).
    (ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
    a -> m Doc
    prettyA Pattern
    p
                 WriterT [ProblemEq] (TCMT IO) [NamedArg Pattern]
    forall a. HasCallStack => a
    __IMPOSSIBLE__

              Pattern
    p -> do
               [Char] -> Int -> TCMT IO Doc -> WriterT [ProblemEq] (TCMT IO) ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "tc.with.strip" Int
    60 (TCMT IO Doc -> WriterT [ProblemEq] (TCMT IO) ())
    -> TCMT IO Doc -> WriterT [ProblemEq] (TCMT IO) ()
    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]
    "with clause pattern is  " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ Pattern -> [Char]
    forall a. Show a => a -> [Char]
    show Pattern
    p
               WriterT [ProblemEq] (TCMT IO) [NamedArg Pattern]
    forall (m :: * -> *) a. (MonadAddContext m, MonadTCError m) => m a
    mismatch

            LitP PatternInfo
    _ Literal
    lit -> case NamedArg Pattern -> Pattern
    forall a. NamedArg a -> a
    namedArg NamedArg Pattern
    p of
              A.LitP PatInfo
    _ Literal
    lit' | Literal
    lit Literal -> Literal -> Bool
    forall a. Eq a => a -> a -> Bool
    == Literal
    lit' -> Term -> WriterT [ProblemEq] (TCMT IO) [NamedArg Pattern]
    recurse (Term -> WriterT [ProblemEq] (TCMT IO) [NamedArg Pattern])
    -> Term -> WriterT [ProblemEq] (TCMT IO) [NamedArg Pattern]
    forall a b. (a -> b) -> a -> b
    $ Literal -> Term
    Lit Literal
    lit
              A.WildP{}                   -> Term -> WriterT [ProblemEq] (TCMT IO) [NamedArg Pattern]
    recurse (Term -> WriterT [ProblemEq] (TCMT IO) [NamedArg Pattern])
    -> Term -> WriterT [ProblemEq] (TCMT IO) [NamedArg Pattern]
    forall a b. (a -> b) -> a -> b
    $ Literal -> Term
    Lit Literal
    lit

              p :: Pattern
    p@(A.PatternSynP PatInfo
    pi' AmbiguousQName
    c' [NamedArg Pattern
    ps']) -> do
                 [Char] -> Int -> TCMT IO Doc -> WriterT [ProblemEq] (TCMT IO) ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "impossible" Int
    10 (TCMT IO Doc -> WriterT [ProblemEq] (TCMT IO) ())
    -> TCMT IO Doc -> WriterT [ProblemEq] (TCMT IO) ()
    forall a b. (a -> b) -> a -> b
    $
                   TCMT IO Doc
    "stripWithClausePatterns: encountered pattern synonym " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Pattern -> TCMT IO Doc
    forall a (m :: * -> *).
    (ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
    a -> m Doc
    prettyA Pattern
    p
                 WriterT [ProblemEq] (TCMT IO) [NamedArg Pattern]
    forall a. HasCallStack => a
    __IMPOSSIBLE__

              Pattern
    _ -> WriterT [ProblemEq] (TCMT IO) [NamedArg Pattern]
    forall (m :: * -> *) a. (MonadAddContext m, MonadTCError m) => m a
    mismatch
          where
            recurse :: Term -> WriterT [ProblemEq] (TCMT IO) [NamedArg Pattern]
    recurse Term
    v = do
              let piOrPathApplyM :: Type -> Term -> m (Elims, Type)
    piOrPathApplyM Type
    t Term
    v = do
                    (TelV tel t', bs) <- Int -> Type -> m (TelV Type, Boundary)
    forall (m :: * -> *).
    PureTCM m =>
    Int -> Type -> m (TelV Type, Boundary)
    telViewUpToPathBoundary' Int
    1 Type
    t
                    unless (size tel == 1) $ __IMPOSSIBLE__
                    return (teleElims tel bs, subst 0 v t')
              (e, t') <- Type -> Term -> WriterT [ProblemEq] (TCMT IO) (Elims, Type)
    forall {m :: * -> *}. PureTCM m => Type -> Term -> m (Elims, Type)
    piOrPathApplyM Type
    t Term
    v
              strip (self `applyE` e) t' ps qs

            mismatch :: forall m a. (MonadAddContext m, MonadTCError m) => m a
            mismatch :: forall (m :: * -> *) a. (MonadAddContext m, MonadTCError m) => m a
    mismatch = Telescope -> m a -> m a
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    forall (m :: * -> *) a.
    MonadAddContext m =>
    Telescope -> m a -> m a
    addContext Telescope
    delta (m a -> m a) -> m a -> m a
    forall a b. (a -> b) -> a -> b
    $ TypeError -> m a
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    TypeError -> m a
    typeError (TypeError -> m a) -> TypeError -> m a
    forall a b. (a -> b) -> a -> b
    $
              Pattern -> NamedArg DeBruijnPattern -> TypeError
    WithClausePatternMismatch (NamedArg Pattern -> Pattern
    forall a. NamedArg a -> a
    namedArg NamedArg Pattern
    p0) NamedArg DeBruijnPattern
    q

            -- Make a WildP, keeping arg. info.
            makeWildP :: NamedArg A.Pattern -> NamedArg A.Pattern
            makeWildP :: NamedArg Pattern -> NamedArg Pattern
    makeWildP = (Pattern -> Pattern) -> NamedArg Pattern -> NamedArg Pattern
    forall a b. (a -> b) -> NamedArg a -> NamedArg b
    updateNamedArg ((Pattern -> Pattern) -> NamedArg Pattern -> NamedArg Pattern)
    -> (Pattern -> Pattern) -> NamedArg Pattern -> NamedArg Pattern
    forall a b. (a -> b) -> a -> b
    $ Pattern -> Pattern -> Pattern
    forall a b. a -> b -> a
    const (Pattern -> Pattern -> Pattern) -> Pattern -> Pattern -> Pattern
    forall a b. (a -> b) -> a -> b
    $ PatInfo -> Pattern
    forall e. PatInfo -> Pattern' e
    A.WildP PatInfo
    patNoRange

            -- case I.ConP / A.ConP
            stripConP
              :: QName       -- Data type name of this constructor pattern.
              -> [Arg Term]  -- Data type arguments of this constructor pattern.
              -> Abs Type    -- Type the remaining patterns eliminate.
              -> ConHead     -- Constructor of this pattern.
              -> ConInfo     -- Constructor info of this pattern (constructor/record).
              -> [NamedArg DeBruijnPattern]  -- Argument patterns (parent clause).
              -> [NamedArg A.Pattern]        -- Argument patterns (with clause).
              -> WriterT [ProblemEq] TCM [NamedArg A.Pattern]  -- Stripped patterns.
            stripConP :: QName
    -> Args
    -> Abs Type
    -> ConHead
    -> ConOrigin
    -> [NamedArg DeBruijnPattern]
    -> [NamedArg Pattern]
    -> WriterT [ProblemEq] (TCMT IO) [NamedArg Pattern]
    stripConP QName
    d Args
    us Abs Type
    b ConHead
    c ConOrigin
    ci [NamedArg DeBruijnPattern]
    qs' [NamedArg Pattern]
    ps' = do

              -- Get the type and number of parameters of the constructor.
              Defn {defType = ct, theDef = Constructor{conPars = np}}  <- ConHead -> WriterT [ProblemEq] (TCMT IO) Definition
    forall (m :: * -> *). HasConstInfo m => ConHead -> m Definition
    getConInfo ConHead
    c
              -- Compute the argument telescope for the constructor
              let ct' = Type
    ct Type -> Args -> Type
    `piApply` Int -> Args -> Args
    forall a. Int -> [a] -> [a]
    take Int
    np Args
    us
              TelV tel' _ <- liftTCM $ telViewPath ct'
              -- (TelV tel' _, _boundary) <- liftTCM $ telViewPathBoundary ct'

              reportSDoc "tc.with.strip" 20 $
                vcat [ "ct  = " <+> prettyTCM ct
                     , "ct' = " <+> prettyTCM ct'
                     , "np  = " <+> text (show np)
                     , "us  = " <+> prettyList (map prettyTCM us)
                     , "us' = " <+> prettyList (map prettyTCM $ take np us)
                     ]

              -- TODO Andrea: preserve IApplyP patterns in v, see _boundary?
              -- Compute the new type
              let v  = ConHead -> ConOrigin -> Elims -> Term
    Con ConHead
    c ConOrigin
    ci [ Arg Term -> Elim' Term
    forall a. Arg a -> Elim' a
    Apply (Arg Term -> Elim' Term) -> Arg Term -> Elim' Term
    forall a b. (a -> b) -> a -> b
    $ ArgInfo -> Term -> Arg Term
    forall e. ArgInfo -> e -> Arg e
    Arg ArgInfo
    info (Int -> Term
    var Int
    i) | (Int
    i, Arg ArgInfo
    info Named NamedName DeBruijnPattern
    _) <- [Int]
    -> [NamedArg DeBruijnPattern] -> [(Int, NamedArg DeBruijnPattern)]
    forall a b. [a] -> [b] -> [(a, b)]
    zip (Int -> [Int]
    forall a. Integral a => a -> [a]
    downFrom (Int -> [Int]) -> Int -> [Int]
    forall a b. (a -> b) -> a -> b
    $ [NamedArg DeBruijnPattern] -> Int
    forall a. Sized a => a -> Int
    size [NamedArg DeBruijnPattern]
    qs') [NamedArg DeBruijnPattern]
    qs' ]
                  t' = Telescope
    tel' Telescope -> Type -> Type
    forall t. Abstract t => Telescope -> t -> t
    `abstract` Abs Type -> SubstArg Type -> Type
    forall a. Subst a => Abs a -> SubstArg a -> a
    absApp (Int -> Abs Type -> Abs Type
    forall a. Subst a => Int -> a -> a
    raise (Telescope -> Int
    forall a. Sized a => a -> Int
    size Telescope
    tel') Abs Type
    b) Term
    SubstArg Type
    v
                  self' = Telescope
    tel' Telescope -> Term -> Term
    forall t. Abstract t => Telescope -> t -> t
    `abstract` Term -> Term -> Term
    forall t. Apply t => t -> Term -> t
    apply1 (Int -> Term -> Term
    forall a. Subst a => Int -> a -> a
    raise (Telescope -> Int
    forall a. Sized a => a -> Int
    size Telescope
    tel') Term
    self) Term
    v  -- Issue 1546

              reportSDoc "tc.with.strip" 15 $ sep
                [ "inserting implicit"
                , nest 2 $ prettyList $ map prettyA (ps' ++ ps)
                , nest 2 $ ":" <+> prettyTCM t'
                ]

              -- Insert implicit patterns (just for the constructor arguments)
              psi' <- liftTCM $ insertImplicitPatterns ExpandLast ps' tel'
              unless (size psi' == size tel') $ typeError $
                WrongNumberOfConstructorArguments (conName c) (size tel') (size psi')

              -- Andreas, Ulf, 2016-06-01, Ulf's variant at issue #679
              -- Since instantiating the type with a constructor pattern
              -- can reveal more hidden arguments, we need to insert them here.
              psi <- liftTCM $ insertImplicitPatternsT ExpandLast (psi' ++ ps) t'

              -- Keep going
              strip self' t' psi (qs' ++ qs)

    -- | Construct the display form for a with function. It will display
    --   applications of the with function as applications to the original function.
    --   For instance,
    --
    --   @
    --     aux a b c
    --   @
    --
    --   as
    --
    --   @
    --     f (suc a) (suc b) | c
    --   @
    withDisplayForm
      :: QName
           -- ^ The name of parent function.
      -> QName
           -- ^ The name of the @with@-function.
      -> Telescope
           -- ^ __@Δ₁@__     The arguments of the @with@ function before the @with@ expressions.
      -> Telescope
           -- ^ __@Δ₂@__     The arguments of the @with@ function after the @with@ expressions.
      -> Nat
           -- ^ __@n@__      The number of @with@ expressions.
      -> [NamedArg DeBruijnPattern]
          -- ^ __@qs@__      The parent patterns.
      -> Permutation
          -- ^ __@perm@__    Permutation to split into needed and unneeded vars.
      -> Permutation
          -- ^ __@lhsPerm@__ Permutation reordering the variables in parent patterns.
      -> TCM DisplayForm
    withDisplayForm :: QName
    -> QName
    -> Telescope
    -> Telescope
    -> Int
    -> [NamedArg DeBruijnPattern]
    -> Permutation
    -> Permutation
    -> TCM DisplayForm
    withDisplayForm QName
    f QName
    aux Telescope
    delta1 Telescope
    delta2 Int
    n [NamedArg DeBruijnPattern]
    qs perm :: Permutation
    perm@(Perm Int
    m [Int]
    _) Permutation
    lhsPerm = do

      -- Compute the arity of the display form.
      let arity0 :: Int
    arity0 = Int
    n Int -> Int -> Int
    forall a. Num a => a -> a -> a
    + Telescope -> Int
    forall a. Sized a => a -> Int
    size Telescope
    delta1 Int -> Int -> Int
    forall a. Num a => a -> a -> a
    + Telescope -> Int
    forall a. Sized a => a -> Int
    size Telescope
    delta2
      -- The currently free variables have to be added to the front.
      topArgs <- Int -> Args -> Args
    forall a. Subst a => Int -> a -> a
    raise Int
    arity0 (Args -> Args) -> TCMT IO Args -> TCMT IO Args
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> TCMT IO Args
    forall (m :: * -> *). MonadTCEnv m => m Args
    getContextArgs
      let top    = Args -> Int
    forall a. [a] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length Args
    topArgs
          arity  = Int
    arity0 Int -> Int -> Int
    forall a. Num a => a -> a -> a
    + Int
    top

      -- Build the rhs of the display form.
      wild <- freshNoName_ <&> \ Name
    x -> QName -> Elims -> Term
    Def (Name -> QName
    qualify_ Name
    x) []
      let -- Convert the parent patterns to terms.
          tqs0       = [NamedArg DeBruijnPattern] -> [Elim' DisplayTerm]
    patsToElims [NamedArg DeBruijnPattern]
    qs
          -- Build a substitution to replace the parent pattern vars
          -- by the pattern vars of the with-function.
          (ys0, ys1) = splitAt (size delta1) $ permute perm $ downFrom m
          ys         = [Maybe Int] -> [Maybe Int]
    forall a. [a] -> [a]
    reverse ((Int -> Maybe Int) -> [Int] -> [Maybe Int]
    forall a b. (a -> b) -> [a] -> [b]
    map Int -> Maybe Int
    forall a. a -> Maybe a
    Just [Int]
    ys0 [Maybe Int] -> [Maybe Int] -> [Maybe Int]
    forall a. [a] -> [a] -> [a]
    ++ Int -> Maybe Int -> [Maybe Int]
    forall a. Int -> a -> [a]
    replicate Int
    n Maybe Int
    forall a. Maybe a
    Nothing [Maybe Int] -> [Maybe Int] -> [Maybe Int]
    forall a. [a] -> [a] -> [a]
    ++ (Int -> Maybe Int) -> [Int] -> [Maybe Int]
    forall a b. (a -> b) -> [a] -> [b]
    map Int -> Maybe Int
    forall a. a -> Maybe a
    Just [Int]
    ys1)
                       [Maybe Int] -> [Maybe Int] -> [Maybe Int]
    forall a. [a] -> [a] -> [a]
    ++ (Int -> Maybe Int) -> [Int] -> [Maybe Int]
    forall a b. (a -> b) -> [a] -> [b]
    map (Int -> Maybe Int
    forall a. a -> Maybe a
    Just (Int -> Maybe Int) -> (Int -> Int) -> Int -> Maybe Int
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Int
    m Int -> Int -> Int
    forall a. Num a => a -> a -> a
    +)) [Int
    0..Int
    topInt -> Int -> Int
    forall a. Num a => a -> a -> a
    -Int
    1]
          rho        = Int -> [Maybe Int] -> Term -> Substitution' Term
    sub Int
    top [Maybe Int]
    ys Term
    wild
          tqs        = Substitution' (SubstArg [Elim' DisplayTerm])
    -> [Elim' DisplayTerm] -> [Elim' DisplayTerm]
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    applySubst Substitution' Term
    Substitution' (SubstArg [Elim' DisplayTerm])
    rho [Elim' DisplayTerm]
    tqs0
          -- Build the arguments to the with function.
          es         = (Arg Term -> Elim' DisplayTerm) -> Args -> [Elim' DisplayTerm]
    forall a b. (a -> b) -> [a] -> [b]
    map (Arg DisplayTerm -> Elim' DisplayTerm
    forall a. Arg a -> Elim' a
    Apply (Arg DisplayTerm -> Elim' DisplayTerm)
    -> (Arg Term -> Arg DisplayTerm) -> Arg Term -> Elim' DisplayTerm
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Term -> DisplayTerm) -> Arg Term -> Arg DisplayTerm
    forall a b. (a -> b) -> Arg a -> Arg b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap Term -> DisplayTerm
    DTerm) Args
    topArgs [Elim' DisplayTerm] -> [Elim' DisplayTerm] -> [Elim' DisplayTerm]
    forall a. [a] -> [a] -> [a]
    ++ [Elim' DisplayTerm]
    tqs
          withArgs   = NonEmpty Term -> [Term] -> NonEmpty Term
    forall a. List1 a -> [a] -> List1 a
    List1.fromListSafe NonEmpty Term
    forall a. HasCallStack => a
    __IMPOSSIBLE__ ([Term] -> NonEmpty Term) -> [Term] -> NonEmpty Term
    forall a b. (a -> b) -> a -> b
    $  -- List is non-empty since n >= 1
                         (Int -> Term) -> [Int] -> [Term]
    forall a b. (a -> b) -> [a] -> [b]
    map Int -> Term
    var ([Int] -> [Term]) -> [Int] -> [Term]
    forall a b. (a -> b) -> a -> b
    $ Int -> [Int] -> [Int]
    forall a. Int -> [a] -> [a]
    take Int
    n ([Int] -> [Int]) -> [Int] -> [Int]
    forall a b. (a -> b) -> a -> b
    $ Int -> [Int]
    forall a. Integral a => a -> [a]
    downFrom (Int -> [Int]) -> Int -> [Int]
    forall a b. (a -> b) -> a -> b
    $ Telescope -> Int
    forall a. Sized a => a -> Int
    size Telescope
    delta2 Int -> Int -> Int
    forall a. Num a => a -> a -> a
    + Int
    n
          dt         = DisplayTerm -> List1 DisplayTerm -> Elims -> DisplayTerm
    DWithApp (QName -> [Elim' DisplayTerm] -> DisplayTerm
    DDef QName
    f [Elim' DisplayTerm]
    es) ((Term -> DisplayTerm) -> NonEmpty Term -> List1 DisplayTerm
    forall a b. (a -> b) -> NonEmpty a -> NonEmpty b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap Term -> DisplayTerm
    DTerm NonEmpty Term
    withArgs) []

      -- Build the lhs of the display form and finish.
      -- @var 0@ is the pattern variable (hole).
      let display = Int -> Elims -> DisplayTerm -> DisplayForm
    Display Int
    arity [Arg Term -> Elim' Term
    forall a. Arg a -> Elim' a
    Apply (Arg Term -> Elim' Term) -> Arg Term -> Elim' Term
    forall a b. (a -> b) -> a -> b
    $ Term -> Arg Term
    forall a. a -> Arg a
    defaultArg (Term -> Arg Term) -> Term -> Arg Term
    forall a b. (a -> b) -> a -> b
    $ Int -> Term
    var Int
    i | Int
    i <- Int -> [Int]
    forall a. Integral a => a -> [a]
    downFrom Int
    arity] DisplayTerm
    dt

      -- Debug printing.
      let addFullCtx = Telescope -> TCMT IO Doc -> TCMT IO Doc
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    forall (m :: * -> *) a.
    MonadAddContext m =>
    Telescope -> m a -> m a
    addContext Telescope
    delta1
                     (TCMT IO Doc -> TCMT IO Doc)
    -> (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (TCMT IO Doc -> [[Char]] -> TCMT IO Doc)
    -> [[Char]] -> TCMT IO Doc -> TCMT IO Doc
    forall a b c. (a -> b -> c) -> b -> a -> c
    flip (([Char] -> TCMT IO Doc -> TCMT IO Doc)
    -> TCMT IO Doc -> [[Char]] -> TCMT IO Doc
    forall a b. (a -> b -> b) -> b -> [a] -> b
    forall (t :: * -> *) a b.
    Foldable t =>
    (a -> b -> b) -> b -> t a -> b
    foldr [Char] -> TCMT IO Doc -> TCMT IO Doc
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    forall (m :: * -> *) a. MonadAddContext m => [Char] -> m a -> m a
    addContext) ([Int] -> (Int -> [Char]) -> [[Char]]
    forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
    for [Int
    1..Int
    n] ((Int -> [Char]) -> [[Char]]) -> (Int -> [Char]) -> [[Char]]
    forall a b. (a -> b) -> a -> b
    $ \ Int
    i -> [Char]
    "w" [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ Int -> [Char]
    forall a. Show a => a -> [Char]
    show Int
    i)
                     (TCMT IO Doc -> TCMT IO Doc)
    -> (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Telescope -> TCMT IO Doc -> TCMT IO Doc
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    forall (m :: * -> *) a.
    MonadAddContext m =>
    Telescope -> m a -> m a
    addContext Telescope
    delta2
      reportSDoc "tc.with.display" 20 $ vcat
        [ "withDisplayForm"
        , nest 2 $ vcat
          [ "f      =" <+> text (prettyShow f)
          , "aux    =" <+> text (prettyShow aux)
          , "delta1 =" <+> prettyTCM delta1
          , "delta2 =" <+> do addContext delta1 $ prettyTCM delta2
          , "n      =" <+> text (show n)
          , "perm   =" <+> text (show perm)
          , "top    =" <+> do addFullCtx $ prettyTCM topArgs
          , "qs     =" <+> prettyList (map pretty qs)
          , "qsToTm =" <+> prettyTCM tqs0 -- ctx would be permuted form of delta1 ++ delta2
          , "ys     =" <+> text (show ys)
          , "rho    =" <+> text (prettyShow rho)
          , "qs[rho]=" <+> do addFullCtx $ prettyTCM tqs
          , "dt     =" <+> do addFullCtx $ prettyTCM dt
          ]
        ]
      reportSDoc "tc.with.display" 70 $ nest 2 $ vcat
          [ "raw    =" <+> text (show display)
          ]

      return display
      where
        -- Ulf, 2014-02-19: We need to rename the module parameters as well! (issue1035)
        -- sub top ys wild = map term [0 .. m - 1] ++# raiseS (length qs)
        -- Andreas, 2015-10-28: Yes, but properly! (Issue 1407)
        sub :: Int -> [Maybe Int] -> Term -> Substitution' Term
    sub Int
    top [Maybe Int]
    ys Term
    wild = [Term] -> Substitution' Term
    forall a. DeBruijn a => [a] -> Substitution' a
    parallelS ([Term] -> Substitution' Term) -> [Term] -> Substitution' Term
    forall a b. (a -> b) -> a -> b
    $ (Int -> Term) -> [Int] -> [Term]
    forall a b. (a -> b) -> [a] -> [b]
    map Int -> Term
    term [Int
    0 .. Int
    m Int -> Int -> Int
    forall a. Num a => a -> a -> a
    + Int
    top Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - Int
    1]
          where
            term :: Int -> Term
    term Int
    i = Term -> (Int -> Term) -> Maybe Int -> Term
    forall b a. b -> (a -> b) -> Maybe a -> b
    maybe Term
    wild Int -> Term
    var (Maybe Int -> Term) -> Maybe Int -> Term
    forall a b. (a -> b) -> a -> b
    $ Maybe Int -> [Maybe Int] -> Maybe Int
    forall a. Eq a => a -> [a] -> Maybe Int
    List.elemIndex (Int -> Maybe Int
    forall a. a -> Maybe a
    Just Int
    i) [Maybe Int]
    ys

    -- Andreas, 2014-12-05 refactored using numberPatVars
    -- Andreas, 2013-02-28 modeled after Coverage/Match/buildMPatterns
    patsToElims :: [NamedArg DeBruijnPattern] -> [I.Elim' DisplayTerm]
    patsToElims :: [NamedArg DeBruijnPattern] -> [Elim' DisplayTerm]
    patsToElims = (NamedArg DeBruijnPattern -> Elim' DisplayTerm)
    -> [NamedArg DeBruijnPattern] -> [Elim' DisplayTerm]
    forall a b. (a -> b) -> [a] -> [b]
    map ((NamedArg DeBruijnPattern -> Elim' DisplayTerm)
     -> [NamedArg DeBruijnPattern] -> [Elim' DisplayTerm])
    -> (NamedArg DeBruijnPattern -> Elim' DisplayTerm)
    -> [NamedArg DeBruijnPattern]
    -> [Elim' DisplayTerm]
    forall a b. (a -> b) -> a -> b
    $ Arg DeBruijnPattern -> Elim' DisplayTerm
    toElim (Arg DeBruijnPattern -> Elim' DisplayTerm)
    -> (NamedArg DeBruijnPattern -> Arg DeBruijnPattern)
    -> NamedArg DeBruijnPattern
    -> Elim' DisplayTerm
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Named NamedName DeBruijnPattern -> DeBruijnPattern)
    -> NamedArg DeBruijnPattern -> Arg DeBruijnPattern
    forall a b. (a -> b) -> Arg a -> Arg b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap Named NamedName DeBruijnPattern -> DeBruijnPattern
    forall name a. Named name a -> a
    namedThing
      where
        toElim :: Arg DeBruijnPattern -> I.Elim' DisplayTerm
        toElim :: Arg DeBruijnPattern -> Elim' DisplayTerm
    toElim (Arg ArgInfo
    ai DeBruijnPattern
    p) = case DeBruijnPattern
    p of
          ProjP ProjOrigin
    o QName
    d -> ProjOrigin -> QName -> Elim' DisplayTerm
    forall a. ProjOrigin -> QName -> Elim' a
    I.Proj ProjOrigin
    o QName
    d
          DeBruijnPattern
    p         -> Arg DisplayTerm -> Elim' DisplayTerm
    forall a. Arg a -> Elim' a
    I.Apply (Arg DisplayTerm -> Elim' DisplayTerm)
    -> Arg DisplayTerm -> Elim' DisplayTerm
    forall a b. (a -> b) -> a -> b
    $ ArgInfo -> DisplayTerm -> Arg DisplayTerm
    forall e. ArgInfo -> e -> Arg e
    Arg ArgInfo
    ai (DisplayTerm -> Arg DisplayTerm) -> DisplayTerm -> Arg DisplayTerm
    forall a b. (a -> b) -> a -> b
    $ DeBruijnPattern -> DisplayTerm
    toTerm DeBruijnPattern
    p

        toTerms :: [NamedArg DeBruijnPattern] -> [Arg DisplayTerm]
        toTerms :: [NamedArg DeBruijnPattern] -> [Arg DisplayTerm]
    toTerms = (NamedArg DeBruijnPattern -> Arg DisplayTerm)
    -> [NamedArg DeBruijnPattern] -> [Arg DisplayTerm]
    forall a b. (a -> b) -> [a] -> [b]
    map ((NamedArg DeBruijnPattern -> Arg DisplayTerm)
     -> [NamedArg DeBruijnPattern] -> [Arg DisplayTerm])
    -> (NamedArg DeBruijnPattern -> Arg DisplayTerm)
    -> [NamedArg DeBruijnPattern]
    -> [Arg DisplayTerm]
    forall a b. (a -> b) -> a -> b
    $ (Named NamedName DeBruijnPattern -> DisplayTerm)
    -> NamedArg DeBruijnPattern -> Arg DisplayTerm
    forall a b. (a -> b) -> Arg a -> Arg b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap ((Named NamedName DeBruijnPattern -> DisplayTerm)
     -> NamedArg DeBruijnPattern -> Arg DisplayTerm)
    -> (Named NamedName DeBruijnPattern -> DisplayTerm)
    -> NamedArg DeBruijnPattern
    -> Arg DisplayTerm
    forall a b. (a -> b) -> a -> b
    $ DeBruijnPattern -> DisplayTerm
    toTerm (DeBruijnPattern -> DisplayTerm)
    -> (Named NamedName DeBruijnPattern -> DeBruijnPattern)
    -> Named NamedName DeBruijnPattern
    -> DisplayTerm
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Named NamedName DeBruijnPattern -> DeBruijnPattern
    forall name a. Named name a -> a
    namedThing

        toTerm :: DeBruijnPattern -> DisplayTerm
        toTerm :: DeBruijnPattern -> DisplayTerm
    toTerm DeBruijnPattern
    p = case PatternInfo -> PatOrigin
    patOrigin (PatternInfo -> PatOrigin) -> PatternInfo -> PatOrigin
    forall a b. (a -> b) -> a -> b
    $ PatternInfo -> Maybe PatternInfo -> PatternInfo
    forall a. a -> Maybe a -> a
    fromMaybe PatternInfo
    forall a. HasCallStack => a
    __IMPOSSIBLE__ (Maybe PatternInfo -> PatternInfo)
    -> Maybe PatternInfo -> PatternInfo
    forall a b. (a -> b) -> a -> b
    $ DeBruijnPattern -> Maybe PatternInfo
    forall x. Pattern' x -> Maybe PatternInfo
    patternInfo DeBruijnPattern
    p of
          PatOrigin
    PatOSystem -> DeBruijnPattern -> DisplayTerm
    toDisplayPattern DeBruijnPattern
    p
          PatOrigin
    PatOSplit  -> DeBruijnPattern -> DisplayTerm
    toDisplayPattern DeBruijnPattern
    p
          PatOSplitArg{} -> DeBruijnPattern -> DisplayTerm
    toVarOrDot DeBruijnPattern
    p
          PatOVar{}  -> DeBruijnPattern -> DisplayTerm
    toVarOrDot DeBruijnPattern
    p
          PatOrigin
    PatODot    -> Term -> DisplayTerm
    DDot (Term -> DisplayTerm) -> Term -> DisplayTerm
    forall a b. (a -> b) -> a -> b
    $ DeBruijnPattern -> Term
    patternToTerm DeBruijnPattern
    p
          PatOrigin
    PatOWild   -> DeBruijnPattern -> DisplayTerm
    toVarOrDot DeBruijnPattern
    p
          PatOrigin
    PatOCon    -> DeBruijnPattern -> DisplayTerm
    toDisplayPattern DeBruijnPattern
    p
          PatOrigin
    PatORec    -> DeBruijnPattern -> DisplayTerm
    toDisplayPattern DeBruijnPattern
    p
          PatOrigin
    PatOLit    -> DeBruijnPattern -> DisplayTerm
    toDisplayPattern DeBruijnPattern
    p
          PatOrigin
    PatOAbsurd -> DeBruijnPattern -> DisplayTerm
    toDisplayPattern DeBruijnPattern
    p -- see test/Succeed/Issue2849.agda

        toDisplayPattern :: DeBruijnPattern -> DisplayTerm
        toDisplayPattern :: DeBruijnPattern -> DisplayTerm
    toDisplayPattern = \case
          IApplyP PatternInfo
    _ Term
    _ Term
    _ DBPatVar
    x -> Term -> DisplayTerm
    DTerm (Term -> DisplayTerm) -> Term -> DisplayTerm
    forall a b. (a -> b) -> a -> b
    $ Int -> Term
    var (Int -> Term) -> Int -> Term
    forall a b. (a -> b) -> a -> b
    $ DBPatVar -> Int
    dbPatVarIndex DBPatVar
    x -- TODO, should be an Elim' DisplayTerm ?
          ProjP ProjOrigin
    _ QName
    d  -> DisplayTerm
    forall a. HasCallStack => a
    __IMPOSSIBLE__
          VarP PatternInfo
    i DBPatVar
    x -> Term -> DisplayTerm
    DTerm  (Term -> DisplayTerm) -> Term -> DisplayTerm
    forall a b. (a -> b) -> a -> b
    $ Int -> Term
    var (Int -> Term) -> Int -> Term
    forall a b. (a -> b) -> a -> b
    $ DBPatVar -> Int
    dbPatVarIndex DBPatVar
    x
          DotP PatternInfo
    i Term
    t -> Term -> DisplayTerm
    DDot   (Term -> DisplayTerm) -> Term -> DisplayTerm
    forall a b. (a -> b) -> a -> b
    $ Term
    t
          p :: DeBruijnPattern
    p@(ConP ConHead
    c ConPatternInfo
    cpi [NamedArg DeBruijnPattern]
    ps) -> ConHead -> ConOrigin -> [Arg DisplayTerm] -> DisplayTerm
    DCon ConHead
    c (ConPatternInfo -> ConOrigin
    fromConPatternInfo ConPatternInfo
    cpi) ([Arg DisplayTerm] -> DisplayTerm)
    -> [Arg DisplayTerm] -> DisplayTerm
    forall a b. (a -> b) -> a -> b
    $ [NamedArg DeBruijnPattern] -> [Arg DisplayTerm]
    toTerms [NamedArg DeBruijnPattern]
    ps
          LitP PatternInfo
    i Literal
    l -> Term -> DisplayTerm
    DTerm  (Term -> DisplayTerm) -> Term -> DisplayTerm
    forall a b. (a -> b) -> a -> b
    $ Literal -> Term
    Lit Literal
    l
          DefP PatternInfo
    _ QName
    q [NamedArg DeBruijnPattern]
    ps -> QName -> [Elim' DisplayTerm] -> DisplayTerm
    DDef QName
    q ([Elim' DisplayTerm] -> DisplayTerm)
    -> [Elim' DisplayTerm] -> DisplayTerm
    forall a b. (a -> b) -> a -> b
    $ (Arg DisplayTerm -> Elim' DisplayTerm)
    -> [Arg DisplayTerm] -> [Elim' DisplayTerm]
    forall a b. (a -> b) -> [a] -> [b]
    map Arg DisplayTerm -> Elim' DisplayTerm
    forall a. Arg a -> Elim' a
    Apply ([Arg DisplayTerm] -> [Elim' DisplayTerm])
    -> [Arg DisplayTerm] -> [Elim' DisplayTerm]
    forall a b. (a -> b) -> a -> b
    $ [NamedArg DeBruijnPattern] -> [Arg DisplayTerm]
    toTerms [NamedArg DeBruijnPattern]
    ps

        toVarOrDot :: DeBruijnPattern -> DisplayTerm
        toVarOrDot :: DeBruijnPattern -> DisplayTerm
    toVarOrDot DeBruijnPattern
    p = case DeBruijnPattern -> Term
    patternToTerm DeBruijnPattern
    p of
          Var Int
    i [] -> Term -> DisplayTerm
    DTerm (Term -> DisplayTerm) -> Term -> DisplayTerm
    forall a b. (a -> b) -> a -> b
    $ Int -> Term
    var Int
    i
          Term
    t        -> Term -> DisplayTerm
    DDot Term
    t