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 (forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith forall {a} {e} {t} {b}.
Arg (Named a (Pattern' e))
-> Dom' t (ArgName, b) -> Dom' t (ArgName, b)
ren [NamedArg Pattern]
ps ListTel
telList forall a. [a] -> [a] -> [a]
++ ListTel
telRemaining)
  where
    telList :: ListTel
telList = forall t. Tele (Dom t) -> [Dom (ArgName, t)]
telToList Telescope
tel
    telRemaining :: ListTel
telRemaining = forall a. Int -> [a] -> [a]
drop (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 (forall a. IsNoName a => a -> Bool
isNoName Name
x)
          , forall a. LensHiding a => a -> Bool
visible Dom' t (ArgName, b)
dom Bool -> Bool -> Bool
|| (forall a. LensOrigin a => a -> Origin
getOrigin ArgInfo
ai forall a. Eq a => a -> a -> Bool
== Origin
UserWritten Bool -> Bool -> 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{} | 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{} -> 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
_ | forall a. LensHiding a => a -> Bool
visible Dom' t (ArgName, b)
dom Bool -> Bool -> 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 = forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
tel forall a b. (a -> b) -> a -> b
$ do
  [Maybe Name]
names <- forall a b. (a, b) -> a
fst forall b c a. (b -> c) -> (a -> b) -> a -> c
. Telescope
-> IntMap [(Name, PatVarPosition)] -> ([Maybe Name], [AsBinding])
getUserVariableNames Telescope
tel forall b c a. (b -> c) -> (a -> b) -> a -> c
. LeftoverPatterns -> IntMap [(Name, PatVarPosition)]
patternVariables forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *).
PureTCM m =>
[ProblemEq] -> m LeftoverPatterns
getLeftoverPatterns [ProblemEq]
eqs
  let argNames :: [Maybe ArgName]
argNames = forall a b. (a -> b) -> [a] -> [b]
map (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Name -> ArgName
nameToArgName) [Maybe Name]
names
  forall (m :: * -> *) a. Monad m => a -> m a
return 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 = forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith forall a b. (a -> b) -> a -> b
$ \a
x b
y -> forall a. LensOrigin a => Origin -> a -> a
setOrigin (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
_) = 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
  forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m ()
reportSDoc ArgName
"tc.lhs.init" Int
40 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
    [ TCMT IO Doc
"initLHSState"
    , forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"delta = " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Telescope
delta
    , forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"a     = " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
delta (forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
a)
    ]
  let problem :: Problem a
problem = 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     = forall a t. DeBruijn a => Tele (Dom t) -> [NamedArg a]
teleNamedArgs Telescope
delta

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

-- | 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 Bool
ixsplit) = forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
tel0 forall a b. (a -> b) -> a -> b
$ do
  [NamedArg Pattern]
ps <- 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 forall a b. (a -> b) -> a -> b
$ forall e. Arg e -> e
unArg Arg Type
a
  forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m ()
reportSDoc ArgName
"tc.lhs.imp" Int
20 forall a b. (a -> b) -> a -> b
$
    TCMT IO Doc
"insertImplicitPatternsT returned" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep (forall a b. (a -> b) -> [a] -> [b]
map 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 = forall (t :: * -> *) a. Foldable t => t a -> Int
length forall a b. (a -> b) -> a -> b
$ forall a. (a -> Bool) -> [a] -> [a]
takeWhile (forall a. Maybe a -> Bool
isNothing forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. IsProjP a => a -> Maybe (ProjOrigin, AmbiguousQName)
A.isProjP) [NamedArg Pattern]
ps
  (TelV Telescope
gamma Type
b, Boundary
boundary) <- forall (m :: * -> *).
PureTCM m =>
Int -> Type -> m (TelView, Boundary)
telViewUpToPathBoundaryP Int
m forall a b. (a -> b) -> a -> b
$ forall e. Arg e -> e
unArg Arg Type
a
  forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ (forall a b. [a] -> [b] -> [(a, b)]
zip [NamedArg Pattern]
ps (forall t. Tele (Dom t) -> [Dom (ArgName, t)]
telToList Telescope
gamma)) forall a b. (a -> b) -> a -> b
$ \(NamedArg Pattern
p, Dom (ArgName, Type)
a) ->
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (forall a b. (LensHiding a, LensHiding b) => a -> b -> Bool
sameHiding NamedArg Pattern
p Dom (ArgName, Type)
a) forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) x a.
(MonadTrace m, HasRange x) =>
x -> m a -> m a
setCurrentRange NamedArg Pattern
p forall a b. (a -> b) -> a -> b
$ 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         = forall a. Sized a => a -> Int
size Telescope
tel1
      ([NamedArg Pattern]
ps1,[NamedArg Pattern]
ps2) = forall a. Int -> [a] -> ([a], [a])
splitAt Int
n [NamedArg Pattern]
ps
      tel :: Telescope
tel       = ListTel -> Telescope
telFromList forall a b. (a -> b) -> a -> b
$ forall t. Tele (Dom t) -> [Dom (ArgName, t)]
telToList Telescope
tel0 forall a. [a] -> [a] -> [a]
++ forall t. Tele (Dom t) -> [Dom (ArgName, t)]
telToList Telescope
tel1
      qs1 :: [NamedArg DeBruijnPattern]
qs1       = forall a.
DeBruijn a =>
Telescope -> Boundary -> [NamedArg (Pattern' a)]
telePatterns Telescope
tel1 Boundary
boundary
      newEqs :: [ProblemEq]
newEqs    = forall a b c d. (a -> b -> c -> d) -> [a] -> [b] -> [c] -> [d]
zipWith3 Pattern -> Term -> Dom Type -> ProblemEq
ProblemEq
                    (forall a b. (a -> b) -> [a] -> [b]
map forall a. NamedArg a -> a
namedArg [NamedArg Pattern]
ps1)
                    (forall a b. (a -> b) -> [a] -> [b]
map (DeBruijnPattern -> Term
patternToTerm forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. NamedArg a -> a
namedArg) [NamedArg DeBruijnPattern]
qs1)
                    (forall a. TermSubst a => Tele (Dom a) -> [Dom a]
flattenTel Telescope
tel1 forall a b. (LensOrigin a, LensOrigin b) => [a] -> [b] -> [a]
`useOriginFrom` [NamedArg Pattern]
ps1)
      tau :: Substitution' DeBruijnPattern
tau       = forall a. Int -> Substitution' a
raiseS Int
n
  forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m ()
reportSDoc ArgName
"tc.lhs.problem" Int
10 forall a b. (a -> b) -> a -> b
$ forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
tel0 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
    [ TCMT IO Doc
"checking lhs -- updated split problem:"
    , forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
      [ TCMT IO Doc
"ps    =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep (forall a b. (a -> b) -> [a] -> [b]
map forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA [NamedArg Pattern]
ps)
      , TCMT IO Doc
"a     =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Arg Type
a
      , TCMT IO Doc
"tel1  =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Telescope
tel1
      , TCMT IO Doc
"ps1   =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep (forall a b. (a -> b) -> [a] -> [b]
map forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA [NamedArg Pattern]
ps1)
      , TCMT IO Doc
"ps2   =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep (forall a b. (a -> b) -> [a] -> [b]
map forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA [NamedArg Pattern]
ps2)
      , TCMT IO Doc
"b     =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
tel1 (forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
b)
      ]
    ]
  forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m ()
reportSDoc ArgName
"tc.lhs.problem" Int
60 forall a b. (a -> b) -> a -> b
$ forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
tel0 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
    [ forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
      [ TCMT IO Doc
"ps    =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> (forall (m :: * -> *). Applicative m => ArgName -> m Doc
text forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => a -> ArgName
show) [NamedArg Pattern]
ps
      , TCMT IO Doc
"a     =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> (forall (m :: * -> *). Applicative m => ArgName -> m Doc
text forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => a -> ArgName
show) Arg Type
a
      , TCMT IO Doc
"tel1  =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> (forall (m :: * -> *). Applicative m => ArgName -> m Doc
text forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => a -> ArgName
show) Telescope
tel1
      , TCMT IO Doc
"ps1   =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> (forall (m :: * -> *). Applicative m => ArgName -> m Doc
text forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => a -> ArgName
show) [NamedArg Pattern]
ps1
      , TCMT IO Doc
"ps2   =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> (forall (m :: * -> *). Applicative m => ArgName -> m Doc
text forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => a -> ArgName
show) [NamedArg Pattern]
ps2
      , TCMT IO Doc
"b     =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> (forall (m :: * -> *). Applicative m => ArgName -> m Doc
text forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => a -> ArgName
show) Type
b
      , TCMT IO Doc
"qs1   =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep (forall a b. (a -> b) -> [a] -> [b]
map forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty [NamedArg DeBruijnPattern]
qs1)
      ]
    ]
  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ LHSState
    { _lhsTel :: Telescope
_lhsTel     = Telescope
tel
    , _lhsOutPat :: [NamedArg DeBruijnPattern]
_lhsOutPat  = forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' DeBruijnPattern
tau [NamedArg DeBruijnPattern]
qs0 forall a. [a] -> [a] -> [a]
++ [NamedArg DeBruijnPattern]
qs1
    , _lhsProblem :: Problem a
_lhsProblem = Problem
                   { _problemEqs :: [ProblemEq]
_problemEqs      = forall a. TermSubst a => Substitution' DeBruijnPattern -> a -> a
applyPatSubst Substitution' DeBruijnPattern
tau [ProblemEq]
oldEqs 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 forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> Type
b
    , _lhsPartialSplit :: [Maybe Int]
_lhsPartialSplit = [Maybe Int]
psplit
    , _lhsIndexedSplit :: Bool
_lhsIndexedSplit = Bool
ixsplit
    }