{-# LANGUAGE CPP #-}

module Agda.TypeChecking.Rules.LHS where

import Data.Maybe
import qualified Data.List as List

import Control.Applicative
import Control.Monad

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

import Agda.TypeChecking.Monad
import Agda.TypeChecking.Pretty
import Agda.TypeChecking.Records -- isRecord
import Agda.TypeChecking.Reduce
import Agda.TypeChecking.Substitute hiding (Substitution)
import Agda.TypeChecking.Telescope
import Agda.TypeChecking.Conversion
import Agda.TypeChecking.Constraints
import Agda.TypeChecking.Irrelevance
import Agda.TypeChecking.Primitive (constructorForm)
import {-# SOURCE #-} Agda.TypeChecking.Empty (isReallyEmptyType)
import Agda.TypeChecking.Telescope (renamingR, teleArgs)

import Agda.TypeChecking.Rules.Term (checkExpr)
import Agda.TypeChecking.Rules.LHS.Problem
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.Permutation
import Agda.Utils.Size
import Agda.Utils.Monad

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

data DotPatternInst = DPI A.Expr Term Type
data AsBinding      = AsB Name Term Type

instance Subst DotPatternInst where
  substs us      (DPI e v a) = uncurry (DPI e) $ substs us (v,a)
  substUnder n u (DPI e v a) = uncurry (DPI e) $ substUnder n u (v,a)

instance PrettyTCM DotPatternInst where
  prettyTCM (DPI e v a) = sep [ prettyA e <+> text "="
                              , nest 2 $ prettyTCM v <+> text ":"
                              , nest 2 $ prettyTCM a
                              ]

instance Subst AsBinding where
  substs us      (AsB x v a) = uncurry (AsB x) $ substs us (v, a)
  substUnder n u (AsB x v a) = uncurry (AsB x) $ substUnder n u (v, a)

instance Raise AsBinding where
  raiseFrom m k (AsB x v a) = uncurry (AsB x) $ raiseFrom m k (v, a)
  renameFrom m k (AsB x v a) = uncurry (AsB x) $ renameFrom m k (v, a)

instance PrettyTCM AsBinding where
  prettyTCM (AsB x v a) =
    sep [ prettyTCM x <> text "@" <> parens (prettyTCM v)
        , nest 2 $ text ":" <+> prettyTCM a
        ]

-- | 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 :: [NamedArg A.Pattern] -> FlexibleVars
flexiblePatterns nps = [ i | (i, p) <- zip [0..] $ reverse ps, flexible p ]
  where
    ps = map (namedThing . unArg) nps
    flexible (A.DotP _ _)    = True
    flexible (A.ImplicitP _) = True
    flexible _               = False

-- | Compute the dot pattern instantiations.
dotPatternInsts :: [NamedArg A.Pattern] -> Substitution -> [Type] -> [DotPatternInst]
dotPatternInsts ps s as = dpi (map (namedThing . unArg) 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 []       _             _       = []
    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
        _           -> __IMPOSSIBLE__

instantiatePattern :: Substitution -> Permutation -> [Arg Pattern] -> [Arg Pattern]
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
    hps = permute perm $ allHoles ps
    inst Nothing  hps = Nothing
    inst (Just t) hps = Just $ plugHole (DotP t) hps

    merge Nothing   ps = ps
    merge (Just qs) ps = zipWith mergeA qs ps
      where
        mergeA a1 a2 = a1 { unArg = mergeP (unArg a1) (unArg a2) }
        mergeP (DotP s)  (DotP t)
          | s == t                    = DotP s
          | otherwise                 = __IMPOSSIBLE__
        mergeP (DotP t)  (VarP _)     = DotP t
        mergeP (VarP _)  (DotP t)     = DotP t
        mergeP (DotP _)  _            = __IMPOSSIBLE__
        mergeP _         (DotP _)     = __IMPOSSIBLE__
        mergeP (ConP c1 mt1 ps) (ConP c2 mt2 qs)
          | c1 == c2                  = ConP (c1 `withRangeOf` c2) (mplus mt1 mt2) $ 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__

-- | Check if a problem is solved. That is, if the patterns are all variables.
isSolvedProblem :: Problem -> Bool
isSolvedProblem = all (isVar . snd . asView . namedThing . unArg) . problemInPat
  where
    isVar (A.VarP _)      = True
    isVar (A.WildP _)     = True
    isVar (A.ImplicitP _) = True
    isVar (A.AbsurdP _)   = True
    isVar _               = 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
  :: A.Clause
     -- ^ The entire clause (used for error reporting).
  -> Problem -> TCM ()
noShadowingOfConstructors c problem =
  traceCall (CheckPatternShadowing c) $ do
    let pat = map (snd . asView . namedThing . unArg) $
                  problemInPat problem
        tel = map (unEl . snd . unArg) $ telToList $ problemTel problem
    zipWithM' noShadowing pat tel
    return ()
  where
  noShadowing (A.WildP     {}) t = return ()
  noShadowing (A.AbsurdP   {}) t = return ()
  noShadowing (A.ImplicitP {}) t = return ()
  noShadowing (A.ConP      {}) t = __IMPOSSIBLE__
  noShadowing (A.DefP      {}) t = __IMPOSSIBLE__
  noShadowing (A.AsP       {}) t = __IMPOSSIBLE__
  noShadowing (A.DotP      {}) t = __IMPOSSIBLE__
  noShadowing (A.LitP      {}) t = __IMPOSSIBLE__
  noShadowing (A.VarP x)       t = do
    t <- normalise t
    case t of
      Def t _ -> do
        d <- theDef <$> getConstInfo t
        case d of
          Datatype { dataCons = cs } -> do
            let ns = map (\c -> (c, A.nameConcrete $ A.qnameName c)) cs
                match x = catMaybes $
                            map (\(c, n) -> if A.nameConcrete x == n
                                            then Just c else Nothing) ns
            case match x of
              []      -> return ()
              (c : _) -> setCurrentRange (getRange x) $
                typeError $ PatternShadowsConstructor x c
          Axiom       {} -> return ()
          Function    {} -> return ()
          Record      {} -> return ()
          Constructor {} -> __IMPOSSIBLE__
          Primitive   {} -> __IMPOSSIBLE__
      Var   {} -> return ()
      Pi    {} -> return ()
      Sort  {} -> return ()
      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__

-- | Check that a dot pattern matches it's instantiation.
checkDotPattern :: DotPatternInst -> TCM ()
checkDotPattern (DPI e v 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
        ]
  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', or 'A.ImplicitP' and the telescope should have
--   the same size as the pattern list.
bindLHSVars :: [NamedArg A.Pattern] -> Telescope -> TCM a -> TCM a
bindLHSVars []       (ExtendTel _ _)   _   = __IMPOSSIBLE__
bindLHSVars (_ : _)   EmptyTel         _   = __IMPOSSIBLE__
bindLHSVars []        EmptyTel         ret = ret
bindLHSVars (p : ps) (ExtendTel a tel) ret =
  case namedThing $ unArg p of
    A.VarP x      -> addCtx x a $ bindLHSVars ps (absBody tel) ret
    A.WildP _     -> bindDummy (absName tel)
    A.ImplicitP _ -> bindDummy (absName tel)
    A.AbsurdP _   -> do
      isReallyEmptyType $ unArg a
      bindDummy (absName tel)
    _             -> __IMPOSSIBLE__
    where
      name "_" = freshNoName_
      name s   = freshName_ ("." ++ s)
      bindDummy s = do
        x <- name s
        addCtx 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 Relevant x v a $ bindAsPatterns asb ret

-- | Rename the variables in a telescope using the names from a given pattern
useNamesFromPattern :: [NamedArg A.Pattern] -> Telescope -> Telescope
useNamesFromPattern ps = telFromList . zipWith ren (toPats ps ++ repeat dummy) . telToList
  where
    dummy = A.WildP __IMPOSSIBLE__
    ren (A.VarP x) (Arg NotHidden r (_, a)) = Arg NotHidden r (show x, a)
    ren _ a = a
    toPats = map (namedThing . unArg)

-- | Check a LHS. Main function.
checkLeftHandSide
  :: A.Clause
     -- ^ The entire clause.
  -> [NamedArg A.Pattern]
     -- ^ The patterns.
  -> Type
     -- ^ The expected type.
  -> (Telescope -> Telescope -> [Term] -> [String] -> [Arg Pattern]
      -> Type -> Permutation -> TCM a)
     -- ^ Continuation.
  -> TCM a
checkLeftHandSide c ps a ret = do
  TelV tel0' b0 <- telView a
  ps <- insertImplicitPatterns ps tel0'
  unless (size tel0' >= size ps) $ typeError $ TooManyArgumentsInLHS (size ps) a
  let tel0     = useNamesFromPattern ps tel0'
      (as, bs) = splitAt (size ps) $ telToList tel0
      gamma    = telFromList as
      b        = telePi (telFromList bs) b0

      -- internal patterns start as all variables
      ips      = map (fmap (VarP . fst)) as

      problem  = Problem ps (idP $ size ps, ips) gamma

  reportSDoc "tc.lhs.top" 10 $
    vcat [ text "checking lhs:"
	 , nest 2 $ vcat
	   [ text "ps    =" <+> fsep (map prettyA ps)
	   , text "a     =" <+> (prettyTCM =<< normalise a)
	   , text "a'    =" <+> prettyTCM (telePi tel0  b0)
	   , text "a''   =" <+> prettyTCM (telePi tel0' b0)
           , text "xs    =" <+> text (show $ map (fst . unArg) as)
	   , text "tel0  =" <+> prettyTCM tel0
	   , text "b0    =" <+> prettyTCM b0
	   , text "gamma =" <+> prettyTCM gamma
	   , text "b     =" <+> addCtxTel gamma (prettyTCM b)
	   ]
	 ]

  let idsub = [ Var i [] | i <- [0..] ]

  (Problem ps (perm, qs) delta, sigma, dpi, asb) <- checkLHS problem idsub [] []
  let b' = substs sigma b

  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)
	   ]
         ]
  bindLHSVars ps delta $ bindAsPatterns asb $ do
    reportSDoc "tc.lhs.top" 10 $ nest 2 $ text "type  = " <+> prettyTCM b'

    -- Check dot patterns
    mapM_ checkDotPattern dpi

    let rho = renamingR perm -- I'm not certain about this...
        Perm n _ = perm
        xs  = [ "h" ++ show n | n <- [0..n - 1] ]
    ret gamma delta rho xs qs b' perm
  where
    checkLHS :: Problem -> [Term] -> [DotPatternInst] -> [AsBinding] ->
                TCM (Problem, [Term], [DotPatternInst], [AsBinding])
    checkLHS problem sigma dpi asb
      | isSolvedProblem problem = do
        problem <- insertImplicitProblem problem -- inserting implicit patterns preserves solvedness
        noShadowingOfConstructors c problem
        return (problem, sigma, dpi, asb)
      | otherwise               = do
        sp <- splitProblem =<< insertImplicitProblem problem
        reportSDoc "tc.lhs.top" 20 $ text "splitting completed"
        case sp of
          Left NothingToSplit   -> nothingToSplitError problem
          Left (SplitPanic err) -> __IMPOSSIBLE__

          -- Split on literal pattern
          Right (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 (fromIntegral 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    = [ var i | i <- [0..size delta2 - 1] ]
                      ++ [ raise (size delta2) $ Lit lit ]
                      ++ [ var i | i <- [size delta2 ..] ]
                  where
                    var i = Var i []
                sigma'   = substs rho sigma
                dpi'     = substs rho dpi
                asb0     = substs rho asb
                ip'      = substs rho ip

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

          -- Split on constructor pattern
          Right (Split p0 xs (Arg h rel
                  ( Focus { focusCon      = c
                          , focusConArgs  = qs
                          , focusRange    = r
                          , focusOutPat   = iph
                          , focusHoleIx   = hix
                          , focusDatatype = d
                          , focusParams   = vs
                          , focusIndices  = ws
                          , focusType     = a
                          }
                  )) p1
                ) -> traceCall (CheckPattern (A.ConP (PatRange r) (A.AmbQ [c]) qs)
                                             (problemTel p0)
                                             (El Prop $ Def d $ vs ++ ws)) $ do

            let delta1 = problemTel p0
            let typeOfSplitVar = Arg h rel a

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

            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)
                ]
              ]

            Con c' [] <- constructorForm =<< normalise (Con c [])
            c  <- return $ c' `withRangeOf` c
            ca <- defType <$> getConstInfo c

            reportSDoc "tc.lhs.top" 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
            TelV gamma' ca@(El _ (Def d' us)) <- telView a

            -- 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
            gamma' <- return $ fmap (applyRelevance rel) gamma'
{-
            reportSDoc "tc.lhs.top" 20 $ nest 2 $ vcat
              [ text "gamma' =" <+> text (show gamma')
              ]
-}
            -- Insert implicit patterns
            qs' <- insertImplicitPatterns qs gamma'

            unless (size qs' == size gamma') $
              typeError $ WrongNumberOfConstructorArguments 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
            let flex = flexiblePatterns (problemInPat p0 ++ qs')

	    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 "ws     =" <+> brackets (fsep $ punctuate comma $ map prettyTCM ws)
		    ]
		  ]

            -- Unify constructor target and given type (in Δ₁Γ)
            sub0 <- addCtxTel (delta1 `abstract` gamma) $
                    unifyIndices_ flex (raise (size gamma) da) (drop (size vs) us) (raise (size gamma) ws)

            -- We should subsitute c ys for x in Δ₂ and sigma
            let ys     = teleArgs gamma
                delta2 = absApp (raise (size gamma) $ fmap problemTel p1) (Con c ys)
                rho0 = [ var i | i <- [0..size delta2 - 1] ]
                    ++ [ raise (size delta2) $ Con c ys ]
                    ++ [ var i | i <- [size delta2 + size gamma ..] ]
                  where
                    var i = Var i []
                sigma0 = substs rho0 sigma
                dpi0   = substs rho0 dpi
                asb0   = substs rho0 asb

            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 a of record pattern.
            -- 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).
            storedPatternType <- ifM (isRecord d)
              (return $ Just $ raise (1 + size delta2) $ typeOfSplitVar)
              (return $ Nothing)

            -- Plug the hole in the out pattern with c ys
            let ysp = map (fmap (VarP . fst)) $ telToList gamma
                ip  = plugHole (ConP c storedPatternType ysp) iph
                ip0 = substs 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 $ take (size delta1 + size gamma + size delta2) rho0)
              ]  -- Andreas, this is showing some inital segment of rho0, not necessarily the most meaningful one

            -- 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)
                newDpi = dotPatternInsts ps0' (substs rho sub) instTypes

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

            -- The final dpis and asbs are the new ones plus the old ones substituted by ρ
            let dpi' = substs rho dpi0 ++ newDpi
                asb' = substs 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'   = substs rho sigma0

            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 (fromIntegral hix) (size gamma) $ fst (problemOutPat problem)
                iperm' = perm `composeP` perm'

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

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

            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)
              ]

            -- Continue splitting
            checkLHS problem' sigma' dpi' asb'

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

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