    {-# LANGUAGE NondecreasingIndentation #-}

    module Agda.TypeChecking.With where

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

    import Data.Either
    import qualified Data.List as List
    import Data.Maybe
    import Data.Foldable ( foldrM )

    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.Monad
    import Agda.TypeChecking.Reduce
    import Agda.TypeChecking.Datatypes
    import Agda.TypeChecking.EtaContract
    import Agda.TypeChecking.Free
    import Agda.TypeChecking.Patterns.Abstract
    import Agda.TypeChecking.Pretty
    import Agda.TypeChecking.Primitive ( getRefl )
    import Agda.TypeChecking.Records
    import Agda.TypeChecking.Substitute
    import Agda.TypeChecking.Telescope
    import Agda.TypeChecking.Telescope.Path

    import Agda.TypeChecking.Abstract
    import Agda.TypeChecking.Rules.LHS.Implicit
    import Agda.TypeChecking.Rules.LHS.Problem (ProblemEq(..))

    import Agda.Utils.Functor
    import Agda.Utils.List
    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.Utils.Pretty (prettyShow)
    import qualified Agda.Utils.Pretty as P
    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.
      -> [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 @π@
         , [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
    -> [Arg (Term, EqualityView)]
    -> (Telescope, Telescope, Permutation, Type,
        [Arg (Term, EqualityView)])
    splitTelForWith Telescope
    delta Type
    t [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 = [Arg (Term, EqualityView)] -> VarSet
    forall t. Free t => t -> VarSet
    allFreeVars [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' :: [Arg (Term, EqualityView)]
    vtys' = Substitution' (SubstArg [Arg (Term, EqualityView)])
    -> [Arg (Term, EqualityView)] -> [Arg (Term, EqualityView)]
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    applySubst Substitution' Term
    Substitution' (SubstArg [Arg (Term, EqualityView)])
    rhopi [Arg (Term, EqualityView)]
    vtys

      in (Telescope
    delta1, Telescope
    delta2, Permutation
    perm, Type
    t', [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 types.
      -> [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.
      -> [(Int,(Term,Term))]                -- ^ @Δ₁,Δ₂ ⊢ [(i,(u0,u1))] : b  boundary.
      -> TCM (Type, Nat)
        -- ^ @Δ₁ → wtel → Δ₂′ → b′@ such that
        --     @[vs/wtel]wtel = as@ and
        --     @[vs/wtel]Δ₂′ = Δ₂@ and
        --     @[vs/wtel]b′ = b@.
        -- Plus the final number of with-arguments.
    withFunctionType :: Telescope
    -> [Arg (Term, EqualityView)]
    -> Telescope
    -> Type
    -> [(Int, (Term, Term))]
    -> TCM (Type, Int)
    withFunctionType Telescope
    delta1 [Arg (Term, EqualityView)]
    vtys Telescope
    delta2 Type
    b [(Int, (Term, Term))]
    bndry = Telescope -> TCM (Type, Int) -> TCM (Type, Int)
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    addContext Telescope
    delta1 (TCM (Type, Int) -> TCM (Type, Int))
    -> TCM (Type, Int) -> TCM (Type, 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
    prettyTCM a
    x

      Type
    d2b <- Telescope -> Type -> [(Int, (Term, Term))] -> TCM Type
    telePiPath_ Telescope
    delta2 Type
    b [(Int, (Term, Term))]
    bndry
      Int -> [Char] -> Type -> TCMT IO ()
    forall {m :: * -> *} {a}.
    (MonadDebug m, PrettyTCM a) =>
    Int -> [Char] -> a -> m ()
    dbg Int
    30 [Char]
    "Δ₂ → B" Type
    d2b
      Type
    d2b  <- Type -> TCM Type
    forall a (m :: * -> *). (Normalise a, MonadReduce m) => a -> m a
    normalise Type
    d2b
      Int -> [Char] -> Type -> TCMT IO ()
    forall {m :: * -> *} {a}.
    (MonadDebug m, PrettyTCM a) =>
    Int -> [Char] -> a -> m ()
    dbg Int
    30 [Char]
    "normal Δ₂ → B" Type
    d2b
      Type
    d2b  <- Type -> TCM Type
    forall (m :: * -> *) a.
    (MonadTCEnv m, HasConstInfo m, HasOptions m, TermLike a) =>
    a -> m a
    etaContract Type
    d2b
      Int -> [Char] -> Type -> TCMT IO ()
    forall {m :: * -> *} {a}.
    (MonadDebug m, PrettyTCM a) =>
    Int -> [Char] -> a -> m ()
    dbg Int
    30 [Char]
    "eta-contracted Δ₂ → B" Type
    d2b

      [Arg (Term, EqualityView)]
    vtys <- [Arg (Term, EqualityView)] -> TCMT IO [Arg (Term, EqualityView)]
    forall (m :: * -> *) a.
    (MonadTCEnv m, HasConstInfo m, HasOptions m, TermLike a) =>
    a -> m a
    etaContract ([Arg (Term, EqualityView)] -> TCMT IO [Arg (Term, EqualityView)])
    -> TCMT IO [Arg (Term, EqualityView)]
    -> TCMT IO [Arg (Term, EqualityView)]
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< [Arg (Term, EqualityView)] -> TCMT IO [Arg (Term, EqualityView)]
    forall a (m :: * -> *). (Normalise a, MonadReduce m) => a -> m a
    normalise [Arg (Term, EqualityView)]
    vtys

      -- wd2db = wtel → [vs : as] (Δ₂ → B)
      Type
    wd2b <- (Arg (Term, EqualityView) -> Type -> TCM Type)
    -> Type -> [Arg (Term, EqualityView)] -> TCM Type
    forall (t :: * -> *) (m :: * -> *) a b.
    (Foldable t, Monad m) =>
    (a -> b -> m b) -> b -> t a -> m b
    foldrM Arg (Term, EqualityView) -> Type -> TCM Type
    piAbstract Type
    d2b [Arg (Term, EqualityView)]
    vtys
      Int -> [Char] -> Type -> TCMT IO ()
    forall {m :: * -> *} {a}.
    (MonadDebug m, PrettyTCM a) =>
    Int -> [Char] -> a -> m ()
    dbg Int
    30 [Char]
    "wΓ → Δ₂ → B" Type
    wd2b

      let nwithargs :: Int
    nwithargs = [EqualityView] -> Int
    countWithArgs ((Arg (Term, EqualityView) -> EqualityView)
    -> [Arg (Term, EqualityView)] -> [EqualityView]
    forall a b. (a -> b) -> [a] -> [b]
    map ((Term, EqualityView) -> EqualityView
    forall a b. (a, b) -> b
    snd ((Term, EqualityView) -> EqualityView)
    -> (Arg (Term, EqualityView) -> (Term, EqualityView))
    -> Arg (Term, EqualityView)
    -> EqualityView
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Arg (Term, EqualityView) -> (Term, EqualityView)
    forall e. Arg e -> e
    unArg) [Arg (Term, EqualityView)]
    vtys)

      TelV Telescope
    wtel Type
    _ <- Int -> Type -> TCMT IO (TelV Type)
    forall (m :: * -> *).
    (MonadReduce m, MonadAddContext m) =>
    Int -> Type -> m (TelV Type)
    telViewUpTo Int
    nwithargs Type
    wd2b

      -- select the boundary for "Δ₁" abstracting over "wΓ.Δ₂"
      let bndry' :: [(Int, (Term, Term))]
    bndry' = [(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)) <- [(Int, (Term, Term))]
    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 Term
    u = Telescope -> Term -> Term
    forall a. TeleNoAbs a => a -> Term -> Term
    teleNoAbs Telescope
    wtel (Telescope -> Term -> Term
    forall t. Abstract t => Telescope -> t -> t
    abstract Telescope
    delta2 Term
    u)

      Type
    d1wd2b <- Telescope -> Type -> [(Int, (Term, Term))] -> TCM Type
    telePiPath_ Telescope
    delta1 Type
    wd2b [(Int, (Term, Term))]
    bndry'

      Int -> [Char] -> Type -> TCMT IO ()
    forall {m :: * -> *} {a}.
    (MonadDebug m, PrettyTCM a) =>
    Int -> [Char] -> a -> m ()
    dbg Int
    30 [Char]
    "Δ₁ → wΓ → Δ₂ → B" Type
    d1wd2b

      (Type, Int) -> TCM (Type, Int)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Type
    d1wd2b, Int
    nwithargs)

    countWithArgs :: [EqualityView] -> Nat
    countWithArgs :: [EqualityView] -> Int
    countWithArgs = [Int] -> Int
    forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
    sum ([Int] -> Int)
    -> ([EqualityView] -> [Int]) -> [EqualityView] -> Int
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (EqualityView -> Int) -> [EqualityView] -> [Int]
    forall a b. (a -> b) -> [a] -> [b]
    map EqualityView -> Int
    forall {p}. Num p => EqualityView -> p
    countArgs
      where
        countArgs :: EqualityView -> p
    countArgs OtherType{}    = p
    1
        countArgs IdiomType{}    = p
    2
        countArgs EqualityType{} = p
    2

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

    -- | 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.
      -> [A.SpineClause]      -- ^ With-clauses.
      -> TCM [A.SpineClause]  -- ^ With-clauses flattened wrt. parent patterns.
    buildWithFunction :: [Name]
    -> QName
    -> QName
    -> Type
    -> Telescope
    -> [NamedArg DeBruijnPattern]
    -> Int
    -> Substitution' Term
    -> Permutation
    -> Int
    -> Int
    -> [Clause' SpineLHS]
    -> TCM [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 [Clause' SpineLHS]
    cs = (Clause' SpineLHS -> TCMT IO (Clause' SpineLHS))
    -> [Clause' SpineLHS] -> TCM [Clause' SpineLHS]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    mapM Clause' SpineLHS -> TCMT IO (Clause' SpineLHS)
    buildWithClause [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 (A.SpineLHS LHSInfo
    i QName
    _ [NamedArg (Pattern' Expr)]
    allPs) [ProblemEq]
    inheritedPats RHS
    rhs WhereDeclarations
    wh Bool
    catchall) = do
          let ([NamedArg (Pattern' Expr)]
    ps, [NamedArg (Pattern' Expr)]
    wps)    = [NamedArg (Pattern' Expr)]
    -> ([NamedArg (Pattern' Expr)], [NamedArg (Pattern' Expr)])
    splitOffTrailingWithPatterns [NamedArg (Pattern' Expr)]
    allPs
              ([NamedArg (Pattern' Expr)]
    wps0, [NamedArg (Pattern' Expr)]
    wps1) = Int
    -> [NamedArg (Pattern' Expr)]
    -> ([NamedArg (Pattern' Expr)], [NamedArg (Pattern' Expr)])
    forall a. Int -> [a] -> ([a], [a])
    splitAt Int
    n [NamedArg (Pattern' Expr)]
    wps
              ps0 :: [NamedArg (Pattern' Expr)]
    ps0          = (NamedArg (Pattern' Expr) -> NamedArg (Pattern' Expr))
    -> [NamedArg (Pattern' Expr)] -> [NamedArg (Pattern' Expr)]
    forall a b. (a -> b) -> [a] -> [b]
    map ((Pattern' Expr -> Pattern' Expr)
    -> NamedArg (Pattern' Expr) -> NamedArg (Pattern' Expr)
    forall a b. (a -> b) -> NamedArg a -> NamedArg b
    updateNamedArg Pattern' Expr -> Pattern' Expr
    forall {e}. Pattern' e -> Pattern' e
    fromWithP) [NamedArg (Pattern' Expr)]
    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" 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' Expr -> TCMT IO Doc
    forall a (m :: * -> *).
    (ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
    a -> m Doc
    prettyA Pattern' Expr
    p TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> TCMT IO Doc
    "=" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Term -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Term
    v TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> TCMT IO Doc
    ":" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Dom Type -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Dom Type
    a
            | A.ProblemEq Pattern' Expr
    p Term
    v Dom Type
    a <- [ProblemEq]
    inheritedPats
            ]
          ([ProblemEq]
    strippedPats, [NamedArg (Pattern' Expr)]
    ps') <- [Name]
    -> QName
    -> QName
    -> Type
    -> Telescope
    -> [NamedArg DeBruijnPattern]
    -> Int
    -> Permutation
    -> [NamedArg (Pattern' Expr)]
    -> TCM ([ProblemEq], [NamedArg (Pattern' Expr)])
    stripWithClausePatterns [Name]
    cxtNames QName
    f QName
    aux Type
    t Telescope
    delta [NamedArg DeBruijnPattern]
    qs Int
    npars Permutation
    perm [NamedArg (Pattern' Expr)]
    ps
          [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 -> Int -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *).
    Applicative m =>
    m Doc -> Int -> m Doc -> m Doc
    hang TCMT IO Doc
    "strippedPats:" Int
    2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $
                                      [TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    vcat [ Pattern' Expr -> TCMT IO Doc
    forall a (m :: * -> *).
    (ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
    a -> m Doc
    prettyA Pattern' Expr
    p TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> TCMT IO Doc
    "==" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Term -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Term
    v TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> (TCMT IO Doc
    ":" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Dom Type -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Dom Type
    t)
                                           | A.ProblemEq Pattern' Expr
    p Term
    v Dom Type
    t <- [ProblemEq]
    strippedPats ]
          RHS
    rhs <- [ProblemEq] -> RHS -> TCMT IO RHS
    buildRHS [ProblemEq]
    strippedPats RHS
    rhs
          let ([NamedArg (Pattern' Expr)]
    ps1, [NamedArg (Pattern' Expr)]
    ps2) = Int
    -> [NamedArg (Pattern' Expr)]
    -> ([NamedArg (Pattern' Expr)], [NamedArg (Pattern' Expr)])
    forall a. Int -> [a] -> ([a], [a])
    splitAt Int
    n1 [NamedArg (Pattern' Expr)]
    ps'
          let result :: Clause' SpineLHS
    result = SpineLHS
    -> [ProblemEq]
    -> RHS
    -> WhereDeclarations
    -> Bool
    -> Clause' SpineLHS
    forall lhs.
    lhs
    -> [ProblemEq] -> RHS -> WhereDeclarations -> Bool -> Clause' lhs
    A.Clause (LHSInfo -> QName -> [NamedArg (Pattern' Expr)] -> SpineLHS
    A.SpineLHS LHSInfo
    i QName
    aux ([NamedArg (Pattern' Expr)] -> SpineLHS)
    -> [NamedArg (Pattern' Expr)] -> SpineLHS
    forall a b. (a -> b) -> a -> b
    $ [NamedArg (Pattern' Expr)]
    ps1 [NamedArg (Pattern' Expr)]
    -> [NamedArg (Pattern' Expr)] -> [NamedArg (Pattern' Expr)]
    forall a. [a] -> [a] -> [a]
    ++ [NamedArg (Pattern' Expr)]
    ps0 [NamedArg (Pattern' Expr)]
    -> [NamedArg (Pattern' Expr)] -> [NamedArg (Pattern' Expr)]
    forall a. [a] -> [a] -> [a]
    ++ [NamedArg (Pattern' Expr)]
    ps2 [NamedArg (Pattern' Expr)]
    -> [NamedArg (Pattern' Expr)] -> [NamedArg (Pattern' Expr)]
    forall a. [a] -> [a] -> [a]
    ++ [NamedArg (Pattern' Expr)]
    wps1)
                         ([ProblemEq]
    inheritedPats [ProblemEq] -> [ProblemEq] -> [ProblemEq]
    forall a. [a] -> [a] -> [a]
    ++ [ProblemEq]
    strippedPats)
                         RHS
    rhs WhereDeclarations
    wh Bool
    catchall
          [Char] -> Int -> TCMT IO Doc -> TCMT IO ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "tc.with" Int
    20 (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 returns" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Clause' SpineLHS -> TCMT IO Doc
    forall a (m :: * -> *).
    (ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
    a -> m Doc
    prettyA Clause' SpineLHS
    result
            ]
          Clause' SpineLHS -> TCMT IO (Clause' SpineLHS)
    forall (m :: * -> *) a. Monad m => a -> m a
    return Clause' SpineLHS
    result

        buildRHS :: [ProblemEq] -> RHS -> TCMT IO RHS
    buildRHS [ProblemEq]
    _ rhs :: RHS
    rhs@A.RHS{}                 = RHS -> TCMT IO RHS
    forall (m :: * -> *) a. Monad m => a -> m a
    return RHS
    rhs
        buildRHS [ProblemEq]
    _ rhs :: RHS
    rhs@RHS
    A.AbsurdRHS             = RHS -> TCMT IO RHS
    forall (m :: * -> *) a. Monad m => a -> m a
    return RHS
    rhs
        buildRHS [ProblemEq]
    _ (A.WithRHS QName
    q [WithExpr]
    es [Clause]
    cs)         = QName -> [WithExpr] -> [Clause] -> RHS
    A.WithRHS QName
    q [WithExpr]
    es ([Clause] -> RHS) -> TCMT IO [Clause] -> TCMT IO RHS
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$>
          (Clause -> TCMT IO Clause) -> [Clause] -> TCMT IO [Clause]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t 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) [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 Bool
    catchall) =
          SpineLHS
    -> [ProblemEq]
    -> RHS
    -> WhereDeclarations
    -> Bool
    -> Clause' SpineLHS
    forall lhs.
    lhs
    -> [ProblemEq] -> RHS -> WhereDeclarations -> Bool -> 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 Bool
    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' Expr)]
    -> TCM ([ProblemEq], [NamedArg (Pattern' Expr)])
    stripWithClausePatterns [Name]
    cxtNames QName
    parent QName
    f Type
    t Telescope
    delta [NamedArg DeBruijnPattern]
    qs Int
    npars Permutation
    perm [NamedArg (Pattern' Expr)]
    ps = do
      -- Andreas, 2014-03-05 expand away pattern synoyms (issue 1074)
      [NamedArg (Pattern' Expr)]
    ps <- [NamedArg (Pattern' Expr)] -> TCM [NamedArg (Pattern' Expr)]
    forall a. ExpandPatternSynonyms a => a -> TCM a
    expandPatternSynonyms [NamedArg (Pattern' Expr)]
    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 -> DeBruijnPattern -> Pattern' Expr
    paramPat Int
    i DeBruijnPattern
    _ = BindName -> Pattern' Expr
    forall e. BindName -> Pattern' e
    A.VarP (BindName -> Pattern' Expr) -> BindName -> Pattern' Expr
    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' :: [NamedArg (Pattern' Expr)]
    ps' = (Int -> NamedArg DeBruijnPattern -> NamedArg (Pattern' Expr))
    -> [Int]
    -> [NamedArg DeBruijnPattern]
    -> [NamedArg (Pattern' Expr)]
    forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
    zipWith ((Named NamedName DeBruijnPattern
     -> Named NamedName (Pattern' Expr))
    -> NamedArg DeBruijnPattern -> NamedArg (Pattern' Expr)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap ((Named NamedName DeBruijnPattern
      -> Named NamedName (Pattern' Expr))
     -> NamedArg DeBruijnPattern -> NamedArg (Pattern' Expr))
    -> (Int
        -> Named NamedName DeBruijnPattern
        -> Named NamedName (Pattern' Expr))
    -> Int
    -> NamedArg DeBruijnPattern
    -> NamedArg (Pattern' Expr)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (DeBruijnPattern -> Pattern' Expr)
    -> Named NamedName DeBruijnPattern
    -> Named NamedName (Pattern' Expr)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap ((DeBruijnPattern -> Pattern' Expr)
     -> Named NamedName DeBruijnPattern
     -> Named NamedName (Pattern' Expr))
    -> (Int -> DeBruijnPattern -> Pattern' Expr)
    -> Int
    -> Named NamedName DeBruijnPattern
    -> Named NamedName (Pattern' Expr)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Int -> DeBruijnPattern -> Pattern' Expr
    paramPat) [Int
    0..] (Int -> [NamedArg DeBruijnPattern] -> [NamedArg DeBruijnPattern]
    forall a. Int -> [a] -> [a]
    take Int
    npars [NamedArg DeBruijnPattern]
    qs) [NamedArg (Pattern' Expr)]
    -> [NamedArg (Pattern' Expr)] -> [NamedArg (Pattern' Expr)]
    forall a. [a] -> [a] -> [a]
    ++ [NamedArg (Pattern' Expr)]
    ps
      [NamedArg (Pattern' Expr)]
    psi <- ExpandHidden
    -> [NamedArg (Pattern' Expr)]
    -> Type
    -> TCM [NamedArg (Pattern' Expr)]
    forall (m :: * -> *).
    (PureTCM m, MonadError TCErr m, MonadFresh NameId m,
     MonadTrace m) =>
    ExpandHidden
    -> [NamedArg (Pattern' Expr)]
    -> Type
    -> m [NamedArg (Pattern' Expr)]
    insertImplicitPatternsT ExpandHidden
    ExpandLast [NamedArg (Pattern' Expr)]
    ps' Type
    t
      [Char] -> Int -> TCMT IO Doc -> TCMT IO ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "tc.with.strip" Int
    10 (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
    "stripping 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
    "t   = " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Type -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Type
    t
        , 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
    "ps  = " 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 (Pattern' Expr) -> TCMT IO Doc)
    -> [NamedArg (Pattern' Expr)] -> [TCMT IO Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map NamedArg (Pattern' Expr) -> TCMT IO Doc
    forall a (m :: * -> *).
    (ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
    a -> m Doc
    prettyA [NamedArg (Pattern' Expr)]
    ps)
        , 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
    "ps' = " 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 (Pattern' Expr) -> TCMT IO Doc)
    -> [NamedArg (Pattern' Expr)] -> [TCMT IO Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map NamedArg (Pattern' Expr) -> TCMT IO Doc
    forall a (m :: * -> *).
    (ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
    a -> m Doc
    prettyA [NamedArg (Pattern' Expr)]
    ps')
        , 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
    "psi = " 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 (Pattern' Expr) -> TCMT IO Doc)
    -> [NamedArg (Pattern' Expr)] -> [TCMT IO Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map NamedArg (Pattern' Expr) -> TCMT IO Doc
    forall a (m :: * -> *).
    (ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
    a -> m Doc
    prettyA [NamedArg (Pattern' Expr)]
    psi)
        , 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
    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
    "perm= " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> [Char] -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => [Char] -> m Doc
    text (Permutation -> [Char]
    forall a. Show a => a -> [Char]
    show Permutation
    perm)
        ]

      -- Andreas, 2015-11-09 Issue 1710: self starts with parent-function, not with-function!
      ([NamedArg (Pattern' Expr)]
    ps', [ProblemEq]
    strippedPats) <- WriterT [ProblemEq] (TCMT IO) [NamedArg (Pattern' Expr)]
    -> TCM ([NamedArg (Pattern' Expr)], [ProblemEq])
    forall w (m :: * -> *) a. WriterT w m a -> m (a, w)
    runWriterT (WriterT [ProblemEq] (TCMT IO) [NamedArg (Pattern' Expr)]
     -> TCM ([NamedArg (Pattern' Expr)], [ProblemEq]))
    -> WriterT [ProblemEq] (TCMT IO) [NamedArg (Pattern' Expr)]
    -> TCM ([NamedArg (Pattern' Expr)], [ProblemEq])
    forall a b. (a -> b) -> a -> b
    $ Term
    -> Type
    -> [NamedArg (Pattern' Expr)]
    -> [NamedArg DeBruijnPattern]
    -> WriterT [ProblemEq] (TCMT IO) [NamedArg (Pattern' Expr)]
    strip (QName -> Elims -> Term
    Def QName
    parent []) Type
    t [NamedArg (Pattern' Expr)]
    psi [NamedArg DeBruijnPattern]
    qs
      [Char] -> Int -> TCMT IO Doc -> TCMT IO ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "tc.with.strip" Int
    50 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $ Int -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
    nest Int
    2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $
        TCMT IO Doc
    "strippedPats:" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> [TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    vcat [ Pattern' Expr -> TCMT IO Doc
    forall a (m :: * -> *).
    (ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
    a -> m Doc
    prettyA Pattern' Expr
    p TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> TCMT IO Doc
    "=" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Term -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Term
    v TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> TCMT IO Doc
    ":" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Dom Type -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Dom Type
    a | A.ProblemEq Pattern' Expr
    p Term
    v Dom Type
    a <- [ProblemEq]
    strippedPats ]
      let psp :: [NamedArg (Pattern' Expr)]
    psp = Permutation
    -> [NamedArg (Pattern' Expr)] -> [NamedArg (Pattern' Expr)]
    forall a. Permutation -> [a] -> [a]
    permute Permutation
    perm [NamedArg (Pattern' Expr)]
    ps'
      [Char] -> Int -> TCMT IO Doc -> TCMT IO ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "tc.with.strip" Int
    10 (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
        [ 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
    "ps' = " 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 (Pattern' Expr) -> TCMT IO Doc)
    -> [NamedArg (Pattern' Expr)] -> [TCMT IO Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map NamedArg (Pattern' Expr) -> TCMT IO Doc
    forall a (m :: * -> *).
    (ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
    a -> m Doc
    prettyA [NamedArg (Pattern' Expr)]
    ps')
        , 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
    "psp = " 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 (Pattern' Expr) -> TCMT IO Doc)
    -> [NamedArg (Pattern' Expr)] -> [TCMT IO Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map NamedArg (Pattern' Expr) -> TCMT IO Doc
    forall a (m :: * -> *).
    (ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
    a -> m Doc
    prettyA ([NamedArg (Pattern' Expr)] -> [TCMT IO Doc])
    -> [NamedArg (Pattern' Expr)] -> [TCMT IO Doc]
    forall a b. (a -> b) -> a -> b
    $ [NamedArg (Pattern' Expr)]
    psp)
        ]
      ([ProblemEq], [NamedArg (Pattern' Expr)])
    -> TCM ([ProblemEq], [NamedArg (Pattern' Expr)])
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([ProblemEq]
    strippedPats, [NamedArg (Pattern' Expr)]
    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 (t :: * -> *) a. Foldable t => t a -> Int
    length [ArgInfo]
    infos then [ArgInfo]
    infos [ArgInfo] -> Int -> ArgInfo
    forall a. [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' Expr) -> NamedArg (Pattern' Expr)
    setVarArgInfo DBPatVar
    x NamedArg (Pattern' Expr)
    p = Origin -> NamedArg (Pattern' Expr) -> NamedArg (Pattern' Expr)
    forall a. LensOrigin a => Origin -> a -> a
    setOrigin (NamedArg (Pattern' Expr) -> Origin
    forall a. LensOrigin a => a -> Origin
    getOrigin NamedArg (Pattern' Expr)
    p) (NamedArg (Pattern' Expr) -> NamedArg (Pattern' Expr))
    -> NamedArg (Pattern' Expr) -> NamedArg (Pattern' Expr)
    forall a b. (a -> b) -> a -> b
    $ ArgInfo -> NamedArg (Pattern' Expr) -> NamedArg (Pattern' Expr)
    forall a. LensArgInfo a => ArgInfo -> a -> a
    setArgInfo (DBPatVar -> ArgInfo
    varArgInfo DBPatVar
    x) NamedArg (Pattern' Expr)
    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' Expr)]
    -> [NamedArg DeBruijnPattern]
    -> WriterT [ProblemEq] (TCMT IO) [NamedArg (Pattern' Expr)]
    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
    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
    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
    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.
          [NamedArg (Pattern' Expr)]
    ps <- TCM [NamedArg (Pattern' Expr)]
    -> WriterT [ProblemEq] (TCMT IO) [NamedArg (Pattern' Expr)]
    forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
    liftTCM (TCM [NamedArg (Pattern' Expr)]
     -> WriterT [ProblemEq] (TCMT IO) [NamedArg (Pattern' Expr)])
    -> TCM [NamedArg (Pattern' Expr)]
    -> WriterT [ProblemEq] (TCMT IO) [NamedArg (Pattern' Expr)]
    forall a b. (a -> b) -> a -> b
    $ ExpandHidden
    -> [NamedArg (Pattern' Expr)]
    -> Type
    -> TCM [NamedArg (Pattern' Expr)]
    forall (m :: * -> *).
    (PureTCM m, MonadError TCErr m, MonadFresh NameId m,
     MonadTrace m) =>
    ExpandHidden
    -> [NamedArg (Pattern' Expr)]
    -> Type
    -> m [NamedArg (Pattern' Expr)]
    insertImplicitPatternsT ExpandHidden
    ExpandLast [] Type
    t
          if [NamedArg (Pattern' Expr)] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null [NamedArg (Pattern' Expr)]
    ps then
            TypeError
    -> WriterT [ProblemEq] (TCMT IO) [NamedArg (Pattern' Expr)]
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    TypeError -> m a
    typeError (TypeError
     -> WriterT [ProblemEq] (TCMT IO) [NamedArg (Pattern' Expr)])
    -> TypeError
    -> WriterT [ProblemEq] (TCMT IO) [NamedArg (Pattern' Expr)]
    forall a b. (a -> b) -> a -> b
    $ [Char] -> TypeError
    GenericError ([Char] -> TypeError) -> [Char] -> TypeError
    forall a b. (a -> b) -> a -> b
    $ [Char]
    "Too few arguments given in with-clause"
           else Term
    -> Type
    -> [NamedArg (Pattern' Expr)]
    -> [NamedArg DeBruijnPattern]
    -> WriterT [ProblemEq] (TCMT IO) [NamedArg (Pattern' Expr)]
    strip Term
    self Type
    t [NamedArg (Pattern' Expr)]
    ps [NamedArg DeBruijnPattern]
    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' Expr)]
    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 (f :: * -> *). Applicative f => Bool -> f () -> f ()
    unless ((NamedArg (Pattern' Expr) -> Bool)
    -> [NamedArg (Pattern' Expr)] -> Bool
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
    all (Pattern' Expr -> Bool
    forall {e}. Pattern' e -> Bool
    implicit (Pattern' Expr -> Bool)
    -> (NamedArg (Pattern' Expr) -> Pattern' Expr)
    -> NamedArg (Pattern' Expr)
    -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . NamedArg (Pattern' Expr) -> Pattern' Expr
    forall a. NamedArg a -> a
    namedArg) [NamedArg (Pattern' Expr)]
    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 -> WriterT [ProblemEq] (TCMT IO) ())
    -> TypeError -> WriterT [ProblemEq] (TCMT IO) ()
    forall a b. (a -> b) -> a -> b
    $ [Char] -> TypeError
    GenericError ([Char] -> TypeError) -> [Char] -> TypeError
    forall a b. (a -> b) -> a -> b
    $ [Char]
    "Too many arguments given in with-clause"
          [NamedArg (Pattern' Expr)]
    -> WriterT [ProblemEq] (TCMT IO) [NamedArg (Pattern' Expr)]
    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' Expr)
    p0 : [NamedArg (Pattern' Expr)]
    ps) qs :: [NamedArg DeBruijnPattern]
    qs@(NamedArg DeBruijnPattern
    q : [NamedArg DeBruijnPattern]
    _)
          | A.AsP PatInfo
    _ BindName
    x Pattern' Expr
    p <- NamedArg (Pattern' Expr) -> Pattern' Expr
    forall a. NamedArg a -> a
    namedArg NamedArg (Pattern' Expr)
    p0 = do
            (Dom Type
    a, Abs Type
    _) <- Type -> WriterT [ProblemEq] (TCMT IO) (Dom Type, Abs Type)
    forall (m :: * -> *).
    MonadReduce m =>
    Type -> m (Dom Type, Abs Type)
    mustBePi Type
    t
            let v :: Term
    v = DeBruijnPattern -> Term
    patternToTerm (NamedArg DeBruijnPattern -> DeBruijnPattern
    forall a. NamedArg a -> a
    namedArg NamedArg DeBruijnPattern
    q)
            [ProblemEq] -> WriterT [ProblemEq] (TCMT IO) ()
    forall w (m :: * -> *). MonadWriter w m => w -> m ()
    tell [Pattern' Expr -> Term -> Dom Type -> ProblemEq
    ProblemEq (BindName -> Pattern' Expr
    forall e. BindName -> Pattern' e
    A.VarP BindName
    x) Term
    v Dom Type
    a]
            Term
    -> Type
    -> [NamedArg (Pattern' Expr)]
    -> [NamedArg DeBruijnPattern]
    -> WriterT [ProblemEq] (TCMT IO) [NamedArg (Pattern' Expr)]
    strip Term
    self Type
    t ((Named NamedName (Pattern' Expr)
     -> Named NamedName (Pattern' Expr))
    -> NamedArg (Pattern' Expr) -> NamedArg (Pattern' Expr)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (Pattern' Expr
    p Pattern' Expr
    -> Named NamedName (Pattern' Expr)
    -> Named NamedName (Pattern' Expr)
    forall (f :: * -> *) a b. Functor f => a -> f b -> f a
    <$) NamedArg (Pattern' Expr)
    p0 NamedArg (Pattern' Expr)
    -> [NamedArg (Pattern' Expr)] -> [NamedArg (Pattern' Expr)]
    forall a. a -> [a] -> [a]
    : [NamedArg (Pattern' Expr)]
    ps) [NamedArg DeBruijnPattern]
    qs
        strip Term
    self Type
    t ps0 :: [NamedArg (Pattern' Expr)]
    ps0@(NamedArg (Pattern' Expr)
    p0 : [NamedArg (Pattern' Expr)]
    ps) qs0 :: [NamedArg DeBruijnPattern]
    qs0@(NamedArg DeBruijnPattern
    q : [NamedArg DeBruijnPattern]
    qs) = do
          NamedArg (Pattern' Expr)
    p <- TCM (NamedArg (Pattern' Expr))
    -> WriterT [ProblemEq] (TCMT IO) (NamedArg (Pattern' Expr))
    forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
    liftTCM (TCM (NamedArg (Pattern' Expr))
     -> WriterT [ProblemEq] (TCMT IO) (NamedArg (Pattern' Expr)))
    -> TCM (NamedArg (Pattern' Expr))
    -> WriterT [ProblemEq] (TCMT IO) (NamedArg (Pattern' Expr))
    forall a b. (a -> b) -> a -> b
    $ ((Named NamedName (Pattern' Expr)
     -> TCMT IO (Named NamedName (Pattern' Expr)))
    -> NamedArg (Pattern' Expr) -> TCM (NamedArg (Pattern' Expr))
    forall (t :: * -> *) (f :: * -> *) a b.
    (Traversable t, Applicative f) =>
    (a -> f b) -> t a -> f (t b)
    traverse ((Named NamedName (Pattern' Expr)
      -> TCMT IO (Named NamedName (Pattern' Expr)))
     -> NamedArg (Pattern' Expr) -> TCM (NamedArg (Pattern' Expr)))
    -> ((Pattern' Expr -> TCMT IO (Pattern' Expr))
        -> Named NamedName (Pattern' Expr)
        -> TCMT IO (Named NamedName (Pattern' Expr)))
    -> (Pattern' Expr -> TCMT IO (Pattern' Expr))
    -> NamedArg (Pattern' Expr)
    -> TCM (NamedArg (Pattern' Expr))
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Pattern' Expr -> TCMT IO (Pattern' Expr))
    -> Named NamedName (Pattern' Expr)
    -> TCMT IO (Named NamedName (Pattern' Expr))
    forall (t :: * -> *) (f :: * -> *) a b.
    (Traversable t, Applicative f) =>
    (a -> f b) -> t a -> f (t b)
    traverse) Pattern' Expr -> TCMT IO (Pattern' Expr)
    forall (m :: * -> *).
    (MonadError TCErr m, MonadTCEnv m, ReadTCState m, HasBuiltins m) =>
    Pattern' Expr -> m (Pattern' Expr)
    expandLitPattern NamedArg (Pattern' Expr)
    p0
          [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"
            , 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
    "ps0 =" 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 (Pattern' Expr) -> TCMT IO Doc)
    -> [NamedArg (Pattern' Expr)] -> [TCMT IO Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map NamedArg (Pattern' Expr) -> TCMT IO Doc
    forall a (m :: * -> *).
    (ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
    a -> m Doc
    prettyA [NamedArg (Pattern' Expr)]
    ps0)
            , 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
    "exp =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> NamedArg (Pattern' Expr) -> TCMT IO Doc
    forall a (m :: * -> *).
    (ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
    a -> m Doc
    prettyA NamedArg (Pattern' Expr)
    p
            , 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
    "qs0 =" 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
    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]
    qs0)
            , 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
    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
    prettyTCM Type
    t
            ]
          case NamedArg DeBruijnPattern -> DeBruijnPattern
    forall a. NamedArg a -> a
    namedArg NamedArg DeBruijnPattern
    q of
            ProjP ProjOrigin
    o QName
    d -> case NamedArg (Pattern' Expr) -> Maybe (ProjOrigin, AmbiguousQName)
    forall a. IsProjP a => a -> Maybe (ProjOrigin, AmbiguousQName)
    A.isProjP NamedArg (Pattern' Expr)
    p of
              Just (ProjOrigin
    o', AmbQ List1 QName
    ds) -> do
                -- We assume here that neither @o@ nor @o'@ can be @ProjSystem@.
                if ProjOrigin
    o ProjOrigin -> ProjOrigin -> Bool
    forall a. Eq a => a -> a -> Bool
    /= ProjOrigin
    o' then TCM [NamedArg (Pattern' Expr)]
    -> WriterT [ProblemEq] (TCMT IO) [NamedArg (Pattern' Expr)]
    forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
    liftTCM (TCM [NamedArg (Pattern' Expr)]
     -> WriterT [ProblemEq] (TCMT IO) [NamedArg (Pattern' Expr)])
    -> TCM [NamedArg (Pattern' Expr)]
    -> WriterT [ProblemEq] (TCMT IO) [NamedArg (Pattern' Expr)]
    forall a b. (a -> b) -> a -> b
    $ ProjOrigin -> ProjOrigin -> TCM [NamedArg (Pattern' Expr)]
    mismatchOrigin ProjOrigin
    o ProjOrigin
    o' else do
                -- Andreas, 2016-12-28, issue #2360:
                -- We disambiguate the projection in the with clause
                -- to the projection in the parent clause.
                QName
    d  <- TCM QName -> WriterT [ProblemEq] (TCMT IO) QName
    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
                Bool
    found <- List1 QName
    -> (QName -> WriterT [ProblemEq] (TCMT IO) Bool)
    -> WriterT [ProblemEq] (TCMT IO) Bool
    forall (f :: * -> *) (m :: * -> *) a.
    (Functor f, Foldable f, Monad m) =>
    f a -> (a -> m Bool) -> m Bool
    anyM List1 QName
    ds ((QName -> WriterT [ProblemEq] (TCMT IO) Bool)
     -> WriterT [ProblemEq] (TCMT IO) Bool)
    -> (QName -> WriterT [ProblemEq] (TCMT IO) Bool)
    -> WriterT [ProblemEq] (TCMT IO) Bool
    forall a b. (a -> b) -> a -> b
    $ \ QName
    d' -> TCM Bool -> WriterT [ProblemEq] (TCMT IO) Bool
    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 (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 Bool -> Bool
    not Bool
    found then WriterT [ProblemEq] (TCMT IO) [NamedArg (Pattern' Expr)]
    forall (m :: * -> *) a. (MonadAddContext m, MonadTCError m) => m a
    mismatch else do
                  (Term
    self1, Type
    t1, [NamedArg (Pattern' Expr)]
    ps) <- TCM (Term, Type, [NamedArg (Pattern' Expr)])
    -> WriterT
         [ProblemEq] (TCMT IO) (Term, Type, [NamedArg (Pattern' Expr)])
    forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
    liftTCM (TCM (Term, Type, [NamedArg (Pattern' Expr)])
     -> WriterT
          [ProblemEq] (TCMT IO) (Term, Type, [NamedArg (Pattern' Expr)]))
    -> TCM (Term, Type, [NamedArg (Pattern' Expr)])
    -> WriterT
         [ProblemEq] (TCMT IO) (Term, Type, [NamedArg (Pattern' Expr)])
    forall a b. (a -> b) -> a -> b
    $ do
                    Type
    t <- Type -> TCM Type
    forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
    reduce Type
    t
                    (Dom Type
    _, Term
    self1, Type
    t1) <- (Dom Type, Term, Type)
    -> Maybe (Dom Type, Term, Type) -> (Dom Type, Term, Type)
    forall a. a -> Maybe a -> a
    fromMaybe (Dom Type, Term, Type)
    forall a. HasCallStack => a
    __IMPOSSIBLE__ (Maybe (Dom Type, Term, Type) -> (Dom Type, Term, Type))
    -> TCMT IO (Maybe (Dom Type, Term, Type))
    -> TCMT IO (Dom Type, Term, Type)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Term
    -> Type
    -> ProjOrigin
    -> QName
    -> TCMT IO (Maybe (Dom Type, Term, Type))
    forall (m :: * -> *).
    PureTCM m =>
    Term
    -> Type -> ProjOrigin -> QName -> m (Maybe (Dom Type, Term, Type))
    projectTyped Term
    self Type
    t ProjOrigin
    o QName
    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.
                    [NamedArg (Pattern' Expr)]
    ps <- ExpandHidden
    -> [NamedArg (Pattern' Expr)]
    -> Type
    -> TCM [NamedArg (Pattern' Expr)]
    forall (m :: * -> *).
    (PureTCM m, MonadError TCErr m, MonadFresh NameId m,
     MonadTrace m) =>
    ExpandHidden
    -> [NamedArg (Pattern' Expr)]
    -> Type
    -> m [NamedArg (Pattern' Expr)]
    insertImplicitPatternsT ExpandHidden
    ExpandLast [NamedArg (Pattern' Expr)]
    ps Type
    t1
                    (Term, Type, [NamedArg (Pattern' Expr)])
    -> TCM (Term, Type, [NamedArg (Pattern' Expr)])
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Term
    self1, Type
    t1, [NamedArg (Pattern' Expr)]
    ps)
                  Term
    -> Type
    -> [NamedArg (Pattern' Expr)]
    -> [NamedArg DeBruijnPattern]
    -> WriterT [ProblemEq] (TCMT IO) [NamedArg (Pattern' Expr)]
    strip Term
    self1 Type
    t1 [NamedArg (Pattern' Expr)]
    ps [NamedArg DeBruijnPattern]
    qs
              Maybe (ProjOrigin, AmbiguousQName)
    Nothing -> WriterT [ProblemEq] (TCMT IO) [NamedArg (Pattern' Expr)]
    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' Expr) -> Pattern' Expr
    forall a. NamedArg a -> a
    namedArg NamedArg (Pattern' Expr)
    p
                     , A.Var Name
    y <- Expr -> Expr
    unScope Expr
    u -> do
              (DBPatVar -> NamedArg (Pattern' Expr) -> NamedArg (Pattern' Expr)
    setVarArgInfo DBPatVar
    x (NamedArg (Pattern' Expr)
    -> Pattern' Expr -> NamedArg (Pattern' Expr)
    forall a b. NamedArg a -> b -> NamedArg b
    setNamedArg NamedArg (Pattern' Expr)
    p (Pattern' Expr -> NamedArg (Pattern' Expr))
    -> Pattern' Expr -> NamedArg (Pattern' Expr)
    forall a b. (a -> b) -> a -> b
    $ BindName -> Pattern' Expr
    forall e. BindName -> Pattern' e
    A.VarP (BindName -> Pattern' Expr) -> BindName -> Pattern' Expr
    forall a b. (a -> b) -> a -> b
    $ Name -> BindName
    A.mkBindName Name
    y) NamedArg (Pattern' Expr)
    -> [NamedArg (Pattern' Expr)] -> [NamedArg (Pattern' Expr)]
    forall a. a -> [a] -> [a]
    :) ([NamedArg (Pattern' Expr)] -> [NamedArg (Pattern' Expr)])
    -> WriterT [ProblemEq] (TCMT IO) [NamedArg (Pattern' Expr)]
    -> WriterT [ProblemEq] (TCMT IO) [NamedArg (Pattern' Expr)]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$>
                Term -> WriterT [ProblemEq] (TCMT IO) [NamedArg (Pattern' Expr)]
    recurse (Int -> Term
    var (DBPatVar -> Int
    dbPatVarIndex DBPatVar
    x))

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

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

            DefP{}  -> TypeError
    -> WriterT [ProblemEq] (TCMT IO) [NamedArg (Pattern' Expr)]
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    TypeError -> m a
    typeError (TypeError
     -> WriterT [ProblemEq] (TCMT IO) [NamedArg (Pattern' Expr)])
    -> TypeError
    -> WriterT [ProblemEq] (TCMT IO) [NamedArg (Pattern' Expr)]
    forall a b. (a -> b) -> a -> b
    $ [Char] -> TypeError
    GenericError ([Char] -> TypeError) -> [Char] -> TypeError
    forall a b. (a -> b) -> a -> b
    $ [Char]
    "with clauses not supported in the presence of hcomp patterns" -- TODO this should actually be impossible

            DotP PatternInfo
    i Term
    v  -> do
              (Dom Type
    a, Abs Type
    _) <- Type -> WriterT [ProblemEq] (TCMT IO) (Dom Type, Abs Type)
    forall (m :: * -> *).
    MonadReduce m =>
    Type -> m (Dom Type, Abs Type)
    mustBePi Type
    t
              [ProblemEq] -> WriterT [ProblemEq] (TCMT IO) ()
    forall w (m :: * -> *). MonadWriter w m => w -> m ()
    tell [Pattern' Expr -> Term -> Dom Type -> ProblemEq
    ProblemEq (NamedArg (Pattern' Expr) -> Pattern' Expr
    forall a. NamedArg a -> a
    namedArg NamedArg (Pattern' Expr)
    p) Term
    v Dom Type
    a]
              case Term
    v of
                Var Int
    x [] | PatOVar{} <- PatternInfo -> PatOrigin
    patOrigin PatternInfo
    i
                   -> (NamedArg (Pattern' Expr)
    p NamedArg (Pattern' Expr)
    -> [NamedArg (Pattern' Expr)] -> [NamedArg (Pattern' Expr)]
    forall a. a -> [a] -> [a]
    :) ([NamedArg (Pattern' Expr)] -> [NamedArg (Pattern' Expr)])
    -> WriterT [ProblemEq] (TCMT IO) [NamedArg (Pattern' Expr)]
    -> WriterT [ProblemEq] (TCMT IO) [NamedArg (Pattern' Expr)]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Term -> WriterT [ProblemEq] (TCMT IO) [NamedArg (Pattern' Expr)]
    recurse (Int -> Term
    var Int
    x)
                Term
    _  -> (NamedArg (Pattern' Expr) -> NamedArg (Pattern' Expr)
    makeWildP NamedArg (Pattern' Expr)
    p NamedArg (Pattern' Expr)
    -> [NamedArg (Pattern' Expr)] -> [NamedArg (Pattern' Expr)]
    forall a. a -> [a] -> [a]
    :) ([NamedArg (Pattern' Expr)] -> [NamedArg (Pattern' Expr)])
    -> WriterT [ProblemEq] (TCMT IO) [NamedArg (Pattern' Expr)]
    -> WriterT [ProblemEq] (TCMT IO) [NamedArg (Pattern' Expr)]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Term -> WriterT [ProblemEq] (TCMT IO) [NamedArg (Pattern' Expr)]
    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
    prettyTCM ConHead
    c
             (Dom Type
    a, Abs Type
    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 QName
    d Elims
    es <- TCM Term -> WriterT [ProblemEq] (TCMT IO) Term
    forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
    liftTCM (TCM Term -> WriterT [ProblemEq] (TCMT IO) Term)
    -> TCM Term -> WriterT [ProblemEq] (TCMT IO) Term
    forall a b. (a -> b) -> a -> b
    $ Term -> TCM Term
    forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
    reduce (Type -> Term
    forall t a. Type'' t a -> a
    unEl (Type -> Term) -> Type -> Term
    forall a b. (a -> b) -> a -> b
    $ Dom Type -> Type
    forall t e. Dom' t e -> e
    unDom Dom Type
    a)
             let us :: Args
    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.
             ConHead
    c <- (SigError -> ConHead)
    -> (ConHead -> ConHead) -> Either SigError ConHead -> ConHead
    forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
    either SigError -> ConHead
    forall a. HasCallStack => a
    __IMPOSSIBLE__ (ConHead -> ConHead -> ConHead
    forall t u. (SetRange t, HasRange u) => t -> u -> t
    `withRangeOf` ConHead
    c) (Either SigError ConHead -> ConHead)
    -> WriterT [ProblemEq] (TCMT IO) (Either SigError ConHead)
    -> WriterT [ProblemEq] (TCMT IO) ConHead
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> do TCM (Either SigError ConHead)
    -> WriterT [ProblemEq] (TCMT IO) (Either SigError ConHead)
    forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
    liftTCM (TCM (Either SigError ConHead)
     -> WriterT [ProblemEq] (TCMT IO) (Either SigError ConHead))
    -> TCM (Either SigError ConHead)
    -> WriterT [ProblemEq] (TCMT IO) (Either SigError ConHead)
    forall a b. (a -> b) -> a -> b
    $ QName -> TCM (Either SigError ConHead)
    getConForm (QName -> TCM (Either SigError ConHead))
    -> QName -> TCM (Either SigError ConHead)
    forall a b. (a -> b) -> a -> b
    $ ConHead -> QName
    conName ConHead
    c

             case NamedArg (Pattern' Expr) -> Pattern' Expr
    forall a. NamedArg a -> a
    namedArg NamedArg (Pattern' Expr)
    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' Expr -> Term -> Dom Type -> ProblemEq
    ProblemEq (PatInfo -> Expr -> Pattern' Expr
    forall e. PatInfo -> e -> Pattern' e
    A.DotP PatInfo
    r Expr
    e) (DeBruijnPattern -> Term
    patternToTerm DeBruijnPattern
    q') Dom Type
    a]
                [NamedArg (Pattern' Expr)]
    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
                      [ConHead]
    cs' <- TCM [ConHead] -> WriterT [ProblemEq] (TCMT IO) [ConHead]
    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)
    mapM QName -> TCM (Either SigError ConHead)
    getConForm List1 QName
    cs'
                      Bool
    -> WriterT [ProblemEq] (TCMT IO) ()
    -> WriterT [ProblemEq] (TCMT IO) ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    unless (ConHead
    c ConHead -> [ConHead] -> Bool
    forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
    `elem` [ConHead]
    cs') WriterT [ProblemEq] (TCMT IO) ()
    forall (m :: * -> *) a. (MonadAddContext m, MonadTCError m) => m a
    mismatch
                      [NamedArg (Pattern' Expr)]
    -> WriterT [ProblemEq] (TCMT IO) [NamedArg (Pattern' Expr)]
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([NamedArg (Pattern' Expr)]
     -> WriterT [ProblemEq] (TCMT IO) [NamedArg (Pattern' Expr)])
    -> [NamedArg (Pattern' Expr)]
    -> WriterT [ProblemEq] (TCMT IO) [NamedArg (Pattern' Expr)]
    forall a b. (a -> b) -> a -> b
    $ ((NamedArg Expr -> NamedArg (Pattern' Expr))
    -> [NamedArg Expr] -> [NamedArg (Pattern' Expr)]
    forall a b. (a -> b) -> [a] -> [b]
    map ((NamedArg Expr -> NamedArg (Pattern' Expr))
     -> [NamedArg Expr] -> [NamedArg (Pattern' Expr)])
    -> ((Expr -> Pattern' Expr)
        -> NamedArg Expr -> NamedArg (Pattern' Expr))
    -> (Expr -> Pattern' Expr)
    -> [NamedArg Expr]
    -> [NamedArg (Pattern' Expr)]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Named NamedName Expr -> Named NamedName (Pattern' Expr))
    -> NamedArg Expr -> NamedArg (Pattern' Expr)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap ((Named NamedName Expr -> Named NamedName (Pattern' Expr))
     -> NamedArg Expr -> NamedArg (Pattern' Expr))
    -> ((Expr -> Pattern' Expr)
        -> Named NamedName Expr -> Named NamedName (Pattern' Expr))
    -> (Expr -> Pattern' Expr)
    -> NamedArg Expr
    -> NamedArg (Pattern' Expr)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Expr -> Pattern' Expr)
    -> Named NamedName Expr -> Named NamedName (Pattern' Expr)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap) (PatInfo -> Expr -> Pattern' Expr
    forall e. PatInfo -> e -> Pattern' e
    A.DotP PatInfo
    r) [NamedArg Expr]
    es
                    AppView
    _  -> [NamedArg (Pattern' Expr)]
    -> WriterT [ProblemEq] (TCMT IO) [NamedArg (Pattern' Expr)]
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([NamedArg (Pattern' Expr)]
     -> WriterT [ProblemEq] (TCMT IO) [NamedArg (Pattern' Expr)])
    -> [NamedArg (Pattern' Expr)]
    -> WriterT [ProblemEq] (TCMT IO) [NamedArg (Pattern' Expr)]
    forall a b. (a -> b) -> a -> b
    $ (NamedArg DeBruijnPattern -> NamedArg (Pattern' Expr))
    -> [NamedArg DeBruijnPattern] -> [NamedArg (Pattern' Expr)]
    forall a b. (a -> b) -> [a] -> [b]
    map (Pattern' Expr -> Named NamedName (Pattern' Expr)
    forall a name. a -> Named name a
    unnamed (PatInfo -> Pattern' Expr
    forall e. PatInfo -> Pattern' e
    A.WildP PatInfo
    forall a. Null a => a
    empty) Named NamedName (Pattern' Expr)
    -> NamedArg DeBruijnPattern -> NamedArg (Pattern' Expr)
    forall (f :: * -> *) a b. Functor f => a -> f b -> f a
    <$) [NamedArg DeBruijnPattern]
    qs'
                QName
    -> Args
    -> Abs Type
    -> ConHead
    -> ConOrigin
    -> [NamedArg DeBruijnPattern]
    -> [NamedArg (Pattern' Expr)]
    -> WriterT [ProblemEq] (TCMT IO) [NamedArg (Pattern' Expr)]
    stripConP QName
    d Args
    us Abs Type
    b ConHead
    c ConOrigin
    ConOCon [NamedArg DeBruijnPattern]
    qs' [NamedArg (Pattern' Expr)]
    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' Expr)]
    ps' = (NamedArg DeBruijnPattern -> NamedArg (Pattern' Expr))
    -> [NamedArg DeBruijnPattern] -> [NamedArg (Pattern' Expr)]
    forall a b. (a -> b) -> [a] -> [b]
    map (Pattern' Expr -> Named NamedName (Pattern' Expr)
    forall a name. a -> Named name a
    unnamed (PatInfo -> Pattern' Expr
    forall e. PatInfo -> Pattern' e
    A.WildP PatInfo
    forall a. Null a => a
    empty) Named NamedName (Pattern' Expr)
    -> NamedArg DeBruijnPattern -> NamedArg (Pattern' Expr)
    forall (f :: * -> *) a b. Functor f => a -> f b -> f a
    <$) [NamedArg DeBruijnPattern]
    qs'
                QName
    -> Args
    -> Abs Type
    -> ConHead
    -> ConOrigin
    -> [NamedArg DeBruijnPattern]
    -> [NamedArg (Pattern' Expr)]
    -> WriterT [ProblemEq] (TCMT IO) [NamedArg (Pattern' Expr)]
    stripConP QName
    d Args
    us Abs Type
    b ConHead
    c ConOrigin
    ConOCon [NamedArg DeBruijnPattern]
    qs' [NamedArg (Pattern' Expr)]
    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' Expr -> Term -> Dom Type -> ProblemEq
    ProblemEq (BindName -> Pattern' Expr
    forall e. BindName -> Pattern' e
    A.VarP BindName
    x) (DeBruijnPattern -> Term
    patternToTerm DeBruijnPattern
    q') Dom Type
    a]
                let ps' :: [NamedArg (Pattern' Expr)]
    ps' = (NamedArg DeBruijnPattern -> NamedArg (Pattern' Expr))
    -> [NamedArg DeBruijnPattern] -> [NamedArg (Pattern' Expr)]
    forall a b. (a -> b) -> [a] -> [b]
    map (Pattern' Expr -> Named NamedName (Pattern' Expr)
    forall a name. a -> Named name a
    unnamed (PatInfo -> Pattern' Expr
    forall e. PatInfo -> Pattern' e
    A.WildP PatInfo
    forall a. Null a => a
    empty) Named NamedName (Pattern' Expr)
    -> NamedArg DeBruijnPattern -> NamedArg (Pattern' Expr)
    forall (f :: * -> *) a b. Functor f => a -> f b -> f a
    <$) [NamedArg DeBruijnPattern]
    qs'
                QName
    -> Args
    -> Abs Type
    -> ConHead
    -> ConOrigin
    -> [NamedArg DeBruijnPattern]
    -> [NamedArg (Pattern' Expr)]
    -> WriterT [ProblemEq] (TCMT IO) [NamedArg (Pattern' Expr)]
    stripConP QName
    d Args
    us Abs Type
    b ConHead
    c ConOrigin
    ConOCon [NamedArg DeBruijnPattern]
    qs' [NamedArg (Pattern' Expr)]
    ps'

              A.ConP ConPatInfo
    _ (A.AmbQ List1 QName
    cs') [NamedArg (Pattern' Expr)]
    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.
                [ConHead]
    cs' <- TCM [ConHead] -> WriterT [ProblemEq] (TCMT IO) [ConHead]
    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)
    mapM QName -> TCM (Either SigError ConHead)
    getConForm List1 QName
    cs'
                Bool
    -> WriterT [ProblemEq] (TCMT IO) ()
    -> WriterT [ProblemEq] (TCMT IO) ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    unless (ConHead
    c ConHead -> [ConHead] -> Bool
    forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
    `elem` [ConHead]
    cs') WriterT [ProblemEq] (TCMT IO) ()
    forall (m :: * -> *) a. (MonadAddContext m, MonadTCError m) => m a
    mismatch
                -- Strip the subpatterns ps' and then continue.
                QName
    -> Args
    -> Abs Type
    -> ConHead
    -> ConOrigin
    -> [NamedArg DeBruijnPattern]
    -> [NamedArg (Pattern' Expr)]
    -> WriterT [ProblemEq] (TCMT IO) [NamedArg (Pattern' Expr)]
    stripConP QName
    d Args
    us Abs Type
    b ConHead
    c ConOrigin
    ConOCon [NamedArg DeBruijnPattern]
    qs' [NamedArg (Pattern' Expr)]
    ps'

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

              p :: Pattern' Expr
    p@(A.PatternSynP PatInfo
    pi' AmbiguousQName
    c' [NamedArg (Pattern' Expr)]
    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' Expr -> TCMT IO Doc
    forall a (m :: * -> *).
    (ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
    a -> m Doc
    prettyA Pattern' Expr
    p
                 WriterT [ProblemEq] (TCMT IO) [NamedArg (Pattern' Expr)]
    forall a. HasCallStack => a
    __IMPOSSIBLE__

              Pattern' Expr
    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' Expr -> [Char]
    forall a. Show a => a -> [Char]
    show Pattern' Expr
    p
               WriterT [ProblemEq] (TCMT IO) [NamedArg (Pattern' Expr)]
    forall (m :: * -> *) a. (MonadAddContext m, MonadTCError m) => m a
    mismatch

            LitP PatternInfo
    _ Literal
    lit -> case NamedArg (Pattern' Expr) -> Pattern' Expr
    forall a. NamedArg a -> a
    namedArg NamedArg (Pattern' Expr)
    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' Expr)]
    recurse (Term -> WriterT [ProblemEq] (TCMT IO) [NamedArg (Pattern' Expr)])
    -> Term -> WriterT [ProblemEq] (TCMT IO) [NamedArg (Pattern' Expr)]
    forall a b. (a -> b) -> a -> b
    $ Literal -> Term
    Lit Literal
    lit
              A.WildP{}                   -> Term -> WriterT [ProblemEq] (TCMT IO) [NamedArg (Pattern' Expr)]
    recurse (Term -> WriterT [ProblemEq] (TCMT IO) [NamedArg (Pattern' Expr)])
    -> Term -> WriterT [ProblemEq] (TCMT IO) [NamedArg (Pattern' Expr)]
    forall a b. (a -> b) -> a -> b
    $ Literal -> Term
    Lit Literal
    lit

              p :: Pattern' Expr
    p@(A.PatternSynP PatInfo
    pi' AmbiguousQName
    c' [NamedArg (Pattern' Expr)
    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' Expr -> TCMT IO Doc
    forall a (m :: * -> *).
    (ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
    a -> m Doc
    prettyA Pattern' Expr
    p
                 WriterT [ProblemEq] (TCMT IO) [NamedArg (Pattern' Expr)]
    forall a. HasCallStack => a
    __IMPOSSIBLE__

              Pattern' Expr
    _ -> WriterT [ProblemEq] (TCMT IO) [NamedArg (Pattern' Expr)]
    forall (m :: * -> *) a. (MonadAddContext m, MonadTCError m) => m a
    mismatch
          where
            recurse :: Term -> WriterT [ProblemEq] (TCMT IO) [NamedArg (Pattern' Expr)]
    recurse Term
    v = do
              -- caseMaybeM (liftTCM $ isPath t) (return ()) $ \ _ ->
              --   typeError $ GenericError $
              --     "With-clauses currently not supported under Path abstraction."

              let piOrPathApplyM :: Type -> Term -> m (Elims, Type)
    piOrPathApplyM Type
    t Term
    v = do
                    (TelV Telescope
    tel Type
    t', Boundary
    bs) <- Int -> Type -> m (TelV Type, Boundary)
    forall (m :: * -> *).
    PureTCM m =>
    Int -> Type -> m (TelV Type, Boundary)
    telViewUpToPathBoundaryP Int
    1 Type
    t
                    Bool -> m () -> m ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    unless (Telescope -> Int
    forall a. Sized a => a -> Int
    size Telescope
    tel Int -> Int -> Bool
    forall a. Eq a => a -> a -> Bool
    == Int
    1) (m () -> m ()) -> m () -> m ()
    forall a b. (a -> b) -> a -> b
    $ m ()
    forall a. HasCallStack => a
    __IMPOSSIBLE__
                    (Elims, Type) -> m (Elims, Type)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Telescope -> Boundary -> Elims
    forall a. DeBruijn a => Telescope -> Boundary' (a, a) -> [Elim' a]
    teleElims Telescope
    tel Boundary
    bs, Int -> SubstArg Type -> Type -> Type
    forall a. Subst a => Int -> SubstArg a -> a -> a
    subst Int
    0 Term
    SubstArg Type
    v Type
    t')
              (Elims
    e, Type
    t') <- Type -> Term -> WriterT [ProblemEq] (TCMT IO) (Elims, Type)
    forall {m :: * -> *}. PureTCM m => Type -> Term -> m (Elims, Type)
    piOrPathApplyM Type
    t Term
    v
              Term
    -> Type
    -> [NamedArg (Pattern' Expr)]
    -> [NamedArg DeBruijnPattern]
    -> WriterT [ProblemEq] (TCMT IO) [NamedArg (Pattern' Expr)]
    strip (Term
    self Term -> Elims -> Term
    forall t. Apply t => t -> Elims -> t
    `applyE` Elims
    e) Type
    t' [NamedArg (Pattern' Expr)]
    ps [NamedArg DeBruijnPattern]
    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
    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' Expr -> NamedArg DeBruijnPattern -> TypeError
    WithClausePatternMismatch (NamedArg (Pattern' Expr) -> Pattern' Expr
    forall a. NamedArg a -> a
    namedArg NamedArg (Pattern' Expr)
    p0) NamedArg DeBruijnPattern
    q
            mismatchOrigin :: ProjOrigin -> ProjOrigin -> TCM [NamedArg (Pattern' Expr)]
    mismatchOrigin ProjOrigin
    o ProjOrigin
    o' = Telescope
    -> TCM [NamedArg (Pattern' Expr)] -> TCM [NamedArg (Pattern' Expr)]
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    addContext Telescope
    delta (TCM [NamedArg (Pattern' Expr)] -> TCM [NamedArg (Pattern' Expr)])
    -> (Doc -> TCM [NamedArg (Pattern' Expr)])
    -> Doc
    -> TCM [NamedArg (Pattern' Expr)]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . TypeError -> TCM [NamedArg (Pattern' Expr)]
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    TypeError -> m a
    typeError (TypeError -> TCM [NamedArg (Pattern' Expr)])
    -> (Doc -> TypeError) -> Doc -> TCM [NamedArg (Pattern' Expr)]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Doc -> TypeError
    GenericDocError (Doc -> TCM [NamedArg (Pattern' Expr)])
    -> TCMT IO Doc -> TCM [NamedArg (Pattern' Expr)]
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< [TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    fsep
              [ TCMT IO Doc
    "With clause pattern"
              , NamedArg (Pattern' Expr) -> TCMT IO Doc
    forall a (m :: * -> *).
    (ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
    a -> m Doc
    prettyA NamedArg (Pattern' Expr)
    p0
              , TCMT IO Doc
    "is not an instance of its parent pattern"
              , [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    P.fsep ([Doc] -> Doc) -> TCMT IO [Doc] -> TCMT IO Doc
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> [NamedArg DeBruijnPattern] -> TCMT IO [Doc]
    forall (m :: * -> *).
    MonadPretty m =>
    [NamedArg DeBruijnPattern] -> m [Doc]
    prettyTCMPatterns [NamedArg DeBruijnPattern
    q]
              , [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]
    "since the parent pattern is " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ ProjOrigin -> [Char]
    forall {p}. IsString p => ProjOrigin -> p
    prettyProjOrigin ProjOrigin
    o [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++
                       [Char]
    " and the with clause pattern is " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ ProjOrigin -> [Char]
    forall {p}. IsString p => ProjOrigin -> p
    prettyProjOrigin ProjOrigin
    o'
              ]
            prettyProjOrigin :: ProjOrigin -> p
    prettyProjOrigin ProjOrigin
    ProjPrefix  = p
    "a prefix projection"
            prettyProjOrigin ProjOrigin
    ProjPostfix = p
    "a postfix projection"
            prettyProjOrigin ProjOrigin
    ProjSystem  = p
    forall a. HasCallStack => a
    __IMPOSSIBLE__

            -- Make a WildP, keeping arg. info.
            makeWildP :: NamedArg A.Pattern -> NamedArg A.Pattern
            makeWildP :: NamedArg (Pattern' Expr) -> NamedArg (Pattern' Expr)
    makeWildP = (Pattern' Expr -> Pattern' Expr)
    -> NamedArg (Pattern' Expr) -> NamedArg (Pattern' Expr)
    forall a b. (a -> b) -> NamedArg a -> NamedArg b
    updateNamedArg ((Pattern' Expr -> Pattern' Expr)
     -> NamedArg (Pattern' Expr) -> NamedArg (Pattern' Expr))
    -> (Pattern' Expr -> Pattern' Expr)
    -> NamedArg (Pattern' Expr)
    -> NamedArg (Pattern' Expr)
    forall a b. (a -> b) -> a -> b
    $ Pattern' Expr -> Pattern' Expr -> Pattern' Expr
    forall a b. a -> b -> a
    const (Pattern' Expr -> Pattern' Expr -> Pattern' Expr)
    -> Pattern' Expr -> Pattern' Expr -> Pattern' Expr
    forall a b. (a -> b) -> a -> b
    $ PatInfo -> Pattern' Expr
    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' Expr)]
    -> WriterT [ProblemEq] (TCMT IO) [NamedArg (Pattern' Expr)]
    stripConP QName
    d Args
    us Abs Type
    b ConHead
    c ConOrigin
    ci [NamedArg DeBruijnPattern]
    qs' [NamedArg (Pattern' Expr)]
    ps' = do

              -- Get the type and number of parameters of the constructor.
              Defn {defType :: Definition -> Type
    defType = Type
    ct, theDef :: Definition -> Defn
    theDef = Constructor{conPars :: Defn -> Int
    conPars = Int
    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
    ct Type -> Args -> Type
    `piApply` Int -> Args -> Args
    forall a. Int -> [a] -> [a]
    take Int
    np Args
    us
              TelV Telescope
    tel' Type
    _ <- TCMT IO (TelV Type) -> WriterT [ProblemEq] (TCMT IO) (TelV Type)
    forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
    liftTCM (TCMT IO (TelV Type) -> WriterT [ProblemEq] (TCMT IO) (TelV Type))
    -> TCMT IO (TelV Type) -> WriterT [ProblemEq] (TCMT IO) (TelV Type)
    forall a b. (a -> b) -> a -> b
    $ Type -> TCMT IO (TelV Type)
    forall (m :: * -> *). PureTCM m => Type -> m (TelV Type)
    telViewPath Type
    ct'
              -- (TelV tel' _, _boundary) <- liftTCM $ telViewPathBoundaryP ct'

              [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
    20 (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
    "ct  = " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Type -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Type
    ct
                     , TCMT IO Doc
    "ct' = " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Type -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Type
    ct'
                     , TCMT IO Doc
    "np  = " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> [Char] -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => [Char] -> m Doc
    text (Int -> [Char]
    forall a. Show a => a -> [Char]
    show Int
    np)
                     , TCMT IO Doc
    "us  = " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> [TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Semigroup (m Doc), Foldable t) =>
    t (m Doc) -> m Doc
    prettyList ((Arg Term -> TCMT IO Doc) -> Args -> [TCMT IO Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map Arg Term -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Args
    us)
                     , TCMT IO Doc
    "us' = " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> [TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Semigroup (m Doc), Foldable t) =>
    t (m Doc) -> m Doc
    prettyList ((Arg Term -> TCMT IO Doc) -> Args -> [TCMT IO Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map Arg Term -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM (Args -> [TCMT IO Doc]) -> Args -> [TCMT IO Doc]
    forall a b. (a -> b) -> a -> b
    $ Int -> Args -> Args
    forall a. Int -> [a] -> [a]
    take Int
    np Args
    us)
                     ]

              -- TODO Andrea: preserve IApplyP patterns in v, see _boundary?
              -- Compute the new type
              let v :: Term
    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' :: Type
    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' :: Term
    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

              [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
    sep
                [ TCMT IO Doc
    "inserting implicit"
                , Int -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
    nest Int
    2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ [TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Semigroup (m Doc), Foldable t) =>
    t (m Doc) -> m Doc
    prettyList ([TCMT IO Doc] -> TCMT IO Doc) -> [TCMT IO Doc] -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ (NamedArg (Pattern' Expr) -> TCMT IO Doc)
    -> [NamedArg (Pattern' Expr)] -> [TCMT IO Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map NamedArg (Pattern' Expr) -> TCMT IO Doc
    forall a (m :: * -> *).
    (ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
    a -> m Doc
    prettyA ([NamedArg (Pattern' Expr)]
    ps' [NamedArg (Pattern' Expr)]
    -> [NamedArg (Pattern' Expr)] -> [NamedArg (Pattern' Expr)]
    forall a. [a] -> [a] -> [a]
    ++ [NamedArg (Pattern' Expr)]
    ps)
                , Int -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
    nest Int
    2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Doc
    ":" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Type -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Type
    t'
                ]

              -- Insert implicit patterns (just for the constructor arguments)
              [NamedArg (Pattern' Expr)]
    psi' <- TCM [NamedArg (Pattern' Expr)]
    -> WriterT [ProblemEq] (TCMT IO) [NamedArg (Pattern' Expr)]
    forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
    liftTCM (TCM [NamedArg (Pattern' Expr)]
     -> WriterT [ProblemEq] (TCMT IO) [NamedArg (Pattern' Expr)])
    -> TCM [NamedArg (Pattern' Expr)]
    -> WriterT [ProblemEq] (TCMT IO) [NamedArg (Pattern' Expr)]
    forall a b. (a -> b) -> a -> b
    $ ExpandHidden
    -> [NamedArg (Pattern' Expr)]
    -> Telescope
    -> TCM [NamedArg (Pattern' Expr)]
    forall (m :: * -> *).
    (PureTCM m, MonadError TCErr m, MonadFresh NameId m,
     MonadTrace m) =>
    ExpandHidden
    -> [NamedArg (Pattern' Expr)]
    -> Telescope
    -> m [NamedArg (Pattern' Expr)]
    insertImplicitPatterns ExpandHidden
    ExpandLast [NamedArg (Pattern' Expr)]
    ps' Telescope
    tel'
              Bool
    -> WriterT [ProblemEq] (TCMT IO) ()
    -> WriterT [ProblemEq] (TCMT IO) ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    unless ([NamedArg (Pattern' Expr)] -> Int
    forall a. Sized a => a -> Int
    size [NamedArg (Pattern' Expr)]
    psi' Int -> Int -> Bool
    forall a. Eq a => a -> a -> Bool
    == Telescope -> Int
    forall a. Sized a => a -> Int
    size Telescope
    tel') (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 -> WriterT [ProblemEq] (TCMT IO) ())
    -> TypeError -> WriterT [ProblemEq] (TCMT IO) ()
    forall a b. (a -> b) -> a -> b
    $
                QName -> Int -> Int -> TypeError
    WrongNumberOfConstructorArguments (ConHead -> QName
    conName ConHead
    c) (Telescope -> Int
    forall a. Sized a => a -> Int
    size Telescope
    tel') ([NamedArg (Pattern' Expr)] -> Int
    forall a. Sized a => a -> Int
    size [NamedArg (Pattern' Expr)]
    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.
              [NamedArg (Pattern' Expr)]
    psi <- TCM [NamedArg (Pattern' Expr)]
    -> WriterT [ProblemEq] (TCMT IO) [NamedArg (Pattern' Expr)]
    forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
    liftTCM (TCM [NamedArg (Pattern' Expr)]
     -> WriterT [ProblemEq] (TCMT IO) [NamedArg (Pattern' Expr)])
    -> TCM [NamedArg (Pattern' Expr)]
    -> WriterT [ProblemEq] (TCMT IO) [NamedArg (Pattern' Expr)]
    forall a b. (a -> b) -> a -> b
    $ ExpandHidden
    -> [NamedArg (Pattern' Expr)]
    -> Type
    -> TCM [NamedArg (Pattern' Expr)]
    forall (m :: * -> *).
    (PureTCM m, MonadError TCErr m, MonadFresh NameId m,
     MonadTrace m) =>
    ExpandHidden
    -> [NamedArg (Pattern' Expr)]
    -> Type
    -> m [NamedArg (Pattern' Expr)]
    insertImplicitPatternsT ExpandHidden
    ExpandLast ([NamedArg (Pattern' Expr)]
    psi' [NamedArg (Pattern' Expr)]
    -> [NamedArg (Pattern' Expr)] -> [NamedArg (Pattern' Expr)]
    forall a. [a] -> [a] -> [a]
    ++ [NamedArg (Pattern' Expr)]
    ps) Type
    t'

              -- Keep going
              Term
    -> Type
    -> [NamedArg (Pattern' Expr)]
    -> [NamedArg DeBruijnPattern]
    -> WriterT [ProblemEq] (TCMT IO) [NamedArg (Pattern' Expr)]
    strip Term
    self' Type
    t' [NamedArg (Pattern' Expr)]
    psi ([NamedArg DeBruijnPattern]
    qs' [NamedArg DeBruijnPattern]
    -> [NamedArg DeBruijnPattern] -> [NamedArg DeBruijnPattern]
    forall a. [a] -> [a] -> [a]
    ++ [NamedArg DeBruijnPattern]
    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.
      Args
    topArgs <- Int -> Args -> Args
    forall a. Subst a => Int -> a -> a
    raise Int
    arity0 (Args -> Args) -> TCM Args -> TCM Args
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> TCM Args
    forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Args
    getContextArgs
      let top :: Int
    top    = Args -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length Args
    topArgs
          arity :: Int
    arity  = Int
    arity0 Int -> Int -> Int
    forall a. Num a => a -> a -> a
    + Int
    top

      -- Build the rhs of the display form.
      Term
    wild <- TCMT IO Name
    forall (m :: * -> *). MonadFresh NameId m => m Name
    freshNoName_ TCMT IO Name -> (Name -> Term) -> TCM Term
    forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
    <&> \ Name
    x -> QName -> Elims -> Term
    Def (Name -> QName
    qualify_ Name
    x) []
      let -- Convert the parent patterns to terms.
          tqs0 :: [Elim' DisplayTerm]
    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.
          ([Int]
    ys0, [Int]
    ys1) = Int -> [Int] -> ([Int], [Int])
    forall a. Int -> [a] -> ([a], [a])
    splitAt (Telescope -> Int
    forall a. Sized a => a -> Int
    size Telescope
    delta1) ([Int] -> ([Int], [Int])) -> [Int] -> ([Int], [Int])
    forall a b. (a -> b) -> a -> b
    $ Permutation -> [Int] -> [Int]
    forall a. Permutation -> [a] -> [a]
    permute Permutation
    perm ([Int] -> [Int]) -> [Int] -> [Int]
    forall a b. (a -> b) -> a -> b
    $ Int -> [Int]
    forall a. Integral a => a -> [a]
    downFrom Int
    m
          ys :: [Maybe Int]
    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 :: Substitution' Term
    rho        = Int -> [Maybe Int] -> Term -> Substitution' Term
    sub Int
    top [Maybe Int]
    ys Term
    wild
          tqs :: [Elim' DisplayTerm]
    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 :: [Elim' DisplayTerm]
    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 (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 :: [Term]
    withArgs   = (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
    dt         = DisplayTerm -> [DisplayTerm] -> Elims -> DisplayTerm
    DWithApp (QName -> [Elim' DisplayTerm] -> DisplayTerm
    DDef QName
    f [Elim' DisplayTerm]
    es) ((Term -> DisplayTerm) -> [Term] -> [DisplayTerm]
    forall a b. (a -> b) -> [a] -> [b]
    map Term -> DisplayTerm
    DTerm [Term]
    withArgs) []

      -- Build the lhs of the display form and finish.
      -- @var 0@ is the pattern variable (hole).
      let display :: DisplayForm
    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 :: TCMT IO Doc -> TCMT IO Doc
    addFullCtx = Telescope -> TCMT IO Doc -> TCMT IO Doc
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> 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 (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
    addContext) ([Int] -> (Int -> [Char]) -> [[Char]]
    forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m 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
    addContext Telescope
    delta2
      [Char] -> Int -> TCMT IO Doc -> TCMT IO ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "tc.with.display" Int
    20 (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
    "withDisplayForm"
        , Int -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
    nest Int
    2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ [TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    vcat
          [ TCMT IO Doc
    "f      =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> [Char] -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => [Char] -> m Doc
    text (QName -> [Char]
    forall a. Pretty a => a -> [Char]
    prettyShow QName
    f)
          , TCMT IO Doc
    "aux    =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> [Char] -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => [Char] -> m Doc
    text (QName -> [Char]
    forall a. Pretty a => a -> [Char]
    prettyShow QName
    aux)
          , TCMT IO Doc
    "delta1 =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Telescope -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Telescope
    delta1
          , TCMT IO Doc
    "delta2 =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> do Telescope -> TCMT IO Doc -> TCMT IO Doc
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    addContext Telescope
    delta1 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ Telescope -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Telescope
    delta2
          , TCMT IO Doc
    "n      =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> [Char] -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => [Char] -> m Doc
    text (Int -> [Char]
    forall a. Show a => a -> [Char]
    show Int
    n)
          , TCMT IO Doc
    "perm   =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> [Char] -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => [Char] -> m Doc
    text (Permutation -> [Char]
    forall a. Show a => a -> [Char]
    show Permutation
    perm)
          , TCMT IO Doc
    "top    =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> do TCMT IO Doc -> TCMT IO Doc
    addFullCtx (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ Args -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Args
    topArgs
          , 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, Semigroup (m Doc), Foldable t) =>
    t (m Doc) -> m Doc
    prettyList ((NamedArg DeBruijnPattern -> TCMT IO Doc)
    -> [NamedArg DeBruijnPattern] -> [TCMT IO Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map NamedArg DeBruijnPattern -> TCMT IO Doc
    forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
    pretty [NamedArg DeBruijnPattern]
    qs)
          , TCMT IO Doc
    "qsToTm =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> [Elim' DisplayTerm] -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM [Elim' DisplayTerm]
    tqs0 -- ctx would be permuted form of delta1 ++ delta2
          , TCMT IO Doc
    "ys     =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> [Char] -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => [Char] -> m Doc
    text ([Maybe Int] -> [Char]
    forall a. Show a => a -> [Char]
    show [Maybe Int]
    ys)
          , TCMT IO Doc
    "rho    =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> [Char] -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => [Char] -> m Doc
    text (Substitution' Term -> [Char]
    forall a. Pretty a => a -> [Char]
    prettyShow Substitution' Term
    rho)
          , TCMT IO Doc
    "qs[rho]=" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> do TCMT IO Doc -> TCMT IO Doc
    addFullCtx (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ [Elim' DisplayTerm] -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM [Elim' DisplayTerm]
    tqs
          , TCMT IO Doc
    "dt     =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> do TCMT IO Doc -> TCMT IO Doc
    addFullCtx (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ DisplayTerm -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM DisplayTerm
    dt
          ]
        ]
      [Char] -> Int -> TCMT IO Doc -> TCMT IO ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "tc.with.display" Int
    70 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $ Int -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
    nest Int
    2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ [TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    vcat
          [ TCMT IO Doc
    "raw    =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> [Char] -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => [Char] -> m Doc
    text (DisplayForm -> [Char]
    forall a. Show a => a -> [Char]
    show DisplayForm
    display)
          ]

      DisplayForm -> TCM DisplayForm
    forall (m :: * -> *) a. Monad m => a -> m a
    return DisplayForm
    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 (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 (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
          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