{-# LANGUAGE CPP #-}

module Agda.TypeChecking.Rules.LHS where

import Prelude hiding (mapM)

import Data.Maybe

import Control.Applicative
import Control.Monad hiding (mapM)
import Control.Monad.State hiding (mapM)

import Data.Traversable

import Agda.Interaction.Options
import Agda.Interaction.Options.Lenses

import Agda.Syntax.Internal as I hiding (Substitution)
import Agda.Syntax.Internal.Pattern
import Agda.Syntax.Abstract (IsProjP(..))
import qualified Agda.Syntax.Abstract as A
import Agda.Syntax.Abstract.Views (asView)
import Agda.Syntax.Common
import Agda.Syntax.Info
import Agda.Syntax.Position

import Agda.TypeChecking.Monad

import Agda.TypeChecking.Conversion
import Agda.TypeChecking.Constraints
import Agda.TypeChecking.Datatypes
import Agda.TypeChecking.Irrelevance
import {-# SOURCE #-} Agda.TypeChecking.Empty
import Agda.TypeChecking.Patterns.Abstract
import Agda.TypeChecking.Pretty
import Agda.TypeChecking.Records
import Agda.TypeChecking.Reduce
import Agda.TypeChecking.Substitute hiding (Substitution)
import qualified Agda.TypeChecking.Substitute as S (Substitution)
import Agda.TypeChecking.Telescope

import {-# SOURCE #-} Agda.TypeChecking.Rules.Term (checkExpr)
import Agda.TypeChecking.Rules.LHS.Problem
import Agda.TypeChecking.Rules.LHS.ProblemRest
import Agda.TypeChecking.Rules.LHS.Unify
import Agda.TypeChecking.Rules.LHS.Split
import Agda.TypeChecking.Rules.LHS.Implicit
import Agda.TypeChecking.Rules.LHS.Instantiate
import Agda.TypeChecking.Rules.Data

import Agda.Utils.Except (MonadError(..))
import Agda.Utils.Functor (($>))
import Agda.Utils.ListT
import Agda.Utils.Monad
import Agda.Utils.Permutation
import Agda.Utils.Size

#include "undefined.h"
import Agda.Utils.Impossible

-- | Compute the set of flexible patterns in a list of patterns. The result is
--   the deBruijn indices of the flexible patterns. A pattern is flexible if it
--   is dotted or implicit.
flexiblePatterns :: [A.NamedArg A.Pattern] -> TCM FlexibleVars
flexiblePatterns nps = map setFlex <$> filterM (flexible . namedArg . snd) (zip [0..] $ reverse nps)
  where
    setFlex (i, Arg ai p)    = FlexibleVar (getHiding ai) (classify $ namedThing p) i
    classify A.DotP{}        = DotFlex
    classify A.ImplicitP{}   = ImplicitFlex
    classify A.ConP{}        = RecordFlex
    classify _               = __IMPOSSIBLE__
    flexible (A.DotP _ _)    = return True
    flexible (A.ImplicitP _) = return True
    flexible (A.ConP _ (A.AmbQ [c]) qs) =
      ifM (isJust <$> isRecordConstructor c)
          (andM $ map (flexible . namedArg) qs)
          (return False)
    flexible _               = return False

-- | Compute the dot pattern instantiations.
dotPatternInsts :: [A.NamedArg A.Pattern] -> Substitution -> [I.Dom Type] -> TCM [DotPatternInst]
dotPatternInsts ps s as = dpi (map namedArg ps) (reverse s) as
  where
    dpi (_ : _)  []            _       = __IMPOSSIBLE__
    dpi (_ : _)  (Just _ : _)  []      = __IMPOSSIBLE__
    -- the substitution also contains entries for module parameters, so it can
    -- be longer than the pattern
    dpi []       _             _       = return []
    dpi (_ : ps) (Nothing : s) as      = dpi ps s as
    dpi (p : ps) (Just u : s) (a : as) =
      case p of
        A.DotP _ e    -> (DPI e u a :) <$> dpi ps s as
        A.ImplicitP _ -> dpi ps s as
        -- record pattern
        A.ConP _ (A.AmbQ [c]) qs -> do
          Def r es   <- ignoreSharing <$> reduce (unEl $ unDom a)
          let Just vs = allApplyElims es
          (ftel, us) <- etaExpandRecord r vs u
          qs <- insertImplicitPatterns ExpandLast qs ftel
          let instTel EmptyTel _                   = []
              instTel (ExtendTel arg tel) (u : us) = arg : instTel (absApp tel u) us
              instTel ExtendTel{} []               = __IMPOSSIBLE__
              bs0 = instTel ftel (map unArg us)
              -- Andreas, 2012-09-19 propagate relevance info to dot patterns
              bs  = map (mapRelevance (composeRelevance (getRelevance a))) bs0
          dpi (map namedArg qs ++ ps) (map (Just . unArg) us ++ s) (bs ++ as)

        _           -> __IMPOSSIBLE__


-- | In an internal pattern, replace some pattern variables
--   by dot patterns, according to the given substitution.
instantiatePattern
  :: Substitution
     -- ^ Partial substitution for the pattern variables,
     --   given in order of the clause telescope,
     --   (not in the order of occurrence in the patterns).
  -> Permutation
     -- ^ Map from the pattern variables to the telescope variables.
  -> [I.NamedArg Pattern]
     -- ^ Input patterns.
  -> [I.NamedArg Pattern]
     -- ^ Output patterns, with some @VarP@ replaced by @DotP@
     --   according to the @Substitution@.
instantiatePattern sub perm ps
  | length sub /= length hps = error $ unlines
      [ "instantiatePattern:"
      , "  sub  = " ++ show sub
      , "  perm = " ++ show perm
      , "  ps   = " ++ show ps
      ]
  | otherwise  = foldr merge ps $ zipWith inst (reverse sub) hps
  where
    -- For each pattern variable get a copy of the patterns
    -- focusing on this variable.
    -- Order them in the dependency (telescope) order.
    hps = permute perm $ allHoles ps
    -- If we do not want to substitute a variable, we
    -- throw away the corresponding one-hole pattern.
    inst Nothing  hps = Nothing
    -- If we want to substitute, we replace the variable
    -- by the dot pattern.
    inst (Just t) hps = Just $ plugHole (DotP t) hps

    -- If we did not instantiate a variable, we can keep the original
    -- patterns in this iteration.
    merge Nothing   ps = ps
    -- Otherwise, we merge the changes in @qs@ into @ps@.
    -- This means we walk simultaneously through @qs@ and @ps@
    -- and expect them to be the same everywhere except that
    -- a @q@ can be a @DotP@ and the corresponding @p@ a @VarP@.
    -- In this case, we take the @DotP@.
    -- Apparently, the other way round can also happen (why?).
    merge (Just qs) ps = zipWith mergeA qs ps
      where
        mergeA a1 a2 = fmap (mergeP (namedArg a1) (namedArg a2) <$) a1

        mergeP (DotP s)  (DotP t)
          | s == t                    = DotP s
          | otherwise                 = __IMPOSSIBLE__
        -- interesting cases:
        mergeP (DotP t)  (VarP _)     = DotP t
        mergeP (VarP _)  (DotP t)     = DotP t
        -- the rest is homomorphical
        mergeP (DotP _)  _            = __IMPOSSIBLE__
        mergeP _         (DotP _)     = __IMPOSSIBLE__
        mergeP (ConP c1 i1 ps) (ConP c2 i2 qs)
          | c1 == c2                  = ConP (c1 `withRangeOf` c2) (mergeCPI i1 i2) $
                                          zipWith mergeA ps qs
          | otherwise                 = __IMPOSSIBLE__
        mergeP (LitP l1) (LitP l2)
          | l1 == l2                  = LitP (l1 `withRangeOf` l2)
          | otherwise                 = __IMPOSSIBLE__
        mergeP (VarP x) (VarP y)
          | x == y                    = VarP x
          | otherwise                 = __IMPOSSIBLE__
        mergeP (ConP _ _ _) (VarP _)  = __IMPOSSIBLE__
        mergeP (ConP _ _ _) (LitP _)  = __IMPOSSIBLE__
        mergeP (VarP _) (ConP _ _ _)  = __IMPOSSIBLE__
        mergeP (VarP _) (LitP _)      = __IMPOSSIBLE__
        mergeP (LitP _) (ConP _ _ _)  = __IMPOSSIBLE__
        mergeP (LitP _) (VarP _)      = __IMPOSSIBLE__
        mergeP (ProjP x) (ProjP y)
          | x == y                    = ProjP x
          | otherwise                 = __IMPOSSIBLE__
        mergeP ProjP{} _              = __IMPOSSIBLE__
        mergeP _       ProjP{}        = __IMPOSSIBLE__

        mergeCPI (ConPatternInfo mr1 mt1) (ConPatternInfo mr2 mt2) =
          ConPatternInfo (mplus mr1 mr2) (mplus mt1 mt2)


-- | In an internal pattern, replace some pattern variables
--   by dot patterns, according to the given substitution.
instantiatePattern'
  :: Substitution
     -- ^ Partial substitution for the pattern variables,
     --   given in order of the clause telescope,
     --   (not in the order of occurrence in the patterns).
  -> Permutation
     -- ^ Map from the pattern variables to the telescope variables.
  -> [I.NamedArg Pattern]
     -- ^ Input patterns.
  -> [I.NamedArg Pattern]
     -- ^ Output patterns, with some @VarP@ replaced by @DotP@
     --   according to the @Substitution@.
instantiatePattern' sub perm ps = evalState (mapM goArg ps) 0
  where
    -- get a partial substitution from pattern variables to terms
    sub'    = inversePermute perm sub
    -- get next pattern variable
    next    = do n <- get; put (n+1); return n
    goArg   = traverse goNamed
    goNamed = traverse goPat
    goPat p = case p of
      VarP x       -> replace p
      DotP t       -> replace p
      ConP c mt ps -> ConP c mt <$> mapM goArg ps
      LitP{}       -> return p
      ProjP{}      -> return p
    replace p = do
      i <- next
      return $ fromMaybe p $ DotP <$> sub' !! i



-- | Check if a problem is solved. That is, if the patterns are all variables.
isSolvedProblem :: Problem -> Bool
isSolvedProblem problem = null (restPats $ problemRest problem) &&
    all (isSolved . snd . asView . namedArg) (problemInPat problem)
  where
    isSolved (A.DefP _ _ []) = False  -- projection pattern
    isSolved (A.VarP _)      = True
    isSolved (A.WildP _)     = True
    isSolved (A.ImplicitP _) = True
    isSolved (A.AbsurdP _)   = True
    isSolved _               = False

-- | For each user-defined pattern variable in the 'Problem', check
-- that the corresponding data type (if any) does not contain a
-- constructor of the same name (which is not in scope); this
-- \"shadowing\" could indicate an error, and is not allowed.
--
-- Precondition: The problem has to be solved.

noShadowingOfConstructors
  :: (Maybe r -> Call) -- ^ Trace, e.g., @CheckPatternShadowing clause@
  -> Problem -> TCM ()
noShadowingOfConstructors mkCall problem =
  traceCall mkCall $ do
    let pat = map (snd . asView . namedArg) $
                  problemInPat problem
        tel = map (unEl . snd . unDom) $ telToList $ problemTel problem
    zipWithM_ noShadowing pat tel -- TODO: does not work for flexible arity and projection patterns
    return ()
  where
  noShadowing (A.WildP     {}) t = return ()
  noShadowing (A.AbsurdP   {}) t = return ()
  noShadowing (A.ImplicitP {}) t = return ()
  noShadowing (A.ConP      {}) t = return ()  -- only happens for eta expanded record patterns
  noShadowing (A.DefP      {}) t = return ()  -- projection pattern
  noShadowing (A.AsP       {}) t = __IMPOSSIBLE__
  noShadowing (A.DotP      {}) t = __IMPOSSIBLE__
  noShadowing (A.LitP      {}) t = __IMPOSSIBLE__
  noShadowing (A.PatternSynP {}) t = __IMPOSSIBLE__
  noShadowing (A.VarP x)       t = do
    reportSDoc "tc.lhs.shadow" 30 $ vcat
      [ text $ "checking whether pattern variable " ++ show x ++ " shadows a constructor"
      , nest 2 $ text "type of variable =" <+> prettyTCM t
      ]
    reportSLn "tc.lhs.shadow" 70 $ "  t = " ++ show t
    t <- reduce t
    case t of
      Def t _ -> do
        d <- theDef <$> getConstInfo t
        case d of
          Datatype { dataCons = cs } -> do
            case filter ((A.nameConcrete x ==) . A.nameConcrete . A.qnameName) cs of
              []      -> return ()
              (c : _) -> setCurrentRange x $
                typeError $ PatternShadowsConstructor x c
          Axiom       {} -> return ()
          Function    {} -> return ()
          Record      {} -> return ()
          Constructor {} -> __IMPOSSIBLE__
          Primitive   {} -> __IMPOSSIBLE__
      Var   {} -> return ()
      Pi    {} -> return ()
      Sort  {} -> return ()
      Shared p -> noShadowing (A.VarP x) $ derefPtr p
      MetaV {} -> return ()
      -- TODO: If the type is a meta-variable, should the test be
      -- postponed? If there is a problem, then it will be caught when
      -- the completed module is type checked, so it is safe to skip
      -- the test here. However, users may be annoyed if they get an
      -- error in code which has already passed the type checker.
      Lam   {} -> __IMPOSSIBLE__
      Lit   {} -> __IMPOSSIBLE__
      Level {} -> __IMPOSSIBLE__
      Con   {} -> __IMPOSSIBLE__
      DontCare{} -> __IMPOSSIBLE__
      ExtLam{}   -> __IMPOSSIBLE__

-- | Check that a dot pattern matches it's instantiation.
checkDotPattern :: DotPatternInst -> TCM ()
checkDotPattern (DPI e v (Dom info a)) =
  traceCall (CheckDotPattern e v) $ do
  reportSDoc "tc.lhs.dot" 15 $
    sep [ text "checking dot pattern"
        , nest 2 $ prettyA e
        , nest 2 $ text "=" <+> prettyTCM v
        , nest 2 $ text ":" <+> prettyTCM a
        ]
  applyRelevanceToContext (argInfoRelevance info) $ do
    u <- checkExpr e a
    -- Should be ok to do noConstraints here
    noConstraints $ equalTerm a u v

-- | Bind the variables in a left hand side. Precondition: the patterns should
--   all be 'A.VarP', 'A.WildP', 'A.AbsurdP', or 'A.ImplicitP' and the
--   telescope should have the same size as the pattern list.
--   There could also be 'A.ConP's resulting from eta expanded implicit record
--   patterns.
bindLHSVars :: [A.NamedArg A.Pattern] -> Telescope -> TCM a -> TCM a
bindLHSVars []        tel@ExtendTel{}  _   = do
  reportSDoc "impossible" 10 $
    text "bindLHSVars: no patterns left, but tel =" <+> prettyTCM tel
  __IMPOSSIBLE__
bindLHSVars (_ : _)   EmptyTel         _   = __IMPOSSIBLE__
bindLHSVars []        EmptyTel         ret = ret
bindLHSVars (p : ps) (ExtendTel a tel) ret =
  case namedArg p of
    A.VarP x      -> addContext (x, a) $ bindLHSVars ps (absBody tel) ret
    A.WildP _     -> bindDummy (absName tel)
    A.ImplicitP _ -> bindDummy (absName tel)
    A.AbsurdP pi  -> do
      -- Andreas, 2012-03-15: allow postponement of emptyness check
      isEmptyType (getRange pi) $ unDom a
      -- OLD CODE: isReallyEmptyType $ unArg a
      bindDummy (absName tel)
    A.ConP _ (A.AmbQ [c]) qs -> do -- eta expanded record pattern
      Def r es <- reduce (unEl $ unDom a)
      let Just vs = allApplyElims es
      ftel     <- (`apply` vs) <$> getRecordFieldTypes r
      con      <- getConHead c
      let n   = size ftel
          eta = Con con [ var i <$ (namedThing <$> setArgColors [] q) | (q, i) <- zip qs [n - 1, n - 2..0] ]
          -- ^ TODO guilhem
      bindLHSVars (qs ++ ps) (ftel `abstract` absApp (raise (size ftel) tel) eta) ret
    A.ConP{}        -> __IMPOSSIBLE__
    A.DefP{}        -> __IMPOSSIBLE__
    A.AsP{}         -> __IMPOSSIBLE__
    A.DotP{}        -> __IMPOSSIBLE__
    A.LitP{}        -> __IMPOSSIBLE__
    A.PatternSynP{} -> __IMPOSSIBLE__
    where
      bindDummy s = do
        x <- if isUnderscore s then freshNoName_ else freshName_ ("." ++ argNameToString s)
        addContext (x, a) $ bindLHSVars ps (absBody tel) ret

-- | Bind as patterns
bindAsPatterns :: [AsBinding] -> TCM a -> TCM a
bindAsPatterns []                ret = ret
bindAsPatterns (AsB x v a : asb) ret = do
  reportSDoc "tc.lhs.as" 10 $ text "as pattern" <+> prettyTCM x <+>
    sep [ text ":" <+> prettyTCM a
        , text "=" <+> prettyTCM v
        ]
  addLetBinding defaultArgInfo x v a $ bindAsPatterns asb ret

-- | Result of checking the LHS of a clause.
data LHSResult = LHSResult
  { lhsVarTele      :: Telescope
    -- ^ Δ : The types of the pattern variables, in internal dependency order.
    -- Corresponds to 'clauseTel'.
  , lhsPatterns     :: [I.NamedArg Pattern]
    -- ^ The patterns in internal syntax.
  , lhsBodyType     :: I.Arg Type
    -- ^ The type of the body. Is @bσ@ if @Γ@ is defined.
    -- 'Irrelevant' to indicate the rhs must be checked in irrelevant mode.
  , lhsPermutation  :: Permutation
    -- ^ The permutation from pattern vars to @Δ@.
    -- Corresponds to 'clausePerm'.
  }

instance InstantiateFull LHSResult where
  instantiateFull' (LHSResult tel ps t perm) = LHSResult
    <$> instantiateFull' tel
    <*> instantiateFull' ps
    <*> instantiateFull' t
    <*> return perm

-- | Check a LHS. Main function.
--
--   @checkLeftHandSide a ps a ret@ checks that user patterns @ps@ eliminate
--   the type @a@ of the defined function, and calls continuation @ret@
--   if successful.

checkLeftHandSide
  :: (Maybe r -> Call)
     -- ^ Trace, e.g. @CheckPatternShadowing clause@
  -> Maybe QName
     -- ^ The name of the definition we are checking.
  -> [A.NamedArg A.Pattern]
     -- ^ The patterns.
  -> Type
     -- ^ The expected type @a = Γ → b@.
  -> (LHSResult -> TCM a)
     -- ^ Continuation.
  -> TCM a
checkLeftHandSide c f ps a ret = do
  problem0 <- problemFromPats ps a
  -- Andreas, 2013-03-15 deactivating the following test allows
  -- flexible arity
  -- unless (noProblemRest problem) $ typeError $ TooManyArgumentsInLHS a

  -- doing the splits:
  LHSState problem@(Problem ps (perm, qs) delta rest) sigma dpi asb
    <- checkLHS f $ LHSState problem0 idS [] []

  unless (null $ restPats rest) $ typeError $ TooManyArgumentsInLHS a

  noShadowingOfConstructors c problem

  noPatternMatchingOnCodata qs

  reportSDoc "tc.lhs.top" 10 $
    vcat [ text "checked lhs:"
         , nest 2 $ vcat
           [ text "ps    = " <+> fsep (map prettyA ps)
           , text "perm  = " <+> text (show perm)
           , text "delta = " <+> prettyTCM delta
           , text "dpi   = " <+> brackets (fsep $ punctuate comma $ map prettyTCM dpi)
           , text "asb   = " <+> brackets (fsep $ punctuate comma $ map prettyTCM asb)
           , text "qs    = " <+> text (show qs)
           ]
         ]

  let b' = restType rest
  bindLHSVars (filter (isNothing . isProjP) ps) delta $ bindAsPatterns asb $ do
    reportSDoc "tc.lhs.top" 10 $ text "bound pattern variables"
    reportSDoc "tc.lhs.top" 10 $ nest 2 $ text "type  = " <+> prettyTCM b'

    -- Check dot patterns
    mapM_ checkDotPattern dpi

    lhsResult <- return $ LHSResult delta qs b' perm
    applyRelevanceToContext (getRelevance b') $ ret lhsResult

-- | The loop (tail-recursive): split at a variable in the problem until problem is solved
checkLHS
  :: Maybe QName       -- ^ The name of the definition we are checking.
  -> LHSState          -- ^ The current state.
  -> TCM LHSState      -- ^ The final state after all splitting is completed
checkLHS f st@(LHSState problem sigma dpi asb) = do

  problem <- insertImplicitProblem problem
  -- Note: inserting implicits no longer preserve solvedness,
  -- since we might insert eta expanded record patterns.
  if isSolvedProblem problem then return $ st { lhsProblem = problem } else do

  unlessM (optPatternMatching <$> gets getPragmaOptions) $
    typeError $ GenericError $ "Pattern matching is disabled"

  sp <- runListT $ splitProblem f problem
  reportSDoc "tc.lhs.split" 20 $ text "splitting completed"
  foldListT trySplit nothingToSplit $ ListT $ return sp
  where

    nothingToSplit = do
      reportSLn "tc.lhs.split" 50 $ "checkLHS: nothing to split in problem " ++ show problem
      nothingToSplitError problem

    -- Split problem rest (projection pattern)
    trySplit (SplitRest projPat projType) _ = do

      -- Compute the new problem
      let Problem ps1 (iperm, ip) delta (ProblemRest (p:ps2) b) = problem
          -- ps'      = ps1 ++ [p]
          ps'      = ps1 -- drop the projection pattern (already splitted)
          rest     = ProblemRest ps2 (projPat $> projType)
          ip'      = ip ++ [fmap (Named Nothing . ProjP) projPat]
          problem' = Problem ps' (iperm, ip') delta rest
      -- Jump the trampolin
      st' <- updateProblemRest (LHSState problem' sigma dpi asb)
      -- If the field is irrelevant, we need to continue in irr. cxt.
      -- (see Issue 939).
      applyRelevanceToContext (getRelevance projPat) $ do
        checkLHS f st'

    -- Split on literal pattern
    trySplit (Split p0 xs (Arg _ (LitFocus lit iph hix a)) p1) _ = do

      -- plug the hole with a lit pattern
      let ip    = plugHole (LitP lit) iph
          iperm = expandP hix 0 $ fst (problemOutPat problem)

      -- substitute the literal in p1 and sigma and dpi and asb
      let delta1 = problemTel p0
          delta2 = absApp (fmap problemTel p1) (Lit lit)
          rho    = liftS (size delta2) $ singletonS (Lit lit)
          -- rho    = [ var i | i <- [0..size delta2 - 1] ]
          --       ++ [ raise (size delta2) $ Lit lit ]
          --       ++ [ var i | i <- [size delta2 ..] ]
          sigma'   = applySubst rho sigma
          dpi'     = applySubst rho dpi
          asb0     = applySubst rho asb
          ip'      = applySubst rho ip
          rest'    = applySubst rho (problemRest problem)

      -- Compute the new problem
      let ps'      = problemInPat p0 ++ problemInPat (absBody p1)
          delta'   = abstract delta1 delta2
          problem' = Problem ps' (iperm, ip') delta' rest'
          asb'     = raise (size delta2) (map (\x -> AsB x (Lit lit) a) xs) ++ asb0
      st' <- updateProblemRest (LHSState problem' sigma' dpi' asb')
      checkLHS f st'

    -- Split on constructor pattern

    trySplit (Split p0 xs focus@(Arg info Focus{}) p1) tryNextSplit = do
      res <- trySplitConstructor p0 xs focus p1
      case res of
        -- Success.  Continue checking LHS.
        Unifies st'    -> checkLHS f st'
        -- Mismatch.  Report and abort.
        NoUnify  tcerr -> throwError tcerr
        -- Unclear situation.  Try next split.
        -- If no split works, give error from first split.
        -- This is conservative, but might not be the best behavior.
        -- It might be better to collect all the errors and print all of them.
        DontKnow tcerr -> tryNextSplit `catchError` \ _ -> throwError tcerr

    whenUnifies
      :: UnificationResult' a
      -> (a -> TCM (UnificationResult' b))
      -> TCM (UnificationResult' b)
    whenUnifies res cont = do
      case res of
        Unifies a      -> cont a
        NoUnify  tcerr -> return $ NoUnify  tcerr
        DontKnow tcerr -> return $ DontKnow tcerr

    trySplitConstructor p0 xs (Arg info LitFocus{}) p1 = __IMPOSSIBLE__
    trySplitConstructor p0 xs (Arg info
             (Focus { focusCon      = c
                    , focusImplicit = impl
                    , focusConArgs  = qs
                    , focusRange    = r
                    , focusOutPat   = iph
                    , focusHoleIx   = hix
                    , focusDatatype = d
                    , focusParams   = vs
                    , focusIndices  = ws
                    , focusType     = a
                    }
             )) p1 = do
      traceCall (CheckPattern (A.ConP (ConPatInfo impl $ PatRange r) (A.AmbQ [c]) qs)
                                       (problemTel p0)
                                       (El Prop $ Def d $ map Apply $ vs ++ ws)) $ do

      let delta1 = problemTel p0
      let typeOfSplitVar = Arg info a

      reportSDoc "tc.lhs.split" 10 $ sep
        [ text "checking lhs"
        , nest 2 $ text "tel =" <+> prettyTCM (problemTel problem)
        , nest 2 $ text "rel =" <+> (text $ show $ argInfoRelevance info)
        ]

      reportSDoc "tc.lhs.split" 15 $ sep
        [ text "split problem"
        , nest 2 $ vcat
          [ text "delta1 = " <+> prettyTCM delta1
          , text "typeOfSplitVar =" <+> prettyTCM typeOfSplitVar
          , text "focusOutPat =" <+> (text . show) iph
          , text "delta2 = " <+> prettyTCM (problemTel $ absBody p1)
          ]
        ]

      c <- (`withRangeOf` c) <$> getConForm c
      ca <- defType <$> getConInfo c

      reportSDoc "tc.lhs.split" 20 $ nest 2 $ vcat
        [ text "ca =" <+> prettyTCM ca
        , text "vs =" <+> prettyList (map prettyTCM vs)
        ]

      -- Lookup the type of the constructor at the given parameters
      let a = ca `piApply` vs

      -- It will end in an application of the datatype
      (gamma', ca, d', us) <- do
        TelV gamma' ca@(El _ def) <- telView a
        let Def d' es = ignoreSharing def
            Just us   = allApplyElims es
        return (gamma', ca, d', us)

      -- This should be the same datatype as we split on
      unless (d == d') $ typeError $ ShouldBeApplicationOf ca d'

      -- reportSDoc "tc.lhs.top" 20 $ nest 2 $ vcat
      --   [ text "gamma' =" <+> text (show gamma')
      --   ]

      -- Andreas 2010-09-07  propagate relevance info to new vars
      let updRel = composeRelevance (getRelevance info)
      gamma' <- return $ mapRelevance updRel <$> gamma'

      -- Insert implicit patterns
      qs' <- insertImplicitPatterns ExpandLast qs gamma'

      unless (size qs' == size gamma') $
        typeError $ WrongNumberOfConstructorArguments (conName c) (size gamma') (size qs')

      let gamma = useNamesFromPattern qs' gamma'

      -- Get the type of the datatype.
      da <- (`piApply` vs) . defType <$> getConstInfo d

      -- Compute the flexible variables
      flex <- flexiblePatterns (problemInPat p0 ++ qs')

      -- Compute the constructor indices by dropping the parameters
      let us' = drop (size vs) us

      reportSDoc "tc.lhs.top" 15 $ addCtxTel delta1 $
        sep [ text "preparing to unify"
            , nest 2 $ vcat
              [ text "c      =" <+> prettyTCM c <+> text ":" <+> prettyTCM a
              , text "d      =" <+> prettyTCM d <+> text ":" <+> prettyTCM da
              , text "gamma  =" <+> prettyTCM gamma
              , text "gamma' =" <+> prettyTCM gamma'
              , text "vs     =" <+> brackets (fsep $ punctuate comma $ map prettyTCM vs)
              , text "us'    =" <+> brackets (fsep $ punctuate comma $ map prettyTCM us')
              , text "ws     =" <+> brackets (fsep $ punctuate comma $ map prettyTCM ws)
              ]
            ]

      -- Unify constructor target and given type (in Δ₁Γ)
      res <- addCtxTel (delta1 `abstract` gamma) $
              unifyIndices flex (raise (size gamma) da) us' (raise (size gamma) ws)
      whenUnifies res $ \ sub0 -> do

      -- Andreas 2014-11-25  clear 'Forced' and 'Unused'
      -- Andreas 2015-01-19  ... only after unification
      gamma <- return $ mapRelevance ignoreForced <$> gamma

      -- We should substitute c ys for x in Δ₂ and sigma
      let ys     = teleArgs gamma
          delta2 = absApp (raise (size gamma) $ fmap problemTel p1) (Con c ys)
          rho0   = liftS (size delta2) $ consS (Con c ys) $ raiseS (size gamma)
          -- rho0 = [ var i | i <- [0..size delta2 - 1] ]
          --     ++ [ raise (size delta2) $ Con c ys ]
          --     ++ [ var i | i <- [size delta2 + size gamma ..] ]
          sigma0 = applySubst rho0 sigma
          dpi0   = applySubst rho0 dpi
          asb0   = applySubst rho0 asb
          rest0  = applySubst rho0 (problemRest problem)

      reportSDoc "tc.lhs.top" 15 $ addCtxTel (delta1 `abstract` gamma) $ nest 2 $ vcat
        [ text "delta2 =" <+> prettyTCM delta2
        , text "sub0   =" <+> brackets (fsep $ punctuate comma $ map (maybe (text "_") prettyTCM) sub0)
        ]
      reportSDoc "tc.lhs.top" 15 $ addCtxTel (delta1 `abstract` gamma `abstract` delta2) $
        nest 2 $ vcat
          [ text "dpi0 = " <+> brackets (fsep $ punctuate comma $ map prettyTCM dpi0)
          , text "asb0 = " <+> brackets (fsep $ punctuate comma $ map prettyTCM asb0)
          ]

      -- Andreas, 2010-09-09, save the type.
      -- It is relative to delta1, but it should be relative to
      -- all variables which will be bound by patterns.
      -- Thus, it has to be raised by 1 (the "hole" variable)
      -- plus the length of delta2 (the variables coming after the hole).
      let storedPatternType = raise (1 + size delta2) typeOfSplitVar
      -- Also remember if we are a record pattern and from an implicit pattern.
      isRec <- isRecord d
      let cpi = ConPatternInfo (isRec $> impl) (Just storedPatternType)

      -- Plug the hole in the out pattern with c ys
      let ysp = map (argFromDom . fmap (namedVarP . fst)) $ telToList gamma
          ip  = plugHole (ConP c cpi ysp) iph
          ip0 = applySubst rho0 ip

      -- Δ₁Γ ⊢ sub0, we need something in Δ₁ΓΔ₂
      -- Also needs to be padded with Nothing's to have the right length.
      let pad n xs x = xs ++ replicate (max 0 $ n - size xs) x
          newTel = problemTel p0 `abstract` (gamma `abstract` delta2)
          sub    = replicate (size delta2) Nothing ++
                   pad (size delta1 + size gamma) (raise (size delta2) sub0) Nothing

      reportSDoc "tc.lhs.top" 15 $ nest 2 $ vcat
        [ text "newTel =" <+> prettyTCM newTel
        , addCtxTel newTel $ text "sub =" <+> brackets (fsep $ punctuate comma $ map (maybe (text "_") prettyTCM) sub)
        , text "ip   =" <+> text (show ip)
        , text "ip0  =" <+> text (show ip0)
        ]
      reportSDoc "tc.lhs.top" 15 $ nest 2 $ vcat
        [ text "rho0 =" <+> text (show rho0)
        ]

      -- Instantiate the new telescope with the given substitution
      (delta', perm, rho, instTypes) <- instantiateTel sub newTel


      reportSDoc "tc.lhs.inst" 12 $
        vcat [ sep [ text "instantiateTel"
                   , nest 4 $ brackets $ fsep $ punctuate comma $ map (maybe (text "_") prettyTCM) sub
                   , nest 4 $ prettyTCM newTel
                   ]
             , nest 2 $ text "delta' =" <+> prettyTCM delta'
             , nest 2 $ text "perm   =" <+> text (show perm)
             , nest 2 $ text "itypes =" <+> fsep (punctuate comma $ map prettyTCM instTypes)
             ]

{-          -- Andreas, 2010-09-09
      -- temporary error message to find non-id perms
      let sorted (Perm _ xs) = xs == List.sort xs
      unless (sorted (perm)) $ typeError $ GenericError $ "detected proper permutation " ++ show perm
-}
      -- Compute the new dot pattern instantiations
      let ps0'   = problemInPat p0 ++ qs' ++ problemInPat (absBody p1)

      reportSDoc "tc.lhs.top" 15 $ nest 2 $ vcat
        [ text "subst rho sub =" <+> brackets (fsep $ punctuate comma $ map (maybe (text "_") prettyTCM) (applySubst rho sub))
        , text "ps0'  =" <+> brackets (fsep $ punctuate comma $ map prettyA ps0')
        ]

      newDpi <- dotPatternInsts ps0' (applySubst rho sub) instTypes

      -- The final dpis and asbs are the new ones plus the old ones substituted by ρ
      let dpi' = applySubst rho dpi0 ++ newDpi
          asb' = applySubst rho $ asb0 ++ raise (size delta2) (map (\x -> AsB x (Con c ys) ca) xs)

      reportSDoc "tc.lhs.top" 15 $ nest 2 $ vcat
        [ text "dpi' = " <+> brackets (fsep $ punctuate comma $ map prettyTCM dpi')
        , text "asb' = " <+> brackets (fsep $ punctuate comma $ map prettyTCM asb')
        ]

      -- Apply the substitution to the type
      let sigma'   = applySubst rho sigma0
          rest'    = applySubst rho rest0

      reportSDoc "tc.lhs.inst" 15 $
        nest 2 $ text "ps0 = " <+> brackets (fsep $ punctuate comma $ map prettyA ps0')

      -- Permute the in patterns
      let ps'  = permute perm ps0'

     -- Compute the new permutation of the out patterns. This is the composition of
      -- the new permutation with the expansion of the old permutation to
      -- reflect the split.
      let perm'  = expandP hix (size gamma) $ fst (problemOutPat problem)
          iperm' = perm `composeP` perm'

      -- Instantiate the out patterns
      let ip'    = instantiatePattern sub perm' ip0
          newip  = applySubst rho ip'

      -- Construct the new problem
      let problem' = Problem ps' (iperm', newip) delta' rest'

      reportSDoc "tc.lhs.top" 12 $ sep
        [ text "new problem"
        , nest 2 $ vcat
          [ text "ps'    = " <+> fsep (map prettyA ps')
          , text "delta' = " <+> prettyTCM delta'
          ]
        ]

      reportSDoc "tc.lhs.top" 14 $ nest 2 $ vcat
        [ text "perm'  =" <+> text (show perm')
        , text "iperm' =" <+> text (show iperm')
        ]
      reportSDoc "tc.lhs.top" 14 $ nest 2 $ vcat
        [ text "ip'    =" <+> text (show ip')
        , text "newip  =" <+> text (show newip)
        ]

      -- if rest type reduces,
      -- extend the split problem by previously not considered patterns
      st'@(LHSState problem'@(Problem ps' (iperm', ip') delta' rest')
                    sigma' dpi' asb')
        <- updateProblemRest $ LHSState problem' sigma' dpi' asb'

      reportSDoc "tc.lhs.top" 12 $ sep
        [ text "new problem from rest"
        , nest 2 $ vcat
          [ text "ps'    = " <+> fsep (map prettyA ps')
          , text "delta' = " <+> prettyTCM delta'
          , text "ip'    =" <+> text (show ip')
          , text "iperm' =" <+> text (show iperm')
          ]
        ]
      return $ Unifies st'


-- | Ensures that we are not performing pattern matching on codata.

noPatternMatchingOnCodata :: [I.NamedArg Pattern] -> TCM ()
noPatternMatchingOnCodata = mapM_ (check . namedArg)
  where
  check (VarP {})   = return ()
  check (DotP {})   = return ()
  check (ProjP{})   = return ()
  check (LitP {})   = return ()  -- Literals are assumed not to be coinductive.
  check (ConP con _ ps) = do
    TelV _ t <- telView' . defType <$> do getConstInfo $ conName con
    c <- isCoinductive t
    case c of
      Nothing    -> __IMPOSSIBLE__
      Just False -> mapM_ (check . namedArg) ps
      Just True  -> typeError $
        GenericError "Pattern matching on coinductive types is not allowed"