{-# LANGUAGE NondecreasingIndentation #-}

module Agda.TypeChecking.Rules.LHS
  ( checkLeftHandSide
  , LHSResult(..)
  , bindAsPatterns
  , IsFlexiblePattern(..)
  , DataOrRecord(..)
  , checkSortOfSplitVar
  ) where

import Prelude hiding ( null )

import Data.Function (on)
import Data.Maybe

import Control.Arrow (left, second)
import Control.Monad
import Control.Monad.Except
import Control.Monad.Reader
import Control.Monad.Writer       ( MonadWriter(..), runWriterT )
import Control.Monad.Trans.Maybe

import Data.IntSet (IntSet)
import qualified Data.IntSet as IntSet
import Data.List (findIndex)
import qualified Data.List as List
import Data.Semigroup ( Semigroup )
import qualified Data.Semigroup as Semigroup
import Data.Map (Map)
import qualified Data.Map as Map

import Agda.Interaction.Highlighting.Generate
  ( storeDisambiguatedConstructor, storeDisambiguatedProjection, disambiguateRecordFields)
import Agda.Interaction.Options
import Agda.Interaction.Options.Lenses

import Agda.Syntax.Internal as I hiding (DataOrRecord(..))
import Agda.Syntax.Internal.Pattern
import qualified Agda.Syntax.Abstract as A
import Agda.Syntax.Abstract.Views (asView, deepUnscope)
import Agda.Syntax.Concrete (FieldAssignment'(..),LensInScope(..))
import Agda.Syntax.Common as Common
import Agda.Syntax.Info as A
import Agda.Syntax.Literal
import Agda.Syntax.Position

import Agda.TypeChecking.Monad

import qualified Agda.TypeChecking.Monad.Benchmark as Bench
import Agda.TypeChecking.Conversion
import Agda.TypeChecking.Constraints
import Agda.TypeChecking.CheckInternal (checkInternal)
import Agda.TypeChecking.Datatypes hiding (isDataOrRecordType)
import Agda.TypeChecking.Errors (dropTopLevelModule)
import Agda.TypeChecking.Irrelevance
-- Prevent "Ambiguous occurrence ‘DontKnow’" when loading with ghci.
-- (DontKnow is one of the constructors of ErrorNonEmpty *and* UnifactionResult').
-- We can't explicitly hide just the constructor here because it isn't in the
-- hs-boot file.
import {-# SOURCE #-} Agda.TypeChecking.Empty (ensureEmptyType)
import Agda.TypeChecking.Patterns.Abstract
import Agda.TypeChecking.Pretty
import Agda.TypeChecking.Records hiding (getRecordConstructor)
import Agda.TypeChecking.Reduce
import Agda.TypeChecking.Substitute
import Agda.TypeChecking.Telescope
import Agda.TypeChecking.Telescope.Path
import Agda.TypeChecking.Primitive hiding (Nat)

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

import Agda.Utils.CallStack ( HasCallStack, withCallerCallStack )
import Agda.Utils.Function
import Agda.Utils.Functor
import Agda.Utils.Lens
import Agda.Utils.List
import Agda.Utils.List1 (List1, pattern (:|))
import qualified Agda.Utils.List  as List
import qualified Agda.Utils.List1 as List1
import Agda.Utils.Maybe
import Agda.Utils.Monad
import Agda.Utils.Null
import Agda.Utils.Pretty (prettyShow)
import Agda.Utils.Singleton
import Agda.Utils.Size
import Agda.Utils.Tuple

import Agda.Utils.Impossible
import Agda.Utils.WithDefault
import Agda.TypeChecking.Free (freeIn)

--UNUSED Liang-Ting Chen 2019-07-16
---- | Compute the set of flexible patterns in a list of patterns. The result is
----   the deBruijn indices of the flexible patterns.
--flexiblePatterns :: [NamedArg A.Pattern] -> TCM FlexibleVars
--flexiblePatterns nps = do
--  forMaybeM (zip (downFrom $ length nps) nps) $ \ (i, Arg ai p) -> do
--    runMaybeT $ (\ f -> FlexibleVar (getHiding ai) (getOrigin ai) f (Just i) i) <$> maybeFlexiblePattern p

-- | A pattern is flexible if it is dotted or implicit, or a record pattern
--   with only flexible subpatterns.
class IsFlexiblePattern a where
  maybeFlexiblePattern :: (HasConstInfo m, MonadDebug m) => a -> MaybeT m FlexibleVarKind

  isFlexiblePattern :: (HasConstInfo m, MonadDebug m) => a -> m Bool
  isFlexiblePattern p =
    maybe False notOtherFlex <$> runMaybeT (maybeFlexiblePattern p)
    where
    notOtherFlex = \case
      RecordFlex fls -> all notOtherFlex fls
      ImplicitFlex   -> True
      DotFlex        -> True
      OtherFlex      -> False

instance IsFlexiblePattern A.Pattern where
  maybeFlexiblePattern p = do
    reportSDoc "tc.lhs.flex" 30 $ "maybeFlexiblePattern" <+> prettyA p
    reportSDoc "tc.lhs.flex" 60 $ "maybeFlexiblePattern (raw) " <+> (text . show . deepUnscope) p
    case p of
      A.DotP{}  -> return DotFlex
      A.VarP{}  -> return ImplicitFlex
      A.WildP{} -> return ImplicitFlex
      A.AsP _ _ p -> maybeFlexiblePattern p
      A.ConP _ cs qs | Just c <- getUnambiguous cs ->
        ifM (isNothing <$> isRecordConstructor c) (return OtherFlex) {-else-}
            (maybeFlexiblePattern qs)
      A.LitP{}  -> return OtherFlex
      A.AnnP _ _ p -> maybeFlexiblePattern p
      _ -> mzero

instance IsFlexiblePattern (I.Pattern' a) where
  maybeFlexiblePattern p =
    case p of
      I.DotP{}  -> return DotFlex
      I.ConP _ i ps
        | conPRecord i , PatOSystem <- patOrigin (conPInfo i) -> return ImplicitFlex  -- expanded from ImplicitP
        | conPRecord i -> maybeFlexiblePattern ps
        | otherwise -> mzero
      I.VarP{}  -> mzero
      I.LitP{}  -> mzero
      I.ProjP{} -> mzero
      I.IApplyP{} -> mzero
      I.DefP{} -> mzero -- TODO Andrea check semantics

-- | Lists of flexible patterns are 'RecordFlex'.
instance IsFlexiblePattern a => IsFlexiblePattern [a] where
  maybeFlexiblePattern ps = RecordFlex <$> mapM maybeFlexiblePattern ps

instance IsFlexiblePattern a => IsFlexiblePattern (Arg a) where
  maybeFlexiblePattern = maybeFlexiblePattern . unArg

instance IsFlexiblePattern a => IsFlexiblePattern (Common.Named name a) where
  maybeFlexiblePattern = maybeFlexiblePattern . namedThing

-- | Update the given LHS state:
--   1. simplify problem equations
--   2. rename telescope variables
--   3. introduce trailing patterns
updateLHSState :: LHSState a -> TCM (LHSState a)
updateLHSState st = do
  let tel     = st ^. lhsTel
      problem = st ^. lhsProblem
  eqs' <- addContext tel $ updateProblemEqs $ problem ^. problemEqs
  tel' <- useNamesFromProblemEqs eqs' tel
  updateProblemRest $ set lhsTel tel' $ set (lhsProblem . problemEqs) eqs' st

-- | Update the user patterns in the given problem, simplifying equations
--   between constructors where possible.
updateProblemEqs
 :: [ProblemEq] -> TCM [ProblemEq]
updateProblemEqs eqs = do
  reportSDoc "tc.lhs.top" 20 $ vcat
    [ "updateProblem: equations to update"
    , nest 2 $ if null eqs then "(none)" else vcat $ map prettyTCM eqs
    ]

  eqs' <- updates eqs

  reportSDoc "tc.lhs.top" 20 $ vcat
    [ "updateProblem: new equations"
    , nest 2 $ if null eqs' then "(none)" else vcat $ map prettyTCM eqs'
    ]

  return eqs'

  where

    updates :: [ProblemEq] -> TCM [ProblemEq]
    updates = concat <.> traverse update

    update :: ProblemEq -> TCM [ProblemEq]
    update eq@(ProblemEq A.WildP{} _ _) = return []
    update eq@(ProblemEq p@A.ProjP{} _ _) = typeError $ IllformedProjectionPattern p
    update eq@(ProblemEq p@(A.AsP info x p') v a) =
      (ProblemEq (A.VarP x) v a :) <$> update (ProblemEq p' v a)

    update eq@(ProblemEq p@(A.AnnP _ _ A.WildP{}) v a) = return [eq]
    update eq@(ProblemEq p@(A.AnnP info ty p') v a) =
      (ProblemEq (A.AnnP info ty (A.WildP patNoRange)) v a :) <$> update (ProblemEq p' v a)

    update eq@(ProblemEq p v a) = reduce v >>= constructorForm >>= \case
      Con c ci es -> do
        let vs = fromMaybe __IMPOSSIBLE__ $ allApplyElims es
        -- we should only simplify equations between fully applied constructors
        contype <- getFullyAppliedConType c =<< reduce (unDom a)
        caseMaybe contype (return [eq]) $ \((d,_,pars),b) -> do
        TelV ctel _ <- telViewPath b

        -- Andrea 15/10/2020: propagate modality to constructor arguments
        let updMod = composeModality (getModality a)
        ctel <- return $ mapModality updMod <$> ctel

        let bs = instTel ctel (map unArg vs)

        p <- expandLitPattern p
        case p of
          A.AsP{} -> __IMPOSSIBLE__
          A.AnnP{} -> __IMPOSSIBLE__
          A.ConP cpi ambC ps -> do
            (c',_) <- disambiguateConstructor ambC d pars

            -- Issue #3014: If the constructor is forced but the user wrote a
            -- different constructor,that's an error. We simply keep the
            -- problem equation, this will result in a proper error message later.
            if conName c /= conName c' then return [eq] else do

            -- Insert implicit patterns
            ps <- insertImplicitPatterns ExpandLast ps ctel
            reportSDoc "tc.lhs.imp" 20 $
              "insertImplicitPatternsT returned" <+> fsep (map prettyA ps)

            -- Check argument count and hiding (not just count: #3074)
            let checkArgs [] [] = return ()
                checkArgs (p : ps) (v : vs)
                  | getHiding p == getHiding v = checkArgs ps vs
                  | otherwise                  = setCurrentRange p $ genericDocError =<< do
                      fsep $ pwords ("Expected an " ++ which (getHiding v) ++ " argument " ++
                                     "instead of "  ++ which (getHiding p) ++ " argument") ++
                             [ prettyA p ]
                  where which NotHidden  = "explicit"
                        which Hidden     = "implicit"
                        which Instance{} = "instance"
                checkArgs [] vs = genericDocError =<< do
                    fsep $ pwords "Too few arguments to constructor" ++ [prettyTCM c <> ","] ++
                           pwords ("expected " ++ show n ++ " more explicit "  ++ arguments)
                  where n = length (filter visible vs)
                        arguments | n == 1    = "argument"
                                  | otherwise = "arguments"
                checkArgs (p : _) [] = setCurrentRange p $ genericDocError =<< do
                  fsep $ pwords "Too many arguments to constructor" ++ [prettyTCM c]
            checkArgs ps vs

            updates $ zipWith3 ProblemEq (map namedArg ps) (map unArg vs) bs

          A.RecP pi fs -> do
            axs <- map argFromDom . recFields . theDef <$> getConstInfo d

            -- Andreas, 2018-09-06, issue #3122.
            -- Associate the concrete record field names used in the record pattern
            -- to their counterpart in the record type definition.
            disambiguateRecordFields (map _nameFieldA fs) (map unArg axs)

            let cxs = map (fmap (nameConcrete . qnameName)) axs

            -- In fs omitted explicit fields are replaced by underscores,
            -- and the fields are put in the correct order.
            ps <- insertMissingFieldsFail d (const $ A.WildP patNoRange) fs cxs

            -- We also need to insert missing implicit or instance fields.
            ps <- insertImplicitPatterns ExpandLast ps ctel

            let eqs = zipWith3 ProblemEq (map namedArg ps) (map unArg vs) bs
            updates eqs

          _ -> return [eq]

      Lit l | A.LitP _ l' <- p , l == l' -> return []

      _ | A.EqualP{} <- p -> do
        itisone <- liftTCM primItIsOne
        ifM (tryConversion $ equalTerm (unDom a) v itisone) (return []) (return [eq])

      _ -> return [eq]

    instTel :: Telescope -> [Term] -> [Dom Type]
    instTel EmptyTel _                   = []
    instTel (ExtendTel arg tel) (u : us) = arg : instTel (absApp tel u) us
    instTel ExtendTel{} []               = __IMPOSSIBLE__


-- | Check if a problem is solved.
--   That is, if the patterns are all variables,
--   and there is no 'problemRest'.
isSolvedProblem :: Problem a -> Bool
isSolvedProblem problem = null (problem ^. problemRestPats) &&
  problemAllVariables problem

-- | Check if a problem consists only of variable patterns.
--   (Includes the 'problemRest').
problemAllVariables :: Problem a -> Bool
problemAllVariables problem =
    all isSolved $
      map namedArg (problem ^. problemRestPats) ++ problemInPats problem
  where
    -- need further splitting:
    isSolved A.ConP{}        = False
    isSolved A.LitP{}        = False
    isSolved A.RecP{}        = False  -- record pattern
    -- solved:
    isSolved A.VarP{}        = True
    isSolved A.WildP{}       = True
    isSolved A.DotP{}        = True
    isSolved A.AbsurdP{}     = True
    -- recursive cases
    isSolved (A.AsP _ _ p)   = isSolved p
    isSolved (A.AnnP _ _ p)  = isSolved p
    -- impossible:
    isSolved A.ProjP{}       = __IMPOSSIBLE__
    isSolved A.DefP{}        = __IMPOSSIBLE__
    isSolved A.PatternSynP{} = __IMPOSSIBLE__  -- expanded before
    isSolved A.EqualP{}      = False -- __IMPOSSIBLE__
    isSolved A.WithP{}       = __IMPOSSIBLE__

-- | 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 :: ProblemEq -> TCM ()
noShadowingOfConstructors problem@(ProblemEq p _ (Dom{domInfo = info, unDom = El _ a})) =
  case p of
   A.WildP       {} -> return ()
   A.AbsurdP     {} -> return ()
   A.DotP        {} -> return ()
   A.EqualP      {} -> return ()
   A.AsP _ _ p      -> noShadowingOfConstructors $ problem { problemInPat = p }
   A.AnnP _ _ p     -> noShadowingOfConstructors $ problem { problemInPat = p }
   A.ConP        {} -> __IMPOSSIBLE__
   A.RecP        {} -> __IMPOSSIBLE__
   A.ProjP       {} -> __IMPOSSIBLE__
   A.DefP        {} -> __IMPOSSIBLE__
   A.LitP        {} -> __IMPOSSIBLE__
   A.PatternSynP {} -> __IMPOSSIBLE__
   A.WithP       {} -> __IMPOSSIBLE__
   -- Andreas, 2017-12-01, issue #2859.
   -- Due to parameter refinement, there can be (invisible) variable patterns from module
   -- parameters that shadow constructors.
   -- Thus, only complain about user written variable that shadow constructors.
   A.VarP A.BindName{unBind = x} -> when (getOrigin info == UserWritten) $ do
    reportSDoc "tc.lhs.shadow" 30 $ vcat
      [ text $ "checking whether pattern variable " ++ prettyShow x ++ " shadows a constructor"
      , nest 2 $ "type of variable =" <+> prettyTCM a
      , nest 2 $ "position of variable =" <+> (text . show) (getRange x)
      ]
    reportSDoc "tc.lhs.shadow" 70 $ nest 2 $ "a =" <+> pretty a
    a <- reduce a
    case a 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 (nameConcrete x) c
          AbstractDefn{} -> return ()
            -- Abstract constructors cannot be brought into scope,
            -- even by a bigger import list.
            -- Thus, they cannot be confused with variables.
            -- Alternatively, we could do getConstInfo in ignoreAbstractMode,
            -- then Agda would complain if a variable shadowed an abstract constructor.
          Axiom       {} -> return ()
          DataOrRecSig{} -> return ()
          Function    {} -> return ()
          Record      {} -> return ()
          Constructor {} -> __IMPOSSIBLE__
          GeneralizableVar{} -> __IMPOSSIBLE__
          -- TODO: in the future some stuck primitives might allow constructors
          Primitive   {} -> return ()
          PrimitiveSort{} -> return ()
      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__
      Dummy s _  -> __IMPOSSIBLE_VERBOSE__ s

-- | Check that a dot pattern matches it's instantiation.
checkDotPattern :: DotPattern -> TCM ()
checkDotPattern (Dot e v (Dom{domInfo = info, unDom = a})) =
  traceCall (CheckDotPattern e v) $ do
  reportSDoc "tc.lhs.dot" 15 $
    sep [ "checking dot pattern"
        , nest 2 $ prettyA e
        , nest 2 $ "=" <+> prettyTCM v
        , nest 2 $ ":" <+> prettyTCM a
        ]
  applyModalityToContext info $ do
    u <- checkExpr e a
    reportSDoc "tc.lhs.dot" 50 $
      sep [ "equalTerm"
          , nest 2 $ pretty a
          , nest 2 $ pretty u
          , nest 2 $ pretty v
          ]
    equalTerm a u v

checkAbsurdPattern :: AbsurdPattern -> TCM ()
checkAbsurdPattern (Absurd r a) = ensureEmptyType r a

checkAnnotationPattern :: AnnotationPattern -> TCM ()
checkAnnotationPattern (Ann t a) = do
  reportSDoc "tc.lhs.ann" 15 $
    sep [ "checking type annotation in pattern"
        , nest 2 $ prettyA t
        , nest 2 $ "=" <+> prettyTCM a
        ]
  b <- isType_ t
  equalType a b

-- | After splitting is complete, we transfer the origins
--   We also transfer the locations of absurd patterns, since these haven't
--   been introduced yet in the internal pattern.
transferOrigins :: [NamedArg A.Pattern]
                -> [NamedArg DeBruijnPattern]
                -> TCM [NamedArg DeBruijnPattern]
transferOrigins ps qs = do
  reportSDoc "tc.lhs.origin" 40 $ vcat
    [ "transferOrigins"
    , nest 2 $ vcat
      [ "ps  =   " <+> prettyA ps
      , "qs  =   " <+> pretty qs
      ]
    ]
  transfers ps qs

  where
    transfers :: [NamedArg A.Pattern]
              -> [NamedArg DeBruijnPattern]
              -> TCM [NamedArg DeBruijnPattern]
    transfers [] qs
      | all notVisible qs = return $ map (setOrigin Inserted) qs
      | otherwise         = __IMPOSSIBLE__
    transfers (p : ps) [] = __IMPOSSIBLE__
    transfers (p : ps) (q : qs)
      | matchingArgs p q = do
          q' <- mapNameOf (maybe id (const . Just) $ getNameOf p) -- take NamedName from p if present
              . setOrigin (getOrigin p)
            <$> (traverse $ traverse $ transfer $ namedArg p) q
          (q' :) <$> transfers ps qs
      | otherwise = (setOrigin Inserted q :) <$> transfers (p : ps) qs

    transfer :: A.Pattern -> DeBruijnPattern -> TCM DeBruijnPattern
    transfer p q = case (asView p , q) of

      ((asB , anns , A.ConP pi _ ps) , ConP c (ConPatternInfo i r ft mb l) qs) -> do
        let cpi = ConPatternInfo (PatternInfo PatOCon asB) r ft mb l
        ConP c cpi <$> transfers ps qs

      ((asB , anns , A.RecP pi fs) , ConP c (ConPatternInfo i r ft mb l) qs) -> do
        let Def d _  = unEl $ unArg $ fromMaybe __IMPOSSIBLE__ mb
            axs = map (nameConcrete . qnameName . unArg) (conFields c) `withArgsFrom` qs
            cpi = ConPatternInfo (PatternInfo PatORec asB) r ft mb l
        ps <- insertMissingFieldsFail d (const $ A.WildP patNoRange) fs axs
        ConP c cpi <$> transfers ps qs

      ((asB , anns , p) , ConP c (ConPatternInfo i r ft mb l) qs) -> do
        let cpi = ConPatternInfo (PatternInfo (patOrig p) asB) r ft mb l
        return $ ConP c cpi qs

      ((asB , anns , p) , VarP _ x) -> return $ VarP (PatternInfo (patOrig p) asB) x

      ((asB , anns , p) , DotP _ u) -> return $ DotP (PatternInfo (patOrig p) asB) u

      ((asB , anns , p) , LitP _ l) -> return $ LitP (PatternInfo (patOrig p) asB) l

      _ -> return q

    patOrig :: A.Pattern -> PatOrigin
    patOrig (A.VarP x)      = PatOVar (A.unBind x)
    patOrig A.DotP{}        = PatODot
    patOrig A.ConP{}        = PatOCon
    patOrig A.RecP{}        = PatORec
    patOrig A.WildP{}       = PatOWild
    patOrig A.AbsurdP{}     = PatOAbsurd
    patOrig A.LitP{}        = PatOLit
    patOrig A.EqualP{}      = PatOCon --TODO: origin for EqualP
    patOrig A.AsP{}         = __IMPOSSIBLE__
    patOrig A.ProjP{}       = __IMPOSSIBLE__
    patOrig A.DefP{}        = __IMPOSSIBLE__
    patOrig A.PatternSynP{} = __IMPOSSIBLE__
    patOrig A.WithP{}       = __IMPOSSIBLE__
    patOrig A.AnnP{}        = __IMPOSSIBLE__

    matchingArgs :: NamedArg A.Pattern -> NamedArg DeBruijnPattern -> Bool
    matchingArgs p q
      -- The arguments match if
      -- 1. they are both projections,
      | isJust (A.isProjP p) = isJust (isProjP q)
      -- 2. or they are both visible,
      | visible p && visible q = True
      -- 3. or they have the same hiding and the argument is not named,
      | sameHiding p q && isNothing (getNameOf p) = True
      -- 4. or they have the same hiding and the same name.
      | sameHiding p q && namedSame p q = True
      -- Otherwise this argument was inserted by the typechecker.
      | otherwise = False


-- | If a user-written variable occurs more than once, it should be bound
--   to the same internal variable (or term) in all positions.
--   Returns the list of patterns with the duplicate user patterns removed.
checkPatternLinearity :: [ProblemEq] -> TCM [ProblemEq]
checkPatternLinearity eqs = do
  reportSDoc "tc.lhs.linear" 30 $ "Checking linearity of pattern variables"
  check Map.empty eqs
  where
    check :: Map A.BindName (Term, Type) -> [ProblemEq] -> TCM [ProblemEq]
    check _ [] = return []
    check vars (eq@(ProblemEq p u a) : eqs) = do
      reportSDoc "tc.lhs.linear" 40 $ sep
        [ "linearity: checking pattern "
        , prettyA p
        , " equal to term "
        , prettyTCM u
        , " of type "
        , prettyTCM a
        ]
      case p of
        A.VarP x -> do
          let y = A.unBind x
          reportSLn "tc.lhs.linear" 60 $
            "pattern variable " ++ prettyShow (A.nameConcrete y) ++ " with id " ++ show (A.nameId y)
          case Map.lookup x vars of
            Just (v , b) -> do
              traceCall (CheckPatternLinearityType $ A.nameConcrete y) $
                noConstraints $ equalType (unDom a) b
              traceCall (CheckPatternLinearityValue $ A.nameConcrete y) $
                noConstraints $ equalTerm (unDom a) u v
              check vars eqs
            Nothing -> (eq:) <$> do
              check (Map.insert x (u,unDom a) vars) eqs
        A.AsP _ x p ->
          check vars $ [ProblemEq (A.VarP x) u a, ProblemEq p u a] ++ eqs
        A.AnnP _ _ A.WildP{} -> continue
        A.AnnP r t p -> (ProblemEq (A.AnnP r t (A.WildP patNoRange)) u a:) <$>
          check vars (ProblemEq p u a : eqs)
        A.WildP{}       -> continue
        A.DotP{}        -> continue
        A.AbsurdP{}     -> continue
        A.ConP{}        -> __IMPOSSIBLE__
        A.ProjP{}       -> __IMPOSSIBLE__
        A.DefP{}        -> __IMPOSSIBLE__
        A.LitP{}        -> __IMPOSSIBLE__
        A.PatternSynP{} -> __IMPOSSIBLE__
        A.RecP{}        -> __IMPOSSIBLE__
        A.EqualP{}      -> __IMPOSSIBLE__
        A.WithP{}       -> __IMPOSSIBLE__

      where continue = (eq:) <$> check vars eqs

-- | Construct the context for a left hand side, making up out-of-scope names
--   for unnamed variables.
computeLHSContext :: [Maybe A.Name] -> Telescope -> TCM Context
computeLHSContext = go [] []
  where
    go cxt _ []        tel@ExtendTel{} = do
      reportSDoc "impossible" 10 $
        "computeLHSContext: no patterns left, but tel =" <+> prettyTCM tel
      __IMPOSSIBLE__
    go cxt _ (_ : _)   EmptyTel = __IMPOSSIBLE__
    go cxt _ []        EmptyTel = return cxt
    go cxt taken (x : xs) tel0@(ExtendTel a tel) = do
        name <- maybe (dummyName taken $ absName tel) return x
        let e = (name,) <$> a
        go (e : cxt) (name : taken) xs (absBody tel)

    dummyName taken s =
      if isUnderscore s then freshNoName_
      else setNotInScope <$> freshName_ (argNameToString s)

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

-- | Since with-abstraction can change the type of a variable, we have to
--   recheck the stripped with patterns when checking a with function.
recheckStrippedWithPattern :: ProblemEq -> TCM ()
recheckStrippedWithPattern (ProblemEq p v a) = checkInternal v CmpLeq (unDom a)
  `catchError` \_ -> typeError . GenericDocError =<< vcat
    [ "Ill-typed pattern after with abstraction: " <+> prettyA p
    , "(perhaps you can replace it by `_`?)"
    ]

-- | Result of checking the LHS of a clause.
data LHSResult = LHSResult
  { lhsParameters   :: Nat
    -- ^ The number of original module parameters. These are present in the
    -- the patterns.
  , lhsVarTele      :: Telescope
    -- ^ Δ : The types of the pattern variables, in internal dependency order.
    -- Corresponds to 'clauseTel'.
  , lhsPatterns     :: [NamedArg DeBruijnPattern]
    -- ^ The patterns in internal syntax.
  , lhsHasAbsurd    :: Bool
    -- ^ Whether the LHS has at least one absurd pattern.
  , lhsBodyType     :: Arg Type
    -- ^ The type of the body. Is @bσ@ if @Γ@ is defined.
    -- 'Irrelevant' to indicate the rhs must be checked in irrelevant mode.
  , lhsPatSubst     :: Substitution
    -- ^ Substitution version of @lhsPatterns@, only up to the first projection
    -- pattern. @Δ |- lhsPatSubst : Γ@. Where @Γ@ is the argument telescope of
    -- the function. This is used to update inherited dot patterns in
    -- with-function clauses.
  , lhsAsBindings   :: [AsBinding]
    -- ^ As-bindings from the left-hand side. Return instead of bound since we
    -- want them in where's and right-hand sides, but not in with-clauses
    -- (Issue 2303).
  , lhsPartialSplit :: IntSet
    -- ^ have we done a partial split?
  , lhsIndexedSplit :: Bool
    -- ^ have we split on an indexed type?
  }

instance InstantiateFull LHSResult where
  instantiateFull' (LHSResult n tel ps abs t sub as psplit ixsplit) = LHSResult n
    <$> instantiateFull' tel
    <*> instantiateFull' ps
    <*> instantiateFull' abs
    <*> instantiateFull' t
    <*> instantiateFull' sub
    <*> instantiateFull' as
    <*> pure psplit
    <*> pure ixsplit

-- | 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 :: forall a.
     Call
     -- ^ Trace, e.g. 'CheckLHS' or 'CheckPattern'.
  -> Maybe QName
     -- ^ The name of the definition we are checking.
  -> [NamedArg A.Pattern]
     -- ^ The patterns.
  -> Type
     -- ^ The expected type @a = Γ → b@.
  -> Maybe Substitution
     -- ^ Module parameter substitution from with-abstraction.
  -> [ProblemEq]
     -- ^ Patterns that have been stripped away by with-desugaring.
     -- ^ These should not contain any proper matches.
  -> (LHSResult -> TCM a)
     -- ^ Continuation.
  -> TCM a
checkLeftHandSide call f ps a withSub' strippedPats =
 Bench.billToCPS [Bench.Typing, Bench.CheckLHS] $
 traceCallCPS call $ \ ret -> do

  -- To allow module parameters to be refined by matching, we're adding the
  -- context arguments as wildcard patterns and extending the type with the
  -- context telescope.
  cxt <- map (setOrigin Inserted) . reverse <$> getContext
  let tel = telFromList' prettyShow cxt
      cps = [ unnamed . A.VarP . A.mkBindName . fst <$> argFromDom d
            | d <- cxt ]
      eqs0 = zipWith3 ProblemEq (map namedArg cps) (map var $ downFrom $ size tel) (flattenTel tel)

  let finalChecks :: LHSState a -> TCM a
      finalChecks (LHSState delta qs0 (Problem eqs rps _) b psplit ixsplit) = do

        reportSDoc "tc.lhs.top" 20 $ vcat
          [ "lhs: final checks with remaining equations"
          , nest 2 $ if null eqs then "(none)" else addContext delta $ vcat $ map prettyTCM eqs
          , "qs0 =" <+> addContext delta (prettyTCMPatternList qs0)
          ]

        unless (null rps) __IMPOSSIBLE__

        addContext delta $ do
          mapM_ noShadowingOfConstructors eqs

          -- When working --without-K or --cubical-compatible, we have
          -- to check that the target type can be used at the “ambient”
          -- modality. For --cubical-compatible, this just improves an
          -- error message (printing the type rather than the generated
          -- RHS). For --without-K, it implements the same check without
          -- necessarily generating --cubical code.
          -- The reason for this check is that a clause
          --    foo : x ≡ y → ... → T y
          --    foo refl ... = ...
          -- in Cubical mode, gets elaborated to an extra clause of the
          -- form
          --    foo (transp p φ x) ... = transp (λ i → T (p i)) φ (foo x ...)
          -- (approximately), where T is the target type. That is: to
          -- implement the substitution T[y/x], we use an actual
          -- transport. See #5448.

        arity_a <- arityPiPath a
        -- Compute substitution from the out patterns @qs0@
        let notProj ProjP{} = False
            notProj _       = True
            numPats  = length $ takeWhile (notProj . namedArg) qs0

            -- We have two slightly different cases here: normal function and
            -- with-function. In both cases the goal is to build a substitution
            -- from the context Γ of the previous checkpoint to the current lhs
            -- context Δ:
            --
            --    Δ ⊢ paramSub : Γ
            --
            --  * Normal function, f
            --
            --    Γ = cxt = module parameter telescope of f
            --    Ψ = non-parameter arguments of f (we have f : Γ Ψ → A)
            --    Δ   ⊢ patSub  : Γ Ψ
            --    Γ Ψ ⊢ weakSub : Γ
            --    paramSub = patSub ∘ weakSub
            --
            --  * With-function
            --
            --    Γ = lhs context of the parent clause (cxt = [])
            --    Ψ = argument telescope of with-function
            --    Θ = inserted implicit patterns not in Ψ (#2827)
            --        (this happens if the goal computes to an implicit
            --         function type after some matching in the with-clause)
            --
            --    Ψ   ⊢ withSub : Γ
            --    Δ   ⊢ patSub  : Ψ Θ
            --    Ψ Θ ⊢ weakSub : Ψ
            --    paramSub = patSub ∘ weakSub ∘ withSub
            --
            --    To compute Θ we can look at the arity of the with-function
            --    and compare it to numPats. This works since the with-function
            --    type is fully reduced.

            weakSub :: Substitution
            weakSub | isJust withSub' = wkS (max 0 $ numPats - arity_a) idS -- if numPats < arity, Θ is empty
                    | otherwise       = wkS (numPats - length cxt) idS
            withSub  = fromMaybe idS withSub'
            patSub   = map (patternToTerm . namedArg) (reverse $ take numPats qs0) ++# EmptyS impossible
            paramSub = patSub `composeS` weakSub `composeS` withSub

        eqs <- addContext delta $ checkPatternLinearity eqs

        leftovers@(LeftoverPatterns patVars asb0 dots absurds annps otherPats)
          <- addContext delta $ getLeftoverPatterns eqs

        reportSDoc "tc.lhs.leftover" 30 $ vcat
          [ "leftover patterns: " , nest 2 (addContext delta $ prettyTCM leftovers) ]

        unless (null otherPats) __IMPOSSIBLE__

        -- Get the user-written names for the pattern variables
        let (vars, asb1) = getUserVariableNames delta patVars
            asb          = asb0 ++ asb1

        -- Rename internal patterns with these names
        let makeVar     = maybe deBruijnVar $ debruijnNamedVar . nameToArgName
            ren         = parallelS $ zipWith makeVar (reverse vars) [0..]

        qs <- transferOrigins (cps ++ ps) $ applySubst ren qs0

        let hasAbsurd = not . null $ absurds

        let lhsResult = LHSResult (length cxt) delta qs hasAbsurd b patSub asb (IntSet.fromList $ catMaybes psplit) ixsplit

        -- Debug output
        reportSDoc "tc.lhs.top" 10 $
          vcat [ "checked lhs:"
               , nest 2 $ vcat
                 [ "delta   = " <+> prettyTCM delta
                 , "dots    = " <+> addContext delta (brackets $ fsep $ punctuate comma $ map prettyTCM dots)
                 , "asb     = " <+> addContext delta (brackets $ fsep $ punctuate comma $ map prettyTCM asb)
                 , "absurds = " <+> addContext delta (brackets $ fsep $ punctuate comma $ map prettyTCM absurds)
                 , "qs      = " <+> addContext delta (prettyList $ map pretty qs)
                 , "b       = " <+> addContext delta (prettyTCM b)
                 ]
               ]
        reportSDoc "tc.lhs.top" 30 $
          nest 2 $ vcat
                 [ "vars   = " <+> pretty vars
                 , "b      = " <+> pretty b
                 ]
        reportSDoc "tc.lhs.top" 20 $ nest 2 $ "withSub  = " <+> pretty withSub
        reportSDoc "tc.lhs.top" 20 $ nest 2 $ "weakSub  = " <+> pretty weakSub
        reportSDoc "tc.lhs.top" 20 $ nest 2 $ "patSub   = " <+> pretty patSub
        reportSDoc "tc.lhs.top" 20 $ nest 2 $ "paramSub = " <+> pretty paramSub

        newCxt <- computeLHSContext vars delta

        updateContext paramSub (const newCxt) $ do

          reportSDoc "tc.lhs.top" 10 $ "bound pattern variables"
          reportSDoc "tc.lhs.top" 60 $ nest 2 $ "context = " <+> (pretty =<< getContextTelescope)
          reportSDoc "tc.lhs.top" 10 $ nest 2 $ "type  = " <+> prettyTCM b
          reportSDoc "tc.lhs.top" 60 $ nest 2 $ "type  = " <+> pretty b

          bindAsPatterns asb $ do

            -- Check dot patterns
            mapM_ checkDotPattern dots
            mapM_ checkAbsurdPattern absurds
            mapM_ checkAnnotationPattern annps

          -- Issue2303: don't bind asb' for the continuation (return in lhsResult instead)
          ret lhsResult

  st0 <- initLHSState tel eqs0 ps a finalChecks

  -- after we have introduced variables, we can add the patterns stripped by
  -- with-desugaring to the state.
  let withSub = fromMaybe __IMPOSSIBLE__ withSub'
  withEqs <- updateProblemEqs $ applySubst withSub strippedPats
  -- Jesper, 2017-05-13: re-check the stripped patterns here!
  inTopContext $ addContext (st0 ^. lhsTel) $
    forM_ withEqs recheckStrippedWithPattern

  let st = over (lhsProblem . problemEqs) (++ withEqs) st0

  -- doing the splits:
  (result, block) <- unsafeInTopContext $ runWriterT $ (`runReaderT` (size cxt)) $ checkLHS f st
  return result

-- | Check that this split will generate a modality-correct internal
-- clause when --cubical-compatible is used. This means that the type of
-- anything which might be transported must be modality-correct. This is
-- necessarily an approximate check. We assume that any argument which
-- (a) comes after and (b) mentions a dotted argument will be
-- transported, which is probably an overestimate.
conSplitModalityCheck
  :: Modality
  -- ^ Modality to check at
  -> PatternSubstitution
  -- ^ Substitution resulting from index unification. @Γ ⊢ ρ : Δ'@,
  -- where @Δ'@ is the context we're in, and @Γ@ is the clause telescope
  -- before unification.
  -> Int       -- ^ Variable x at which we split
  -> Telescope -- ^ The telescope @Γ@ itself
  -> Type      -- ^ Target type of the clause.
  -> TCM ()
conSplitModalityCheck mod rho blocking gamma target = when (any ((/= defaultModality) . getModality) gamma) $ do
  reportSDoc "tc.lhs.top" 30 $ vcat
    [ "LHS modality check for modality: " <+> prettyTCM mod
    , "rho:    " <+> inTopContext (prettyTCM rho)
    , "gamma:  " <+> inTopContext (prettyTCM gamma)
    , "target: " <+> prettyTCM target <+> parens (pretty target)
    , "Δ'target: " <+> prettyTCM (applyPatSubst rho target)
    , "blocking:" <+> prettyTCM blocking
    ]
  case firstForced rho (length gamma) of
    Just ix -> do
      -- We've found a forced argument. This means that the unifier has
      -- decided to kill a unification variable, and any of its
      -- occurrences in the generated term will be replaced by an
      -- occurrence of a path, and any terms whose types mention that
      -- variable will be transported.
      let
        (gamma0, delta) = splitTelescopeAt (length gamma - ix) gamma
        name = inTopContext . addContext gamma . nameOfBV
        delta'target = applyPatSubst rho target
      reportSDoc "tc.lhs.top" 30 $ vcat
        [ "found forced argument!"
        , "forced: " <+> prettyTCM ix
        , "before: " <+> inTopContext (prettyTCM gamma0)
        , "after:  " <+> inTopContext (addContext gamma0 (prettyTCM delta))
        ]
      forced <- name ix
      forM_ (zip [ix - 1, ix - 2 ..] (telToList delta)) $ \(arg, d) -> do
        -- Example: The first argument after the first forced variable. So
        -- we have e.g.:
        --   Γ = Γ₀.x.Δ
        --   Δ' ⊢ ρ : Γ₀.x.Δ
        --   Γ₀ ⊢ x : Type
        -- but we need
        --   Δ' ⊢ x : Type,
        -- since Δ' is the context we are in. Then we have
        --   Γ ⊢ x[wkS |Δ|] : Type
        -- and consequently
        --   Δ' ⊢ x[wkS |Δ|][ρ] : Type
        let
          rho' = composeS rho (wkS (arg + 1) idS)
        ty' <- reduce (applyPatSubst rho' (unEl (snd (unDom d))))
        let
          -- It's actually rather tricky to know when, exactly, a
          -- transport will be needed in a position that forces an
          -- usable-at-modality check. Our current heuristic is:
          --
          -- The variable we're looking at has a fibrant type, with the
          -- first forced variable free.
          -- The variable appears free in the result type.
          docheck = and
            [ ix `freeIn` applySubst (wkS (arg + 1) idS) (unEl (snd (unDom d)))
            , arg /= blocking
            , arg `freeIn` target
            ]
        reportSDoc "tc.lhs.top" 30 $ vcat
          [ "arg:        " <+> pretty arg
          , "arg type:   " <+> prettyTCM (applySubst (wkS (arg + 1) idS) (unEl (snd (unDom d))))
          , "check       " <+> pretty docheck
          ]
        argn <- name arg
        when docheck $
          usableAtModality (IndexedClauseArg forced argn) mod ty'
    Nothing -> pure ()

  -- ALways check the target clause type. Specifically, we check it both
  -- in Δ' and in Γ. The check in Δ' will sometimes let slip by a
  -- quantity violation which is masked by an indexed match (recall that
  -- the unifier likes to replace @0-variables for @ω-variables). A
  -- concrete case where this happens is #5468. Check in Δ' first since
  -- that will have the forced variable names.
  usableAtModality IndexedClause mod (unEl (applyPatSubst rho target))
  inTopContext $ addContext gamma $ usableAtModality IndexedClause mod (unEl target)
  where
    -- Find the first dotted pattern in the substitution. "First" =
    -- "earliest bound", so counts down from the length of the
    -- telescope.
    firstForced :: PatternSubstitution -> Int -> Maybe Int
    firstForced pat level
      | level >= 0 = case lookupS pat level of
        DotP{} -> Just level
        _ -> firstForced pat (level - 1)
      | otherwise = Nothing

-- | Determine which splits should be tried.
splitStrategy :: [ProblemEq] -> [ProblemEq]
splitStrategy = filter shouldSplit
  where
    shouldSplit :: ProblemEq -> Bool
    shouldSplit problem@(ProblemEq p v a) = case p of
      A.LitP{}    -> True
      A.RecP{}    -> True
      A.ConP{}    -> True
      A.EqualP{}  -> True

      A.VarP{}    -> False
      A.WildP{}   -> False
      A.DotP{}    -> False
      A.AbsurdP{} -> False

      A.AsP _ _ p  -> shouldSplit $ problem { problemInPat = p }
      A.AnnP _ _ p -> shouldSplit $ problem { problemInPat = p }

      A.ProjP{}       -> __IMPOSSIBLE__
      A.DefP{}        -> __IMPOSSIBLE__
      A.PatternSynP{} -> __IMPOSSIBLE__
      A.WithP{}       -> __IMPOSSIBLE__


-- | The loop (tail-recursive): split at a variable in the problem until problem is solved
checkLHS
  :: forall tcm a. (MonadTCM tcm, PureTCM tcm, MonadWriter Blocked_ tcm, MonadError TCErr tcm, MonadTrace tcm, MonadReader Nat tcm)
  => Maybe QName      -- ^ The name of the definition we are checking.
  -> LHSState a       -- ^ The current state.
  -> tcm a
checkLHS mf = updateModality checkLHS_ where
    -- If the target type is irrelevant or in Prop,
    -- we need to check the lhs in irr. cxt. (see Issue 939).
 updateModality cont st@(LHSState tel ip problem target psplit _) = do
      let m = getModality target
      applyModalityToContext m $ do
        cont $ over (lhsTel . listTel)
                 (map $ inverseApplyModalityButNotQuantity m) st
        -- Andreas, 2018-10-23, issue #3309
        -- the modalities in the clause telescope also need updating.

 checkLHS_ st@(LHSState tel ip problem target psplit ixsplit) = do
  reportSDoc "tc.lhs" 40 $ "tel is" <+> prettyTCM tel
  reportSDoc "tc.lhs" 40 $ "ip is" <+> pretty ip
  reportSDoc "tc.lhs" 40 $ "target is" <+> addContext tel (prettyTCM target)
  if isSolvedProblem problem then
    liftTCM $ (problem ^. problemCont) st
  else do

    reportSDoc "tc.lhs.top" 30 $ vcat
      [ "LHS state: " , nest 2 (prettyTCM st) ]

    unlessM (optPatternMatching <$> getsTC getPragmaOptions) $
      unless (problemAllVariables problem) $
        typeError $ GenericError $ "Pattern matching is disabled"

    let splitsToTry = splitStrategy $ problem ^. problemEqs

    foldr trySplit trySplitRest splitsToTry >>= \case
      Right st' -> checkLHS mf st'
      -- If no split works, give error from first split.
      -- This is conservative, but might not be the best behavior.
      -- It might be better to print all the errors instead.
      Left (err:_) -> throwError err
      Left []      -> __IMPOSSIBLE__

  where

    trySplit :: ProblemEq
             -> tcm (Either [TCErr] (LHSState a))
             -> tcm (Either [TCErr] (LHSState a))
    trySplit eq tryNextSplit = runExceptT (splitArg eq) >>= \case
      Right st' -> return $ Right st'
      Left err  -> left (err:) <$> tryNextSplit

    -- If there are any remaining user patterns, try to split on them
    trySplitRest :: tcm (Either [TCErr] (LHSState a))
    trySplitRest = case problem ^. problemRestPats of
      []    -> return $ Left []
      (p:_) -> left singleton <$> runExceptT (splitRest p)

    splitArg :: ProblemEq -> ExceptT TCErr tcm (LHSState a)
    -- Split on constructor/literal pattern
    splitArg (ProblemEq p v Dom{unDom = a}) = traceCall (CheckPattern p tel a) $ do

      reportSDoc "tc.lhs.split" 30 $ sep
        [ "split looking at pattern"
        , nest 2 $ "p =" <+> prettyA p
        ]

      -- in order to split, v must be a variable.
      i <- liftTCM $ addContext tel $ ifJustM (isEtaVar v a) return $
             softTypeError $ SplitOnNonVariable v a

      let pos = size tel - (i+1)
          (delta1, tel'@(ExtendTel dom adelta2)) = splitTelescopeAt pos tel -- TODO:: tel' defined but not used

      p <- liftTCM $ expandLitPattern p
      let splitOnPat = \case
            (A.LitP _ l)      -> splitLit delta1 dom adelta2 l
            p@A.RecP{}        -> splitCon delta1 dom adelta2 p Nothing
            p@(A.ConP _ c ps) -> splitCon delta1 dom adelta2 p $ Just c
            p@(A.EqualP _ ts) -> splitPartial delta1 dom adelta2 ts
            A.AsP _ _ p       -> splitOnPat p
            A.AnnP _ _ p      -> splitOnPat p

            A.VarP{}        -> __IMPOSSIBLE__
            A.WildP{}       -> __IMPOSSIBLE__
            A.DotP{}        -> __IMPOSSIBLE__
            A.AbsurdP{}     -> __IMPOSSIBLE__
            A.ProjP{}       -> __IMPOSSIBLE__
            A.DefP{}        -> __IMPOSSIBLE__
            A.PatternSynP{} -> __IMPOSSIBLE__
            A.WithP{}       -> __IMPOSSIBLE__
      splitOnPat p


    splitRest :: NamedArg A.Pattern -> ExceptT TCErr tcm (LHSState a)
    splitRest p = setCurrentRange p $ do
      reportSDoc "tc.lhs.split" 20 $ sep
        [ "splitting problem rest"
        , nest 2 $ "projection pattern =" <+> prettyA p
        , nest 2 $ "eliminates type    =" <+> prettyTCM target
        ]
      reportSDoc "tc.lhs.split" 80 $ sep
        [ nest 2 $ text $ "projection pattern (raw) = " ++ show p
        ]

      -- @p@ should be a projection pattern projection from @target@
      (orig, ambProjName) <- ifJust (A.isProjP p) return $ addContext tel $ do
        block <- isBlocked target
        softTypeError $ CannotEliminateWithPattern block p (unArg target)

      (projName, comatchingAllowed, recName, projType, ai) <- suspendErrors $ do
        -- Andreas, 2018-10-18, issue #3289: postfix projections do not have hiding
        -- information for their principal argument; we do not parse @{r}.p@ and the like.
        let h = if orig == ProjPostfix then Nothing else Just $ getHiding p
        addContext tel $ disambiguateProjection h ambProjName target

      unless comatchingAllowed $ do
        hardTypeError . GenericDocError =<< do
          liftTCM $ "Copattern matching is disabled for record" <+> prettyTCM recName

      -- Compute the new rest type by applying the projection type to 'self'.
      -- Note: we cannot be in a let binding.
      f <- ifJust mf return $ hardTypeError $
             GenericError "Cannot use copatterns in a let binding"
      let self = Def f $ patternsToElims ip
      target' <- traverse (`piApplyM` self) projType

      -- Compute the new state
      let projP    = applyWhen (orig == ProjPostfix) (setHiding NotHidden) $
                       Arg ai $ Named Nothing (ProjP orig projName)
          ip'      = ip ++ [projP]
          -- drop the projection pattern (already splitted)
          problem' = over problemRestPats tail problem
      liftTCM $ updateLHSState (LHSState tel ip' problem' target' psplit ixsplit)


    -- Split a Partial.
    --
    -- Example for splitPartial:
    -- @
    --   g : ∀ i j → Partial (i ∨ j) A
    --   g i j (i = 1) = a i j
    --   g i j (j = 1) = b i j
    -- @
    -- leads to, in the first clause:
    -- @
    --   dom   = IsOne (i ∨ j)
    --   ts    = [(i, 1)]
    --   phi   = i
    --   sigma = [1/i]
    -- @
    -- Final clauses:
    -- @
    --   g : ∀ i j → Partial (i ∨ j) A
    --   g 1? j  .itIsOne = a 1 j
    --   g i  1? .itIsOne = b i 1
    -- @
    -- Herein, ? indicates a 'conPFallThrough' pattern.
    --
    -- Example for splitPartial:
    -- @
    --   h : ∀ i j → Partial (i & ¬ j) A
    --   h i j (i = 1) (j = 0)
    --   -- ALT: h i j (i & ¬ j = 1)
    -- @
    -- gives
    -- @
    --   dom = IsOne (i & ¬ j)
    --   ts  = [(i,1), (j,0)]  -- ALT: [(i & ¬ j, 1)]
    --   phi = i & ¬ j
    --   sigma = [1/i,0/j]
    -- @
    --
    -- Example for splitPartial:
    -- @
    --   g : ∀ i j → Partial (i ∨ j) A
    --   g i j (i ∨ j = 1) = a i j
    -- @
    -- leads to, in the first clause:
    -- @
    --   dom   = IsOne (i ∨ j)
    --   ts    = [(i ∨ j, 1)]
    --   phi   = i ∨ j
    --   sigma = fails because several substitutions [[1/i],[1/j]] correspond to phi
    -- @

    splitPartial :: Telescope     -- The types of arguments before the one we split on
                 -> Dom Type      -- The type of the argument we split on
                 -> Abs Telescope -- The types of arguments after the one we split on
                 -> [(A.Expr, A.Expr)] -- [(φ₁ = b1),..,(φn = bn)]
                 -> ExceptT TCErr tcm (LHSState a)
    splitPartial delta1 dom adelta2 ts = do

      unless (domIsFinite dom) $ liftTCM $ addContext delta1 $
        softTypeError . GenericDocError =<<
        vcat [ "Splitting on partial elements is only allowed at the type Partial, but the domain here is" , nest 2 $ prettyTCM $ unDom dom ]

      tInterval <- liftTCM $ primIntervalType

      names <- liftTCM $ addContext tel $ do
        LeftoverPatterns{patternVariables = vars} <- getLeftoverPatterns $ problem ^. problemEqs
        return $ take (size delta1) $ fst $ getUserVariableNames tel vars

      -- Problem: The context does not match the checkpoints in checkLHS,
      --          however we still need a proper checkpoint substitution
      --          for checkExpr below.
      --
      -- Solution: partial splits are not allowed when there are
      --           constructor patterns (checked in checkDef), so
      --           newContext is an extension of the definition
      --           context.
      --
      -- i.e.: Given
      --
      --             Γ = context where def is checked, also last checkpoint.
      --
      --       Then
      --
      --             newContext = Γ Ξ
      --             cpSub = raiseS |Ξ|
      --
      lhsCxtSize <- ask -- size of the context before checkLHS call.
      reportSDoc "tc.lhs.split.partial" 10 $ "lhsCxtSize =" <+> prettyTCM lhsCxtSize

      newContext <- liftTCM $ computeLHSContext names delta1
      reportSDoc "tc.lhs.split.partial" 10 $ "newContext =" <+> prettyTCM newContext

      let cpSub = raiseS $ size newContext - lhsCxtSize

      (gamma,sigma) <- liftTCM $ updateContext cpSub (const newContext) $ do
         ts <- forM ts $ \ (t,u) -> do
                 reportSDoc "tc.lhs.split.partial" 10 $ "currentCxt =" <+> (prettyTCM =<< getContext)
                 reportSDoc "tc.lhs.split.partial" 10 $ text "t, u (Expr) =" <+> prettyTCM (t,u)
                 t <- checkExpr t tInterval
                 u <- checkExpr u tInterval
                 reportSDoc "tc.lhs.split.partial" 10 $ text "t, u        =" <+> pretty (t, u)
                 u <- intervalView =<< reduce u
                 case u of
                   IZero -> primINeg <@> pure t
                   IOne  -> return t
                   _     -> typeError $ GenericError $ "Only 0 or 1 allowed on the rhs of face"
         -- Example: ts = (i=0) (j=1) will result in phi = ¬ i & j
         phi <- case ts of
                   [] -> do
                     a <- reduce (unEl $ unDom dom)
                     -- builtinIsOne is defined, since this is a precondition for having Partial
                     isone <- fromMaybe __IMPOSSIBLE__ <$>  -- newline because of CPP
                       getBuiltinName' builtinIsOne
                     case a of
                       Def q [Apply phi] | q == isone -> return (unArg phi)
                       _           -> typeError . GenericDocError =<< do
                         prettyTCM a <+> " is not IsOne."

                   _  -> foldl (\ x y -> primIMin <@> x <@> y) primIOne (map pure ts)
         reportSDoc "tc.lhs.split.partial" 10 $ text "phi           =" <+> prettyTCM phi
         reportSDoc "tc.lhs.split.partial" 30 $ text "phi           =" <+> pretty phi
         phi <- reduce phi
         reportSDoc "tc.lhs.split.partial" 10 $ text "phi (reduced) =" <+> prettyTCM phi
         refined <- forallFaceMaps phi (\ bs m t -> typeError $ GenericError $ "face blocked on meta")
                            (\_ sigma -> (,sigma) <$> getContextTelescope)
         case refined of
           [(gamma,sigma)] -> return (gamma,sigma)
           []              -> typeError $ GenericError $ "The face constraint is unsatisfiable."
           _               -> typeError $ GenericError $ "Cannot have disjunctions in a face constraint."
      itisone <- liftTCM primItIsOne
      -- substitute the literal in p1 and dpi
      reportSDoc "tc.lhs.faces" 60 $ text $ show sigma

      let oix = size adelta2 -- de brujin index of IsOne
          o_n = fromMaybe __IMPOSSIBLE__ $
            findIndex (\ x -> case namedThing (unArg x) of
                                   VarP _ x -> dbPatVarIndex x == oix
                                   _        -> False) ip
          delta2' = absApp adelta2 itisone
          delta2 = applySubst sigma delta2'
          mkConP (Con c _ [])
             = ConP c (noConPatternInfo { conPType = Just (Arg defaultArgInfo tInterval)
                                              , conPFallThrough = True })
                          []
          mkConP (Var i []) = VarP defaultPatternInfo (DBPatVar "x" i)
          mkConP _          = __IMPOSSIBLE__
          rho0 = fmap mkConP sigma

          rho    = liftS (size delta2) $ consS (DotP defaultPatternInfo itisone) rho0

          delta'   = abstract gamma delta2
          eqs'     = applyPatSubst rho $ problem ^. problemEqs
          ip'      = applySubst rho ip
          target'  = applyPatSubst rho target

      -- Compute the new state
      let problem' = set problemEqs eqs' problem
      reportSDoc "tc.lhs.split.partial" 60 $ text (show problem')
      liftTCM $ updateLHSState (LHSState delta' ip' problem' target' (psplit ++ [Just o_n]) ixsplit)


    splitLit :: Telescope      -- The types of arguments before the one we split on
             -> Dom Type       -- The type of the literal we split on
             -> Abs Telescope  -- The types of arguments after the one we split on
             -> Literal        -- The literal written by the user
             -> ExceptT TCErr tcm (LHSState a)
    splitLit delta1 dom@Dom{domInfo = info, unDom = a} adelta2 lit = do
      let delta2 = absApp adelta2 (Lit lit)
          delta' = abstract delta1 delta2
          rho    = singletonS (size delta2) (litP lit)
          -- Andreas, 2015-06-13 Literals are closed, so no need to raise them!
          -- rho    = liftS (size delta2) $ singletonS 0 (Lit lit)
          -- rho    = [ var i | i <- [0..size delta2 - 1] ]
          --       ++ [ raise (size delta2) $ Lit lit ]
          --       ++ [ var i | i <- [size delta2 ..] ]
          eqs'     = applyPatSubst rho $ problem ^. problemEqs
          ip'      = applySubst rho ip
          target'  = applyPatSubst rho target

      -- Andreas, 2010-09-07 cannot split on irrelevant args
      unless (usableRelevance info) $
        addContext delta1 $ softTypeError $ SplitOnIrrelevant dom

      -- Andreas, 2018-10-17, we can however split on erased things
      -- if there is a single constructor (checked in Coverage).
      --
      -- Thus, no checking of (usableQuantity info) here.

      unlessM (splittableCohesion info) $
        addContext delta1 $ softTypeError $ SplitOnUnusableCohesion dom

      -- check that a is indeed the type of lit (otherwise fail softly)
      -- if not, fail softly since it could be instantiated by a later split.
      suspendErrors $ equalType a =<< litType lit

      -- Compute the new state
      let problem' = set problemEqs eqs' problem
      liftTCM $ updateLHSState (LHSState delta' ip' problem' target' psplit ixsplit)


    splitCon :: Telescope      -- The types of arguments before the one we split on
             -> Dom Type       -- The type of the constructor we split on
             -> Abs Telescope  -- The types of arguments after the one we split on
             -> A.Pattern      -- The pattern written by the user
             -> Maybe AmbiguousQName  -- @Just c@ for a (possibly ambiguous) constructor @c@, or
                                      -- @Nothing@ for a record pattern
             -> ExceptT TCErr tcm (LHSState a)
    splitCon delta1 dom@Dom{domInfo = info, unDom = a} adelta2 focusPat ambC = do
      let delta2 = absBody adelta2

      reportSDoc "tc.lhs.split" 10 $ vcat
        [ "checking lhs"
        , nest 2 $ "tel =" <+> prettyTCM tel
        , nest 2 $ "rel =" <+> text (show $ getRelevance info)
        , nest 2 $ "mod =" <+> text (show $ getModality  info)
        ]

      reportSDoc "tc.lhs.split" 15 $ vcat
        [ "split problem"
        , nest 2 $ vcat
          [ "delta1 = " <+> prettyTCM delta1
          , "a      = " <+> addContext delta1 (prettyTCM a)
          , "delta2 = " <+> addContext delta1
                              (addContext ("x" :: String, dom) (prettyTCM delta2))
          ]
        ]

      -- We cannot split on (shape-)irrelevant arguments.
      reportSLn "tc.lhs.split" 30 $ "split ConP: relevance is " ++ show (getRelevance info)
      unless (usableRelevance info) $ addContext delta1 $
        softTypeError $ SplitOnIrrelevant dom

      -- Andreas, 2018-10-17, we can however split on erased things
      -- if there is a single constructor (checked in Coverage).
      --
      -- Thus, no checking of (usableQuantity info) here.

      unlessM (splittableCohesion info) $
        addContext delta1 $ softTypeError $ SplitOnUnusableCohesion dom

      -- Should we attempt to compute a left inverse for this clause? When
      -- --cubical-compatible --flat-split is given, we don't generate a
      -- left inverse (at all). This means that, when the coverage checker
      -- gets to the clause this was in, it won't generate a (malformed!)
      -- transpX clause for @♭ matching.
      -- TODO(Amy): properly support transpX when @♭ stuff is in the
      -- context.
      let genTrx = boolToMaybe ((getCohesion info == Flat)) SplitOnFlat

      -- We should be at a data/record type
      (dr, d, pars, ixs) <- addContext delta1 $ isDataOrRecordType a
      let isRec = case dr of
            IsData{}   -> False
            IsRecord{} -> True

      checkMatchingAllowed d dr  -- No splitting on coinductive constructors.
      addContext delta1 $ checkSortOfSplitVar dr a delta2 (Just target)

      -- Jesper, 2019-09-13: if the data type we split on is a strict
      -- set, we locally enable --with-K during unification.
      withKIfStrict <- reduce (getSort a) >>= \case
        SSet{} -> return $ locallyTC eSplitOnStrict $ const True
        _      -> return id

      -- The constructor should construct an element of this datatype
      (c :: ConHead, b :: Type) <- liftTCM $ addContext delta1 $ case ambC of
        Just ambC -> disambiguateConstructor ambC d pars
        Nothing   -> getRecordConstructor d pars a

      -- Don't split on lazy (non-eta) constructor
      case focusPat of
        A.ConP cpi _ _ | conPatLazy cpi == ConPatLazy ->
          unlessM (isEtaRecord d) $ softTypeError $ ForcedConstructorNotInstantiated focusPat
        _ -> return ()

      -- The type of the constructor will end in an application of the datatype
      (TelV gamma (El _ ctarget), boundary) <- liftTCM $ telViewPathBoundaryP b
      let Def d' es' = ctarget
          cixs = drop (size pars) $ fromMaybe __IMPOSSIBLE__ $ allApplyElims es'

      -- Δ₁Γ ⊢ boundary
      reportSDoc "tc.lhs.split.con" 50 $ text "  boundary = " <+> prettyTCM boundary

      unless (d == d') {-'-} __IMPOSSIBLE__

      -- Get names for the constructor arguments from the user patterns
      gamma <- liftTCM $ case focusPat of
        A.ConP _ _ ps -> do
          ps <- insertImplicitPatterns ExpandLast ps gamma
          return $ useNamesFromPattern ps gamma
        A.RecP _ fs -> do
          axs <- map argFromDom . recordFieldNames . theDef <$> getConstInfo d
          ps <- insertMissingFieldsFail d (const $ A.WildP patNoRange) fs axs
          ps <- insertImplicitPatterns ExpandLast ps gamma
          return $ useNamesFromPattern ps gamma
        _ -> __IMPOSSIBLE__

      -- Andreas 2010-09-07  propagate relevance info to new vars
      -- Andreas 2018-10-17  propagate modality
      let updMod = composeModality (getModality info)
      gamma <- return $ mapModality updMod <$> gamma

      -- Get the type of the datatype.
      da <- (`piApply` pars) . defType <$> getConstInfo d
      reportSDoc "tc.lhs.split" 30 $ "  da = " <+> prettyTCM da

      reportSDoc "tc.lhs.top" 15 $ addContext delta1 $
        sep [ "preparing to unify"
            , nest 2 $ vcat
              [ "c      =" <+> prettyTCM c <+> ":" <+> prettyTCM b
              , "d      =" <+> prettyTCM (Def d (map Apply pars)) <+> ":" <+> prettyTCM da
              , "isRec  =" <+> (text . show) isRec
              , "gamma  =" <+> prettyTCM gamma
              , "pars   =" <+> brackets (fsep $ punctuate comma $ map prettyTCM pars)
              , "ixs    =" <+> brackets (fsep $ punctuate comma $ map prettyTCM ixs)
              , "cixs   =" <+> addContext gamma (brackets (fsep $ punctuate comma $ map prettyTCM cixs))
              ]
            ]
                 -- We ignore forcing for make-case
      cforced <- ifM (viewTC eMakeCase) (return []) $
                 {-else-} defForced <$> getConstInfo (conName c)

      let delta1Gamma = delta1 `abstract` gamma
          da'  = raise (size gamma) da
          ixs' = raise (size gamma) ixs
          -- Variables in Δ₁ are not forced, since the unifier takes care to not introduce forced
          -- variables.
          forced = replicate (size delta1) NotForced ++ cforced

      -- All variables are flexible.
      let flex = allFlexVars forced $ delta1Gamma

      -- Unify constructor target and given type (in Δ₁Γ)
      -- Given: Δ₁  ⊢ D pars : Φ → Setᵢ
      --        Δ₁  ⊢ c      : Γ → D pars cixs
      --        Δ₁  ⊢ ixs    : Φ
      --        Δ₁Γ ⊢ cixs   : Φ
      -- unification of ixs and cixs in context Δ₁Γ gives us a telescope Δ₁'
      -- and a substitution ρ₀ such that
      --        Δ₁' ⊢ ρ₀ : Δ₁Γ
      --        Δ₁' ⊢ (ixs)ρ₀ ≡ (cixs)ρ₀ : Φρ₀
      -- We can split ρ₀ into two parts ρ₁ and ρ₂, giving
      --        Δ₁' ⊢ ρ₁ : Δ₁
      --        Δ₁' ⊢ ρ₂ : Γρ₁
      -- Application of the constructor c gives
      --        Δ₁' ⊢ (c Γ)(ρ₀) : (D pars cixs)(ρ₁;ρ₂)
      -- We have
      --        cixs(ρ₁;ρ₂)
      --         ≡ cixs(ρ₀)   (since ρ₀=ρ₁;ρ₂)
      --         ≡ ixs(ρ₀)    (by unification)
      --         ≡ ixs(ρ₁)    (since ixs doesn't actually depend on Γ)
      -- so     Δ₁' ⊢ (c Γ)(ρ₀) : (D pars ixs)ρ₁
      -- Putting this together with ρ₁ gives ρ₃ = ρ₁;c ρ₂
      --        Δ₁' ⊢ ρ₁;(c Γ)(ρ₀) : Δ₁(x : D vs ws)
      -- and lifting over Δ₂ gives the final substitution ρ = ρ₃;Δ₂
      -- from Δ' = Δ₁';Δ₂ρ₃
      --        Δ' ⊢ ρ : Δ₁(x : D vs ws)Δ₂

      -- Andrea 2019-07-17 propagate the Cohesion to the equation telescope
      -- TODO: should we propagate the modality in general?
      -- See also Coverage checking.
      da' <- addContext delta1Gamma $ do
             let updCoh = composeCohesion (getCohesion info)
             TelV tel dt <- telView da'
             return $ abstract (mapCohesion updCoh <$> tel) a

      let stuck b errs = softTypeError $ SplitError $
            UnificationStuck b (conName c) (delta1 `abstract` gamma) cixs ixs' errs

      liftTCM (withKIfStrict $ unifyIndices genTrx delta1Gamma flex da' cixs ixs') >>= \case

        -- Mismatch.  Report and abort.
        NoUnify neg -> hardTypeError $ ImpossibleConstructor (conName c) neg

        UnifyBlocked block -> stuck (Just block) []

        -- Unclear situation.  Try next split.
        UnifyStuck errs -> stuck Nothing errs

        -- Success.
        Unifies (delta1',rho0,es) -> do

          reportSDoc "tc.lhs.top" 15 $ "unification successful"
          reportSDoc "tc.lhs.top" 20 $ nest 2 $ vcat
            [ "delta1' =" <+> prettyTCM delta1'
            , "rho0    =" <+> addContext delta1' (prettyTCM rho0)
            , "es      =" <+> addContext delta1' (prettyTCM $ (fmap . fmap . fmap) patternToTerm es)
            ]

          -- split substitution into part for Δ₁ and part for Γ
          let (rho1,rho2) = splitS (size gamma) rho0

          reportSDoc "tc.lhs.top" 20 $ addContext delta1' $ nest 2 $ vcat
            [ "rho1    =" <+> prettyTCM rho1
            , "rho2    =" <+> prettyTCM rho2
            ]

          -- Andreas, 2010-09-09, save the type.
          -- It is relative to Δ₁, but it should be relative to Δ₁'
          let a' = applyPatSubst rho1 a

          -- Also remember if we are a record pattern.
          let cpi = ConPatternInfo { conPInfo   = PatternInfo PatOCon []
                                   , conPRecord = isRec
                                   , conPFallThrough = False
                                   , conPType   = Just $ Arg info a'
                                   , conPLazy   = False } -- Don't mark eta-record matches as lazy (#4254)

          -- compute final context and substitution
          let crho    = ConP c cpi $ applySubst rho0 $ (telePatterns gamma boundary)
              rho3    = consS crho rho1
              delta2' = applyPatSubst rho3 delta2
              delta'  = delta1' `abstract` delta2'
              rho     = liftS (size delta2) rho3

          reportSDoc "tc.lhs.top" 20 $ addContext delta1' $ nest 2 $ vcat
            [ "crho    =" <+> prettyTCM crho
            , "rho3    =" <+> prettyTCM rho3
            , "delta2' =" <+> prettyTCM delta2'
            ]
          reportSDoc "tc.lhs.top" 70 $ addContext delta1' $ nest 2 $ vcat
            [ "crho    =" <+> pretty crho
            , "rho3    =" <+> pretty rho3
            , "delta2' =" <+> pretty delta2'
            ]

          reportSDoc "tc.lhs.top" 15 $ nest 2 $ vcat
            [ "delta'  =" <+> prettyTCM delta'
            , "rho     =" <+> addContext delta' (prettyTCM rho)
            ]

          -- Compute the new out patterns and target type.
          let ip'      = applySubst rho ip
              target'  = applyPatSubst rho target

          -- Update the problem equations
          let eqs' = applyPatSubst rho $ problem ^. problemEqs
              problem' = set problemEqs eqs' problem

          -- The result type's quantity is set to 0 for erased
          -- constructors, but not if the match is made in an erased
          -- position, or if the original constructor definition is
          -- not erased.
          cq <- getQuantity <$> getOriginalConstInfo (conName c)
          let target'' = mapQuantity updResMod target'
                where
                  erased = case getQuantity info of
                    Quantity0{} -> True
                    Quantity1{} -> __IMPOSSIBLE__
                    Quantityω{} -> False
                  -- either sets to Quantity0 or is the identity.
                  updResMod q =
                    case cq of
                     _ | erased  -> q
                     Quantity0{} -> composeQuantity cq q
                                 -- zero-out, preserves origin
                     Quantity1{} -> __IMPOSSIBLE__
                     Quantityω{} -> q

          liftTCM $ addContext delta' $ do
            withoutK <- collapseDefault . optWithoutK <$> pragmaOptions
            cubical <- collapseDefault . optCubicalCompatible <$> pragmaOptions
            mod <- viewTC eModality
            when ((withoutK || cubical) && not (null ixs)) $
              conSplitModalityCheck mod rho (length delta2) tel (unArg target)

          -- if rest type reduces,
          -- extend the split problem by previously not considered patterns
          st' <- liftTCM $ updateLHSState $ LHSState delta' ip' problem' target'' psplit (ixsplit || not (null ixs))

          reportSDoc "tc.lhs.top" 12 $ sep
            [ "new problem from rest"
            , nest 2 $ vcat
              [ "delta'  =" <+> prettyTCM (st' ^. lhsTel)
              , "eqs'    =" <+> addContext (st' ^. lhsTel) (prettyTCM $ st' ^. (lhsProblem . problemEqs))
              , "ip'     =" <+> addContext (st' ^. lhsTel) (pretty $ st' ^. lhsOutPat)
              ]
            ]
          return st'


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

checkMatchingAllowed :: (MonadTCError m)
  => QName         -- ^ The name of the data or record type the constructor belongs to.
  -> DataOrRecord  -- ^ Information about data or (co)inductive (no-)eta-equality record.
  -> m ()
checkMatchingAllowed d = \case
  IsRecord ind eta
    | Just CoInductive <- ind -> typeError $
        GenericError "Pattern matching on coinductive types is not allowed"
    | not $ patternMatchingAllowed eta -> typeError $ SplitOnNonEtaRecord d
    | otherwise -> return ()
  IsData -> return ()

-- | When working with a monad @m@ implementing @MonadTCM@ and @MonadError TCErr@,
--   @suspendErrors f@ performs the TCM action @f@ but catches any errors and throws
--   them in the monad @m@ instead.
suspendErrors :: (MonadTCM m, MonadError TCErr m) => TCM a -> m a
suspendErrors f = do
  ok <- liftTCM $ (Right <$> f) `catchError` (return . Left)
  either throwError return ok

-- | A more direct implementation of the specification
--   @softTypeError err == suspendErrors (typeError err)@
softTypeError :: (HasCallStack, ReadTCState m, MonadError TCErr m, MonadTCEnv m) => TypeError -> m a
softTypeError err = withCallerCallStack $ \loc ->
  throwError =<< typeError' loc err

-- | A convenient alias for @liftTCM . typeError@. Throws the error directly
--   in the TCM even if there is a surrounding monad also implementing
--   @MonadError TCErr@.
hardTypeError :: (HasCallStack, MonadTCM m) => TypeError -> m a
hardTypeError = withCallerCallStack $ \loc -> liftTCM . typeError' loc

data DataOrRecord
  = IsData
  | IsRecord
    { recordInduction   :: Maybe Induction
    , recordEtaEquality :: EtaEquality
    }
  deriving (Show)

-- | Check if the type is a data or record type and return its name,
--   definition, parameters, and indices. Fails softly if the type could become
--   a data/record type by instantiating a variable/metavariable, or fail hard
--   otherwise.
isDataOrRecordType
  :: (MonadTCM m, PureTCM m)
  => Type
  -> ExceptT TCErr m (DataOrRecord, QName, Args, Args)
       -- ^ The 'Args' are parameters and indices.

isDataOrRecordType a0 = ifBlocked a0 blocked $ \case
  ReallyNotBlocked -> \ a -> case unEl a of

    -- Subcase: split type is a Def.
    Def d es -> liftTCM (theDef <$> getConstInfo d) >>= \case

      Datatype{dataPars = np} -> do

        whenM (isInterval a) $ hardTypeError =<< notData

        let (pars, ixs) = splitAt np $ fromMaybe __IMPOSSIBLE__ $ allApplyElims es
        return (IsData, d, pars, ixs)

      Record{ recInduction, recEtaEquality' } -> do
        let pars = fromMaybe __IMPOSSIBLE__ $ allApplyElims es
        return (IsRecord recInduction recEtaEquality', d, pars, [])

      -- Issue #2253: the data type could be abstract.
      AbstractDefn{} -> hardTypeError . GenericDocError =<< do
        liftTCM $ "Cannot split on abstract data type" <+> prettyTCM d

      -- the type could be an axiom
      Axiom{} -> hardTypeError =<< notData

      -- Can't match before we have the definition
      DataOrRecSig{} -> hardTypeError . GenericDocError =<< do
        liftTCM $ "Cannot split on data type" <+> prettyTCM d <+> "whose definition has not yet been checked"

      -- Issue #2997: the type could be a Def that does not reduce for some reason
      -- (abstract, failed termination checking, NON_TERMINATING, ...)
      Function{}    -> hardTypeError =<< notData

      Constructor{} -> __IMPOSSIBLE__

      -- Issue #3620: Some primitives are types too.
      -- Not data though, at least currently 11/03/2018.
      Primitive{}   -> hardTypeError =<< notData

      PrimitiveSort{} -> hardTypeError =<< notData

      GeneralizableVar{} -> __IMPOSSIBLE__

    -- variable: fail softly
    Var{}      -> softTypeError =<< notData
    MetaV{}    -> __IMPOSSIBLE__  -- That is handled in @blocked@.

    -- pi or sort: fail hard
    Pi{}       -> hardTypeError =<< notData
    Sort{}     -> hardTypeError =<< notData

    Lam{}      -> __IMPOSSIBLE__
    Lit{}      -> __IMPOSSIBLE__
    Con{}      -> __IMPOSSIBLE__
    Level{}    -> __IMPOSSIBLE__
    DontCare{} -> __IMPOSSIBLE__
    Dummy s _  -> __IMPOSSIBLE_VERBOSE__ s

  -- neutral type: fail softly
  StuckOn{}     -> \ _a -> softTypeError =<< notData
  AbsurdMatch{} -> \ _a -> softTypeError =<< notData

  -- missing clauses: fail hard
  -- TODO: postpone checking of the whole clause until later?
  MissingClauses{} -> \ _a -> hardTypeError =<< notData

  -- underapplied type: should not happen
  Underapplied{} -> __IMPOSSIBLE__

  where
  notData      = liftTCM $ SplitError . NotADatatype <$> buildClosure a0
  blocked b _a = softTypeError =<< do liftTCM $ SplitError . BlockedType b <$> buildClosure a0

-- | Get the constructor of the given record type together with its type.
--   Throws an error if the type is not a record type.
getRecordConstructor
  :: QName  -- ^ Name @d@ of the record type
  -> Args   -- ^ Parameters @pars@ of the record type
  -> Type   -- ^ The record type @Def d pars@ (for error reporting)
  -> TCM (ConHead, Type)
getRecordConstructor d pars a = do
  con <- (theDef <$> getConstInfo d) >>= \case
    Record{recConHead = con} -> return $ killRange con
    _ -> typeError $ ShouldBeRecordType a
  b <- (`piApply` pars) . defType <$> getConstInfo (conName con)
  return (con, b)


-- | Disambiguate a projection based on the record type it is supposed to be
--   projecting from. Returns the unambiguous projection name and its type.
--   Throws an error if the type is not a record type.
disambiguateProjection
  :: Maybe Hiding   -- ^ Hiding info of the projection's principal argument.
                    --   @Nothing@ if 'Postfix' projection.
  -> AmbiguousQName -- ^ Name of the projection to be disambiguated.
  -> Arg Type       -- ^ Record type we are projecting from.
  -> TCM (QName, Bool, QName, Arg Type, ArgInfo)
       -- ^ @Bool@ signifies whether copattern matching is allowed at
       --   the inferred record type.
disambiguateProjection h ambD@(AmbQ ds) b = do
  -- If the target is not a record type, that's an error.
  -- It could be a meta, but since we cannot postpone lhs checking, we crash here.
  caseMaybeM (liftTCM $ isRecordType $ unArg b) notRecord $ \(r, vs, def) -> case def of
    Record{ recFields = fs, recInduction, recEtaEquality' = eta } -> do
      reportSDoc "tc.lhs.split" 20 $ sep
        [ text $ "we are of record type r  = " ++ prettyShow r
        , text   "applied to parameters vs = " <+> prettyTCM vs
        , text $ "and have fields       fs = " ++ prettyShow (map argFromDom fs)
        ]
      let comatching = recInduction == Just CoInductive
                    || copatternMatchingAllowed eta
      -- Try the projection candidates.
      -- First, we try to find a disambiguation that doesn't produce
      -- any new constraints.
      tryDisambiguate False fs r vs comatching $ \ _ ->
          -- If this fails, we try again with constraints, but we require
          -- the solution to be unique.
          tryDisambiguate True fs r vs comatching $ \case
            ([]   , []      ) -> __IMPOSSIBLE__
            (err:_, []      ) -> throwError err
            (_    , disambs@((d,a):_)) -> typeError . GenericDocError =<< vcat
              [ "Ambiguous projection " <> prettyTCM d <> "."
              , "It could refer to any of"
              , nest 2 $ vcat $ map (prettyDisambProj . fst) disambs
              ]
    _ -> __IMPOSSIBLE__

  where
    tryDisambiguate constraintsOk fs r vs comatching failure = do
      -- Note that tryProj wraps TCM in an ExceptT, collecting errors
      -- instead of throwing them to the user immediately.
      disambiguations <- mapM (runExceptT . tryProj constraintsOk fs r vs) ds
      case List1.partitionEithers disambiguations of
        (_ , (d, (a, ai, mst)) : disambs) | constraintsOk <= null disambs -> do
          mapM_ putTC mst -- Activate state changes
          -- From here, we have the correctly disambiguated projection.
          -- For highlighting, we remember which name we disambiguated to.
          -- This is safe here (fingers crossed) as we won't decide on a
          -- different projection even if we backtrack and come here again.
          liftTCM $ storeDisambiguatedProjection d
          return (d, comatching, r, a, ai)
        other -> failure other

    notRecord = wrongProj $ List1.head ds

    wrongProj :: (MonadTCM m, MonadError TCErr m, ReadTCState m) => QName -> m a
    wrongProj d = softTypeError =<< do
      liftTCM $ GenericDocError <$> sep
        [ "Cannot eliminate type "
        , prettyTCM (unArg b)
        , " with projection "
        , if isAmbiguous ambD then
            text . prettyShow =<< dropTopLevelModule d
          else
            prettyTCM d
        ]

    wrongHiding :: (MonadTCM m, MonadError TCErr m, ReadTCState m) => QName -> m a
    wrongHiding d = softTypeError =<< do
      liftTCM $ GenericDocError <$> sep
        [ "Wrong hiding used for projection " , prettyTCM d ]

    tryProj
      :: Bool                 -- Are we allowed to create new constraints?
      -> [Dom QName]          -- Fields of record type under consideration.
      -> QName                -- Name of record type we are eliminating.
      -> Args                 -- Parameters of record type we are eliminating.
      -> QName                -- Candidate projection.
      -> ExceptT TCErr TCM (QName, (Arg Type, ArgInfo, Maybe TCState))
           -- TCState contains possibly new constraints/meta solutions.
    tryProj constraintsOk fs r vs d0 = isProjection d0 >>= \case
      -- Not a projection
      Nothing -> wrongProj d0
      Just proj -> do
        let d = projOrig proj

        -- Andreas, 2015-05-06 issue 1413 projProper=Nothing is not impossible
        qr <- maybe (wrongProj d) return $ projProper proj

        -- If projIndex==0, then the projection is already applied
        -- to the record value (like in @open R r@), and then it
        -- is no longer a projection but a record field.
        when (null $ projLams proj) $ wrongProj d
        reportSLn "tc.lhs.split" 90 "we are a projection pattern"
        -- If the target is not a record type, that's an error.
        -- It could be a meta, but since we cannot postpone lhs checking, we crash here.
        reportSDoc "tc.lhs.split" 20 $ sep
          [ text $ "proj                  d0 = " ++ prettyShow d0
          , text $ "original proj         d  = " ++ prettyShow d
          ]
        -- Get the field decoration.
        -- If the projection pattern name @d@ is not a field name,
        -- we have to try the next projection name.
        -- If this was not an ambiguous projection, that's an error.
        argd <- maybe (wrongProj d) return $ List.find ((d ==) . unDom) fs

        -- Issue4998: This used to use the hiding from the principal argument, but this is not
        -- relevant for the ArgInfo of the clause rhs. We return that separately so we can set the
        -- correct hiding for the projection pattern in splitRest above.
        let ai = getArgInfo argd

        reportSDoc "tc.lhs.split" 20 $ vcat
          [ text $ "original proj relevance  = " ++ show (getRelevance argd)
          , text $ "original proj quantity   = " ++ show (getQuantity  argd)
          ]
        -- Andreas, 2016-12-31, issue #2374:
        -- We can also disambiguate by hiding info.
        -- Andreas, 2018-10-18, issue #3289: postfix projections have no hiding info.
        unless (caseMaybe h True $ sameHiding $ projArgInfo proj) $ wrongHiding d

        -- Andreas, 2016-12-31, issue #1976: Check parameters.
        let chk = checkParameters qr r vs
        mst <- suspendErrors $
          if constraintsOk then Just . snd <$> localTCStateSaving chk
          else Nothing <$ nonConstraining chk

        -- Get the type of projection d applied to "self"
        dType <- liftTCM $ defType <$> getConstInfo d  -- full type!
        reportSDoc "tc.lhs.split" 20 $ sep
          [ "we are being projected by dType = " <+> prettyTCM dType
          ]
        projType <- liftTCM $ dType `piApplyM` vs
        return (d0, (Arg ai projType, projArgInfo proj, mst))

-- | Disambiguate a constructor based on the data type it is supposed to be
--   constructing. Returns the unambiguous constructor name and its type.
--   Precondition: type should be a data/record type.
disambiguateConstructor
  :: AmbiguousQName    -- ^ The name of the constructor to be disambiguated.
  -> QName             -- ^ Name of the datatype.
  -> Args              -- ^ Parameters of the datatype
  -> TCM (ConHead, Type)
disambiguateConstructor ambC@(AmbQ cs) d pars = do
  d <- canonicalName d
  cons <- theDef <$> getConstInfo d >>= \case
    def@Datatype{} -> return $ dataCons def
    def@Record{}   -> return $ [conName $ recConHead def]
    _              -> __IMPOSSIBLE__

  -- First, try do disambiguate with nonConstraining,
  -- if that fails, try again allowing constraint/solution generation.
  tryDisambiguate False d cons $ \ _ ->
    tryDisambiguate True d cons $ \case
        ([]   , [] ) -> __IMPOSSIBLE__
        (err:_, [] ) -> throwError err
        -- If all disambiguations point to the same original constructor
        -- meaning that only the parameters may differ,
        -- then throw more specific error.
        (_    , [_]) -> typeError $ CantResolveOverloadedConstructorsTargetingSameDatatype d cs
        (_    , disambs@(((c,_,_):|_):_)) -> typeError . GenericDocError =<< vcat
          [ "Ambiguous constructor " <> pretty (qnameName c) <> "."
          , "It could refer to any of"
          , nest 2 $ vcat $ map (prettyDisambCons . conName . snd3) $ List1.concat disambs
          ]

  where
    tryDisambiguate
      :: Bool     -- May we constrain/solve metas to arrive at unique disambiguation?
      -> QName    -- Data/record type.
      -> [QName]  -- Its constructor(s).
      -> ( ( [TCErr]
           , [List1 (QName, ConHead, (Type, Maybe TCState))]
           )
           -> TCM (ConHead, Type) )  -- Failure continuation, taking
                                     -- possible disambiguations
                                     -- grouped by the original
                                     -- constructor name in 'ConHead'.
      -> TCM (ConHead, Type)  -- Unique disambiguation and its type.
    tryDisambiguate constraintsOk d cons failure = do
      reportSDoc "tc.lhs.disamb" 30 $ sep $ List.concat $
        [ [ "tryDisambiguate" ]
        , if constraintsOk then [ "(allowing new constraints)" ] else empty
        , map (nest 2 . pretty) $ List1.toList cs
        , [ "against" ]
        , map (nest 2 . pretty) cons
        ]
      disambiguations <- mapM (runExceptT . tryCon constraintsOk cons d pars) cs
      -- Q: can we be more lazy, like using the ListT monad?
      -- Andreas, 2020-06-17: Not really, since we need to make sure
      -- that only a single candidate remains, and if not,
      -- report all alternatives in the error message.
      let (errs, fits0) = List1.partitionEithers disambiguations
      reportSDoc "tc.lhs.disamb" 40 $ vcat $ do
        let hideSt (c0,c,(a,mst)) = (c0, c, (a, ("(state change)" :: String) <$ mst))
        "remaining candidates: " : map (nest 2 . prettyTCM . hideSt) fits0
      dedupCons fits0 >>= \case

        -- Single candidate remains.
        [ (c0,c,(a,mst)) :| [] ] -> do
          reportSDoc "tc.lhs.disamb" 30 $ sep $
            [ "tryDisambiguate suceeds with"
            , pretty c0
            , ":"
            , prettyTCM a
            ]
          -- Andreas, 2020-06-16, issue #4135
          -- If disambiguation succeeded with new constraints/solutions,
          -- put them into action.
          whenJust mst putTC
          -- If there are multiple candidates for the constructor pattern, exactly one of
          -- which type checks, remember our choice for highlighting info.
          when (isAmbiguous ambC) $ liftTCM $
            storeDisambiguatedConstructor (conInductive c) c0
          return (c,a)

        -- Either no candidate constructor in 'cs' type checks, or multiple candidates
        -- type check.
        groups -> failure (errs, groups)

    abstractConstructor c = softTypeError $
      AbstractConstructorNotInScope c

    wrongDatatype c d = softTypeError $
      ConstructorPatternInWrongDatatype c d

    tryCon
      :: Bool        -- Are we allowed to constrain metas?
      -> [QName]     -- Constructors of data type under consideration.
      -> QName       -- Name of data/record type we are eliminating.
      -> Args        -- Parameters of data/record type we are eliminating.
      -> QName       -- Candidate constructor.
      -> ExceptT TCErr TCM (QName, ConHead, (Type, Maybe TCState))
           -- If this candidate succeeds, return its disambiguation
           -- its type, and maybe the state obtained after checking it
           -- (which may contain new constraints/solutions).
    tryCon constraintsOk cons d pars c = getConstInfo' c >>= \case
      Left (SigUnknown err) -> __IMPOSSIBLE__
      Left SigAbstract -> abstractConstructor c
      Right def -> do
        let con = conSrcCon (theDef def) `withRangeOf` c
        unless (conName con `elem` cons) $ wrongDatatype c d

        -- Andreas, 2013-03-22 fixing issue 279
        -- To resolve ambiguous constructors, Agda always looks up
        -- their original definition and reconstructs the parameters
        -- from the type @Def d vs@ we check against.
        -- However, the constructor could come from a module instantiation
        -- with some of the parameters already fixed.
        -- Agda did not make sure the two parameter lists coincide,
        -- so we add a check here.
        -- I guess this issue could be solved more systematically,
        -- but the extra check here is non-invasive to the existing code.
        -- Andreas, 2016-12-31 fixing issue #1975
        -- Do this also for constructors which were originally ambiguous.
        let chk = checkConstructorParameters c d pars
        mst <- suspendErrors $
          if constraintsOk then Just . snd <$> localTCStateSaving chk
          else Nothing <$ nonConstraining chk

        -- Get the type from the original constructor.
        -- Andreas, 2020-06-17 TODO:
        -- Couldn't we return this type from checkConstructorParameters?
        cType <- (`piApply` pars) . defType <$> getConInfo con

        return (c, con, (cType, mst))

    -- This deduplication identifies different names of the same
    -- constructor, ensuring that the "ambiguous constructor" error
    -- does not fire for the case described in #4130.
    --
    -- Andreas, 2020-06-17, issue #4135:
    -- However, we need to distinguish different occurrences
    -- of the same original constructor if it is used
    -- with different data parameters, as recorded in the @Type@.
    dedupCons ::
      forall a.       [ (a, ConHead, (Type, Maybe TCState)) ]
         -> TCM [ List1 (a, ConHead, (Type, Maybe TCState)) ]
    dedupCons cands = do
      -- Group candidates by original constructor name.
      let groups = List1.groupWith (conName . snd3) cands
      -- Eliminate duplicates (same type) from groups.
      mapM (List1.nubM (cmpM `on` thd3)) groups
      where
      -- The types come possibly with their own state.
      cmpM (a1, mst1) (a2, mst2) = do
        let cmpTypes = tryConversion $ equalType a1 a2
        case (mst1, mst2) of
          (Nothing, Nothing) -> cmpTypes
          (Just st, Nothing) -> inState st cmpTypes
          (Nothing, Just st) -> inState st cmpTypes
          -- Andreas, 2020-06-17, issue #4135.
          -- If the state has diverged into two states we give up.
          -- For instance, one state may say `?0 := true`
          -- and the other `?0 := false`.
          -- The types may be both `D ?0`, which is the same
          -- but diverges in the different states.
          -- We do not check states for equality.
          --
          -- Of course, this is conservative and not maximally extensional.
          -- We might throw an ambiguity error too eagerly,
          -- but this can always be worked around.
          (Just{},  Just{})  -> return False
      inState st m = localTCState $ do putTC st; m


prettyDisamb :: (QName -> Maybe (Range' SrcFile)) -> QName -> TCM Doc
prettyDisamb f x = do
  let d  = pretty =<< dropTopLevelModule x
  caseMaybe (f x) d $ \ r -> d <+> ("(introduced at " <> prettyTCM r <> ")")

-- | For Ambiguous Projection errors, print the last range in 'qnameModule'.
--   For Ambiguous Constructor errors, print the range in 'qnameName'. This fixes the bad
--   error message in #4130.
prettyDisambProj, prettyDisambCons :: QName -> TCM Doc
prettyDisambProj = prettyDisamb $ lastMaybe . filter (noRange /=) . map nameBindingSite . mnameToList . qnameModule
prettyDisambCons = prettyDisamb $ Just . nameBindingSite . qnameName

-- | @checkConstructorParameters c d pars@ checks that the data/record type
--   behind @c@ is has initial parameters (coming e.g. from a module instantiation)
--   that coincide with an prefix of @pars@.
checkConstructorParameters :: MonadTCM tcm => QName -> QName -> Args -> tcm ()
checkConstructorParameters c d pars = do
  dc <- liftTCM $ getConstructorData c
  checkParameters dc d pars

-- | Check that given parameters match the parameters of the inferred
--   constructor/projection.
checkParameters
  :: MonadTCM tcm
  => QName  -- ^ The record/data type name of the chosen constructor/projection.
  -> QName  -- ^ The record/data type name as supplied by the type signature.
  -> Args   -- ^ The parameters.
  -> tcm ()
checkParameters dc d pars = liftTCM $ do
  a  <- reduce (Def dc [])
  case a of
    Def d0 es -> do -- compare parameters
      let vs = fromMaybe __IMPOSSIBLE__ $ allApplyElims es
      reportSDoc "tc.lhs.split" 40 $ vcat $
        [ "checkParameters"
        , nest 2 $ "d                   =" <+> (text . prettyShow) d
        , nest 2 $ "d0 (should be == d) =" <+> (text . prettyShow) d0
        , nest 2 $ "dc                  =" <+> (text . prettyShow) dc
        , nest 2 $ "vs                  =" <+> prettyTCM vs
        , nest 2 $ "pars                =" <+> prettyTCM pars
        ]
      -- when (d0 /= d) __IMPOSSIBLE__ -- d could have extra qualification
      t <- typeOfConst d
      compareArgs [] [] t (Def d []) vs (take (length vs) pars)
    _ -> __IMPOSSIBLE__

checkSortOfSplitVar :: (MonadTCM m, PureTCM m, MonadError TCErr m,
                        LensSort a, PrettyTCM a, LensSort ty, PrettyTCM ty)
                    => DataOrRecord -> a -> Telescope -> Maybe ty -> m ()
checkSortOfSplitVar dr a tel mtarget = do
  liftTCM (reduce $ getSort a) >>= \case
    sa@Type{} -> whenM isTwoLevelEnabled checkFibrantSplit
    Prop{} -> checkPropSplit
    Inf IsFibrant _ -> whenM isTwoLevelEnabled checkFibrantSplit
    Inf IsStrict _ -> return ()
    SSet{} -> return ()
    sa      -> softTypeError =<< do
      liftTCM $ SortOfSplitVarError <$> isBlocked sa <*> sep
        [ "Cannot split on datatype in sort" , prettyTCM (getSort a) ]

  where
    checkPropSplit
      | IsRecord Nothing _ <- dr = return ()
      | Just target <- mtarget = do
        reportSDoc "tc.sort.check" 20 $ "target prop:" <+> prettyTCM target
        checkIsProp target
      | otherwise              = do
          reportSDoc "tc.sort.check" 20 $ "no target prop"
          splitOnPropError dr

    checkIsProp t = runBlocked (isPropM t) >>= \case
      Left b      -> splitOnPropError dr -- TODO
      Right False -> splitOnPropError dr
      Right True  -> return ()

    checkFibrantSplit
      | IsRecord _ _ <- dr     = return ()
      | Just target <- mtarget = do
          reportSDoc "tc.sort.check" 20 $ "target:" <+> prettyTCM target
          checkIsFibrant target
          forM_ (telToList tel) $ \ d -> do
            let ty = snd $ unDom d
            checkIsCoFibrant ty
      | otherwise              = do
          reportSDoc "tc.sort.check" 20 $ "no target"
          splitOnFibrantError Nothing

    -- Cofibrant types are those that could be the domain of a fibrant
    -- pi type. (Notion by C. Sattler).
    checkIsCoFibrant t = runBlocked (isCoFibrantSort t) >>= \case
      Left b      -> splitOnFibrantError' t $ Just b
      Right False -> unlessM (isInterval t) $
                       splitOnFibrantError' t $ Nothing
      Right True  -> return ()

    checkIsFibrant t = runBlocked (isFibrant t) >>= \case
      Left b      -> splitOnFibrantError $ Just b
      Right False -> splitOnFibrantError Nothing
      Right True  -> return ()

    splitOnPropError dr = softTypeError =<< do
      liftTCM $ GenericDocError <$>
        ("Cannot split on" <+> kindOfData dr <+> "in Prop unless target is in Prop")
      where
        kindOfData :: DataOrRecord -> TCM Doc
        kindOfData IsData                          = "datatype"
        kindOfData (IsRecord Nothing _)            = "record type"
        kindOfData (IsRecord (Just Inductive) _)   = "inductive record type"
        kindOfData (IsRecord (Just CoInductive) _) = "coinductive record type"

    splitOnFibrantError' t mb = softTypeError =<< do
      liftTCM $ SortOfSplitVarError mb <$> fsep
        [ "Cannot eliminate fibrant type" , prettyTCM a
        , "unless context type", prettyTCM t, "is also fibrant."
        ]

    splitOnFibrantError mb = softTypeError =<< do
      liftTCM $ SortOfSplitVarError mb <$> fsep
        [ "Cannot eliminate fibrant type" , prettyTCM a
        , "unless target type is also fibrant"
        ]