    module Agda.TypeChecking.Rules.LHS.ProblemRest where

    import Control.Monad
    import Control.Monad.Except

    import Data.Maybe

    import Agda.Syntax.Common
    import Agda.Syntax.Internal
    import Agda.Syntax.Internal.Pattern
    import qualified Agda.Syntax.Abstract as A

    import Agda.TypeChecking.Monad
    import Agda.TypeChecking.Pretty
    import Agda.TypeChecking.Telescope
    import Agda.TypeChecking.Substitute

    import Agda.TypeChecking.Rules.LHS.Problem
    import Agda.TypeChecking.Rules.LHS.Implicit

    import Agda.Utils.Functor
    import Agda.Utils.Size

    import Agda.Utils.Impossible

    -- | Rename the variables in a telescope using the names from a given pattern.
    --
    --   If there are not at least as many patterns as entries as in the telescope,
    --   the names of the remaining entries in the telescope are unchanged.
    --   If there are too many patterns, there should be a type error later.
    --
    useNamesFromPattern :: [NamedArg A.Pattern] -> Telescope -> Telescope
    useNamesFromPattern :: [NamedArg Pattern] -> Telescope -> Telescope
    useNamesFromPattern [NamedArg Pattern]
    ps Telescope
    tel = ListTel -> Telescope
    telFromList ((NamedArg Pattern
     -> Dom' Term (ArgName, Type) -> Dom' Term (ArgName, Type))
    -> [NamedArg Pattern] -> ListTel -> ListTel
    forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
    zipWith NamedArg Pattern
    -> Dom' Term (ArgName, Type) -> Dom' Term (ArgName, Type)
    forall {a} {e} {t} {b}.
    Arg (Named a (Pattern' e))
    -> Dom' t (ArgName, b) -> Dom' t (ArgName, b)
    ren [NamedArg Pattern]
    ps ListTel
    telList ListTel -> ListTel -> ListTel
    forall a. [a] -> [a] -> [a]
    ++ ListTel
    telRemaining)
      where
        telList :: ListTel
    telList = Telescope -> ListTel
    forall t. Tele (Dom t) -> [Dom (ArgName, t)]
    telToList Telescope
    tel
        telRemaining :: ListTel
    telRemaining = Int -> ListTel -> ListTel
    forall a. Int -> [a] -> [a]
    drop ([NamedArg Pattern] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length [NamedArg Pattern]
    ps) ListTel
    telList -- telescope entries beyond patterns
        ren :: Arg (Named a (Pattern' e))
    -> Dom' t (ArgName, b) -> Dom' t (ArgName, b)
    ren (Arg ArgInfo
    ai (Named Maybe a
    nm Pattern' e
    p)) dom :: Dom' t (ArgName, b)
    dom@Dom{ unDom :: forall t e. Dom' t e -> e
    unDom = (ArgName
    y, b
    a) } =
          case Pattern' e
    p of
            -- Andreas, 2017-10-12, issue #2803, also preserve user-written hidden names.
            -- However, not if the argument is named, because then the name in the telescope
            -- is significant for implicit insertion.
            A.VarP A.BindName{unBind :: BindName -> Name
    unBind = Name
    x}
              | Bool -> Bool
    not (Name -> Bool
    forall a. IsNoName a => a -> Bool
    isNoName Name
    x)
              , Dom' t (ArgName, b) -> Bool
    forall a. LensHiding a => a -> Bool
    visible Dom' t (ArgName, b)
    dom Bool -> Bool -> Bool
    || (ArgInfo -> Origin
    forall a. LensOrigin a => a -> Origin
    getOrigin ArgInfo
    ai Origin -> Origin -> Bool
    forall a. Eq a => a -> a -> Bool
    == Origin
    UserWritten Bool -> Bool -> Bool
    && Maybe a -> Bool
    forall a. Maybe a -> Bool
    isNothing Maybe a
    nm) ->
              Dom' t (ArgName, b)
    dom{ unDom :: (ArgName, b)
    unDom = (Name -> ArgName
    nameToArgName Name
    x, b
    a) }
            A.AbsurdP{} | Dom' t (ArgName, b) -> Bool
    forall a. LensHiding a => a -> Bool
    visible Dom' t (ArgName, b)
    dom -> Dom' t (ArgName, b)
    dom{ unDom :: (ArgName, b)
    unDom = (ArgName -> ArgName
    stringToArgName ArgName
    "()", b
    a) }
            A.PatternSynP{} -> Dom' t (ArgName, b)
    forall a. HasCallStack => a
    __IMPOSSIBLE__  -- ensure there are no syns left
            -- Andreas, 2016-05-10, issue 1848: if context variable has no name, call it "x"
            Pattern' e
    _ | Dom' t (ArgName, b) -> Bool
    forall a. LensHiding a => a -> Bool
    visible Dom' t (ArgName, b)
    dom Bool -> Bool -> Bool
    && ArgName -> Bool
    forall a. IsNoName a => a -> Bool
    isNoName ArgName
    y -> Dom' t (ArgName, b)
    dom{ unDom :: (ArgName, b)
    unDom = (ArgName -> ArgName
    stringToArgName ArgName
    "x", b
    a) }
              | Bool
    otherwise                  -> Dom' t (ArgName, b)
    dom

    useNamesFromProblemEqs
      :: forall m. PureTCM m
      => [ProblemEq] -> Telescope -> m Telescope
    useNamesFromProblemEqs :: forall (m :: * -> *).
    PureTCM m =>
    [ProblemEq] -> Telescope -> m Telescope
    useNamesFromProblemEqs [ProblemEq]
    eqs Telescope
    tel = Telescope -> m Telescope -> m Telescope
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    addContext Telescope
    tel (m Telescope -> m Telescope) -> m Telescope -> m Telescope
    forall a b. (a -> b) -> a -> b
    $ do
      [Maybe Name]
    names <- ([Maybe Name], [AsBinding]) -> [Maybe Name]
    forall a b. (a, b) -> a
    fst (([Maybe Name], [AsBinding]) -> [Maybe Name])
    -> (LeftoverPatterns -> ([Maybe Name], [AsBinding]))
    -> LeftoverPatterns
    -> [Maybe Name]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Telescope
    -> IntMap [(Name, PatVarPosition)] -> ([Maybe Name], [AsBinding])
    getUserVariableNames Telescope
    tel (IntMap [(Name, PatVarPosition)] -> ([Maybe Name], [AsBinding]))
    -> (LeftoverPatterns -> IntMap [(Name, PatVarPosition)])
    -> LeftoverPatterns
    -> ([Maybe Name], [AsBinding])
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . LeftoverPatterns -> IntMap [(Name, PatVarPosition)]
    patternVariables (LeftoverPatterns -> [Maybe Name])
    -> m LeftoverPatterns -> m [Maybe Name]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> [ProblemEq] -> m LeftoverPatterns
    forall (m :: * -> *).
    PureTCM m =>
    [ProblemEq] -> m LeftoverPatterns
    getLeftoverPatterns [ProblemEq]
    eqs
      let argNames :: [Maybe ArgName]
    argNames = (Maybe Name -> Maybe ArgName) -> [Maybe Name] -> [Maybe ArgName]
    forall a b. (a -> b) -> [a] -> [b]
    map ((Name -> ArgName) -> Maybe Name -> Maybe ArgName
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap Name -> ArgName
    nameToArgName) [Maybe Name]
    names
      Telescope -> m Telescope
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Telescope -> m Telescope) -> Telescope -> m Telescope
    forall a b. (a -> b) -> a -> b
    $ [Maybe ArgName] -> Telescope -> Telescope
    renameTel [Maybe ArgName]
    argNames Telescope
    tel

    useOriginFrom :: (LensOrigin a, LensOrigin b) => [a] -> [b] -> [a]
    useOriginFrom :: forall a b. (LensOrigin a, LensOrigin b) => [a] -> [b] -> [a]
    useOriginFrom = (a -> b -> a) -> [a] -> [b] -> [a]
    forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
    zipWith ((a -> b -> a) -> [a] -> [b] -> [a])
    -> (a -> b -> a) -> [a] -> [b] -> [a]
    forall a b. (a -> b) -> a -> b
    $ \a
    x b
    y -> Origin -> a -> a
    forall a. LensOrigin a => Origin -> a -> a
    setOrigin (b -> Origin
    forall a. LensOrigin a => a -> Origin
    getOrigin b
    y) a
    x

    -- | Are there any untyped user patterns left?
    noProblemRest :: Problem a -> Bool
    noProblemRest :: forall a. Problem a -> Bool
    noProblemRest (Problem [ProblemEq]
    _ [NamedArg Pattern]
    rp LHSState a -> TCM a
    _) = [NamedArg Pattern] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null [NamedArg Pattern]
    rp

    -- | Construct an initial 'LHSState' from user patterns.
    --   Example:
    --   @
    --
    --      Case : {A : Set} → Maybe A → Set → Set → Set
    --      Case nothing  B C = B
    --      Case (just _) B C = C
    --
    --      sample : {A : Set} (m : Maybe A) → Case m Bool (Maybe A → Bool)
    --      sample (just a) (just b) = true
    --      sample (just a) nothing  = false
    --      sample nothing           = true
    --   @
    --   The problem generated for the first clause of @sample@
    --   with patterns @just a, just b@ would be:
    --   @
    --      lhsTel        = [A : Set, m : Maybe A]
    --      lhsOutPat     = ["A", "m"]
    --      lhsProblem    = Problem ["A" = _, "just a" = "a"]
    --                              ["_", "just a"]
    --                              ["just b"] []
    --      lhsTarget     = "Case m Bool (Maybe A -> Bool)"
    --   @
    initLHSState
      :: Telescope             -- ^ The initial telescope @delta@ of parameters.
      -> [ProblemEq]           -- ^ The problem equations inherited from the parent clause (living in @delta@).
      -> [NamedArg A.Pattern]  -- ^ The user patterns.
      -> Type                  -- ^ The type the user patterns eliminate (living in @delta@).
      -> (LHSState a -> TCM a) -- ^ Continuation for when checking the patterns is complete.
      -> TCM (LHSState a)      -- ^ The initial LHS state constructed from the user patterns.
    initLHSState :: forall a.
    Telescope
    -> [ProblemEq]
    -> [NamedArg Pattern]
    -> Type
    -> (LHSState a -> TCM a)
    -> TCM (LHSState a)
    initLHSState Telescope
    delta [ProblemEq]
    eqs [NamedArg Pattern]
    ps Type
    a LHSState a -> TCM a
    ret = do
      let problem :: Problem a
    problem = [ProblemEq]
    -> [NamedArg Pattern] -> (LHSState a -> TCM a) -> Problem a
    forall a.
    [ProblemEq]
    -> [NamedArg Pattern] -> (LHSState a -> TCM a) -> Problem a
    Problem [ProblemEq]
    eqs [NamedArg Pattern]
    ps LHSState a -> TCM a
    ret
          qs0 :: [NamedArg DeBruijnPattern]
    qs0     = Telescope -> [NamedArg DeBruijnPattern]
    forall a. DeBruijn a => Telescope -> [NamedArg a]
    teleNamedArgs Telescope
    delta

      LHSState a -> TCM (LHSState a)
    forall (m :: * -> *) a.
    (PureTCM m, MonadError TCErr m, MonadTrace m,
     MonadFresh NameId m) =>
    LHSState a -> m (LHSState a)
    updateProblemRest (LHSState a -> TCM (LHSState a)) -> LHSState a -> TCM (LHSState a)
    forall a b. (a -> b) -> a -> b
    $ Telescope
    -> [NamedArg DeBruijnPattern]
    -> Problem a
    -> Arg Type
    -> [Maybe Int]
    -> LHSState a
    forall a.
    Telescope
    -> [NamedArg DeBruijnPattern]
    -> Problem a
    -> Arg Type
    -> [Maybe Int]
    -> LHSState a
    LHSState Telescope
    delta [NamedArg DeBruijnPattern]
    qs0 Problem a
    problem (Type -> Arg Type
    forall a. a -> Arg a
    defaultArg Type
    a) []

    -- | Try to move patterns from the problem rest into the problem.
    --   Possible if type of problem rest has been updated to a function type.
    updateProblemRest
      :: forall m a. (PureTCM m, MonadError TCErr m, MonadTrace m, MonadFresh NameId m)
      => LHSState a -> m (LHSState a)
    updateProblemRest :: forall (m :: * -> *) a.
    (PureTCM m, MonadError TCErr m, MonadTrace m,
     MonadFresh NameId m) =>
    LHSState a -> m (LHSState a)
    updateProblemRest st :: LHSState a
    st@(LHSState Telescope
    tel0 [NamedArg DeBruijnPattern]
    qs0 p :: Problem a
    p@(Problem [ProblemEq]
    oldEqs [NamedArg Pattern]
    ps LHSState a -> TCM a
    ret) Arg Type
    a [Maybe Int]
    psplit) = do
      [NamedArg Pattern]
    ps <- Telescope -> m [NamedArg Pattern] -> m [NamedArg Pattern]
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    addContext Telescope
    tel0 (m [NamedArg Pattern] -> m [NamedArg Pattern])
    -> m [NamedArg Pattern] -> m [NamedArg Pattern]
    forall a b. (a -> b) -> a -> b
    $ ExpandHidden -> [NamedArg Pattern] -> Type -> m [NamedArg Pattern]
    forall (m :: * -> *).
    (PureTCM m, MonadError TCErr m, MonadFresh NameId m,
     MonadTrace m) =>
    ExpandHidden -> [NamedArg Pattern] -> Type -> m [NamedArg Pattern]
    insertImplicitPatternsT ExpandHidden
    ExpandLast [NamedArg Pattern]
    ps (Type -> m [NamedArg Pattern]) -> Type -> m [NamedArg Pattern]
    forall a b. (a -> b) -> a -> b
    $ Arg Type -> Type
    forall e. Arg e -> e
    unArg Arg Type
    a
      ArgName -> Int -> TCMT IO Doc -> m ()
    forall (m :: * -> *).
    MonadDebug m =>
    ArgName -> Int -> TCMT IO Doc -> m ()
    reportSDoc ArgName
    "tc.lhs.imp" Int
    20 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
    forall a b. (a -> b) -> a -> b
    $
        TCMT IO Doc
    "insertImplicitPatternsT returned" 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 ((NamedArg Pattern -> TCMT IO Doc)
    -> [NamedArg Pattern] -> [TCMT IO Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map NamedArg Pattern -> TCMT IO Doc
    forall a (m :: * -> *).
    (ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
    a -> m Doc
    prettyA [NamedArg Pattern]
    ps)
      -- (Issue 734: Do only the necessary telView to preserve clause types as much as possible.)
      let m :: Int
    m = [NamedArg Pattern] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length ([NamedArg Pattern] -> Int) -> [NamedArg Pattern] -> Int
    forall a b. (a -> b) -> a -> b
    $ (NamedArg Pattern -> Bool)
    -> [NamedArg Pattern] -> [NamedArg Pattern]
    forall a. (a -> Bool) -> [a] -> [a]
    takeWhile (Maybe (ProjOrigin, AmbiguousQName) -> Bool
    forall a. Maybe a -> Bool
    isNothing (Maybe (ProjOrigin, AmbiguousQName) -> Bool)
    -> (NamedArg Pattern -> Maybe (ProjOrigin, AmbiguousQName))
    -> NamedArg Pattern
    -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . NamedArg Pattern -> Maybe (ProjOrigin, AmbiguousQName)
    forall a. IsProjP a => a -> Maybe (ProjOrigin, AmbiguousQName)
    A.isProjP) [NamedArg Pattern]
    ps
      (TelV Telescope
    gamma Type
    b, Boundary
    boundary) <- Int -> Type -> m (TelView, Boundary)
    forall (m :: * -> *).
    PureTCM m =>
    Int -> Type -> m (TelView, Boundary)
    telViewUpToPathBoundaryP Int
    m (Type -> m (TelView, Boundary)) -> Type -> m (TelView, Boundary)
    forall a b. (a -> b) -> a -> b
    $ Arg Type -> Type
    forall e. Arg e -> e
    unArg Arg Type
    a
      [(NamedArg Pattern, Dom' Term (ArgName, Type))]
    -> ((NamedArg Pattern, Dom' Term (ArgName, Type)) -> m ()) -> m ()
    forall (t :: * -> *) (m :: * -> *) a b.
    (Foldable t, Monad m) =>
    t a -> (a -> m b) -> m ()
    forM_ ([NamedArg Pattern]
    -> ListTel -> [(NamedArg Pattern, Dom' Term (ArgName, Type))]
    forall a b. [a] -> [b] -> [(a, b)]
    zip [NamedArg Pattern]
    ps (Telescope -> ListTel
    forall t. Tele (Dom t) -> [Dom (ArgName, t)]
    telToList Telescope
    gamma)) (((NamedArg Pattern, Dom' Term (ArgName, Type)) -> m ()) -> m ())
    -> ((NamedArg Pattern, Dom' Term (ArgName, Type)) -> m ()) -> m ()
    forall a b. (a -> b) -> a -> b
    $ \(NamedArg Pattern
    p, Dom' Term (ArgName, Type)
    a) ->
        Bool -> m () -> m ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    unless (NamedArg Pattern -> Dom' Term (ArgName, Type) -> Bool
    forall a b. (LensHiding a, LensHiding b) => a -> b -> Bool
    sameHiding NamedArg Pattern
    p Dom' Term (ArgName, Type)
    a) (m () -> m ()) -> m () -> m ()
    forall a b. (a -> b) -> a -> b
    $ NamedArg Pattern -> m () -> m ()
    forall (m :: * -> *) x a.
    (MonadTrace m, HasRange x) =>
    x -> m a -> m a
    setCurrentRange NamedArg Pattern
    p (m () -> m ()) -> m () -> m ()
    forall a b. (a -> b) -> a -> b
    $ TypeError -> m ()
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    TypeError -> m a
    typeError TypeError
    WrongHidingInLHS
      let tel1 :: Telescope
    tel1      = [NamedArg Pattern] -> Telescope -> Telescope
    useNamesFromPattern [NamedArg Pattern]
    ps Telescope
    gamma
          n :: Int
    n         = Telescope -> Int
    forall a. Sized a => a -> Int
    size Telescope
    tel1
          ([NamedArg Pattern]
    ps1,[NamedArg Pattern]
    ps2) = Int
    -> [NamedArg Pattern] -> ([NamedArg Pattern], [NamedArg Pattern])
    forall a. Int -> [a] -> ([a], [a])
    splitAt Int
    n [NamedArg Pattern]
    ps
          tel :: Telescope
    tel       = ListTel -> Telescope
    telFromList (ListTel -> Telescope) -> ListTel -> Telescope
    forall a b. (a -> b) -> a -> b
    $ Telescope -> ListTel
    forall t. Tele (Dom t) -> [Dom (ArgName, t)]
    telToList Telescope
    tel0 ListTel -> ListTel -> ListTel
    forall a. [a] -> [a] -> [a]
    ++ Telescope -> ListTel
    forall t. Tele (Dom t) -> [Dom (ArgName, t)]
    telToList Telescope
    tel1
          qs1 :: [NamedArg DeBruijnPattern]
    qs1       = Telescope -> Boundary -> [NamedArg DeBruijnPattern]
    forall a.
    DeBruijn a =>
    Telescope -> Boundary -> [NamedArg (Pattern' a)]
    telePatterns Telescope
    tel1 Boundary
    boundary
          newEqs :: [ProblemEq]
    newEqs    = (Pattern -> Term -> Dom Type -> ProblemEq)
    -> [Pattern] -> [Term] -> [Dom Type] -> [ProblemEq]
    forall a b c d. (a -> b -> c -> d) -> [a] -> [b] -> [c] -> [d]
    zipWith3 Pattern -> Term -> Dom Type -> ProblemEq
    ProblemEq
                        ((NamedArg Pattern -> Pattern) -> [NamedArg Pattern] -> [Pattern]
    forall a b. (a -> b) -> [a] -> [b]
    map NamedArg Pattern -> Pattern
    forall a. NamedArg a -> a
    namedArg [NamedArg Pattern]
    ps1)
                        ((NamedArg DeBruijnPattern -> Term)
    -> [NamedArg DeBruijnPattern] -> [Term]
    forall a b. (a -> b) -> [a] -> [b]
    map (DeBruijnPattern -> Term
    patternToTerm (DeBruijnPattern -> Term)
    -> (NamedArg DeBruijnPattern -> DeBruijnPattern)
    -> NamedArg DeBruijnPattern
    -> Term
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . NamedArg DeBruijnPattern -> DeBruijnPattern
    forall a. NamedArg a -> a
    namedArg) [NamedArg DeBruijnPattern]
    qs1)
                        (Telescope -> [Dom Type]
    forall a. TermSubst a => Tele (Dom a) -> [Dom a]
    flattenTel Telescope
    tel1 [Dom Type] -> [NamedArg Pattern] -> [Dom Type]
    forall a b. (LensOrigin a, LensOrigin b) => [a] -> [b] -> [a]
    `useOriginFrom` [NamedArg Pattern]
    ps1)
          tau :: Substitution' DeBruijnPattern
    tau       = Int -> Substitution' DeBruijnPattern
    forall a. Int -> Substitution' a
    raiseS Int
    n
      ArgName -> Int -> TCMT IO Doc -> m ()
    forall (m :: * -> *).
    MonadDebug m =>
    ArgName -> Int -> TCMT IO Doc -> m ()
    reportSDoc ArgName
    "tc.lhs.problem" Int
    10 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
    forall a b. (a -> b) -> a -> b
    $ Telescope -> TCMT IO Doc -> TCMT IO Doc
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    addContext Telescope
    tel0 (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
    "checking lhs -- updated split problem:"
        , Int -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
    nest Int
    2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ [TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    vcat
          [ TCMT IO Doc
    "ps    =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> [TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    fsep ((NamedArg Pattern -> TCMT IO Doc)
    -> [NamedArg Pattern] -> [TCMT IO Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map NamedArg Pattern -> TCMT IO Doc
    forall a (m :: * -> *).
    (ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
    a -> m Doc
    prettyA [NamedArg Pattern]
    ps)
          , TCMT IO Doc
    "a     =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Arg Type -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Arg Type
    a
          , TCMT IO Doc
    "tel1  =" 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
    tel1
          , TCMT IO Doc
    "ps1   =" 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 ((NamedArg Pattern -> TCMT IO Doc)
    -> [NamedArg Pattern] -> [TCMT IO Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map NamedArg Pattern -> TCMT IO Doc
    forall a (m :: * -> *).
    (ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
    a -> m Doc
    prettyA [NamedArg Pattern]
    ps1)
          , TCMT IO Doc
    "ps2   =" 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 ((NamedArg Pattern -> TCMT IO Doc)
    -> [NamedArg Pattern] -> [TCMT IO Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map NamedArg Pattern -> TCMT IO Doc
    forall a (m :: * -> *).
    (ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
    a -> m Doc
    prettyA [NamedArg Pattern]
    ps2)
          , TCMT IO Doc
    "b     =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Telescope -> TCMT IO Doc -> TCMT IO Doc
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    addContext Telescope
    tel1 (Type -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Type
    b)
          ]
        ]
      ArgName -> Int -> TCMT IO Doc -> m ()
    forall (m :: * -> *).
    MonadDebug m =>
    ArgName -> Int -> TCMT IO Doc -> m ()
    reportSDoc ArgName
    "tc.lhs.problem" Int
    60 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
    forall a b. (a -> b) -> a -> b
    $ Telescope -> TCMT IO Doc -> TCMT IO Doc
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    addContext Telescope
    tel0 (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
        [ Int -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
    nest Int
    2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ [TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    vcat
          [ TCMT IO Doc
    "ps    =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> (ArgName -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => ArgName -> m Doc
    text (ArgName -> TCMT IO Doc)
    -> ([NamedArg Pattern] -> ArgName)
    -> [NamedArg Pattern]
    -> TCMT IO Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [NamedArg Pattern] -> ArgName
    forall a. Show a => a -> ArgName
    show) [NamedArg Pattern]
    ps
          , TCMT IO Doc
    "a     =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> (ArgName -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => ArgName -> m Doc
    text (ArgName -> TCMT IO Doc)
    -> (Arg Type -> ArgName) -> Arg Type -> TCMT IO Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Arg Type -> ArgName
    forall a. Show a => a -> ArgName
    show) Arg Type
    a
          , TCMT IO Doc
    "tel1  =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> (ArgName -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => ArgName -> m Doc
    text (ArgName -> TCMT IO Doc)
    -> (Telescope -> ArgName) -> Telescope -> TCMT IO Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Telescope -> ArgName
    forall a. Show a => a -> ArgName
    show) Telescope
    tel1
          , TCMT IO Doc
    "ps1   =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> (ArgName -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => ArgName -> m Doc
    text (ArgName -> TCMT IO Doc)
    -> ([NamedArg Pattern] -> ArgName)
    -> [NamedArg Pattern]
    -> TCMT IO Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [NamedArg Pattern] -> ArgName
    forall a. Show a => a -> ArgName
    show) [NamedArg Pattern]
    ps1
          , TCMT IO Doc
    "ps2   =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> (ArgName -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => ArgName -> m Doc
    text (ArgName -> TCMT IO Doc)
    -> ([NamedArg Pattern] -> ArgName)
    -> [NamedArg Pattern]
    -> TCMT IO Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [NamedArg Pattern] -> ArgName
    forall a. Show a => a -> ArgName
    show) [NamedArg Pattern]
    ps2
          , TCMT IO Doc
    "b     =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> (ArgName -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => ArgName -> m Doc
    text (ArgName -> TCMT IO Doc)
    -> (Type -> ArgName) -> Type -> TCMT IO Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Type -> ArgName
    forall a. Show a => a -> ArgName
    show) Type
    b
          , TCMT IO Doc
    "qs1   =" 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 ((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]
    qs1)
          ]
        ]
      LHSState a -> m (LHSState a)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (LHSState a -> m (LHSState a)) -> LHSState a -> m (LHSState a)
    forall a b. (a -> b) -> a -> b
    $ LHSState :: forall a.
    Telescope
    -> [NamedArg DeBruijnPattern]
    -> Problem a
    -> Arg Type
    -> [Maybe Int]
    -> LHSState a
    LHSState
        { _lhsTel :: Telescope
    _lhsTel     = Telescope
    tel
        , _lhsOutPat :: [NamedArg DeBruijnPattern]
    _lhsOutPat  = Substitution' (SubstArg [NamedArg DeBruijnPattern])
    -> [NamedArg DeBruijnPattern] -> [NamedArg DeBruijnPattern]
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    applySubst Substitution' DeBruijnPattern
    Substitution' (SubstArg [NamedArg DeBruijnPattern])
    tau [NamedArg DeBruijnPattern]
    qs0 [NamedArg DeBruijnPattern]
    -> [NamedArg DeBruijnPattern] -> [NamedArg DeBruijnPattern]
    forall a. [a] -> [a] -> [a]
    ++ [NamedArg DeBruijnPattern]
    qs1
        , _lhsProblem :: Problem a
    _lhsProblem = Problem :: forall a.
    [ProblemEq]
    -> [NamedArg Pattern] -> (LHSState a -> TCM a) -> Problem a
    Problem
                       { _problemEqs :: [ProblemEq]
    _problemEqs      = Substitution' DeBruijnPattern -> [ProblemEq] -> [ProblemEq]
    forall a. TermSubst a => Substitution' DeBruijnPattern -> a -> a
    applyPatSubst Substitution' DeBruijnPattern
    tau [ProblemEq]
    oldEqs [ProblemEq] -> [ProblemEq] -> [ProblemEq]
    forall a. [a] -> [a] -> [a]
    ++ [ProblemEq]
    newEqs
                       , _problemRestPats :: [NamedArg Pattern]
    _problemRestPats = [NamedArg Pattern]
    ps2
                       , _problemCont :: LHSState a -> TCM a
    _problemCont     = LHSState a -> TCM a
    ret
                       }
        , _lhsTarget :: Arg Type
    _lhsTarget  = Arg Type
    a Arg Type -> Type -> Arg Type
    forall (f :: * -> *) a b. Functor f => f a -> b -> f b
    $> Type
    b
        , _lhsPartialSplit :: [Maybe Int]
    _lhsPartialSplit = [Maybe Int]
    psplit
        }