{-# 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)
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 Agda.TypeChecking.Warnings (warning)

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.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.List1 as List1
import Agda.Utils.Maybe
import Agda.Utils.Monad
import Agda.Utils.Null
import Agda.Syntax.Common.Pretty (prettyShow)
import Agda.Utils.Singleton
import Agda.Utils.Size
import Agda.Utils.Tuple

import Agda.Utils.Impossible
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 a
p =
    forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
False FlexibleVarKind -> Bool
notOtherFlex forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *) a. MaybeT m a -> m (Maybe a)
runMaybeT (forall a (m :: * -> *).
(IsFlexiblePattern a, HasConstInfo m, MonadDebug m) =>
a -> MaybeT m FlexibleVarKind
maybeFlexiblePattern a
p)
    where
    notOtherFlex :: FlexibleVarKind -> Bool
notOtherFlex = \case
      RecordFlex [FlexibleVarKind]
fls -> forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all FlexibleVarKind -> Bool
notOtherFlex [FlexibleVarKind]
fls
      FlexibleVarKind
ImplicitFlex   -> Bool
True
      FlexibleVarKind
DotFlex        -> Bool
True
      FlexibleVarKind
OtherFlex      -> Bool
False

instance IsFlexiblePattern A.Pattern where
  maybeFlexiblePattern :: forall (m :: * -> *).
(HasConstInfo m, MonadDebug m) =>
Pattern -> MaybeT m FlexibleVarKind
maybeFlexiblePattern Pattern
p = do
    forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.lhs.flex" Int
30 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"maybeFlexiblePattern" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA Pattern
p
    forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.lhs.flex" Int
60 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"maybeFlexiblePattern (raw) " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> (forall (m :: * -> *). Applicative m => [Char] -> m Doc
text forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => a -> [Char]
show forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. ExprLike a => a -> a
deepUnscope) Pattern
p
    case Pattern
p of
      A.DotP{}  -> forall (m :: * -> *) a. Monad m => a -> m a
return FlexibleVarKind
DotFlex
      A.VarP{}  -> forall (m :: * -> *) a. Monad m => a -> m a
return FlexibleVarKind
ImplicitFlex
      A.WildP{} -> forall (m :: * -> *) a. Monad m => a -> m a
return FlexibleVarKind
ImplicitFlex
      A.AsP PatInfo
_ BindName
_ Pattern
p -> forall a (m :: * -> *).
(IsFlexiblePattern a, HasConstInfo m, MonadDebug m) =>
a -> MaybeT m FlexibleVarKind
maybeFlexiblePattern Pattern
p
      A.ConP ConPatInfo
_ AmbiguousQName
cs [NamedArg Pattern]
qs | Just QName
c <- AmbiguousQName -> Maybe QName
getUnambiguous AmbiguousQName
cs ->
        forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM (forall a. Maybe a -> Bool
isNothing forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *).
HasConstInfo m =>
QName -> m (Maybe (QName, Defn))
isRecordConstructor QName
c) (forall (m :: * -> *) a. Monad m => a -> m a
return FlexibleVarKind
OtherFlex) {-else-}
            (forall a (m :: * -> *).
(IsFlexiblePattern a, HasConstInfo m, MonadDebug m) =>
a -> MaybeT m FlexibleVarKind
maybeFlexiblePattern [NamedArg Pattern]
qs)
      A.LitP{}  -> forall (m :: * -> *) a. Monad m => a -> m a
return FlexibleVarKind
OtherFlex
      A.AnnP PatInfo
_ Expr
_ Pattern
p -> forall a (m :: * -> *).
(IsFlexiblePattern a, HasConstInfo m, MonadDebug m) =>
a -> MaybeT m FlexibleVarKind
maybeFlexiblePattern Pattern
p
      Pattern
_ -> forall (m :: * -> *) a. MonadPlus m => m a
mzero

instance IsFlexiblePattern (I.Pattern' a) where
  maybeFlexiblePattern :: forall (m :: * -> *).
(HasConstInfo m, MonadDebug m) =>
Pattern' a -> MaybeT m FlexibleVarKind
maybeFlexiblePattern Pattern' a
p =
    case Pattern' a
p of
      I.DotP{}  -> forall (m :: * -> *) a. Monad m => a -> m a
return FlexibleVarKind
DotFlex
      I.ConP ConHead
_ ConPatternInfo
i [NamedArg (Pattern' a)]
ps
        | ConPatternInfo -> Bool
conPRecord ConPatternInfo
i , PatOrigin
PatOSystem <- PatternInfo -> PatOrigin
patOrigin (ConPatternInfo -> PatternInfo
conPInfo ConPatternInfo
i) -> forall (m :: * -> *) a. Monad m => a -> m a
return FlexibleVarKind
ImplicitFlex  -- expanded from ImplicitP
        | ConPatternInfo -> Bool
conPRecord ConPatternInfo
i -> forall a (m :: * -> *).
(IsFlexiblePattern a, HasConstInfo m, MonadDebug m) =>
a -> MaybeT m FlexibleVarKind
maybeFlexiblePattern [NamedArg (Pattern' a)]
ps
        | Bool
otherwise -> forall (m :: * -> *) a. MonadPlus m => m a
mzero
      I.VarP{}  -> forall (m :: * -> *) a. MonadPlus m => m a
mzero
      I.LitP{}  -> forall (m :: * -> *) a. MonadPlus m => m a
mzero
      I.ProjP{} -> forall (m :: * -> *) a. MonadPlus m => m a
mzero
      I.IApplyP{} -> forall (m :: * -> *) a. MonadPlus m => m a
mzero
      I.DefP{} -> forall (m :: * -> *) a. MonadPlus m => m a
mzero -- TODO Andrea check semantics

-- | Lists of flexible patterns are 'RecordFlex'.
instance IsFlexiblePattern a => IsFlexiblePattern [a] where
  maybeFlexiblePattern :: forall (m :: * -> *).
(HasConstInfo m, MonadDebug m) =>
[a] -> MaybeT m FlexibleVarKind
maybeFlexiblePattern [a]
ps = [FlexibleVarKind] -> FlexibleVarKind
RecordFlex forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM forall a (m :: * -> *).
(IsFlexiblePattern a, HasConstInfo m, MonadDebug m) =>
a -> MaybeT m FlexibleVarKind
maybeFlexiblePattern [a]
ps

instance IsFlexiblePattern a => IsFlexiblePattern (Arg a) where
  maybeFlexiblePattern :: forall (m :: * -> *).
(HasConstInfo m, MonadDebug m) =>
Arg a -> MaybeT m FlexibleVarKind
maybeFlexiblePattern = forall a (m :: * -> *).
(IsFlexiblePattern a, HasConstInfo m, MonadDebug m) =>
a -> MaybeT m FlexibleVarKind
maybeFlexiblePattern forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall e. Arg e -> e
unArg

instance IsFlexiblePattern a => IsFlexiblePattern (Common.Named name a) where
  maybeFlexiblePattern :: forall (m :: * -> *).
(HasConstInfo m, MonadDebug m) =>
Named name a -> MaybeT m FlexibleVarKind
maybeFlexiblePattern = forall a (m :: * -> *).
(IsFlexiblePattern a, HasConstInfo m, MonadDebug m) =>
a -> MaybeT m FlexibleVarKind
maybeFlexiblePattern forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall name a. Named name a -> a
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 :: forall a. LHSState a -> TCM (LHSState a)
updateLHSState LHSState a
st = do
  let tel :: Telescope
tel     = LHSState a
st forall o i. o -> Lens' o i -> i
^. forall a. Lens' (LHSState a) Telescope
lhsTel
      problem :: Problem a
problem = LHSState a
st forall o i. o -> Lens' o i -> i
^. forall a. Lens' (LHSState a) (Problem a)
lhsProblem
  [ProblemEq]
eqs' <- forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
tel forall a b. (a -> b) -> a -> b
$ [ProblemEq] -> TCMT IO [ProblemEq]
updateProblemEqs forall a b. (a -> b) -> a -> b
$ Problem a
problem forall o i. o -> Lens' o i -> i
^. forall a. Lens' (Problem a) [ProblemEq]
problemEqs
  Telescope
tel' <- forall (m :: * -> *).
PureTCM m =>
[ProblemEq] -> Telescope -> m Telescope
useNamesFromProblemEqs [ProblemEq]
eqs' Telescope
tel
  forall (m :: * -> *) a.
(PureTCM m, MonadError TCErr m, MonadTrace m,
 MonadFresh NameId m) =>
LHSState a -> m (LHSState a)
updateProblemRest forall a b. (a -> b) -> a -> b
$ forall o i. Lens' o i -> LensSet o i
set forall a. Lens' (LHSState a) Telescope
lhsTel Telescope
tel' forall a b. (a -> b) -> a -> b
$ forall o i. Lens' o i -> LensSet o i
set (forall a. Lens' (LHSState a) (Problem a)
lhsProblem forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Lens' (Problem a) [ProblemEq]
problemEqs) [ProblemEq]
eqs' LHSState a
st

-- | Update the user patterns in the given problem, simplifying equations
--   between constructors where possible.
updateProblemEqs
 :: [ProblemEq] -> TCM [ProblemEq]
updateProblemEqs :: [ProblemEq] -> TCMT IO [ProblemEq]
updateProblemEqs [ProblemEq]
eqs = do
  forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.lhs.top" Int
20 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
    [ TCMT IO Doc
"updateProblem: equations to update"
    , forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ if forall a. Null a => a -> Bool
null [ProblemEq]
eqs then TCMT IO Doc
"(none)" else forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM [ProblemEq]
eqs
    ]

  [ProblemEq]
eqs' <- [ProblemEq] -> TCMT IO [ProblemEq]
updates [ProblemEq]
eqs

  forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.lhs.top" Int
20 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
    [ TCMT IO Doc
"updateProblem: new equations"
    , forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ if forall a. Null a => a -> Bool
null [ProblemEq]
eqs' then TCMT IO Doc
"(none)" else forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM [ProblemEq]
eqs'
    ]

  forall (m :: * -> *) a. Monad m => a -> m a
return [ProblemEq]
eqs'

  where

    updates :: [ProblemEq] -> TCM [ProblemEq]
    updates :: [ProblemEq] -> TCMT IO [ProblemEq]
updates = forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat forall (m :: * -> *) b c a.
Functor m =>
(b -> c) -> (a -> m b) -> a -> m c
<.> forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse ProblemEq -> TCMT IO [ProblemEq]
update

    update :: ProblemEq -> TCM [ProblemEq]
    update :: ProblemEq -> TCMT IO [ProblemEq]
update eq :: ProblemEq
eq@(ProblemEq A.WildP{} Term
_ Dom Type
_) = forall (m :: * -> *) a. Monad m => a -> m a
return []
    update eq :: ProblemEq
eq@(ProblemEq p :: Pattern
p@A.ProjP{} Term
_ Dom Type
_) = forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError forall a b. (a -> b) -> a -> b
$ Pattern -> TypeError
IllformedProjectionPatternAbstract Pattern
p
    update eq :: ProblemEq
eq@(ProblemEq p :: Pattern
p@(A.AsP PatInfo
info BindName
x Pattern
p') Term
v Dom Type
a) =
      (Pattern -> Term -> Dom Type -> ProblemEq
ProblemEq (forall e. BindName -> Pattern' e
A.VarP BindName
x) Term
v Dom Type
a forall a. a -> [a] -> [a]
:) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ProblemEq -> TCMT IO [ProblemEq]
update (Pattern -> Term -> Dom Type -> ProblemEq
ProblemEq Pattern
p' Term
v Dom Type
a)

    update eq :: ProblemEq
eq@(ProblemEq p :: Pattern
p@(A.AnnP PatInfo
_ Expr
_ A.WildP{}) Term
v Dom Type
a) = forall (m :: * -> *) a. Monad m => a -> m a
return [ProblemEq
eq]
    update eq :: ProblemEq
eq@(ProblemEq p :: Pattern
p@(A.AnnP PatInfo
info Expr
ty Pattern
p') Term
v Dom Type
a) =
      (Pattern -> Term -> Dom Type -> ProblemEq
ProblemEq (forall e. PatInfo -> e -> Pattern' e -> Pattern' e
A.AnnP PatInfo
info Expr
ty (forall e. PatInfo -> Pattern' e
A.WildP PatInfo
patNoRange)) Term
v Dom Type
a forall a. a -> [a] -> [a]
:) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ProblemEq -> TCMT IO [ProblemEq]
update (Pattern -> Term -> Dom Type -> ProblemEq
ProblemEq Pattern
p' Term
v Dom Type
a)

    update eq :: ProblemEq
eq@(ProblemEq Pattern
p Term
v Dom Type
a) = forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce Term
v forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall (m :: * -> *). HasBuiltins m => Term -> m Term
constructorForm forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
      Con ConHead
c ConInfo
ci Elims
es -> do
        let vs :: Args
vs = forall a. a -> Maybe a -> a
fromMaybe forall a. HasCallStack => a
__IMPOSSIBLE__ forall a b. (a -> b) -> a -> b
$ forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims Elims
es
        -- we should only simplify equations between fully applied constructors
        Maybe ((QName, Type, Args), Type)
contype <- forall (m :: * -> *).
PureTCM m =>
ConHead -> Type -> m (Maybe ((QName, Type, Args), Type))
getFullyAppliedConType ConHead
c forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce (forall t e. Dom' t e -> e
unDom Dom Type
a)
        forall a b. Maybe a -> b -> (a -> b) -> b
caseMaybe Maybe ((QName, Type, Args), Type)
contype (forall (m :: * -> *) a. Monad m => a -> m a
return [ProblemEq
eq]) forall a b. (a -> b) -> a -> b
$ \((QName
d,Type
_,Args
pars),Type
b) -> do
        TelV Telescope
ctel Type
_ <- forall (m :: * -> *). PureTCM m => Type -> m (TelV Type)
telViewPath Type
b

        -- Andrea 15/10/2020: propagate modality to constructor arguments
        let updMod :: Modality -> Modality
updMod = Modality -> Modality -> Modality
composeModality (forall a. LensModality a => a -> Modality
getModality Dom Type
a)
        Telescope
ctel <- forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. LensModality a => (Modality -> Modality) -> a -> a
mapModality Modality -> Modality
updMod forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Telescope
ctel

        let bs :: [Dom Type]
bs = Telescope -> [Term] -> [Dom Type]
instTel Telescope
ctel (forall a b. (a -> b) -> [a] -> [b]
map forall e. Arg e -> e
unArg Args
vs)

        Pattern
p <- forall (m :: * -> *).
(MonadError TCErr m, MonadTCEnv m, ReadTCState m, HasBuiltins m) =>
Pattern -> m Pattern
expandLitPattern Pattern
p
        case Pattern
p of
          A.AsP{} -> forall a. HasCallStack => a
__IMPOSSIBLE__
          A.AnnP{} -> forall a. HasCallStack => a
__IMPOSSIBLE__
          A.ConP ConPatInfo
cpi AmbiguousQName
ambC [NamedArg Pattern]
ps -> do
            (ConHead
c',Type
_) <- AmbiguousQName -> QName -> Args -> TCM (ConHead, Type)
disambiguateConstructor AmbiguousQName
ambC QName
d Args
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 ConHead -> QName
conName ConHead
c forall a. Eq a => a -> a -> Bool
/= ConHead -> QName
conName ConHead
c' then forall (m :: * -> *) a. Monad m => a -> m a
return [ProblemEq
eq] else do

            -- Insert implicit patterns
            [NamedArg Pattern]
ps <- forall (m :: * -> *).
(PureTCM m, MonadError TCErr m, MonadFresh NameId m,
 MonadTrace m) =>
ExpandHidden
-> [NamedArg Pattern] -> Telescope -> m [NamedArg Pattern]
insertImplicitPatterns ExpandHidden
ExpandLast [NamedArg Pattern]
ps Telescope
ctel
            forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.lhs.imp" Int
20 forall a b. (a -> b) -> a -> b
$
              TCMT IO Doc
"insertImplicitPatternsT returned" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep (forall a b. (a -> b) -> [a] -> [b]
map forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA [NamedArg Pattern]
ps)

            -- Check argument count and hiding (not just count: #3074)
            let checkArgs :: [NamedArg Pattern] -> Args -> Int -> Int -> TCMT IO ()
checkArgs [] [] Int
_ Int
_ = forall (m :: * -> *) a. Monad m => a -> m a
return ()
                checkArgs (NamedArg Pattern
p : [NamedArg Pattern]
ps) (Arg Term
v : Args
vs) Int
nExpected Int
nActual
                  | forall a. LensHiding a => a -> Hiding
getHiding NamedArg Pattern
p forall a. Eq a => a -> a -> Bool
== forall a. LensHiding a => a -> Hiding
getHiding Arg Term
v = [NamedArg Pattern] -> Args -> Int -> Int -> TCMT IO ()
checkArgs [NamedArg Pattern]
ps Args
vs (Int
nExpected forall a. Num a => a -> a -> a
+ Int
1) (Int
nActual forall a. Num a => a -> a -> a
+ Int
1)
                  | Bool
otherwise                  = forall (m :: * -> *) x a.
(MonadTrace m, HasRange x) =>
x -> m a -> m a
setCurrentRange NamedArg Pattern
p forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError TypeError
WrongHidingInLHS
                checkArgs [] Args
vs Int
nExpected Int
nActual = forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError forall a b. (a -> b) -> a -> b
$
                  QName -> Int -> Int -> TypeError
WrongNumberOfConstructorArguments (ConHead -> QName
conName ConHead
c) (Int
nExpected forall a. Num a => a -> a -> a
+ forall (t :: * -> *) a. Foldable t => t a -> Int
length Args
vs) Int
nActual
                checkArgs (NamedArg Pattern
p : [NamedArg Pattern]
ps) [] Int
nExpected Int
nActual = forall (m :: * -> *) x a.
(MonadTrace m, HasRange x) =>
x -> m a -> m a
setCurrentRange NamedArg Pattern
p forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError forall a b. (a -> b) -> a -> b
$
                  QName -> Int -> Int -> TypeError
WrongNumberOfConstructorArguments (ConHead -> QName
conName ConHead
c) Int
nExpected (Int
nActual forall a. Num a => a -> a -> a
+ Int
1 forall a. Num a => a -> a -> a
+ (forall (t :: * -> *) a. Foldable t => t a -> Int
length [NamedArg Pattern]
ps))

            [NamedArg Pattern] -> Args -> Int -> Int -> TCMT IO ()
checkArgs [NamedArg Pattern]
ps Args
vs Int
0 Int
0

            [ProblemEq] -> TCMT IO [ProblemEq]
updates forall a b. (a -> b) -> a -> b
$ forall a b c d. (a -> b -> c -> d) -> [a] -> [b] -> [c] -> [d]
zipWith3 Pattern -> Term -> Dom Type -> ProblemEq
ProblemEq (forall a b. (a -> b) -> [a] -> [b]
map forall a. NamedArg a -> a
namedArg [NamedArg Pattern]
ps) (forall a b. (a -> b) -> [a] -> [b]
map forall e. Arg e -> e
unArg Args
vs) [Dom Type]
bs

          A.RecP PatInfo
pi [FieldAssignment' Pattern]
fs -> do
            [Arg QName]
axs <- forall a b. (a -> b) -> [a] -> [b]
map forall t a. Dom' t a -> Arg a
argFromDom forall b c a. (b -> c) -> (a -> b) -> a -> c
. Defn -> [Dom' Term QName]
recFields forall b c a. (b -> c) -> (a -> b) -> a -> c
. Definition -> Defn
theDef forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
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.
            [Name] -> [QName] -> TCMT IO ()
disambiguateRecordFields (forall a b. (a -> b) -> [a] -> [b]
map forall a. FieldAssignment' a -> Name
_nameFieldA [FieldAssignment' Pattern]
fs) (forall a b. (a -> b) -> [a] -> [b]
map forall e. Arg e -> e
unArg [Arg QName]
axs)

            let cxs :: [Arg Name]
cxs = forall a b. (a -> b) -> [a] -> [b]
map (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Name -> Name
nameConcrete forall b c a. (b -> c) -> (a -> b) -> a -> c
. QName -> Name
qnameName)) [Arg QName]
axs

            -- In fs omitted explicit fields are replaced by underscores,
            -- and the fields are put in the correct order.
            [NamedArg Pattern]
ps <- forall a.
HasRange a =>
QName
-> (Name -> a)
-> [FieldAssignment' a]
-> [Arg Name]
-> TCM [NamedArg a]
insertMissingFieldsFail QName
d (forall a b. a -> b -> a
const forall a b. (a -> b) -> a -> b
$ forall e. PatInfo -> Pattern' e
A.WildP PatInfo
patNoRange) [FieldAssignment' Pattern]
fs [Arg Name]
cxs

            -- We also need to insert missing implicit or instance fields.
            [NamedArg Pattern]
ps <- forall (m :: * -> *).
(PureTCM m, MonadError TCErr m, MonadFresh NameId m,
 MonadTrace m) =>
ExpandHidden
-> [NamedArg Pattern] -> Telescope -> m [NamedArg Pattern]
insertImplicitPatterns ExpandHidden
ExpandLast [NamedArg Pattern]
ps Telescope
ctel

            let eqs :: [ProblemEq]
eqs = forall a b c d. (a -> b -> c -> d) -> [a] -> [b] -> [c] -> [d]
zipWith3 Pattern -> Term -> Dom Type -> ProblemEq
ProblemEq (forall a b. (a -> b) -> [a] -> [b]
map forall a. NamedArg a -> a
namedArg [NamedArg Pattern]
ps) (forall a b. (a -> b) -> [a] -> [b]
map forall e. Arg e -> e
unArg Args
vs) [Dom Type]
bs
            [ProblemEq] -> TCMT IO [ProblemEq]
updates [ProblemEq]
eqs

          Pattern
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return [ProblemEq
eq]

      Lit Literal
l | A.LitP PatInfo
_ Literal
l' <- Pattern
p , Literal
l forall a. Eq a => a -> a -> Bool
== Literal
l' -> forall (m :: * -> *) a. Monad m => a -> m a
return []

      Term
_ | A.EqualP{} <- Pattern
p -> do
        Term
itisone <- forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primItIsOne
        forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM (forall (m :: * -> *).
(MonadConstraint m, MonadWarning m, MonadError TCErr m,
 MonadFresh ProblemId m) =>
m () -> m Bool
tryConversion forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
MonadConversion m =>
Type -> Term -> Term -> m ()
equalTerm (forall t e. Dom' t e -> e
unDom Dom Type
a) Term
v Term
itisone) (forall (m :: * -> *) a. Monad m => a -> m a
return []) (forall (m :: * -> *) a. Monad m => a -> m a
return [ProblemEq
eq])

      Term
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return [ProblemEq
eq]

    instTel :: Telescope -> [Term] -> [Dom Type]
    instTel :: Telescope -> [Term] -> [Dom Type]
instTel Telescope
EmptyTel [Term]
_                   = []
    instTel (ExtendTel Dom Type
arg Abs Telescope
tel) (Term
u : [Term]
us) = Dom Type
arg forall a. a -> [a] -> [a]
: Telescope -> [Term] -> [Dom Type]
instTel (forall a. Subst a => Abs a -> SubstArg a -> a
absApp Abs Telescope
tel Term
u) [Term]
us
    instTel ExtendTel{} []               = forall a. HasCallStack => a
__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 :: forall a. Problem a -> Bool
isSolvedProblem Problem a
problem = forall a. Null a => a -> Bool
null (Problem a
problem forall o i. o -> Lens' o i -> i
^. forall a. Lens' (Problem a) [NamedArg Pattern]
problemRestPats) Bool -> Bool -> Bool
&&
  forall a. Problem a -> Bool
problemAllVariables Problem a
problem

-- | Check if a problem consists only of variable patterns.
--   (Includes the 'problemRest').
problemAllVariables :: Problem a -> Bool
problemAllVariables :: forall a. Problem a -> Bool
problemAllVariables Problem a
problem =
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all forall {e}. Pattern' e -> Bool
isSolved forall a b. (a -> b) -> a -> b
$
      forall a b. (a -> b) -> [a] -> [b]
map forall a. NamedArg a -> a
namedArg (Problem a
problem forall o i. o -> Lens' o i -> i
^. forall a. Lens' (Problem a) [NamedArg Pattern]
problemRestPats) forall a. [a] -> [a] -> [a]
++ forall a. Problem a -> [Pattern]
problemInPats Problem a
problem
  where
    -- need further splitting:
    isSolved :: Pattern' e -> Bool
isSolved A.ConP{}        = Bool
False
    isSolved A.LitP{}        = Bool
False
    isSolved A.RecP{}        = Bool
False  -- record pattern
    -- solved:
    isSolved A.VarP{}        = Bool
True
    isSolved A.WildP{}       = Bool
True
    isSolved A.DotP{}        = Bool
True
    isSolved A.AbsurdP{}     = Bool
True
    -- recursive cases
    isSolved (A.AsP PatInfo
_ BindName
_ Pattern' e
p)   = Pattern' e -> Bool
isSolved Pattern' e
p
    isSolved (A.AnnP PatInfo
_ e
_ Pattern' e
p)  = Pattern' e -> Bool
isSolved Pattern' e
p
    -- impossible:
    isSolved A.ProjP{}       = forall a. HasCallStack => a
__IMPOSSIBLE__
    isSolved A.DefP{}        = forall a. HasCallStack => a
__IMPOSSIBLE__
    isSolved A.PatternSynP{} = forall a. HasCallStack => a
__IMPOSSIBLE__  -- expanded before
    isSolved A.EqualP{}      = Bool
False -- __IMPOSSIBLE__
    isSolved A.WithP{}       = forall a. HasCallStack => a
__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 :: ProblemEq -> TCMT IO ()
noShadowingOfConstructors problem :: ProblemEq
problem@(ProblemEq Pattern
p Term
_ (Dom{domInfo :: forall t e. Dom' t e -> ArgInfo
domInfo = ArgInfo
info, unDom :: forall t e. Dom' t e -> e
unDom = El Sort' Term
_ Term
a})) =
  case Pattern
p of
   A.WildP       {} -> forall (m :: * -> *) a. Monad m => a -> m a
return ()
   A.AbsurdP     {} -> forall (m :: * -> *) a. Monad m => a -> m a
return ()
   A.DotP        {} -> forall (m :: * -> *) a. Monad m => a -> m a
return ()
   A.EqualP      {} -> forall (m :: * -> *) a. Monad m => a -> m a
return ()
   A.AsP PatInfo
_ BindName
_ Pattern
p      -> ProblemEq -> TCMT IO ()
noShadowingOfConstructors forall a b. (a -> b) -> a -> b
$ ProblemEq
problem { problemInPat :: Pattern
problemInPat = Pattern
p }
   A.AnnP PatInfo
_ Expr
_ Pattern
p     -> ProblemEq -> TCMT IO ()
noShadowingOfConstructors forall a b. (a -> b) -> a -> b
$ ProblemEq
problem { problemInPat :: Pattern
problemInPat = Pattern
p }
   A.ConP        {} -> forall a. HasCallStack => a
__IMPOSSIBLE__
   A.RecP        {} -> forall a. HasCallStack => a
__IMPOSSIBLE__
   A.ProjP       {} -> forall a. HasCallStack => a
__IMPOSSIBLE__
   A.DefP        {} -> forall a. HasCallStack => a
__IMPOSSIBLE__
   A.LitP        {} -> forall a. HasCallStack => a
__IMPOSSIBLE__
   A.PatternSynP {} -> forall a. HasCallStack => a
__IMPOSSIBLE__
   A.WithP       {} -> forall a. HasCallStack => a
__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 :: BindName -> Name
unBind = Name
x} -> forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (forall a. LensOrigin a => a -> Origin
getOrigin ArgInfo
info forall a. Eq a => a -> a -> Bool
== Origin
UserWritten) forall a b. (a -> b) -> a -> b
$ do
    forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.lhs.shadow" Int
30 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
      [ forall (m :: * -> *). Applicative m => [Char] -> m Doc
text forall a b. (a -> b) -> a -> b
$ [Char]
"checking whether pattern variable " forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> [Char]
prettyShow Name
x forall a. [a] -> [a] -> [a]
++ [Char]
" shadows a constructor"
      , forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"type of variable =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
a
      , forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"position of variable =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> (forall (m :: * -> *). Applicative m => [Char] -> m Doc
text forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => a -> [Char]
show) (forall a. HasRange a => a -> Range
getRange Name
x)
      ]
    forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.lhs.shadow" Int
70 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"a =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Term
a

    -- Get a conflicting data or record constructor, if any.
    Maybe QName
mc <- forall (m :: * -> *) a. MaybeT m a -> m (Maybe a)
runMaybeT do

      -- Is the type of the pattern variable a data or pattern record type?
      Term
a  <- forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce Term
a
      (QName
d, DataOrRecord
dr) <- forall (m :: * -> *) a. m (Maybe a) -> MaybeT m a
MaybeT forall a b. (a -> b) -> a -> b
$ Term -> TCM (Maybe (QName, DataOrRecord))
isDataOrRecord Term
a
      forall (f :: * -> *). Alternative f => Bool -> f ()
guard forall a b. (a -> b) -> a -> b
$ forall a. PatternMatchingAllowed a => a -> Bool
patternMatchingAllowed DataOrRecord
dr

      -- Look for a constructor with the same name as the pattern variable.
      [QName]
cs <- forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ QName -> TCM [QName]
getConstructors QName
d
      forall (m :: * -> *) a. m (Maybe a) -> MaybeT m a
MaybeT forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
List.find ((Name -> Name
A.nameConcrete Name
x forall a. Eq a => a -> a -> Bool
==) forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> Name
A.nameConcrete forall b c a. (b -> c) -> (a -> b) -> a -> c
. QName -> Name
A.qnameName) [QName]
cs

    -- Alert if there is a constructor of the same name.
    forall (m :: * -> *) a. Monad m => Maybe a -> (a -> m ()) -> m ()
whenJust Maybe QName
mc \ QName
c -> forall (m :: * -> *) x a.
(MonadTrace m, HasRange x) =>
x -> m a -> m a
setCurrentRange Name
x forall a b. (a -> b) -> a -> b
$
      forall (m :: * -> *).
(HasCallStack, MonadWarning m) =>
Warning -> m ()
warning forall a b. (a -> b) -> a -> b
$ Name -> QName -> Warning
PatternShadowsConstructor (Name -> Name
nameConcrete Name
x) QName
c
    --
    -- Andreas, 2023-09-08, issue #6829:
    -- I rewrote the code originally dating from 2009, commit:
    -- https://github.com/agda/agda/commit/5d5095ba080b04f16867d4ed5af4ba7091f1a773
    -- The code survived for almost 15 years, but it slept through the advent
    -- of matchable record constructors in 2010 (Agda 2.2.8):
    -- https://github.com/agda/agda/blob/283730b392d7c21c54b53b0f486802ec143e4af7/doc/release-notes/2.2.8.md#L7-L9
    -- Here are comments on the last version of the code I'd like to preserve,
    -- as they reflect some considerations and design decisions:
    --
            -- 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.
          -- TODO: in the future some stuck primitives might allow constructors
      -- 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.

-- | Check that a dot pattern matches it's instantiation.
checkDotPattern :: DotPattern -> TCM ()
checkDotPattern :: DotPattern -> TCMT IO ()
checkDotPattern (Dot Expr
e Term
v (Dom{domInfo :: forall t e. Dom' t e -> ArgInfo
domInfo = ArgInfo
info, unDom :: forall t e. Dom' t e -> e
unDom = Type
a})) =
  forall (m :: * -> *) a. MonadTrace m => Call -> m a -> m a
traceCall (Expr -> Term -> Call
CheckDotPattern Expr
e Term
v) forall a b. (a -> b) -> a -> b
$ do
  forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.lhs.dot" Int
15 forall a b. (a -> b) -> a -> b
$
    forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep [ TCMT IO Doc
"checking dot pattern"
        , forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA Expr
e
        , forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"=" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
v
        , forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
":" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
a
        ]
  forall (tcm :: * -> *) m a.
(MonadTCEnv tcm, LensModality m) =>
m -> tcm a -> tcm a
applyModalityToContext ArgInfo
info forall a b. (a -> b) -> a -> b
$ do
    Term
u <- Expr -> Type -> TCMT IO Term
checkExpr Expr
e Type
a
    forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.lhs.dot" Int
50 forall a b. (a -> b) -> a -> b
$
      forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep [ TCMT IO Doc
"equalTerm"
          , forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Type
a
          , forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Term
u
          , forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Term
v
          ]
    forall (m :: * -> *).
MonadConversion m =>
Type -> Term -> Term -> m ()
equalTerm Type
a Term
u Term
v

checkAbsurdPattern :: AbsurdPattern -> TCM ()
checkAbsurdPattern :: AbsurdPattern -> TCMT IO ()
checkAbsurdPattern (Absurd Range
r Type
a) = Range -> Type -> TCMT IO ()
ensureEmptyType Range
r Type
a

checkAnnotationPattern :: AnnotationPattern -> TCM ()
checkAnnotationPattern :: AnnotationPattern -> TCMT IO ()
checkAnnotationPattern (Ann Expr
t Type
a) = do
  forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.lhs.ann" Int
15 forall a b. (a -> b) -> a -> b
$
    forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep [ TCMT IO Doc
"checking type annotation in pattern"
        , forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA Expr
t
        , forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"=" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
a
        ]
  Type
b <- Expr -> TCM Type
isType_ Expr
t
  forall (m :: * -> *). MonadConversion m => Type -> Type -> m ()
equalType Type
a Type
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 :: [NamedArg Pattern]
-> [NamedArg DeBruijnPattern] -> TCM [NamedArg DeBruijnPattern]
transferOrigins [NamedArg Pattern]
ps [NamedArg DeBruijnPattern]
qs = do
  forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.lhs.origin" Int
40 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
    [ TCMT IO Doc
"transferOrigins"
    , forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
      [ TCMT IO Doc
"ps  =   " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA [NamedArg Pattern]
ps
      , TCMT IO Doc
"qs  =   " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty [NamedArg DeBruijnPattern]
qs
      ]
    ]
  [NamedArg Pattern]
-> [NamedArg DeBruijnPattern] -> TCM [NamedArg DeBruijnPattern]
transfers [NamedArg Pattern]
ps [NamedArg DeBruijnPattern]
qs

  where
    transfers :: [NamedArg A.Pattern]
              -> [NamedArg DeBruijnPattern]
              -> TCM [NamedArg DeBruijnPattern]
    transfers :: [NamedArg Pattern]
-> [NamedArg DeBruijnPattern] -> TCM [NamedArg DeBruijnPattern]
transfers [] [NamedArg DeBruijnPattern]
qs
      | forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all forall a. LensHiding a => a -> Bool
notVisible [NamedArg DeBruijnPattern]
qs = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (forall a. LensOrigin a => Origin -> a -> a
setOrigin Origin
Inserted) [NamedArg DeBruijnPattern]
qs
      | Bool
otherwise         = forall a. HasCallStack => a
__IMPOSSIBLE__
    transfers (NamedArg Pattern
p : [NamedArg Pattern]
ps) [] = forall a. HasCallStack => a
__IMPOSSIBLE__
    transfers (NamedArg Pattern
p : [NamedArg Pattern]
ps) (NamedArg DeBruijnPattern
q : [NamedArg DeBruijnPattern]
qs)
      | NamedArg Pattern -> NamedArg DeBruijnPattern -> Bool
matchingArgs NamedArg Pattern
p NamedArg DeBruijnPattern
q = do
          NamedArg DeBruijnPattern
q' <- forall a.
LensNamed a =>
(Maybe (NameOf a) -> Maybe (NameOf a)) -> a -> a
mapNameOf (forall b a. b -> (a -> b) -> Maybe a -> b
maybe forall a. a -> a
id (forall a b. a -> b -> a
const forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. a -> Maybe a
Just) forall a b. (a -> b) -> a -> b
$ forall a. LensNamed a => a -> Maybe (NameOf a)
getNameOf NamedArg Pattern
p) -- take NamedName from p if present
              forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. LensOrigin a => Origin -> a -> a
setOrigin (forall a. LensOrigin a => a -> Origin
getOrigin NamedArg Pattern
p)
            forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse forall a b. (a -> b) -> a -> b
$ Pattern -> DeBruijnPattern -> TCM DeBruijnPattern
transfer forall a b. (a -> b) -> a -> b
$ forall a. NamedArg a -> a
namedArg NamedArg Pattern
p) NamedArg DeBruijnPattern
q
          (NamedArg DeBruijnPattern
q' forall a. a -> [a] -> [a]
:) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [NamedArg Pattern]
-> [NamedArg DeBruijnPattern] -> TCM [NamedArg DeBruijnPattern]
transfers [NamedArg Pattern]
ps [NamedArg DeBruijnPattern]
qs
      | Bool
otherwise = (forall a. LensOrigin a => Origin -> a -> a
setOrigin Origin
Inserted NamedArg DeBruijnPattern
q forall a. a -> [a] -> [a]
:) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [NamedArg Pattern]
-> [NamedArg DeBruijnPattern] -> TCM [NamedArg DeBruijnPattern]
transfers (NamedArg Pattern
p forall a. a -> [a] -> [a]
: [NamedArg Pattern]
ps) [NamedArg DeBruijnPattern]
qs

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

      (([Name]
asB , [Expr]
anns , A.ConP ConPatInfo
pi AmbiguousQName
_ [NamedArg Pattern]
ps) , ConP ConHead
c (ConPatternInfo PatternInfo
i Bool
r Bool
ft Maybe (Arg Type)
mb Bool
l) [NamedArg DeBruijnPattern]
qs) -> do
        let cpi :: ConPatternInfo
cpi = PatternInfo
-> Bool -> Bool -> Maybe (Arg Type) -> Bool -> ConPatternInfo
ConPatternInfo (PatOrigin -> [Name] -> PatternInfo
PatternInfo PatOrigin
PatOCon [Name]
asB) Bool
r Bool
ft Maybe (Arg Type)
mb Bool
l
        forall x.
ConHead -> ConPatternInfo -> [NamedArg (Pattern' x)] -> Pattern' x
ConP ConHead
c ConPatternInfo
cpi forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [NamedArg Pattern]
-> [NamedArg DeBruijnPattern] -> TCM [NamedArg DeBruijnPattern]
transfers [NamedArg Pattern]
ps [NamedArg DeBruijnPattern]
qs

      (([Name]
asB , [Expr]
anns , A.RecP PatInfo
pi [FieldAssignment' Pattern]
fs) , ConP ConHead
c (ConPatternInfo PatternInfo
i Bool
r Bool
ft Maybe (Arg Type)
mb Bool
l) [NamedArg DeBruijnPattern]
qs) -> do
        let Def QName
d Elims
_  = forall t a. Type'' t a -> a
unEl forall a b. (a -> b) -> a -> b
$ forall e. Arg e -> e
unArg forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a -> a
fromMaybe forall a. HasCallStack => a
__IMPOSSIBLE__ Maybe (Arg Type)
mb
            axs :: [Arg Name]
axs = forall a b. (a -> b) -> [a] -> [b]
map (Name -> Name
nameConcrete forall b c a. (b -> c) -> (a -> b) -> a -> c
. QName -> Name
qnameName forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall e. Arg e -> e
unArg) (ConHead -> [Arg QName]
conFields ConHead
c) forall a b. [a] -> [Arg b] -> [Arg a]
`withArgsFrom` [NamedArg DeBruijnPattern]
qs
            cpi :: ConPatternInfo
cpi = PatternInfo
-> Bool -> Bool -> Maybe (Arg Type) -> Bool -> ConPatternInfo
ConPatternInfo (PatOrigin -> [Name] -> PatternInfo
PatternInfo PatOrigin
PatORec [Name]
asB) Bool
r Bool
ft Maybe (Arg Type)
mb Bool
l
        [NamedArg Pattern]
ps <- forall a.
HasRange a =>
QName
-> (Name -> a)
-> [FieldAssignment' a]
-> [Arg Name]
-> TCM [NamedArg a]
insertMissingFieldsFail QName
d (forall a b. a -> b -> a
const forall a b. (a -> b) -> a -> b
$ forall e. PatInfo -> Pattern' e
A.WildP PatInfo
patNoRange) [FieldAssignment' Pattern]
fs [Arg Name]
axs
        forall x.
ConHead -> ConPatternInfo -> [NamedArg (Pattern' x)] -> Pattern' x
ConP ConHead
c ConPatternInfo
cpi forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [NamedArg Pattern]
-> [NamedArg DeBruijnPattern] -> TCM [NamedArg DeBruijnPattern]
transfers [NamedArg Pattern]
ps [NamedArg DeBruijnPattern]
qs

      (([Name]
asB , [Expr]
anns , Pattern
p) , ConP ConHead
c (ConPatternInfo PatternInfo
i Bool
r Bool
ft Maybe (Arg Type)
mb Bool
l) [NamedArg DeBruijnPattern]
qs) -> do
        let cpi :: ConPatternInfo
cpi = PatternInfo
-> Bool -> Bool -> Maybe (Arg Type) -> Bool -> ConPatternInfo
ConPatternInfo (PatOrigin -> [Name] -> PatternInfo
PatternInfo (Pattern -> PatOrigin
patOrig Pattern
p) [Name]
asB) Bool
r Bool
ft Maybe (Arg Type)
mb Bool
l
        forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall x.
ConHead -> ConPatternInfo -> [NamedArg (Pattern' x)] -> Pattern' x
ConP ConHead
c ConPatternInfo
cpi [NamedArg DeBruijnPattern]
qs

      (([Name]
asB , [Expr]
anns , Pattern
p) , VarP PatternInfo
_ DBPatVar
x) -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall x. PatternInfo -> x -> Pattern' x
VarP (PatOrigin -> [Name] -> PatternInfo
PatternInfo (Pattern -> PatOrigin
patOrig Pattern
p) [Name]
asB) DBPatVar
x

      (([Name]
asB , [Expr]
anns , Pattern
p) , DotP PatternInfo
_ Term
u) -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall x. PatternInfo -> Term -> Pattern' x
DotP (PatOrigin -> [Name] -> PatternInfo
PatternInfo (Pattern -> PatOrigin
patOrig Pattern
p) [Name]
asB) Term
u

      (([Name]
asB , [Expr]
anns , Pattern
p) , LitP PatternInfo
_ Literal
l) -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall x. PatternInfo -> Literal -> Pattern' x
LitP (PatOrigin -> [Name] -> PatternInfo
PatternInfo (Pattern -> PatOrigin
patOrig Pattern
p) [Name]
asB) Literal
l

      (([Name], [Expr], Pattern), DeBruijnPattern)
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return DeBruijnPattern
q

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

    matchingArgs :: NamedArg A.Pattern -> NamedArg DeBruijnPattern -> Bool
    matchingArgs :: NamedArg Pattern -> NamedArg DeBruijnPattern -> Bool
matchingArgs NamedArg Pattern
p NamedArg DeBruijnPattern
q
      -- The arguments match if
      -- 1. they are both projections,
      | forall a. Maybe a -> Bool
isJust (forall a. IsProjP a => a -> Maybe (ProjOrigin, AmbiguousQName)
A.isProjP NamedArg Pattern
p) = forall a. Maybe a -> Bool
isJust (forall a. IsProjP a => a -> Maybe (ProjOrigin, AmbiguousQName)
isProjP NamedArg DeBruijnPattern
q)
      -- 2. or they are both visible,
      | forall a. LensHiding a => a -> Bool
visible NamedArg Pattern
p Bool -> Bool -> Bool
&& forall a. LensHiding a => a -> Bool
visible NamedArg DeBruijnPattern
q = Bool
True
      -- 3. or they have the same hiding and the argument is not named,
      | forall a b. (LensHiding a, LensHiding b) => a -> b -> Bool
sameHiding NamedArg Pattern
p NamedArg DeBruijnPattern
q Bool -> Bool -> Bool
&& forall a. Maybe a -> Bool
isNothing (forall a. LensNamed a => a -> Maybe (NameOf a)
getNameOf NamedArg Pattern
p) = Bool
True
      -- 4. or they have the same hiding and the same name.
      | forall a b. (LensHiding a, LensHiding b) => a -> b -> Bool
sameHiding NamedArg Pattern
p NamedArg DeBruijnPattern
q Bool -> Bool -> Bool
&& forall a b.
(LensNamed a, LensNamed b, NameOf a ~ NamedName,
 NameOf b ~ NamedName) =>
a -> b -> Bool
namedSame NamedArg Pattern
p NamedArg DeBruijnPattern
q = Bool
True
      -- Otherwise this argument was inserted by the typechecker.
      | Bool
otherwise = Bool
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 :: [ProblemEq] -> TCMT IO [ProblemEq]
checkPatternLinearity [ProblemEq]
eqs = do
  forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.lhs.linear" Int
30 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"Checking linearity of pattern variables"
  Map BindName (Term, Type) -> [ProblemEq] -> TCMT IO [ProblemEq]
check forall k a. Map k a
Map.empty [ProblemEq]
eqs
  where
    check :: Map A.BindName (Term, Type) -> [ProblemEq] -> TCM [ProblemEq]
    check :: Map BindName (Term, Type) -> [ProblemEq] -> TCMT IO [ProblemEq]
check Map BindName (Term, Type)
_ [] = forall (m :: * -> *) a. Monad m => a -> m a
return []
    check Map BindName (Term, Type)
vars (eq :: ProblemEq
eq@(ProblemEq Pattern
p Term
u Dom Type
a) : [ProblemEq]
eqs) = do
      forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.lhs.linear" Int
40 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep
        [ TCMT IO Doc
"linearity: checking pattern "
        , forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA Pattern
p
        , TCMT IO Doc
" equal to term "
        , forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
u
        , TCMT IO Doc
" of type "
        , forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Dom Type
a
        ]
      case Pattern
p of
        A.VarP BindName
x -> do
          let y :: Name
y = BindName -> Name
A.unBind BindName
x
          forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"tc.lhs.linear" Int
60 forall a b. (a -> b) -> a -> b
$
            [Char]
"pattern variable " forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> [Char]
prettyShow (Name -> Name
A.nameConcrete Name
y) forall a. [a] -> [a] -> [a]
++ [Char]
" with id " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show (Name -> NameId
A.nameId Name
y)
          case forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup BindName
x Map BindName (Term, Type)
vars of
            Just (Term
v , Type
b) -> do
              forall (m :: * -> *) a. MonadTrace m => Call -> m a -> m a
traceCall (Name -> Call
CheckPatternLinearityType forall a b. (a -> b) -> a -> b
$ Name -> Name
A.nameConcrete Name
y) forall a b. (a -> b) -> a -> b
$
                forall (m :: * -> *) a.
(MonadConstraint m, MonadWarning m, MonadError TCErr m,
 MonadFresh ProblemId m) =>
m a -> m a
noConstraints forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). MonadConversion m => Type -> Type -> m ()
equalType (forall t e. Dom' t e -> e
unDom Dom Type
a) Type
b
              forall (m :: * -> *) a. MonadTrace m => Call -> m a -> m a
traceCall (Name -> Call
CheckPatternLinearityValue forall a b. (a -> b) -> a -> b
$ Name -> Name
A.nameConcrete Name
y) forall a b. (a -> b) -> a -> b
$
                forall (m :: * -> *) a.
(MonadConstraint m, MonadWarning m, MonadError TCErr m,
 MonadFresh ProblemId m) =>
m a -> m a
noConstraints forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
MonadConversion m =>
Type -> Term -> Term -> m ()
equalTerm (forall t e. Dom' t e -> e
unDom Dom Type
a) Term
u Term
v
              Map BindName (Term, Type) -> [ProblemEq] -> TCMT IO [ProblemEq]
check Map BindName (Term, Type)
vars [ProblemEq]
eqs
            Maybe (Term, Type)
Nothing -> (ProblemEq
eqforall a. a -> [a] -> [a]
:) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do
              Map BindName (Term, Type) -> [ProblemEq] -> TCMT IO [ProblemEq]
check (forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert BindName
x (Term
u,forall t e. Dom' t e -> e
unDom Dom Type
a) Map BindName (Term, Type)
vars) [ProblemEq]
eqs
        A.AsP PatInfo
_ BindName
x Pattern
p ->
          Map BindName (Term, Type) -> [ProblemEq] -> TCMT IO [ProblemEq]
check Map BindName (Term, Type)
vars forall a b. (a -> b) -> a -> b
$ [Pattern -> Term -> Dom Type -> ProblemEq
ProblemEq (forall e. BindName -> Pattern' e
A.VarP BindName
x) Term
u Dom Type
a, Pattern -> Term -> Dom Type -> ProblemEq
ProblemEq Pattern
p Term
u Dom Type
a] forall a. [a] -> [a] -> [a]
++ [ProblemEq]
eqs
        A.AnnP PatInfo
_ Expr
_ A.WildP{} -> TCMT IO [ProblemEq]
continue
        A.AnnP PatInfo
r Expr
t Pattern
p -> (Pattern -> Term -> Dom Type -> ProblemEq
ProblemEq (forall e. PatInfo -> e -> Pattern' e -> Pattern' e
A.AnnP PatInfo
r Expr
t (forall e. PatInfo -> Pattern' e
A.WildP PatInfo
patNoRange)) Term
u Dom Type
aforall a. a -> [a] -> [a]
:) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
          Map BindName (Term, Type) -> [ProblemEq] -> TCMT IO [ProblemEq]
check Map BindName (Term, Type)
vars (Pattern -> Term -> Dom Type -> ProblemEq
ProblemEq Pattern
p Term
u Dom Type
a forall a. a -> [a] -> [a]
: [ProblemEq]
eqs)
        A.WildP{}       -> TCMT IO [ProblemEq]
continue
        A.DotP{}        -> TCMT IO [ProblemEq]
continue
        A.AbsurdP{}     -> TCMT IO [ProblemEq]
continue
        A.ConP{}        -> forall a. HasCallStack => a
__IMPOSSIBLE__
        A.ProjP{}       -> forall a. HasCallStack => a
__IMPOSSIBLE__
        A.DefP{}        -> forall a. HasCallStack => a
__IMPOSSIBLE__
        A.LitP{}        -> forall a. HasCallStack => a
__IMPOSSIBLE__
        A.PatternSynP{} -> forall a. HasCallStack => a
__IMPOSSIBLE__
        A.RecP{}        -> forall a. HasCallStack => a
__IMPOSSIBLE__
        A.EqualP{}      -> forall a. HasCallStack => a
__IMPOSSIBLE__
        A.WithP{}       -> forall a. HasCallStack => a
__IMPOSSIBLE__

      where continue :: TCMT IO [ProblemEq]
continue = (ProblemEq
eqforall a. a -> [a] -> [a]
:) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Map BindName (Term, Type) -> [ProblemEq] -> TCMT IO [ProblemEq]
check Map BindName (Term, Type)
vars [ProblemEq]
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 :: [Maybe Name] -> Telescope -> TCM Context
computeLHSContext = forall {m :: * -> *} {f :: * -> *} {a}.
(MonadDebug m, PrettyTCM (Tele (f a)), MonadFresh NameId m,
 Subst (f a), Functor f) =>
[f (Name, a)]
-> [Name] -> [Maybe Name] -> Tele (f a) -> m [f (Name, a)]
go [] []
  where
    go :: [f (Name, a)]
-> [Name] -> [Maybe Name] -> Tele (f a) -> m [f (Name, a)]
go [f (Name, a)]
cxt [Name]
_ []        tel :: Tele (f a)
tel@ExtendTel{} = do
      forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"impossible" Int
10 forall a b. (a -> b) -> a -> b
$
        TCMT IO Doc
"computeLHSContext: no patterns left, but tel =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Tele (f a)
tel
      forall a. HasCallStack => a
__IMPOSSIBLE__
    go [f (Name, a)]
cxt [Name]
_ (Maybe Name
_ : [Maybe Name]
_)   Tele (f a)
EmptyTel = forall a. HasCallStack => a
__IMPOSSIBLE__
    go [f (Name, a)]
cxt [Name]
_ []        Tele (f a)
EmptyTel = forall (m :: * -> *) a. Monad m => a -> m a
return [f (Name, a)]
cxt
    go [f (Name, a)]
cxt [Name]
taken (Maybe Name
x : [Maybe Name]
xs) tel0 :: Tele (f a)
tel0@(ExtendTel f a
a Abs (Tele (f a))
tel) = do
        Name
name <- forall b a. b -> (a -> b) -> Maybe a -> b
maybe (forall {m :: * -> *} {p}.
MonadFresh NameId m =>
p -> [Char] -> m Name
dummyName [Name]
taken forall a b. (a -> b) -> a -> b
$ forall a. Abs a -> [Char]
absName Abs (Tele (f a))
tel) forall (m :: * -> *) a. Monad m => a -> m a
return Maybe Name
x
        let e :: f (Name, a)
e = (Name
name,) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> f a
a
        [f (Name, a)]
-> [Name] -> [Maybe Name] -> Tele (f a) -> m [f (Name, a)]
go (f (Name, a)
e forall a. a -> [a] -> [a]
: [f (Name, a)]
cxt) (Name
name forall a. a -> [a] -> [a]
: [Name]
taken) [Maybe Name]
xs (forall a. Subst a => Abs a -> a
absBody Abs (Tele (f a))
tel)

    dummyName :: p -> [Char] -> m Name
dummyName p
taken [Char]
s =
      if forall a. Underscore a => a -> Bool
isUnderscore [Char]
s then forall (m :: * -> *). MonadFresh NameId m => m Name
freshNoName_
      else forall a. LensInScope a => a -> a
setNotInScope forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a (m :: * -> *).
(FreshName a, MonadFresh NameId m) =>
a -> m Name
freshName_ ([Char] -> [Char]
argNameToString [Char]
s)

-- | Bind as patterns
bindAsPatterns :: [AsBinding] -> TCM a -> TCM a
bindAsPatterns :: forall a. [AsBinding] -> TCM a -> TCM a
bindAsPatterns []                TCM a
ret = TCM a
ret
bindAsPatterns (AsB Name
x Term
v Type
a Modality
m : [AsBinding]
asb) TCM a
ret = do
  forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.lhs.as" Int
10 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"as pattern" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Name
x forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+>
    forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep [ TCMT IO Doc
":" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
a
        , TCMT IO Doc
"=" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
v
        ]
  forall (m :: * -> *) a.
MonadAddContext m =>
ArgInfo -> Origin -> Name -> Term -> Type -> m a -> m a
addLetBinding (forall a. LensModality a => Modality -> a -> a
setModality Modality
m ArgInfo
defaultArgInfo) Origin
Inserted Name
x Term
v Type
a forall a b. (a -> b) -> a -> b
$ forall a. [AsBinding] -> TCM a -> TCM a
bindAsPatterns [AsBinding]
asb TCM a
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 -> TCMT IO ()
recheckStrippedWithPattern (ProblemEq Pattern
p Term
v Dom Type
a) = forall a (m :: * -> *).
(CheckInternal a, MonadCheckInternal m) =>
a -> Comparison -> TypeOf a -> m ()
checkInternal Term
v Comparison
CmpLeq (forall t e. Dom' t e -> e
unDom Dom Type
a)
  forall e (m :: * -> *) a.
MonadError e m =>
m a -> (e -> m a) -> m a
`catchError` \TCErr
_ -> forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError forall a b. (a -> b) -> a -> b
$ Pattern -> TypeError
IllTypedPatternAfterWithAbstraction Pattern
p

-- | Result of checking the LHS of a clause.
data LHSResult = LHSResult
  { LHSResult -> Int
lhsParameters   :: Nat
    -- ^ The number of original module parameters. These are present in the
    -- the patterns.
  , LHSResult -> Telescope
lhsVarTele      :: Telescope
    -- ^ Δ : The types of the pattern variables, in internal dependency order.
    -- Corresponds to 'clauseTel'.
  , LHSResult -> [NamedArg DeBruijnPattern]
lhsPatterns     :: [NamedArg DeBruijnPattern]
    -- ^ The patterns in internal syntax.
  , LHSResult -> Bool
lhsHasAbsurd    :: Bool
    -- ^ Whether the LHS has at least one absurd pattern.
  , LHSResult -> Arg Type
lhsBodyType     :: Arg Type
    -- ^ The type of the body. Is @bσ@ if @Γ@ is defined.
    -- 'Irrelevant' to indicate the rhs must be checked in irrelevant mode.
  , LHSResult -> Substitution
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.
  , LHSResult -> [AsBinding]
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).
  , LHSResult -> IntSet
lhsPartialSplit :: IntSet
    -- ^ have we done a partial split?
  , LHSResult -> Bool
lhsIndexedSplit :: Bool
    -- ^ have we split on an indexed type?
  }

instance InstantiateFull LHSResult where
  instantiateFull' :: LHSResult -> ReduceM LHSResult
instantiateFull' (LHSResult Int
n Telescope
tel [NamedArg DeBruijnPattern]
ps Bool
abs Arg Type
t Substitution
sub [AsBinding]
as IntSet
psplit Bool
ixsplit) = Int
-> Telescope
-> [NamedArg DeBruijnPattern]
-> Bool
-> Arg Type
-> Substitution
-> [AsBinding]
-> IntSet
-> Bool
-> LHSResult
LHSResult Int
n
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall t. InstantiateFull t => t -> ReduceM t
instantiateFull' Telescope
tel
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall t. InstantiateFull t => t -> ReduceM t
instantiateFull' [NamedArg DeBruijnPattern]
ps
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall t. InstantiateFull t => t -> ReduceM t
instantiateFull' Bool
abs
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall t. InstantiateFull t => t -> ReduceM t
instantiateFull' Arg Type
t
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall t. InstantiateFull t => t -> ReduceM t
instantiateFull' Substitution
sub
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall t. InstantiateFull t => t -> ReduceM t
instantiateFull' [AsBinding]
as
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (f :: * -> *) a. Applicative f => a -> f a
pure IntSet
psplit
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
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 :: forall a.
Call
-> Maybe QName
-> [NamedArg Pattern]
-> Type
-> Maybe Substitution
-> [ProblemEq]
-> (LHSResult -> TCM a)
-> TCM a
checkLeftHandSide Call
call Maybe QName
f [NamedArg Pattern]
ps Type
a Maybe Substitution
withSub' [ProblemEq]
strippedPats =
 forall (m :: * -> *) b c.
MonadBench m =>
Account (BenchPhase m) -> ((b -> m c) -> m c) -> (b -> m c) -> m c
Bench.billToCPS [Phase
Bench.Typing, Phase
Bench.CheckLHS] forall a b. (a -> b) -> a -> b
$
 forall (m :: * -> *) a b.
MonadTrace m =>
Call -> ((a -> m b) -> m b) -> (a -> m b) -> m b
traceCallCPS Call
call forall a b. (a -> b) -> a -> b
$ \ LHSResult -> TCMT IO a
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.
  Context
cxt <- forall a b. (a -> b) -> [a] -> [b]
map (forall a. LensOrigin a => Origin -> a -> a
setOrigin Origin
Inserted) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. [a] -> [a]
reverse forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). MonadTCEnv m => m Context
getContext
  let tel :: Telescope
tel = forall a. (a -> [Char]) -> ListTel' a -> Telescope
telFromList' forall a. Pretty a => a -> [Char]
prettyShow Context
cxt
      cps :: [NamedArg Pattern]
cps = [ forall a name. a -> Named name a
unnamed forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall e. BindName -> Pattern' e
A.VarP forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> BindName
A.mkBindName forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> a
fst forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall t a. Dom' t a -> Arg a
argFromDom ContextEntry
d
            | ContextEntry
d <- Context
cxt ]
      eqs0 :: [ProblemEq]
eqs0 = forall a b c d. (a -> b -> c -> d) -> [a] -> [b] -> [c] -> [d]
zipWith3 Pattern -> Term -> Dom Type -> ProblemEq
ProblemEq (forall a b. (a -> b) -> [a] -> [b]
map forall a. NamedArg a -> a
namedArg [NamedArg Pattern]
cps) (forall a b. (a -> b) -> [a] -> [b]
map Int -> Term
var forall a b. (a -> b) -> a -> b
$ forall a. Integral a => a -> [a]
downFrom forall a b. (a -> b) -> a -> b
$ forall a. Sized a => a -> Int
size Telescope
tel) (forall a. TermSubst a => Tele (Dom a) -> [Dom a]
flattenTel Telescope
tel)

  let finalChecks :: LHSState a -> TCM a
      finalChecks :: LHSState a -> TCMT IO a
finalChecks (LHSState Telescope
delta [NamedArg DeBruijnPattern]
qs0 (Problem [ProblemEq]
eqs [NamedArg Pattern]
rps LHSState a -> TCMT IO a
_) Arg Type
b [Maybe Int]
psplit Bool
ixsplit) = do

        forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.lhs.top" Int
20 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
          [ TCMT IO Doc
"lhs: final checks with remaining equations"
          , forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ if forall a. Null a => a -> Bool
null [ProblemEq]
eqs then TCMT IO Doc
"(none)" else forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
delta forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM [ProblemEq]
eqs
          , TCMT IO Doc
"qs0 =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
delta (forall (m :: * -> *).
MonadPretty m =>
[NamedArg DeBruijnPattern] -> m Doc
prettyTCMPatternList [NamedArg DeBruijnPattern]
qs0)
          ]

        forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (forall a. Null a => a -> Bool
null [NamedArg Pattern]
rps) forall a. HasCallStack => a
__IMPOSSIBLE__

        forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
delta forall a b. (a -> b) -> a -> b
$ do
          forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ ProblemEq -> TCMT IO ()
noShadowingOfConstructors [ProblemEq]
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.

        Int
arity_a <- Type -> TCM Int
arityPiPath Type
a
        -- Compute substitution from the out patterns @qs0@
        let notProj :: Pattern' x -> Bool
notProj ProjP{} = Bool
False
            notProj Pattern' x
_       = Bool
True
            numPats :: Int
numPats  = forall (t :: * -> *) a. Foldable t => t a -> Int
length forall a b. (a -> b) -> a -> b
$ forall a. (a -> Bool) -> [a] -> [a]
takeWhile (forall {x}. Pattern' x -> Bool
notProj forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. NamedArg a -> a
namedArg) [NamedArg DeBruijnPattern]
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 :: Substitution
weakSub | forall a. Maybe a -> Bool
isJust Maybe Substitution
withSub' = forall a. Int -> Substitution' a -> Substitution' a
wkS (forall a. Ord a => a -> a -> a
max Int
0 forall a b. (a -> b) -> a -> b
$ Int
numPats forall a. Num a => a -> a -> a
- Int
arity_a) forall a. Substitution' a
idS -- if numPats < arity, Θ is empty
                    | Bool
otherwise       = forall a. Int -> Substitution' a -> Substitution' a
wkS (Int
numPats forall a. Num a => a -> a -> a
- forall (t :: * -> *) a. Foldable t => t a -> Int
length Context
cxt) forall a. Substitution' a
idS
            withSub :: Substitution
withSub  = forall a. a -> Maybe a -> a
fromMaybe forall a. Substitution' a
idS Maybe Substitution
withSub'
            patSub :: Substitution
patSub   = forall a b. (a -> b) -> [a] -> [b]
map (DeBruijnPattern -> Term
patternToTerm forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. NamedArg a -> a
namedArg) (forall a. [a] -> [a]
reverse forall a b. (a -> b) -> a -> b
$ forall a. Int -> [a] -> [a]
take Int
numPats [NamedArg DeBruijnPattern]
qs0) forall a. DeBruijn a => [a] -> Substitution' a -> Substitution' a
++# forall a. Impossible -> Substitution' a
EmptyS HasCallStack => Impossible
impossible
            paramSub :: Substitution
paramSub = Substitution
patSub forall a.
EndoSubst a =>
Substitution' a -> Substitution' a -> Substitution' a
`composeS` Substitution
weakSub forall a.
EndoSubst a =>
Substitution' a -> Substitution' a -> Substitution' a
`composeS` Substitution
withSub

        [ProblemEq]
eqs <- forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
delta forall a b. (a -> b) -> a -> b
$ [ProblemEq] -> TCMT IO [ProblemEq]
checkPatternLinearity [ProblemEq]
eqs

        leftovers :: LeftoverPatterns
leftovers@(LeftoverPatterns IntMap [(Name, PatVarPosition)]
patVars [AsBinding]
asb0 [DotPattern]
dots [AbsurdPattern]
absurds [AnnotationPattern]
annps [Pattern]
otherPats)
          <- forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
delta forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
PureTCM m =>
[ProblemEq] -> m LeftoverPatterns
getLeftoverPatterns [ProblemEq]
eqs

        forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.lhs.leftover" Int
30 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
          [ TCMT IO Doc
"leftover patterns: " , forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
delta forall a b. (a -> b) -> a -> b
$ forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM LeftoverPatterns
leftovers) ]

        forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (forall a. Null a => a -> Bool
null [Pattern]
otherPats) forall a. HasCallStack => a
__IMPOSSIBLE__

        -- Get the user-written names for the pattern variables
        let ([Maybe Name]
vars, [AsBinding]
asb1) = Telescope
-> IntMap [(Name, PatVarPosition)] -> ([Maybe Name], [AsBinding])
getUserVariableNames Telescope
delta IntMap [(Name, PatVarPosition)]
patVars
            asb :: [AsBinding]
asb          = [AsBinding]
asb0 forall a. [a] -> [a] -> [a]
++ [AsBinding]
asb1

        -- Rename internal patterns with these names
        let makeVar :: Maybe Name -> Int -> DeBruijnPattern
makeVar     = forall b a. b -> (a -> b) -> Maybe a -> b
maybe forall a. DeBruijn a => Int -> a
deBruijnVar forall a b. (a -> b) -> a -> b
$ forall a. DeBruijn a => [Char] -> Int -> a
debruijnNamedVar forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> [Char]
nameToArgName
            ren :: PatternSubstitution
ren         = forall a. DeBruijn a => [a] -> Substitution' a
parallelS forall a b. (a -> b) -> a -> b
$ forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith Maybe Name -> Int -> DeBruijnPattern
makeVar (forall a. [a] -> [a]
reverse [Maybe Name]
vars) [Int
0..]

        [NamedArg DeBruijnPattern]
qs <- [NamedArg Pattern]
-> [NamedArg DeBruijnPattern] -> TCM [NamedArg DeBruijnPattern]
transferOrigins ([NamedArg Pattern]
cps forall a. [a] -> [a] -> [a]
++ [NamedArg Pattern]
ps) forall a b. (a -> b) -> a -> b
$ forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst PatternSubstitution
ren [NamedArg DeBruijnPattern]
qs0

        let hasAbsurd :: Bool
hasAbsurd = Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Null a => a -> Bool
null forall a b. (a -> b) -> a -> b
$ [AbsurdPattern]
absurds

        let lhsResult :: LHSResult
lhsResult = Int
-> Telescope
-> [NamedArg DeBruijnPattern]
-> Bool
-> Arg Type
-> Substitution
-> [AsBinding]
-> IntSet
-> Bool
-> LHSResult
LHSResult (forall (t :: * -> *) a. Foldable t => t a -> Int
length Context
cxt) Telescope
delta [NamedArg DeBruijnPattern]
qs Bool
hasAbsurd Arg Type
b Substitution
patSub [AsBinding]
asb ([Int] -> IntSet
IntSet.fromList forall a b. (a -> b) -> a -> b
$ forall a. [Maybe a] -> [a]
catMaybes [Maybe Int]
psplit) Bool
ixsplit

        -- Debug output
        forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.lhs.top" Int
10 forall a b. (a -> b) -> a -> b
$
          forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat [ TCMT IO Doc
"checked lhs:"
               , forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
                 [ TCMT IO Doc
"delta   = " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Telescope
delta
                 , TCMT IO Doc
"dots    = " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
delta (forall (m :: * -> *). Functor m => m Doc -> m Doc
brackets forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Semigroup (m Doc), Foldable t) =>
m Doc -> t (m Doc) -> [m Doc]
punctuate forall (m :: * -> *). Applicative m => m Doc
comma forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM [DotPattern]
dots)
                 , TCMT IO Doc
"asb     = " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
delta (forall (m :: * -> *). Functor m => m Doc -> m Doc
brackets forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Semigroup (m Doc), Foldable t) =>
m Doc -> t (m Doc) -> [m Doc]
punctuate forall (m :: * -> *). Applicative m => m Doc
comma forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM [AsBinding]
asb)
                 , TCMT IO Doc
"absurds = " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
delta (forall (m :: * -> *). Functor m => m Doc -> m Doc
brackets forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Semigroup (m Doc), Foldable t) =>
m Doc -> t (m Doc) -> [m Doc]
punctuate forall (m :: * -> *). Applicative m => m Doc
comma forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM [AbsurdPattern]
absurds)
                 , TCMT IO Doc
"qs      = " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
delta (forall (m :: * -> *) (t :: * -> *).
(Applicative m, Semigroup (m Doc), Foldable t) =>
t (m Doc) -> m Doc
prettyList forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty [NamedArg DeBruijnPattern]
qs)
                 , TCMT IO Doc
"b       = " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
delta (forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Arg Type
b)
                 ]
               ]
        forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.lhs.top" Int
30 forall a b. (a -> b) -> a -> b
$
          forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
                 [ TCMT IO Doc
"vars   = " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty [Maybe Name]
vars
                 , TCMT IO Doc
"b      = " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Arg Type
b
                 ]
        forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.lhs.top" Int
20 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"withSub  = " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Substitution
withSub
        forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.lhs.top" Int
20 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"weakSub  = " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Substitution
weakSub
        forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.lhs.top" Int
20 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"patSub   = " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Substitution
patSub
        forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.lhs.top" Int
20 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"paramSub = " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Substitution
paramSub

        Context
newCxt <- [Maybe Name] -> Telescope -> TCM Context
computeLHSContext [Maybe Name]
vars Telescope
delta

        forall (m :: * -> *) a.
MonadAddContext m =>
Substitution -> (Context -> Context) -> m a -> m a
updateContext Substitution
paramSub (forall a b. a -> b -> a
const Context
newCxt) forall a b. (a -> b) -> a -> b
$ do

          forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.lhs.top" Int
10 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"bound pattern variables"
          forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.lhs.top" Int
60 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"context = " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> (forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Telescope
getContextTelescope)
          forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.lhs.top" Int
10 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"type  = " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Arg Type
b
          forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.lhs.top" Int
60 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"type  = " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Arg Type
b

          forall a. [AsBinding] -> TCM a -> TCM a
bindAsPatterns [AsBinding]
asb forall a b. (a -> b) -> a -> b
$ do

            -- Check dot patterns
            forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ DotPattern -> TCMT IO ()
checkDotPattern [DotPattern]
dots
            forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ AbsurdPattern -> TCMT IO ()
checkAbsurdPattern [AbsurdPattern]
absurds
            forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ AnnotationPattern -> TCMT IO ()
checkAnnotationPattern [AnnotationPattern]
annps

          -- Issue2303: don't bind asb' for the continuation (return in lhsResult instead)
          LHSResult -> TCMT IO a
ret LHSResult
lhsResult

  LHSState a
st0 <- forall a.
Telescope
-> [ProblemEq]
-> [NamedArg Pattern]
-> Type
-> (LHSState a -> TCM a)
-> TCM (LHSState a)
initLHSState Telescope
tel [ProblemEq]
eqs0 [NamedArg Pattern]
ps Type
a LHSState a -> TCMT IO a
finalChecks

  -- after we have introduced variables, we can add the patterns stripped by
  -- with-desugaring to the state.
  let withSub :: Substitution
withSub = forall a. a -> Maybe a -> a
fromMaybe forall a. HasCallStack => a
__IMPOSSIBLE__ Maybe Substitution
withSub'
  [ProblemEq]
withEqs <- [ProblemEq] -> TCMT IO [ProblemEq]
updateProblemEqs forall a b. (a -> b) -> a -> b
$ forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution
withSub [ProblemEq]
strippedPats
  -- Jesper, 2017-05-13: re-check the stripped patterns here!
  forall (tcm :: * -> *) a.
(MonadTCEnv tcm, ReadTCState tcm) =>
tcm a -> tcm a
inTopContext forall a b. (a -> b) -> a -> b
$ forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext (LHSState a
st0 forall o i. o -> Lens' o i -> i
^. forall a. Lens' (LHSState a) Telescope
lhsTel) forall a b. (a -> b) -> a -> b
$
    forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [ProblemEq]
withEqs ProblemEq -> TCMT IO ()
recheckStrippedWithPattern

  let st :: LHSState a
st = forall o i. Lens' o i -> LensMap o i
over (forall a. Lens' (LHSState a) (Problem a)
lhsProblem forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Lens' (Problem a) [ProblemEq]
problemEqs) (forall a. [a] -> [a] -> [a]
++ [ProblemEq]
withEqs) LHSState a
st0

  -- doing the splits:
  (a
result, Blocked' Term ()
block) <- forall (tcm :: * -> *) a.
(MonadTCEnv tcm, ReadTCState tcm) =>
tcm a -> tcm a
unsafeInTopContext forall a b. (a -> b) -> a -> b
$ forall w (m :: * -> *) a. WriterT w m a -> m (a, w)
runWriterT forall a b. (a -> b) -> a -> b
$ (forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
`runReaderT` (forall a. Sized a => a -> Int
size Context
cxt)) forall a b. (a -> b) -> a -> b
$ forall (tcm :: * -> *) a.
(MonadTCM tcm, PureTCM tcm, MonadWriter (Blocked' Term ()) tcm,
 MonadError TCErr tcm, MonadTrace tcm, MonadReader Int tcm) =>
Maybe QName -> LHSState a -> tcm a
checkLHS Maybe QName
f LHSState a
st
  forall (m :: * -> *) a. Monad m => a -> m a
return a
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 :: Modality
-> PatternSubstitution -> Int -> Telescope -> Type -> TCMT IO ()
conSplitModalityCheck Modality
mod PatternSubstitution
rho Int
blocking Telescope
gamma Type
target = forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any ((forall a. Eq a => a -> a -> Bool
/= Modality
defaultModality) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. LensModality a => a -> Modality
getModality) Telescope
gamma) forall a b. (a -> b) -> a -> b
$ do
  forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.lhs.top" Int
30 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
    [ TCMT IO Doc
"LHS modality check for modality: " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Modality
mod
    , TCMT IO Doc
"rho:    " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (tcm :: * -> *) a.
(MonadTCEnv tcm, ReadTCState tcm) =>
tcm a -> tcm a
inTopContext (forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM PatternSubstitution
rho)
    , TCMT IO Doc
"gamma:  " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (tcm :: * -> *) a.
(MonadTCEnv tcm, ReadTCState tcm) =>
tcm a -> tcm a
inTopContext (forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Telescope
gamma)
    , TCMT IO Doc
"target: " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
target forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *). Functor m => m Doc -> m Doc
parens (forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Type
target)
    , TCMT IO Doc
"Δ'target: " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM (forall a. TermSubst a => PatternSubstitution -> a -> a
applyPatSubst PatternSubstitution
rho Type
target)
    , TCMT IO Doc
"blocking:" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Int
blocking
    ]
  case PatternSubstitution -> Int -> Maybe Int
firstForced PatternSubstitution
rho (forall (t :: * -> *) a. Foldable t => t a -> Int
length Telescope
gamma) of
    Just Int
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
        (Telescope
gamma0, Telescope
delta) = Int -> Telescope -> (Telescope, Telescope)
splitTelescopeAt (forall (t :: * -> *) a. Foldable t => t a -> Int
length Telescope
gamma forall a. Num a => a -> a -> a
- Int
ix) Telescope
gamma
        name :: Int -> TCMT IO Name
name = forall (tcm :: * -> *) a.
(MonadTCEnv tcm, ReadTCState tcm) =>
tcm a -> tcm a
inTopContext forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
gamma forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (m :: * -> *).
(Applicative m, MonadFail m, MonadTCEnv m) =>
Int -> m Name
nameOfBV
        delta'target :: Type
delta'target = forall a. TermSubst a => PatternSubstitution -> a -> a
applyPatSubst PatternSubstitution
rho Type
target
      forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.lhs.top" Int
30 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
        [ TCMT IO Doc
"found forced argument!"
        , TCMT IO Doc
"forced: " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Int
ix
        , TCMT IO Doc
"before: " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (tcm :: * -> *) a.
(MonadTCEnv tcm, ReadTCState tcm) =>
tcm a -> tcm a
inTopContext (forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Telescope
gamma0)
        , TCMT IO Doc
"after:  " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (tcm :: * -> *) a.
(MonadTCEnv tcm, ReadTCState tcm) =>
tcm a -> tcm a
inTopContext (forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
gamma0 (forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Telescope
delta))
        ]
      Name
forced <- Int -> TCMT IO Name
name Int
ix
      forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ (forall a b. [a] -> [b] -> [(a, b)]
zip [Int
ix forall a. Num a => a -> a -> a
- Int
1, Int
ix forall a. Num a => a -> a -> a
- Int
2 ..] (forall t. Tele (Dom t) -> [Dom ([Char], t)]
telToList Telescope
delta)) forall a b. (a -> b) -> a -> b
$ \(Int
arg, Dom ([Char], Type)
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' :: PatternSubstitution
rho' = forall a.
EndoSubst a =>
Substitution' a -> Substitution' a -> Substitution' a
composeS PatternSubstitution
rho (forall a. Int -> Substitution' a -> Substitution' a
wkS (Int
arg forall a. Num a => a -> a -> a
+ Int
1) forall a. Substitution' a
idS)
        Term
ty' <- forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce (forall a. TermSubst a => PatternSubstitution -> a -> a
applyPatSubst PatternSubstitution
rho' (forall t a. Type'' t a -> a
unEl (forall a b. (a, b) -> b
snd (forall t e. Dom' t e -> e
unDom Dom ([Char], Type)
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 :: Bool
docheck = forall (t :: * -> *). Foldable t => t Bool -> Bool
and
            [ Int
ix forall a. Free a => Int -> a -> Bool
`freeIn` forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst (forall a. Int -> Substitution' a -> Substitution' a
wkS (Int
arg forall a. Num a => a -> a -> a
+ Int
1) forall a. Substitution' a
idS) (forall t a. Type'' t a -> a
unEl (forall a b. (a, b) -> b
snd (forall t e. Dom' t e -> e
unDom Dom ([Char], Type)
d)))
            , Int
arg forall a. Eq a => a -> a -> Bool
/= Int
blocking
            , Int
arg forall a. Free a => Int -> a -> Bool
`freeIn` Type
target
            ]
        forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.lhs.top" Int
30 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
          [ TCMT IO Doc
"arg:        " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Int
arg
          , TCMT IO Doc
"arg type:   " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM (forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst (forall a. Int -> Substitution' a -> Substitution' a
wkS (Int
arg forall a. Num a => a -> a -> a
+ Int
1) forall a. Substitution' a
idS) (forall t a. Type'' t a -> a
unEl (forall a b. (a, b) -> b
snd (forall t e. Dom' t e -> e
unDom Dom ([Char], Type)
d))))
          , TCMT IO Doc
"check       " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Bool
docheck
          ]
        Name
argn <- Int -> TCMT IO Name
name Int
arg
        forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
docheck forall a b. (a -> b) -> a -> b
$
          MonadConstraint (TCMT IO) =>
WhyCheckModality -> Modality -> Term -> TCMT IO ()
usableAtModality (Name -> Name -> WhyCheckModality
IndexedClauseArg Name
forced Name
argn) Modality
mod Term
ty'
    Maybe Int
Nothing -> forall (f :: * -> *) a. Applicative f => a -> f a
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.
  MonadConstraint (TCMT IO) =>
WhyCheckModality -> Modality -> Term -> TCMT IO ()
usableAtModality WhyCheckModality
IndexedClause Modality
mod (forall t a. Type'' t a -> a
unEl (forall a. TermSubst a => PatternSubstitution -> a -> a
applyPatSubst PatternSubstitution
rho Type
target))
  forall (tcm :: * -> *) a.
(MonadTCEnv tcm, ReadTCState tcm) =>
tcm a -> tcm a
inTopContext forall a b. (a -> b) -> a -> b
$ forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
gamma forall a b. (a -> b) -> a -> b
$ MonadConstraint (TCMT IO) =>
WhyCheckModality -> Modality -> Term -> TCMT IO ()
usableAtModality WhyCheckModality
IndexedClause Modality
mod (forall t a. Type'' t a -> a
unEl Type
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 :: PatternSubstitution -> Int -> Maybe Int
firstForced PatternSubstitution
pat Int
level
      | Int
level forall a. Ord a => a -> a -> Bool
>= Int
0 = case forall a. EndoSubst a => Substitution' a -> Int -> a
lookupS PatternSubstitution
pat Int
level of
        DotP{} -> forall a. a -> Maybe a
Just Int
level
        DeBruijnPattern
_ -> PatternSubstitution -> Int -> Maybe Int
firstForced PatternSubstitution
pat (Int
level forall a. Num a => a -> a -> a
- Int
1)
      | Bool
otherwise = forall a. Maybe a
Nothing

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

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

      A.AsP PatInfo
_ BindName
_ Pattern
p  -> ProblemEq -> Bool
shouldSplit forall a b. (a -> b) -> a -> b
$ ProblemEq
problem { problemInPat :: Pattern
problemInPat = Pattern
p }
      A.AnnP PatInfo
_ Expr
_ Pattern
p -> ProblemEq -> Bool
shouldSplit forall a b. (a -> b) -> a -> b
$ ProblemEq
problem { problemInPat :: Pattern
problemInPat = Pattern
p }

      A.ProjP{}       -> forall a. HasCallStack => a
__IMPOSSIBLE__
      A.DefP{}        -> forall a. HasCallStack => a
__IMPOSSIBLE__
      A.PatternSynP{} -> forall a. HasCallStack => a
__IMPOSSIBLE__
      A.WithP{}       -> forall a. HasCallStack => a
__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 :: forall (tcm :: * -> *) a.
(MonadTCM tcm, PureTCM tcm, MonadWriter (Blocked' Term ()) tcm,
 MonadError TCErr tcm, MonadTrace tcm, MonadReader Int tcm) =>
Maybe QName -> LHSState a -> tcm a
checkLHS Maybe QName
mf = forall {tcm :: * -> *} {a} {a}.
MonadTCEnv tcm =>
(LHSState a -> tcm a) -> LHSState a -> tcm a
updateModality LHSState a -> tcm a
checkLHS_ where
    -- If the target type is irrelevant or in Prop,
    -- we need to check the lhs in irr. cxt. (see Issue 939).
 updateModality :: (LHSState a -> tcm a) -> LHSState a -> tcm a
updateModality LHSState a -> tcm a
cont st :: LHSState a
st@(LHSState Telescope
tel [NamedArg DeBruijnPattern]
ip Problem a
problem Arg Type
target [Maybe Int]
psplit Bool
_) = do
      let m :: Modality
m = forall a. LensModality a => a -> Modality
getModality Arg Type
target
      forall (tcm :: * -> *) m a.
(MonadTCEnv tcm, LensModality m) =>
m -> tcm a -> tcm a
applyModalityToContext Modality
m forall a b. (a -> b) -> a -> b
$ do
        LHSState a -> tcm a
cont forall a b. (a -> b) -> a -> b
$ forall o i. Lens' o i -> LensMap o i
over (forall a. Lens' (LHSState a) Telescope
lhsTel forall b c a. (b -> c) -> (a -> b) -> a -> c
. Lens' Telescope [Dom ([Char], Type)]
listTel)
                 (forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a -> b) -> a -> b
$ forall a. LensModality a => Modality -> a -> a
inverseApplyModalityButNotQuantity Modality
m) LHSState a
st
        -- Andreas, 2018-10-23, issue #3309
        -- the modalities in the clause telescope also need updating.

 checkLHS_ :: LHSState a -> tcm a
checkLHS_ st :: LHSState a
st@(LHSState Telescope
tel [NamedArg DeBruijnPattern]
ip Problem a
problem Arg Type
target [Maybe Int]
psplit Bool
ixsplit) = do
  forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.lhs" Int
40 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"tel is" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Telescope
tel
  forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.lhs" Int
40 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"ip is" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty [NamedArg DeBruijnPattern]
ip
  forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.lhs" Int
40 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"target is" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
tel (forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Arg Type
target)
  if forall a. Problem a -> Bool
isSolvedProblem Problem a
problem then
    forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM forall a b. (a -> b) -> a -> b
$ (Problem a
problem forall o i. o -> Lens' o i -> i
^. forall a. Lens' (Problem a) (LHSState a -> TCM a)
problemCont) LHSState a
st
  else do

    forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.lhs.top" Int
30 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
      [ TCMT IO Doc
"LHS state: " , forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM LHSState a
st) ]

    forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
unlessM (PragmaOptions -> Bool
optPatternMatching forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *) a. ReadTCState m => (TCState -> a) -> m a
getsTC forall a. LensPragmaOptions a => a -> PragmaOptions
getPragmaOptions) forall a b. (a -> b) -> a -> b
$
      forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (forall a. Problem a -> Bool
problemAllVariables Problem a
problem) forall a b. (a -> b) -> a -> b
$
        forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError forall a b. (a -> b) -> a -> b
$ [Char] -> TypeError
GenericError forall a b. (a -> b) -> a -> b
$ [Char]
"Pattern matching is disabled"

    let splitsToTry :: [ProblemEq]
splitsToTry = [ProblemEq] -> [ProblemEq]
splitStrategy forall a b. (a -> b) -> a -> b
$ Problem a
problem forall o i. o -> Lens' o i -> i
^. forall a. Lens' (Problem a) [ProblemEq]
problemEqs

    forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr ProblemEq
-> tcm (Either [TCErr] (LHSState a))
-> tcm (Either [TCErr] (LHSState a))
trySplit tcm (Either [TCErr] (LHSState a))
trySplitRest [ProblemEq]
splitsToTry forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
      Right LHSState a
st' -> forall (tcm :: * -> *) a.
(MonadTCM tcm, PureTCM tcm, MonadWriter (Blocked' Term ()) tcm,
 MonadError TCErr tcm, MonadTrace tcm, MonadReader Int tcm) =>
Maybe QName -> LHSState a -> tcm a
checkLHS Maybe QName
mf LHSState a
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 (TCErr
err:[TCErr]
_) -> forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError TCErr
err
      Left []      -> forall a. HasCallStack => a
__IMPOSSIBLE__

  where

    trySplit :: ProblemEq
             -> tcm (Either [TCErr] (LHSState a))
             -> tcm (Either [TCErr] (LHSState a))
    trySplit :: ProblemEq
-> tcm (Either [TCErr] (LHSState a))
-> tcm (Either [TCErr] (LHSState a))
trySplit ProblemEq
eq tcm (Either [TCErr] (LHSState a))
tryNextSplit = forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
runExceptT (ProblemEq -> ExceptT TCErr tcm (LHSState a)
splitArg ProblemEq
eq) forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
      Right LHSState a
st' -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a b. b -> Either a b
Right LHSState a
st'
      Left TCErr
err  -> forall (a :: * -> * -> *) b c d.
ArrowChoice a =>
a b c -> a (Either b d) (Either c d)
left (TCErr
errforall a. a -> [a] -> [a]
:) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> tcm (Either [TCErr] (LHSState a))
tryNextSplit

    -- If there are any remaining user patterns, try to split on them
    trySplitRest :: tcm (Either [TCErr] (LHSState a))
    trySplitRest :: tcm (Either [TCErr] (LHSState a))
trySplitRest = case Problem a
problem forall o i. o -> Lens' o i -> i
^. forall a. Lens' (Problem a) [NamedArg Pattern]
problemRestPats of
      []    -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a b. a -> Either a b
Left []
      (NamedArg Pattern
p:[NamedArg Pattern]
_) -> forall (a :: * -> * -> *) b c d.
ArrowChoice a =>
a b c -> a (Either b d) (Either c d)
left forall el coll. Singleton el coll => el -> coll
singleton forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
runExceptT (NamedArg Pattern -> ExceptT TCErr tcm (LHSState a)
splitRest NamedArg Pattern
p)

    splitArg :: ProblemEq -> ExceptT TCErr tcm (LHSState a)
    -- Split on constructor/literal pattern
    splitArg :: ProblemEq -> ExceptT TCErr tcm (LHSState a)
splitArg (ProblemEq Pattern
p Term
v Dom{unDom :: forall t e. Dom' t e -> e
unDom = Type
a}) = forall (m :: * -> *) a. MonadTrace m => Call -> m a -> m a
traceCall (Pattern -> Telescope -> Type -> Call
CheckPattern Pattern
p Telescope
tel Type
a) forall a b. (a -> b) -> a -> b
$ do

      forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.lhs.split" Int
30 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep
        [ TCMT IO Doc
"split looking at pattern"
        , forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"p =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA Pattern
p
        ]

      -- in order to split, v must be a variable.
      Int
i <- forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM forall a b. (a -> b) -> a -> b
$ forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
tel forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a b.
Monad m =>
m (Maybe a) -> (a -> m b) -> m b -> m b
ifJustM (forall (m :: * -> *). PureTCM m => Term -> Type -> m (Maybe Int)
isEtaVar Term
v Type
a) forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$
             forall (m :: * -> *) a.
(HasCallStack, ReadTCState m, MonadError TCErr m, MonadTCEnv m) =>
TypeError -> m a
softTypeError forall a b. (a -> b) -> a -> b
$ Term -> Type -> TypeError
SplitOnNonVariable Term
v Type
a

      let pos :: Int
pos = forall a. Sized a => a -> Int
size Telescope
tel forall a. Num a => a -> a -> a
- (Int
i forall a. Num a => a -> a -> a
+ Int
1)
          (Telescope
delta1, tel' :: Telescope
tel'@(ExtendTel Dom Type
dom Abs Telescope
adelta2)) = Int -> Telescope -> (Telescope, Telescope)
splitTelescopeAt Int
pos Telescope
tel -- TODO:: tel' defined but not used

      Pattern
p <- forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
(MonadError TCErr m, MonadTCEnv m, ReadTCState m, HasBuiltins m) =>
Pattern -> m Pattern
expandLitPattern Pattern
p
      let splitOnPat :: Pattern -> ExceptT TCErr tcm (LHSState a)
splitOnPat = \case
            (A.LitP PatInfo
_ Literal
l)      -> Telescope
-> Dom Type
-> Abs Telescope
-> Literal
-> ExceptT TCErr tcm (LHSState a)
splitLit Telescope
delta1 Dom Type
dom Abs Telescope
adelta2 Literal
l
            p :: Pattern
p@A.RecP{}        -> Telescope
-> Dom Type
-> Abs Telescope
-> Pattern
-> Maybe AmbiguousQName
-> ExceptT TCErr tcm (LHSState a)
splitCon Telescope
delta1 Dom Type
dom Abs Telescope
adelta2 Pattern
p forall a. Maybe a
Nothing
            p :: Pattern
p@(A.ConP ConPatInfo
_ AmbiguousQName
c [NamedArg Pattern]
ps) -> Telescope
-> Dom Type
-> Abs Telescope
-> Pattern
-> Maybe AmbiguousQName
-> ExceptT TCErr tcm (LHSState a)
splitCon Telescope
delta1 Dom Type
dom Abs Telescope
adelta2 Pattern
p forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just AmbiguousQName
c
            p :: Pattern
p@(A.EqualP PatInfo
_ [(Expr, Expr)]
ts) -> Telescope
-> Dom Type
-> Abs Telescope
-> [(Expr, Expr)]
-> ExceptT TCErr tcm (LHSState a)
splitPartial Telescope
delta1 Dom Type
dom Abs Telescope
adelta2 [(Expr, Expr)]
ts
            A.AsP PatInfo
_ BindName
_ Pattern
p       -> Pattern -> ExceptT TCErr tcm (LHSState a)
splitOnPat Pattern
p
            A.AnnP PatInfo
_ Expr
_ Pattern
p      -> Pattern -> ExceptT TCErr tcm (LHSState a)
splitOnPat Pattern
p

            A.VarP{}        -> forall a. HasCallStack => a
__IMPOSSIBLE__
            A.WildP{}       -> forall a. HasCallStack => a
__IMPOSSIBLE__
            A.DotP{}        -> forall a. HasCallStack => a
__IMPOSSIBLE__
            A.AbsurdP{}     -> forall a. HasCallStack => a
__IMPOSSIBLE__
            A.ProjP{}       -> forall a. HasCallStack => a
__IMPOSSIBLE__
            A.DefP{}        -> forall a. HasCallStack => a
__IMPOSSIBLE__
            A.PatternSynP{} -> forall a. HasCallStack => a
__IMPOSSIBLE__
            A.WithP{}       -> forall a. HasCallStack => a
__IMPOSSIBLE__
      Pattern -> ExceptT TCErr tcm (LHSState a)
splitOnPat Pattern
p


    splitRest :: NamedArg A.Pattern -> ExceptT TCErr tcm (LHSState a)
    splitRest :: NamedArg Pattern -> ExceptT TCErr tcm (LHSState a)
splitRest NamedArg Pattern
p = forall (m :: * -> *) x a.
(MonadTrace m, HasRange x) =>
x -> m a -> m a
setCurrentRange NamedArg Pattern
p forall a b. (a -> b) -> a -> b
$ do
      forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.lhs.split" Int
20 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep
        [ TCMT IO Doc
"splitting problem rest"
        , forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"projection pattern =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA NamedArg Pattern
p
        , forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"eliminates type    =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Arg Type
target
        ]
      forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.lhs.split" Int
80 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep
        [ forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). Applicative m => [Char] -> m Doc
text forall a b. (a -> b) -> a -> b
$ [Char]
"projection pattern (raw) = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show NamedArg Pattern
p
        ]

      -- @p@ should be a projection pattern projection from @target@
      (ProjOrigin
orig, AmbiguousQName
ambProjName) <- forall a b. Maybe a -> (a -> b) -> b -> b
ifJust (forall a. IsProjP a => a -> Maybe (ProjOrigin, AmbiguousQName)
A.isProjP NamedArg Pattern
p) forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
tel forall a b. (a -> b) -> a -> b
$ do
        Maybe Blocker
block <- forall t (m :: * -> *).
(Reduce t, IsMeta t, MonadReduce m) =>
t -> m (Maybe Blocker)
isBlocked Arg Type
target
        forall (m :: * -> *) a.
(HasCallStack, ReadTCState m, MonadError TCErr m, MonadTCEnv m) =>
TypeError -> m a
softTypeError forall a b. (a -> b) -> a -> b
$ Maybe Blocker -> NamedArg Pattern -> Type -> TypeError
CannotEliminateWithPattern Maybe Blocker
block NamedArg Pattern
p (forall e. Arg e -> e
unArg Arg Type
target)

      (QName
projName, Bool
comatchingAllowed, QName
recName, Arg Type
projType, ArgInfo
ai) <- forall (m :: * -> *) a.
(MonadTCM m, MonadError TCErr m) =>
TCM a -> m a
suspendErrors forall a b. (a -> b) -> a -> b
$ 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 :: Maybe Hiding
h = if ProjOrigin
orig forall a. Eq a => a -> a -> Bool
== ProjOrigin
ProjPostfix then forall a. Maybe a
Nothing else forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall a. LensHiding a => a -> Hiding
getHiding NamedArg Pattern
p
        forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
tel forall a b. (a -> b) -> a -> b
$ Maybe Hiding
-> AmbiguousQName
-> Arg Type
-> TCM (QName, Bool, QName, Arg Type, ArgInfo)
disambiguateProjection Maybe Hiding
h AmbiguousQName
ambProjName Arg Type
target

      forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless Bool
comatchingAllowed forall a b. (a -> b) -> a -> b
$ do
        forall (m :: * -> *) a.
(HasCallStack, MonadTCM m) =>
TypeError -> m a
hardTypeError forall a b. (a -> b) -> a -> b
$ QName -> TypeError
ComatchingDisabledForRecord QName
recName

      -- Compute the new rest type by applying the projection type to 'self'.
      -- Note: we cannot be in a let binding.
      QName
f <- forall a b. Maybe a -> (a -> b) -> b -> b
ifJust Maybe QName
mf forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a.
(HasCallStack, MonadTCM m) =>
TypeError -> m a
hardTypeError forall a b. (a -> b) -> a -> b
$
             [Char] -> TypeError
GenericError [Char]
"Cannot use copatterns in a let binding"
      let self :: Term
self = QName -> Elims -> Term
Def QName
f forall a b. (a -> b) -> a -> b
$ [NamedArg DeBruijnPattern] -> Elims
patternsToElims [NamedArg DeBruijnPattern]
ip
      Arg Type
target' <- forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (forall a (m :: * -> *).
(PiApplyM a, MonadReduce m, HasBuiltins m) =>
Type -> a -> m Type
`piApplyM` Term
self) Arg Type
projType

      -- Compute the new state
      let projP :: NamedArg DeBruijnPattern
projP    = forall b a. IsBool b => b -> (a -> a) -> a -> a
applyWhen (ProjOrigin
orig forall a. Eq a => a -> a -> Bool
== ProjOrigin
ProjPostfix) (forall a. LensHiding a => Hiding -> a -> a
setHiding Hiding
NotHidden) forall a b. (a -> b) -> a -> b
$
                       forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
ai forall a b. (a -> b) -> a -> b
$ forall name a. Maybe name -> a -> Named name a
Named forall a. Maybe a
Nothing (forall x. ProjOrigin -> QName -> Pattern' x
ProjP ProjOrigin
orig QName
projName)
          ip' :: [NamedArg DeBruijnPattern]
ip'      = [NamedArg DeBruijnPattern]
ip forall a. [a] -> [a] -> [a]
++ [NamedArg DeBruijnPattern
projP]
          -- drop the projection pattern (already splitted)
          problem' :: Problem a
problem' = forall o i. Lens' o i -> LensMap o i
over forall a. Lens' (Problem a) [NamedArg Pattern]
problemRestPats (forall a. Int -> [a] -> [a]
drop Int
1) Problem a
problem
      forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM forall a b. (a -> b) -> a -> b
$ forall a. LHSState a -> TCM (LHSState a)
updateLHSState (forall a.
Telescope
-> [NamedArg DeBruijnPattern]
-> Problem a
-> Arg Type
-> [Maybe Int]
-> Bool
-> LHSState a
LHSState Telescope
tel [NamedArg DeBruijnPattern]
ip' Problem a
problem' Arg Type
target' [Maybe Int]
psplit Bool
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 :: Telescope
-> Dom Type
-> Abs Telescope
-> [(Expr, Expr)]
-> ExceptT TCErr tcm (LHSState a)
splitPartial Telescope
delta1 Dom Type
dom Abs Telescope
adelta2 [(Expr, Expr)]
ts = do

      forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (forall t e. Dom' t e -> Bool
domIsFinite Dom Type
dom) forall a b. (a -> b) -> a -> b
$ forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM forall a b. (a -> b) -> a -> b
$ forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
delta1 forall a b. (a -> b) -> a -> b
$
        forall (m :: * -> *) a.
(HasCallStack, ReadTCState m, MonadError TCErr m, MonadTCEnv m) =>
TypeError -> m a
softTypeError forall a b. (a -> b) -> a -> b
$ Dom Type -> TypeError
SplitOnPartial Dom Type
dom

      Type
tInterval <- forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Type
primIntervalType

      [Maybe Name]
names <- forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM forall a b. (a -> b) -> a -> b
$ forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
tel forall a b. (a -> b) -> a -> b
$ do
        LeftoverPatterns{patternVariables :: LeftoverPatterns -> IntMap [(Name, PatVarPosition)]
patternVariables = IntMap [(Name, PatVarPosition)]
vars} <- forall (m :: * -> *).
PureTCM m =>
[ProblemEq] -> m LeftoverPatterns
getLeftoverPatterns forall a b. (a -> b) -> a -> b
$ Problem a
problem forall o i. o -> Lens' o i -> i
^. forall a. Lens' (Problem a) [ProblemEq]
problemEqs
        forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. Int -> [a] -> [a]
take (forall a. Sized a => a -> Int
size Telescope
delta1) forall a b. (a -> b) -> a -> b
$ forall a b. (a, b) -> a
fst forall a b. (a -> b) -> a -> b
$ Telescope
-> IntMap [(Name, PatVarPosition)] -> ([Maybe Name], [AsBinding])
getUserVariableNames Telescope
tel IntMap [(Name, PatVarPosition)]
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 |Ξ|
      --
      Int
lhsCxtSize <- forall r (m :: * -> *). MonadReader r m => m r
ask -- size of the context before checkLHS call.
      forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.lhs.split.partial" Int
10 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"lhsCxtSize =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Int
lhsCxtSize

      Context
newContext <- forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM forall a b. (a -> b) -> a -> b
$ [Maybe Name] -> Telescope -> TCM Context
computeLHSContext [Maybe Name]
names Telescope
delta1
      forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.lhs.split.partial" Int
10 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"newContext =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Context
newContext

      let cpSub :: Substitution
cpSub = forall a. Int -> Substitution' a
raiseS forall a b. (a -> b) -> a -> b
$ forall a. Sized a => a -> Int
size Context
newContext forall a. Num a => a -> a -> a
- Int
lhsCxtSize

      (Telescope
gamma,Substitution
sigma) <- forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a.
MonadAddContext m =>
Substitution -> (Context -> Context) -> m a -> m a
updateContext Substitution
cpSub (forall a b. a -> b -> a
const Context
newContext) forall a b. (a -> b) -> a -> b
$ do
         [Term]
ts <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [(Expr, Expr)]
ts forall a b. (a -> b) -> a -> b
$ \ (Expr
t,Expr
u) -> do
                 forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.lhs.split.partial" Int
10 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"currentCxt =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> (forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (m :: * -> *). MonadTCEnv m => m Context
getContext)
                 forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.lhs.split.partial" Int
10 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). Applicative m => [Char] -> m Doc
text [Char]
"t, u (Expr) =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM (Expr
t,Expr
u)
                 Term
t <- Expr -> Type -> TCMT IO Term
checkExpr Expr
t Type
tInterval
                 Term
u <- Expr -> Type -> TCMT IO Term
checkExpr Expr
u Type
tInterval
                 forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.lhs.split.partial" Int
10 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). Applicative m => [Char] -> m Doc
text [Char]
"t, u        =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty (Term
t, Term
u)
                 IntervalView
u <- forall (m :: * -> *). HasBuiltins m => Term -> m IntervalView
intervalView forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce Term
u
                 case IntervalView
u of
                   IntervalView
IZero -> forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primINeg forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
t
                   IntervalView
IOne  -> forall (m :: * -> *) a. Monad m => a -> m a
return Term
t
                   IntervalView
_     -> forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError forall a b. (a -> b) -> a -> b
$ [Char] -> TypeError
GenericError forall a b. (a -> b) -> a -> b
$ [Char]
"Only 0 or 1 allowed on the rhs of face"
         -- Example: ts = (i=0) (j=1) will result in phi = ¬ i & j
         Term
phi <- case [Term]
ts of
                   [] -> do
                     Term
a <- forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce (forall t a. Type'' t a -> a
unEl forall a b. (a -> b) -> a -> b
$ forall t e. Dom' t e -> e
unDom Dom Type
dom)
                     -- builtinIsOne is defined, since this is a precondition for having Partial
                     QName
isone <- forall a. a -> Maybe a -> a
fromMaybe forall a. HasCallStack => a
__IMPOSSIBLE__ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>  -- newline because of CPP
                       forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe QName)
getBuiltinName' BuiltinId
builtinIsOne
                     case Term
a of
                       Def QName
q [Apply Arg Term
phi] | QName
q forall a. Eq a => a -> a -> Bool
== QName
isone -> forall (m :: * -> *) a. Monad m => a -> m a
return (forall e. Arg e -> e
unArg Arg Term
phi)
                       Term
_           -> forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError forall a b. (a -> b) -> a -> b
$ Term -> TypeError
BuiltinMustBeIsOne Term
a

                   [Term]
_  -> forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (\ TCMT IO Term
x TCMT IO Term
y -> forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primIMin forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> TCMT IO Term
x forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> TCMT IO Term
y) forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primIOne (forall a b. (a -> b) -> [a] -> [b]
map forall (f :: * -> *) a. Applicative f => a -> f a
pure [Term]
ts)
         forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.lhs.split.partial" Int
10 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). Applicative m => [Char] -> m Doc
text [Char]
"phi           =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
phi
         forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.lhs.split.partial" Int
30 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). Applicative m => [Char] -> m Doc
text [Char]
"phi           =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Term
phi
         Term
phi <- forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce Term
phi
         forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.lhs.split.partial" Int
10 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). Applicative m => [Char] -> m Doc
text [Char]
"phi (reduced) =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
phi
         [(Telescope, Substitution)]
refined <- forall (m :: * -> *) a.
MonadConversion m =>
Term
-> (IntMap Bool -> Blocker -> Term -> m a)
-> (IntMap Bool -> Substitution -> m a)
-> m [a]
forallFaceMaps Term
phi (\ IntMap Bool
bs Blocker
m Term
t -> forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError forall a b. (a -> b) -> a -> b
$ [Char] -> TypeError
GenericError forall a b. (a -> b) -> a -> b
$ [Char]
"face blocked on meta")
                            (\IntMap Bool
_ Substitution
sigma -> (,Substitution
sigma) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Telescope
getContextTelescope)
         case [(Telescope, Substitution)]
refined of
           [(Telescope
gamma,Substitution
sigma)] -> forall (m :: * -> *) a. Monad m => a -> m a
return (Telescope
gamma,Substitution
sigma)
           []              -> forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError forall a b. (a -> b) -> a -> b
$ [Char] -> TypeError
GenericError forall a b. (a -> b) -> a -> b
$ [Char]
"The face constraint is unsatisfiable."
           [(Telescope, Substitution)]
_               -> forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError forall a b. (a -> b) -> a -> b
$ [Char] -> TypeError
GenericError forall a b. (a -> b) -> a -> b
$ [Char]
"Cannot have disjunctions in a face constraint."
      Term
itisone <- forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primItIsOne
      -- substitute the literal in p1 and dpi
      forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.lhs.faces" Int
60 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). Applicative m => [Char] -> m Doc
text forall a b. (a -> b) -> a -> b
$ forall a. Show a => a -> [Char]
show Substitution
sigma

      let oix :: Int
oix = forall a. Sized a => a -> Int
size Abs Telescope
adelta2 -- de brujin index of IsOne
          o_n :: Int
o_n = forall a. a -> Maybe a -> a
fromMaybe forall a. HasCallStack => a
__IMPOSSIBLE__ forall a b. (a -> b) -> a -> b
$
            forall a. (a -> Bool) -> [a] -> Maybe Int
findIndex (\ NamedArg DeBruijnPattern
x -> case forall name a. Named name a -> a
namedThing (forall e. Arg e -> e
unArg NamedArg DeBruijnPattern
x) of
                                   VarP PatternInfo
_ DBPatVar
x -> DBPatVar -> Int
dbPatVarIndex DBPatVar
x forall a. Eq a => a -> a -> Bool
== Int
oix
                                   DeBruijnPattern
_        -> Bool
False) [NamedArg DeBruijnPattern]
ip
          delta2' :: Telescope
delta2' = forall a. Subst a => Abs a -> SubstArg a -> a
absApp Abs Telescope
adelta2 Term
itisone
          delta2 :: Telescope
delta2 = forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution
sigma Telescope
delta2'
          mkConP :: Term -> DeBruijnPattern
mkConP (Con ConHead
c ConInfo
_ [])
             = forall x.
ConHead -> ConPatternInfo -> [NamedArg (Pattern' x)] -> Pattern' x
ConP ConHead
c (ConPatternInfo
noConPatternInfo { conPType :: Maybe (Arg Type)
conPType = forall a. a -> Maybe a
Just (forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
defaultArgInfo Type
tInterval)
                                              , conPFallThrough :: Bool
conPFallThrough = Bool
True })
                          []
          mkConP (Var Int
i []) = forall x. PatternInfo -> x -> Pattern' x
VarP PatternInfo
defaultPatternInfo ([Char] -> Int -> DBPatVar
DBPatVar [Char]
"x" Int
i)
          mkConP Term
_          = forall a. HasCallStack => a
__IMPOSSIBLE__
          rho0 :: PatternSubstitution
rho0 = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Term -> DeBruijnPattern
mkConP Substitution
sigma

          rho :: PatternSubstitution
rho    = forall a. Int -> Substitution' a -> Substitution' a
liftS (forall a. Sized a => a -> Int
size Telescope
delta2) forall a b. (a -> b) -> a -> b
$ forall a. DeBruijn a => a -> Substitution' a -> Substitution' a
consS (forall x. PatternInfo -> Term -> Pattern' x
DotP PatternInfo
defaultPatternInfo Term
itisone) PatternSubstitution
rho0

          delta' :: Telescope
delta'   = forall t. Abstract t => Telescope -> t -> t
abstract Telescope
gamma Telescope
delta2
          eqs' :: [ProblemEq]
eqs'     = forall a. TermSubst a => PatternSubstitution -> a -> a
applyPatSubst PatternSubstitution
rho forall a b. (a -> b) -> a -> b
$ Problem a
problem forall o i. o -> Lens' o i -> i
^. forall a. Lens' (Problem a) [ProblemEq]
problemEqs
          ip' :: [NamedArg DeBruijnPattern]
ip'      = forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst PatternSubstitution
rho [NamedArg DeBruijnPattern]
ip
          target' :: Arg Type
target'  = forall a. TermSubst a => PatternSubstitution -> a -> a
applyPatSubst PatternSubstitution
rho Arg Type
target

      -- Compute the new state
      let problem' :: Problem a
problem' = forall o i. Lens' o i -> LensSet o i
set forall a. Lens' (Problem a) [ProblemEq]
problemEqs [ProblemEq]
eqs' Problem a
problem
      forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.lhs.split.partial" Int
60 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). Applicative m => [Char] -> m Doc
text (forall a. Show a => a -> [Char]
show Problem a
problem')
      forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM forall a b. (a -> b) -> a -> b
$ forall a. LHSState a -> TCM (LHSState a)
updateLHSState (forall a.
Telescope
-> [NamedArg DeBruijnPattern]
-> Problem a
-> Arg Type
-> [Maybe Int]
-> Bool
-> LHSState a
LHSState Telescope
delta' [NamedArg DeBruijnPattern]
ip' Problem a
problem' Arg Type
target' ([Maybe Int]
psplit forall a. [a] -> [a] -> [a]
++ [forall a. a -> Maybe a
Just Int
o_n]) Bool
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 :: Telescope
-> Dom Type
-> Abs Telescope
-> Literal
-> ExceptT TCErr tcm (LHSState a)
splitLit Telescope
delta1 dom :: Dom Type
dom@Dom{domInfo :: forall t e. Dom' t e -> ArgInfo
domInfo = ArgInfo
info, unDom :: forall t e. Dom' t e -> e
unDom = Type
a} Abs Telescope
adelta2 Literal
lit = do
      let delta2 :: Telescope
delta2 = forall a. Subst a => Abs a -> SubstArg a -> a
absApp Abs Telescope
adelta2 (Literal -> Term
Lit Literal
lit)
          delta' :: Telescope
delta' = forall t. Abstract t => Telescope -> t -> t
abstract Telescope
delta1 Telescope
delta2
          rho :: PatternSubstitution
rho    = forall a. DeBruijn a => Int -> a -> Substitution' a
singletonS (forall a. Sized a => a -> Int
size Telescope
delta2) (forall a. Literal -> Pattern' a
litP Literal
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' :: [ProblemEq]
eqs'     = forall a. TermSubst a => PatternSubstitution -> a -> a
applyPatSubst PatternSubstitution
rho forall a b. (a -> b) -> a -> b
$ Problem a
problem forall o i. o -> Lens' o i -> i
^. forall a. Lens' (Problem a) [ProblemEq]
problemEqs
          ip' :: [NamedArg DeBruijnPattern]
ip'      = forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst PatternSubstitution
rho [NamedArg DeBruijnPattern]
ip
          target' :: Arg Type
target'  = forall a. TermSubst a => PatternSubstitution -> a -> a
applyPatSubst PatternSubstitution
rho Arg Type
target

      -- Andreas, 2010-09-07 cannot split on irrelevant args
      forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (forall a. LensRelevance a => a -> Bool
usableRelevance ArgInfo
info) forall a b. (a -> b) -> a -> b
$
        forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
delta1 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a.
(HasCallStack, ReadTCState m, MonadError TCErr m, MonadTCEnv m) =>
TypeError -> m a
softTypeError forall a b. (a -> b) -> a -> b
$ Dom Type -> TypeError
SplitOnIrrelevant Dom Type
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.

      forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
unlessM (forall (m :: * -> *) a.
(HasOptions m, LensCohesion a) =>
a -> m Bool
splittableCohesion ArgInfo
info) forall a b. (a -> b) -> a -> b
$
        forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
delta1 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a.
(HasCallStack, ReadTCState m, MonadError TCErr m, MonadTCEnv m) =>
TypeError -> m a
softTypeError forall a b. (a -> b) -> a -> b
$ Dom Type -> TypeError
SplitOnUnusableCohesion Dom Type
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.
      forall (m :: * -> *) a.
(MonadTCM m, MonadError TCErr m) =>
TCM a -> m a
suspendErrors forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). MonadConversion m => Type -> Type -> m ()
equalType Type
a forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
Literal -> m Type
litType Literal
lit

      -- Compute the new state
      let problem' :: Problem a
problem' = forall o i. Lens' o i -> LensSet o i
set forall a. Lens' (Problem a) [ProblemEq]
problemEqs [ProblemEq]
eqs' Problem a
problem
      forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM forall a b. (a -> b) -> a -> b
$ forall a. LHSState a -> TCM (LHSState a)
updateLHSState (forall a.
Telescope
-> [NamedArg DeBruijnPattern]
-> Problem a
-> Arg Type
-> [Maybe Int]
-> Bool
-> LHSState a
LHSState Telescope
delta' [NamedArg DeBruijnPattern]
ip' Problem a
problem' Arg Type
target' [Maybe Int]
psplit Bool
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 :: Telescope
-> Dom Type
-> Abs Telescope
-> Pattern
-> Maybe AmbiguousQName
-> ExceptT TCErr tcm (LHSState a)
splitCon Telescope
delta1 dom :: Dom Type
dom@Dom{domInfo :: forall t e. Dom' t e -> ArgInfo
domInfo = ArgInfo
info, unDom :: forall t e. Dom' t e -> e
unDom = Type
a} Abs Telescope
adelta2 Pattern
focusPat Maybe AmbiguousQName
ambC = do
      let delta2 :: Telescope
delta2 = forall a. Subst a => Abs a -> a
absBody Abs Telescope
adelta2

      forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.lhs.split" Int
10 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
        [ TCMT IO Doc
"checking lhs"
        , forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"tel =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Telescope
tel
        , forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"rel =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *). Applicative m => [Char] -> m Doc
text (forall a. Show a => a -> [Char]
show forall a b. (a -> b) -> a -> b
$ forall a. LensRelevance a => a -> Relevance
getRelevance ArgInfo
info)
        , forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"mod =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *). Applicative m => [Char] -> m Doc
text (forall a. Show a => a -> [Char]
show forall a b. (a -> b) -> a -> b
$ forall a. LensModality a => a -> Modality
getModality  ArgInfo
info)
        ]

      forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.lhs.split" Int
15 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
        [ TCMT IO Doc
"split problem"
        , forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
          [ TCMT IO Doc
"delta1 = " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Telescope
delta1
          , TCMT IO Doc
"a      = " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
delta1 (forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
a)
          , TCMT IO Doc
"delta2 = " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
delta1
                              (forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext ([Char]
"x" :: String, Dom Type
dom) (forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Telescope
delta2))
          ]
        ]

      -- We cannot split on (shape-)irrelevant arguments.
      forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"tc.lhs.split" Int
30 forall a b. (a -> b) -> a -> b
$ [Char]
"split ConP: relevance is " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show (forall a. LensRelevance a => a -> Relevance
getRelevance ArgInfo
info)
      forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (forall a. LensRelevance a => a -> Bool
usableRelevance ArgInfo
info) forall a b. (a -> b) -> a -> b
$ forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
delta1 forall a b. (a -> b) -> a -> b
$
        forall (m :: * -> *) a.
(HasCallStack, ReadTCState m, MonadError TCErr m, MonadTCEnv m) =>
TypeError -> m a
softTypeError forall a b. (a -> b) -> a -> b
$ Dom Type -> TypeError
SplitOnIrrelevant Dom Type
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.

      forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
unlessM (forall (m :: * -> *) a.
(HasOptions m, LensCohesion a) =>
a -> m Bool
splittableCohesion ArgInfo
info) forall a b. (a -> b) -> a -> b
$
        forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
delta1 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a.
(HasCallStack, ReadTCState m, MonadError TCErr m, MonadTCEnv m) =>
TypeError -> m a
softTypeError forall a b. (a -> b) -> a -> b
$ Dom Type -> TypeError
SplitOnUnusableCohesion Dom Type
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 :: Maybe NoLeftInv
genTrx = forall a. Bool -> a -> Maybe a
boolToMaybe ((forall a. LensCohesion a => a -> Cohesion
getCohesion ArgInfo
info forall a. Eq a => a -> a -> Bool
== Cohesion
Flat)) NoLeftInv
SplitOnFlat

      -- We should be at a data/record type
      (DataOrRecord
dr, QName
d, Args
pars, Args
ixs) <- forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
delta1 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
(MonadTCM m, PureTCM m) =>
Type -> ExceptT TCErr m (DataOrRecord, QName, Args, Args)
isDataOrRecordType Type
a
      let isRec :: Bool
isRec = case DataOrRecord
dr of
            IsData{}   -> Bool
False
            IsRecord{} -> Bool
True

      forall (m :: * -> *).
MonadTCError m =>
QName -> DataOrRecord -> m ()
checkMatchingAllowed QName
d DataOrRecord
dr  -- No splitting on coinductive constructors.
      forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
delta1 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a ty.
(MonadTCM m, PureTCM m, MonadError TCErr m, LensSort a,
 PrettyTCM a, LensSort ty, PrettyTCM ty) =>
DataOrRecord -> a -> Telescope -> Maybe ty -> m ()
checkSortOfSplitVar DataOrRecord
dr Type
a Telescope
delta2 (forall a. a -> Maybe a
Just Arg Type
target)

      -- Jesper, 2019-09-13: if the data type we split on is a strict
      -- set, we locally enable --with-K during unification.
      TCMT IO UnificationResult -> TCMT IO UnificationResult
withKIfStrict <- forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce (forall a. LensSort a => a -> Sort' Term
getSort Type
a) forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \ Sort' Term
dsort ->
        forall b a. IsBool b => b -> (a -> a) -> a -> a
applyWhen (forall t. Sort' t -> Bool
isStrictDataSort Sort' Term
dsort) forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a b.
MonadTCEnv m =>
Lens' TCEnv a -> (a -> a) -> m b -> m b
locallyTC Lens' TCEnv Bool
eSplitOnStrict forall a b. (a -> b) -> a -> b
$ forall a b. a -> b -> a
const Bool
True

      -- The constructor should construct an element of this datatype
      (ConHead
c :: ConHead, Type
b :: Type) <- forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM forall a b. (a -> b) -> a -> b
$ forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
delta1 forall a b. (a -> b) -> a -> b
$ case Maybe AmbiguousQName
ambC of
        Just AmbiguousQName
ambC -> AmbiguousQName -> QName -> Args -> TCM (ConHead, Type)
disambiguateConstructor AmbiguousQName
ambC QName
d Args
pars
        Maybe AmbiguousQName
Nothing   -> QName -> Args -> Type -> TCM (ConHead, Type)
getRecordConstructor QName
d Args
pars Type
a

      -- Don't split on lazy (non-eta) constructor
      case Pattern
focusPat of
        A.ConP ConPatInfo
cpi AmbiguousQName
_ [NamedArg Pattern]
_ | ConPatInfo -> ConPatLazy
conPatLazy ConPatInfo
cpi forall a. Eq a => a -> a -> Bool
== ConPatLazy
ConPatLazy ->
          forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
unlessM (forall (m :: * -> *). HasConstInfo m => QName -> m Bool
isEtaRecord QName
d) forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a.
(HasCallStack, ReadTCState m, MonadError TCErr m, MonadTCEnv m) =>
TypeError -> m a
softTypeError forall a b. (a -> b) -> a -> b
$ Pattern -> TypeError
ForcedConstructorNotInstantiated Pattern
focusPat
        Pattern
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return ()

      -- The type of the constructor will end in an application of the datatype
      (TelV Telescope
gamma (El Sort' Term
_ Term
ctarget), Boundary
boundary) <- forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). PureTCM m => Type -> m (TelV Type, Boundary)
telViewPathBoundaryP Type
b
      let Def QName
d' Elims
es' = Term
ctarget
          cixs :: Args
cixs = forall a. Int -> [a] -> [a]
drop (forall a. Sized a => a -> Int
size Args
pars) forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a -> a
fromMaybe forall a. HasCallStack => a
__IMPOSSIBLE__ forall a b. (a -> b) -> a -> b
$ forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims Elims
es'

      -- Δ₁Γ ⊢ boundary
      forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.lhs.split.con" Int
50 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). Applicative m => [Char] -> m Doc
text [Char]
"  boundary = " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Boundary
boundary

      forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (QName
d forall a. Eq a => a -> a -> Bool
== QName
d') {-'-} forall a. HasCallStack => a
__IMPOSSIBLE__

      -- Get names for the constructor arguments from the user patterns
      Telescope
gamma <- forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM forall a b. (a -> b) -> a -> b
$ case Pattern
focusPat of
        A.ConP ConPatInfo
_ AmbiguousQName
_ [NamedArg Pattern]
ps -> do
          [NamedArg Pattern]
ps <- forall (m :: * -> *).
(PureTCM m, MonadError TCErr m, MonadFresh NameId m,
 MonadTrace m) =>
ExpandHidden
-> [NamedArg Pattern] -> Telescope -> m [NamedArg Pattern]
insertImplicitPatterns ExpandHidden
ExpandLast [NamedArg Pattern]
ps Telescope
gamma
          forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ [NamedArg Pattern] -> Telescope -> Telescope
useNamesFromPattern [NamedArg Pattern]
ps Telescope
gamma
        A.RecP PatInfo
_ [FieldAssignment' Pattern]
fs -> do
          [Arg Name]
axs <- forall a b. (a -> b) -> [a] -> [b]
map forall t a. Dom' t a -> Arg a
argFromDom forall b c a. (b -> c) -> (a -> b) -> a -> c
. Defn -> [Dom' Term Name]
recordFieldNames forall b c a. (b -> c) -> (a -> b) -> a -> c
. Definition -> Defn
theDef forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
d
          [NamedArg Pattern]
ps <- forall a.
HasRange a =>
QName
-> (Name -> a)
-> [FieldAssignment' a]
-> [Arg Name]
-> TCM [NamedArg a]
insertMissingFieldsFail QName
d (forall a b. a -> b -> a
const forall a b. (a -> b) -> a -> b
$ forall e. PatInfo -> Pattern' e
A.WildP PatInfo
patNoRange) [FieldAssignment' Pattern]
fs [Arg Name]
axs
          [NamedArg Pattern]
ps <- forall (m :: * -> *).
(PureTCM m, MonadError TCErr m, MonadFresh NameId m,
 MonadTrace m) =>
ExpandHidden
-> [NamedArg Pattern] -> Telescope -> m [NamedArg Pattern]
insertImplicitPatterns ExpandHidden
ExpandLast [NamedArg Pattern]
ps Telescope
gamma
          forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ [NamedArg Pattern] -> Telescope -> Telescope
useNamesFromPattern [NamedArg Pattern]
ps Telescope
gamma
        Pattern
_ -> forall a. HasCallStack => a
__IMPOSSIBLE__

      -- Andreas 2010-09-07  propagate relevance info to new vars
      -- Andreas 2018-10-17  propagate modality
      let updMod :: Modality -> Modality
updMod = Modality -> Modality -> Modality
composeModality (forall a. LensModality a => a -> Modality
getModality ArgInfo
info)
      Telescope
gamma <- forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. LensModality a => (Modality -> Modality) -> a -> a
mapModality Modality -> Modality
updMod forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Telescope
gamma

      -- Get the type of the datatype.
      Type
da <- (Type -> Args -> Type
`piApply` Args
pars) forall b c a. (b -> c) -> (a -> b) -> a -> c
. Definition -> Type
defType forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
d
      forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.lhs.split" Int
30 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"  da = " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
da

      forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.lhs.top" Int
15 forall a b. (a -> b) -> a -> b
$ forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
delta1 forall a b. (a -> b) -> a -> b
$
        forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep [ TCMT IO Doc
"preparing to unify"
            , forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
              [ TCMT IO Doc
"c      =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM ConHead
c forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
":" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
b
              , TCMT IO Doc
"d      =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM (QName -> Elims -> Term
Def QName
d (forall a b. (a -> b) -> [a] -> [b]
map forall a. Arg a -> Elim' a
Apply Args
pars)) forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
":" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
da
              , TCMT IO Doc
"isRec  =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> (forall (m :: * -> *). Applicative m => [Char] -> m Doc
text forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => a -> [Char]
show) Bool
isRec
              , TCMT IO Doc
"gamma  =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Telescope
gamma
              , TCMT IO Doc
"pars   =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *). Functor m => m Doc -> m Doc
brackets (forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Semigroup (m Doc), Foldable t) =>
m Doc -> t (m Doc) -> [m Doc]
punctuate forall (m :: * -> *). Applicative m => m Doc
comma forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Args
pars)
              , TCMT IO Doc
"ixs    =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *). Functor m => m Doc -> m Doc
brackets (forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Semigroup (m Doc), Foldable t) =>
m Doc -> t (m Doc) -> [m Doc]
punctuate forall (m :: * -> *). Applicative m => m Doc
comma forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Args
ixs)
              , TCMT IO Doc
"cixs   =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
gamma (forall (m :: * -> *). Functor m => m Doc -> m Doc
brackets (forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Semigroup (m Doc), Foldable t) =>
m Doc -> t (m Doc) -> [m Doc]
punctuate forall (m :: * -> *). Applicative m => m Doc
comma forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Args
cixs))
              ]
            ]
                 -- We ignore forcing for make-case
      [IsForced]
cforced <- forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM (forall (m :: * -> *) a. MonadTCEnv m => Lens' TCEnv a -> m a
viewTC Lens' TCEnv Bool
eMakeCase) (forall (m :: * -> *) a. Monad m => a -> m a
return []) forall a b. (a -> b) -> a -> b
$
                 {-else-} Definition -> [IsForced]
defForced forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo (ConHead -> QName
conName ConHead
c)

      let delta1Gamma :: Telescope
delta1Gamma = Telescope
delta1 forall t. Abstract t => Telescope -> t -> t
`abstract` Telescope
gamma
          da' :: Type
da'  = forall a. Subst a => Int -> a -> a
raise (forall a. Sized a => a -> Int
size Telescope
gamma) Type
da
          ixs' :: Args
ixs' = forall a. Subst a => Int -> a -> a
raise (forall a. Sized a => a -> Int
size Telescope
gamma) Args
ixs
          -- Variables in Δ₁ are not forced, since the unifier takes care to not introduce forced
          -- variables.
          forced :: [IsForced]
forced = forall a. Int -> a -> [a]
replicate (forall a. Sized a => a -> Int
size Telescope
delta1) IsForced
NotForced forall a. [a] -> [a] -> [a]
++ [IsForced]
cforced

      -- All variables are flexible.
      let flex :: FlexibleVars
flex = [IsForced] -> Telescope -> FlexibleVars
allFlexVars [IsForced]
forced forall a b. (a -> b) -> a -> b
$ Telescope
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.
      Type
da' <- forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
delta1Gamma forall a b. (a -> b) -> a -> b
$ do
             let updCoh :: Cohesion -> Cohesion
updCoh = Cohesion -> Cohesion -> Cohesion
composeCohesion (forall a. LensCohesion a => a -> Cohesion
getCohesion ArgInfo
info)
             TelV Telescope
tel Type
dt <- forall (m :: * -> *).
(MonadReduce m, MonadAddContext m) =>
Type -> m (TelV Type)
telView Type
da'
             forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall t. Abstract t => Telescope -> t -> t
abstract (forall a. LensCohesion a => (Cohesion -> Cohesion) -> a -> a
mapCohesion Cohesion -> Cohesion
updCoh forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Telescope
tel) Type
a

      let stuck :: Maybe Blocker
-> [UnificationFailure] -> ExceptT TCErr tcm (LHSState a)
stuck Maybe Blocker
b [UnificationFailure]
errs = forall (m :: * -> *) a.
(HasCallStack, ReadTCState m, MonadError TCErr m, MonadTCEnv m) =>
TypeError -> m a
softTypeError forall a b. (a -> b) -> a -> b
$ SplitError -> TypeError
SplitError forall a b. (a -> b) -> a -> b
$
            Maybe Blocker
-> QName
-> Telescope
-> Args
-> Args
-> [UnificationFailure]
-> SplitError
UnificationStuck Maybe Blocker
b (ConHead -> QName
conName ConHead
c) (Telescope
delta1 forall t. Abstract t => Telescope -> t -> t
`abstract` Telescope
gamma) Args
cixs Args
ixs' [UnificationFailure]
errs

      forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCMT IO UnificationResult -> TCMT IO UnificationResult
withKIfStrict forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
(PureTCM m, MonadBench m, BenchPhase m ~ Phase,
 MonadError TCErr m) =>
Maybe NoLeftInv
-> Telescope
-> FlexibleVars
-> Type
-> Args
-> Args
-> m UnificationResult
unifyIndices Maybe NoLeftInv
genTrx Telescope
delta1Gamma FlexibleVars
flex Type
da' Args
cixs Args
ixs') forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case

        -- Mismatch.  Report and abort.
        NoUnify NegativeUnification
neg -> forall (m :: * -> *) a.
(HasCallStack, MonadTCM m) =>
TypeError -> m a
hardTypeError forall a b. (a -> b) -> a -> b
$ QName -> NegativeUnification -> TypeError
ImpossibleConstructor (ConHead -> QName
conName ConHead
c) NegativeUnification
neg

        UnifyBlocked Blocker
block -> Maybe Blocker
-> [UnificationFailure] -> ExceptT TCErr tcm (LHSState a)
stuck (forall a. a -> Maybe a
Just Blocker
block) []

        -- Unclear situation.  Try next split.
        UnifyStuck [UnificationFailure]
errs -> Maybe Blocker
-> [UnificationFailure] -> ExceptT TCErr tcm (LHSState a)
stuck forall a. Maybe a
Nothing [UnificationFailure]
errs

        -- Success.
        Unifies (Telescope
delta1',PatternSubstitution
rho0,[NamedArg DeBruijnPattern]
es) -> do

          forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.lhs.top" Int
15 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"unification successful"
          forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.lhs.top" Int
20 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
            [ TCMT IO Doc
"delta1' =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Telescope
delta1'
            , TCMT IO Doc
"rho0    =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
delta1' (forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM PatternSubstitution
rho0)
            , TCMT IO Doc
"es      =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
delta1' (forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM forall a b. (a -> b) -> a -> b
$ (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap) DeBruijnPattern -> Term
patternToTerm [NamedArg DeBruijnPattern]
es)
            ]

          -- split substitution into part for Δ₁ and part for Γ
          let (PatternSubstitution
rho1,PatternSubstitution
rho2) = forall a.
Int -> Substitution' a -> (Substitution' a, Substitution' a)
splitS (forall a. Sized a => a -> Int
size Telescope
gamma) PatternSubstitution
rho0

          forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.lhs.top" Int
20 forall a b. (a -> b) -> a -> b
$ forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
delta1' forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
            [ TCMT IO Doc
"rho1    =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM PatternSubstitution
rho1
            , TCMT IO Doc
"rho2    =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM PatternSubstitution
rho2
            ]

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

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

          -- compute final context and substitution
          let crho :: DeBruijnPattern
crho    = forall x.
ConHead -> ConPatternInfo -> [NamedArg (Pattern' x)] -> Pattern' x
ConP ConHead
c ConPatternInfo
cpi forall a b. (a -> b) -> a -> b
$ forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst PatternSubstitution
rho0 forall a b. (a -> b) -> a -> b
$ (forall a.
DeBruijn a =>
Telescope -> Boundary -> [NamedArg (Pattern' a)]
telePatterns Telescope
gamma Boundary
boundary)
              rho3 :: PatternSubstitution
rho3    = forall a. DeBruijn a => a -> Substitution' a -> Substitution' a
consS DeBruijnPattern
crho PatternSubstitution
rho1
              delta2' :: Telescope
delta2' = forall a. TermSubst a => PatternSubstitution -> a -> a
applyPatSubst PatternSubstitution
rho3 Telescope
delta2
              delta' :: Telescope
delta'  = Telescope
delta1' forall t. Abstract t => Telescope -> t -> t
`abstract` Telescope
delta2'
              rho :: PatternSubstitution
rho     = forall a. Int -> Substitution' a -> Substitution' a
liftS (forall a. Sized a => a -> Int
size Telescope
delta2) PatternSubstitution
rho3

          forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.lhs.top" Int
20 forall a b. (a -> b) -> a -> b
$ forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
delta1' forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
            [ TCMT IO Doc
"crho    =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM DeBruijnPattern
crho
            , TCMT IO Doc
"rho3    =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM PatternSubstitution
rho3
            , TCMT IO Doc
"delta2' =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Telescope
delta2'
            ]
          forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.lhs.top" Int
70 forall a b. (a -> b) -> a -> b
$ forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
delta1' forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
            [ TCMT IO Doc
"crho    =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty DeBruijnPattern
crho
            , TCMT IO Doc
"rho3    =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty PatternSubstitution
rho3
            , TCMT IO Doc
"delta2' =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Telescope
delta2'
            ]

          forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.lhs.top" Int
15 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
            [ TCMT IO Doc
"delta'  =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Telescope
delta'
            , TCMT IO Doc
"rho     =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
delta' (forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM PatternSubstitution
rho)
            ]

          -- Compute the new out patterns and target type.
          let ip' :: [NamedArg DeBruijnPattern]
ip'      = forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst PatternSubstitution
rho [NamedArg DeBruijnPattern]
ip
              target' :: Arg Type
target'  = forall a. TermSubst a => PatternSubstitution -> a -> a
applyPatSubst PatternSubstitution
rho Arg Type
target

          -- Update the problem equations
          let eqs' :: [ProblemEq]
eqs' = forall a. TermSubst a => PatternSubstitution -> a -> a
applyPatSubst PatternSubstitution
rho forall a b. (a -> b) -> a -> b
$ Problem a
problem forall o i. o -> Lens' o i -> i
^. forall a. Lens' (Problem a) [ProblemEq]
problemEqs
              problem' :: Problem a
problem' = forall o i. Lens' o i -> LensSet o i
set forall a. Lens' (Problem a) [ProblemEq]
problemEqs [ProblemEq]
eqs' Problem a
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.
          Quantity
cq <- forall a. LensQuantity a => a -> Quantity
getQuantity forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *).
(ReadTCState m, HasConstInfo m) =>
QName -> m Definition
getOriginalConstInfo (ConHead -> QName
conName ConHead
c)
          let target'' :: Arg Type
target'' = forall a. LensQuantity a => (Quantity -> Quantity) -> a -> a
mapQuantity Quantity -> Quantity
updResMod Arg Type
target'
                where
                  erased :: Bool
erased = case forall a. LensQuantity a => a -> Quantity
getQuantity ArgInfo
info of
                    Quantity0{} -> Bool
True
                    Quantity1{} -> forall a. HasCallStack => a
__IMPOSSIBLE__
                    Quantityω{} -> Bool
False
                  -- either sets to Quantity0 or is the identity.
                  updResMod :: Quantity -> Quantity
updResMod Quantity
q =
                    case Quantity
cq of
                     Quantity
_ | Bool
erased  -> Quantity
q
                     Quantity0{} -> Quantity -> Quantity -> Quantity
composeQuantity Quantity
cq Quantity
q
                                 -- zero-out, preserves origin
                     Quantity1{} -> forall a. HasCallStack => a
__IMPOSSIBLE__
                     Quantityω{} -> Quantity
q

          forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM forall a b. (a -> b) -> a -> b
$ forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
delta' forall a b. (a -> b) -> a -> b
$ do
            Bool
withoutK <- PragmaOptions -> Bool
optWithoutK forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasOptions m => m PragmaOptions
pragmaOptions
            Bool
cubical <- PragmaOptions -> Bool
optCubicalCompatible forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasOptions m => m PragmaOptions
pragmaOptions
            Modality
mod <- forall (m :: * -> *). MonadTCEnv m => m Modality
currentModality
            forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when ((Bool
withoutK Bool -> Bool -> Bool
|| Bool
cubical) Bool -> Bool -> Bool
&& Bool -> Bool
not (forall a. Null a => a -> Bool
null Args
ixs)) forall a b. (a -> b) -> a -> b
$
              Modality
-> PatternSubstitution -> Int -> Telescope -> Type -> TCMT IO ()
conSplitModalityCheck Modality
mod PatternSubstitution
rho (forall (t :: * -> *) a. Foldable t => t a -> Int
length Telescope
delta2) Telescope
tel (forall e. Arg e -> e
unArg Arg Type
target)

          -- if rest type reduces,
          -- extend the split problem by previously not considered patterns
          LHSState a
st' <- forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM forall a b. (a -> b) -> a -> b
$ forall a. LHSState a -> TCM (LHSState a)
updateLHSState forall a b. (a -> b) -> a -> b
$ forall a.
Telescope
-> [NamedArg DeBruijnPattern]
-> Problem a
-> Arg Type
-> [Maybe Int]
-> Bool
-> LHSState a
LHSState Telescope
delta' [NamedArg DeBruijnPattern]
ip' Problem a
problem' Arg Type
target'' [Maybe Int]
psplit (Bool
ixsplit Bool -> Bool -> Bool
|| Bool -> Bool
not (forall a. Null a => a -> Bool
null Args
ixs))

          forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.lhs.top" Int
12 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep
            [ TCMT IO Doc
"new problem from rest"
            , forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
              [ TCMT IO Doc
"delta'  =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM (LHSState a
st' forall o i. o -> Lens' o i -> i
^. forall a. Lens' (LHSState a) Telescope
lhsTel)
              , TCMT IO Doc
"eqs'    =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext (LHSState a
st' forall o i. o -> Lens' o i -> i
^. forall a. Lens' (LHSState a) Telescope
lhsTel) (forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM forall a b. (a -> b) -> a -> b
$ LHSState a
st' forall o i. o -> Lens' o i -> i
^. (forall a. Lens' (LHSState a) (Problem a)
lhsProblem forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Lens' (Problem a) [ProblemEq]
problemEqs))
              , TCMT IO Doc
"ip'     =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext (LHSState a
st' forall o i. o -> Lens' o i -> i
^. forall a. Lens' (LHSState a) Telescope
lhsTel) (forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty forall a b. (a -> b) -> a -> b
$ LHSState a
st' forall o i. o -> Lens' o i -> i
^. forall a. Lens' (LHSState a) [NamedArg DeBruijnPattern]
lhsOutPat)
              ]
            ]
          forall (m :: * -> *) a. Monad m => a -> m a
return LHSState a
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 :: forall (m :: * -> *).
MonadTCError m =>
QName -> DataOrRecord -> m ()
checkMatchingAllowed QName
d = \case
  IsRecord InductionAndEta { recordInduction :: InductionAndEta -> Maybe Induction
recordInduction=Maybe Induction
ind, recordEtaEquality :: InductionAndEta -> EtaEquality
recordEtaEquality=EtaEquality
eta }
    | Just Induction
CoInductive <- Maybe Induction
ind -> forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError forall a b. (a -> b) -> a -> b
$
        [Char] -> TypeError
GenericError [Char]
"Pattern matching on coinductive types is not allowed"
    | Bool -> Bool
not forall a b. (a -> b) -> a -> b
$ forall a. PatternMatchingAllowed a => a -> Bool
patternMatchingAllowed EtaEquality
eta -> forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError forall a b. (a -> b) -> a -> b
$ QName -> TypeError
SplitOnNonEtaRecord QName
d
    | Bool
otherwise -> forall (m :: * -> *) a. Monad m => a -> m a
return ()
  DataOrRecord
IsData -> forall (m :: * -> *) a. Monad m => a -> m a
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 :: forall (m :: * -> *) a.
(MonadTCM m, MonadError TCErr m) =>
TCM a -> m a
suspendErrors TCM a
f = do
  Either TCErr a
ok <- forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM forall a b. (a -> b) -> a -> b
$ (forall a b. b -> Either a b
Right forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCM a
f) forall e (m :: * -> *) a.
MonadError e m =>
m a -> (e -> m a) -> m a
`catchError` (forall (m :: * -> *) a. Monad m => a -> m a
return forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. a -> Either a b
Left)
  forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError forall (m :: * -> *) a. Monad m => a -> m a
return Either TCErr a
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 :: forall (m :: * -> *) a.
(HasCallStack, ReadTCState m, MonadError TCErr m, MonadTCEnv m) =>
TypeError -> m a
softTypeError TypeError
err = forall b. HasCallStack => (CallStack -> b) -> b
withCallerCallStack forall a b. (a -> b) -> a -> b
$ \CallStack
loc ->
  forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (m :: * -> *) a.
MonadTCError m =>
CallStack -> TypeError -> m a
typeError' CallStack
loc TypeError
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 :: forall (m :: * -> *) a.
(HasCallStack, MonadTCM m) =>
TypeError -> m a
hardTypeError = forall b. HasCallStack => (CallStack -> b) -> b
withCallerCallStack forall a b. (a -> b) -> a -> b
$ \CallStack
loc -> forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (m :: * -> *) a.
MonadTCError m =>
CallStack -> TypeError -> m a
typeError' CallStack
loc

type DataOrRecord = DataOrRecord' InductionAndEta

-- | 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 :: forall (m :: * -> *).
(MonadTCM m, PureTCM m) =>
Type -> ExceptT TCErr m (DataOrRecord, QName, Args, Args)
isDataOrRecordType Type
a0 = forall t (m :: * -> *) a.
(Reduce t, IsMeta t, MonadReduce m) =>
t -> (Blocker -> t -> m a) -> (NotBlocked -> t -> m a) -> m a
ifBlocked Type
a0 Blocker
-> Type -> ExceptT TCErr m (DataOrRecord, QName, Args, Args)
blocked forall a b. (a -> b) -> a -> b
$ \case
  NotBlocked
ReallyNotBlocked -> \ Type
a -> case forall t a. Type'' t a -> a
unEl Type
a of

    -- Subcase: split type is a Def.
    Def QName
d Elims
es -> forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (Definition -> Defn
theDef forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
d) forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case

      Datatype{dataPars :: Defn -> Int
dataPars = Int
np} -> do

        forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
whenM (forall (m :: * -> *). (MonadTCM m, MonadReduce m) => Type -> m Bool
isInterval Type
a) forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a.
(HasCallStack, MonadTCM m) =>
TypeError -> m a
hardTypeError forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< ExceptT TCErr m TypeError
notData

        let (Args
pars, Args
ixs) = forall a. Int -> [a] -> ([a], [a])
splitAt Int
np forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a -> a
fromMaybe forall a. HasCallStack => a
__IMPOSSIBLE__ forall a b. (a -> b) -> a -> b
$ forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims Elims
es
        forall (m :: * -> *) a. Monad m => a -> m a
return (forall p. DataOrRecord' p
IsData, QName
d, Args
pars, Args
ixs)

      Record{ Maybe Induction
recInduction :: Defn -> Maybe Induction
recInduction :: Maybe Induction
recInduction, EtaEquality
recEtaEquality' :: Defn -> EtaEquality
recEtaEquality' :: EtaEquality
recEtaEquality' } -> do
        let pars :: Args
pars = forall a. a -> Maybe a -> a
fromMaybe forall a. HasCallStack => a
__IMPOSSIBLE__ forall a b. (a -> b) -> a -> b
$ forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims Elims
es
        forall (m :: * -> *) a. Monad m => a -> m a
return (forall p. p -> DataOrRecord' p
IsRecord InductionAndEta {recordInduction :: Maybe Induction
recordInduction=Maybe Induction
recInduction, recordEtaEquality :: EtaEquality
recordEtaEquality=EtaEquality
recEtaEquality' }, QName
d, Args
pars, [])

      -- Issue #2253: the data type could be abstract.
      AbstractDefn{} -> forall (m :: * -> *) a.
(HasCallStack, MonadTCM m) =>
TypeError -> m a
hardTypeError forall a b. (a -> b) -> a -> b
$ QName -> TypeError
SplitOnAbstract QName
d

      -- the type could be an axiom
      Axiom{} -> forall (m :: * -> *) a.
(HasCallStack, MonadTCM m) =>
TypeError -> m a
hardTypeError forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< ExceptT TCErr m TypeError
notData

      -- Can't match before we have the definition
      DataOrRecSig{} -> forall (m :: * -> *) a.
(HasCallStack, MonadTCM m) =>
TypeError -> m a
hardTypeError forall a b. (a -> b) -> a -> b
$ QName -> TypeError
SplitOnUnchecked QName
d

      -- Issue #2997: the type could be a Def that does not reduce for some reason
      -- (abstract, failed termination checking, NON_TERMINATING, ...)
      Function{}    -> forall (m :: * -> *) a.
(HasCallStack, MonadTCM m) =>
TypeError -> m a
hardTypeError forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< ExceptT TCErr m TypeError
notData

      Constructor{} -> forall a. HasCallStack => a
__IMPOSSIBLE__

      -- Issue #3620: Some primitives are types too.
      -- Not data though, at least currently 11/03/2018.
      Primitive{}   -> forall (m :: * -> *) a.
(HasCallStack, MonadTCM m) =>
TypeError -> m a
hardTypeError forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< ExceptT TCErr m TypeError
notData

      PrimitiveSort{} -> forall (m :: * -> *) a.
(HasCallStack, MonadTCM m) =>
TypeError -> m a
hardTypeError forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< ExceptT TCErr m TypeError
notData

      GeneralizableVar{} -> forall a. HasCallStack => a
__IMPOSSIBLE__

    -- variable: fail softly
    Var{}      -> forall (m :: * -> *) a.
(HasCallStack, ReadTCState m, MonadError TCErr m, MonadTCEnv m) =>
TypeError -> m a
softTypeError forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< ExceptT TCErr m TypeError
notData
    MetaV{}    -> forall a. HasCallStack => a
__IMPOSSIBLE__  -- That is handled in @blocked@.

    -- pi or sort: fail hard
    Pi{}       -> forall (m :: * -> *) a.
(HasCallStack, MonadTCM m) =>
TypeError -> m a
hardTypeError forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< ExceptT TCErr m TypeError
notData
    Sort{}     -> forall (m :: * -> *) a.
(HasCallStack, MonadTCM m) =>
TypeError -> m a
hardTypeError forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< ExceptT TCErr m TypeError
notData

    Lam{}      -> forall a. HasCallStack => a
__IMPOSSIBLE__
    Lit{}      -> forall a. HasCallStack => a
__IMPOSSIBLE__
    Con{}      -> forall a. HasCallStack => a
__IMPOSSIBLE__
    Level{}    -> forall a. HasCallStack => a
__IMPOSSIBLE__
    DontCare{} -> forall a. HasCallStack => a
__IMPOSSIBLE__
    Dummy [Char]
s Elims
_  -> forall (m :: * -> *) a.
(HasCallStack, MonadDebug m) =>
[Char] -> m a
__IMPOSSIBLE_VERBOSE__ [Char]
s

  -- neutral type: fail softly
  StuckOn{}     -> \ Type
_a -> forall (m :: * -> *) a.
(HasCallStack, ReadTCState m, MonadError TCErr m, MonadTCEnv m) =>
TypeError -> m a
softTypeError forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< ExceptT TCErr m TypeError
notData
  AbsurdMatch{} -> \ Type
_a -> forall (m :: * -> *) a.
(HasCallStack, ReadTCState m, MonadError TCErr m, MonadTCEnv m) =>
TypeError -> m a
softTypeError forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< ExceptT TCErr m TypeError
notData

  -- missing clauses: fail hard
  -- TODO: postpone checking of the whole clause until later?
  MissingClauses{} -> \ Type
_a -> forall (m :: * -> *) a.
(HasCallStack, MonadTCM m) =>
TypeError -> m a
hardTypeError forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< ExceptT TCErr m TypeError
notData

  -- underapplied type: should not happen
  Underapplied{} -> forall a. HasCallStack => a
__IMPOSSIBLE__

  where
  notData :: ExceptT TCErr m TypeError
notData      = forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM forall a b. (a -> b) -> a -> b
$ SplitError -> TypeError
SplitError forall b c a. (b -> c) -> (a -> b) -> a -> c
. Closure Type -> SplitError
NotADatatype forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m) =>
a -> m (Closure a)
buildClosure Type
a0
  blocked :: Blocker
-> Type -> ExceptT TCErr m (DataOrRecord, QName, Args, Args)
blocked Blocker
b Type
_a = forall (m :: * -> *) a.
(HasCallStack, ReadTCState m, MonadError TCErr m, MonadTCEnv m) =>
TypeError -> m a
softTypeError forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< do forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM forall a b. (a -> b) -> a -> b
$ SplitError -> TypeError
SplitError forall b c a. (b -> c) -> (a -> b) -> a -> c
. Blocker -> Closure Type -> SplitError
BlockedType Blocker
b forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m) =>
a -> m (Closure a)
buildClosure Type
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 :: QName -> Args -> Type -> TCM (ConHead, Type)
getRecordConstructor QName
d Args
pars Type
a = do
  ConHead
con <- (Definition -> Defn
theDef forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
d) forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
    Record{recConHead :: Defn -> ConHead
recConHead = ConHead
con} -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. KillRange a => KillRangeT a
killRange ConHead
con
    Defn
_ -> forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError forall a b. (a -> b) -> a -> b
$ Type -> TypeError
ShouldBeRecordType Type
a
  Type
b <- (Type -> Args -> Type
`piApply` Args
pars) forall b c a. (b -> c) -> (a -> b) -> a -> c
. Definition -> Type
defType forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo (ConHead -> QName
conName ConHead
con)
  forall (m :: * -> *) a. Monad m => a -> m a
return (ConHead
con, Type
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 :: Maybe Hiding
-> AmbiguousQName
-> Arg Type
-> TCM (QName, Bool, QName, Arg Type, ArgInfo)
disambiguateProjection Maybe Hiding
h ambD :: AmbiguousQName
ambD@(AmbQ List1 QName
ds) Arg Type
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.
  forall (m :: * -> *) a b.
Monad m =>
m (Maybe a) -> m b -> (a -> m b) -> m b
caseMaybeM (forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
PureTCM m =>
Type -> m (Maybe (QName, Args, Defn))
isRecordType forall a b. (a -> b) -> a -> b
$ forall e. Arg e -> e
unArg Arg Type
b) TCM (QName, Bool, QName, Arg Type, ArgInfo)
notRecord forall a b. (a -> b) -> a -> b
$ \(QName
r, Args
vs, Defn
def) -> case Defn
def of
    Record{ recFields :: Defn -> [Dom' Term QName]
recFields = [Dom' Term QName]
fs, Maybe Induction
recInduction :: Maybe Induction
recInduction :: Defn -> Maybe Induction
recInduction, recEtaEquality' :: Defn -> EtaEquality
recEtaEquality' = EtaEquality
eta } -> do
      forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.lhs.split" Int
20 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep
        [ forall (m :: * -> *). Applicative m => [Char] -> m Doc
text forall a b. (a -> b) -> a -> b
$ [Char]
"we are of record type r  = " forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> [Char]
prettyShow QName
r
        , forall (m :: * -> *). Applicative m => [Char] -> m Doc
text   [Char]
"applied to parameters vs = " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Args
vs
        , forall (m :: * -> *). Applicative m => [Char] -> m Doc
text forall a b. (a -> b) -> a -> b
$ [Char]
"and have fields       fs = " forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> [Char]
prettyShow (forall a b. (a -> b) -> [a] -> [b]
map forall t a. Dom' t a -> Arg a
argFromDom [Dom' Term QName]
fs)
        ]
      let comatching :: Bool
comatching = Maybe Induction
recInduction forall a. Eq a => a -> a -> Bool
== forall a. a -> Maybe a
Just Induction
CoInductive
                    Bool -> Bool -> Bool
|| forall a. CopatternMatchingAllowed a => a -> Bool
copatternMatchingAllowed EtaEquality
eta
      -- Try the projection candidates.
      -- First, we try to find a disambiguation that doesn't produce
      -- any new constraints.
      Bool
-> [Dom' Term QName]
-> QName
-> Args
-> Bool
-> (([TCErr], [(QName, (Arg Type, ArgInfo, Maybe TCState))])
    -> TCM (QName, Bool, QName, Arg Type, ArgInfo))
-> TCM (QName, Bool, QName, Arg Type, ArgInfo)
tryDisambiguate Bool
False [Dom' Term QName]
fs QName
r Args
vs Bool
comatching forall a b. (a -> b) -> a -> b
$ \ ([TCErr], [(QName, (Arg Type, ArgInfo, Maybe TCState))])
_ ->
          -- If this fails, we try again with constraints, but we require
          -- the solution to be unique.
          Bool
-> [Dom' Term QName]
-> QName
-> Args
-> Bool
-> (([TCErr], [(QName, (Arg Type, ArgInfo, Maybe TCState))])
    -> TCM (QName, Bool, QName, Arg Type, ArgInfo))
-> TCM (QName, Bool, QName, Arg Type, ArgInfo)
tryDisambiguate Bool
True [Dom' Term QName]
fs QName
r Args
vs Bool
comatching forall a b. (a -> b) -> a -> b
$ \case
            ([]   , []      ) -> forall a. HasCallStack => a
__IMPOSSIBLE__
            (TCErr
err:[TCErr]
_, []      ) -> forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError TCErr
err
            ([TCErr]
_    , disambs :: [(QName, (Arg Type, ArgInfo, Maybe TCState))]
disambs@((QName
d,(Arg Type, ArgInfo, Maybe TCState)
a):[(QName, (Arg Type, ArgInfo, Maybe TCState))]
_)) -> forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError forall a b. (a -> b) -> a -> b
$ QName -> [QName] -> TypeError
AmbiguousProjection QName
d (forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst [(QName, (Arg Type, ArgInfo, Maybe TCState))]
disambs)
    Defn
_ -> forall a. HasCallStack => a
__IMPOSSIBLE__

  where
    tryDisambiguate :: Bool
-> [Dom' Term QName]
-> QName
-> Args
-> Bool
-> (([TCErr], [(QName, (Arg Type, ArgInfo, Maybe TCState))])
    -> TCM (QName, Bool, QName, Arg Type, ArgInfo))
-> TCM (QName, Bool, QName, Arg Type, ArgInfo)
tryDisambiguate Bool
constraintsOk [Dom' Term QName]
fs QName
r Args
vs Bool
comatching ([TCErr], [(QName, (Arg Type, ArgInfo, Maybe TCState))])
-> TCM (QName, Bool, QName, Arg Type, ArgInfo)
failure = do
      -- Note that tryProj wraps TCM in an ExceptT, collecting errors
      -- instead of throwing them to the user immediately.
      NonEmpty (Either TCErr (QName, (Arg Type, ArgInfo, Maybe TCState)))
disambiguations <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
runExceptT forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bool
-> [Dom' Term QName]
-> QName
-> Args
-> QName
-> ExceptT
     TCErr (TCMT IO) (QName, (Arg Type, ArgInfo, Maybe TCState))
tryProj Bool
constraintsOk [Dom' Term QName]
fs QName
r Args
vs) List1 QName
ds
      case forall a b. List1 (Either a b) -> ([a], [b])
List1.partitionEithers NonEmpty (Either TCErr (QName, (Arg Type, ArgInfo, Maybe TCState)))
disambiguations of
        ([TCErr]
_ , (QName
d, (Arg Type
a, ArgInfo
ai, Maybe TCState
mst)) : [(QName, (Arg Type, ArgInfo, Maybe TCState))]
disambs) | Bool
constraintsOk forall a. Ord a => a -> a -> Bool
<= forall a. Null a => a -> Bool
null [(QName, (Arg Type, ArgInfo, Maybe TCState))]
disambs -> do
          forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ forall (m :: * -> *). MonadTCState m => TCState -> m ()
putTC Maybe TCState
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.
          forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM forall a b. (a -> b) -> a -> b
$ QName -> TCMT IO ()
storeDisambiguatedProjection QName
d
          forall (m :: * -> *) a. Monad m => a -> m a
return (QName
d, Bool
comatching, QName
r, Arg Type
a, ArgInfo
ai)
        ([TCErr], [(QName, (Arg Type, ArgInfo, Maybe TCState))])
other -> ([TCErr], [(QName, (Arg Type, ArgInfo, Maybe TCState))])
-> TCM (QName, Bool, QName, Arg Type, ArgInfo)
failure ([TCErr], [(QName, (Arg Type, ArgInfo, Maybe TCState))])
other

    notRecord :: TCM (QName, Bool, QName, Arg Type, ArgInfo)
notRecord = forall (m :: * -> *) a.
(MonadTCM m, MonadError TCErr m, ReadTCState m) =>
QName -> m a
wrongProj forall a b. (a -> b) -> a -> b
$ forall a. NonEmpty a -> a
List1.head List1 QName
ds

    wrongProj :: (MonadTCM m, MonadError TCErr m, ReadTCState m) => QName -> m a
    wrongProj :: forall (m :: * -> *) a.
(MonadTCM m, MonadError TCErr m, ReadTCState m) =>
QName -> m a
wrongProj QName
d = forall (m :: * -> *) a.
(HasCallStack, ReadTCState m, MonadError TCErr m, MonadTCEnv m) =>
TypeError -> m a
softTypeError forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< do
      forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM forall a b. (a -> b) -> a -> b
$ if AmbiguousQName -> Bool
isAmbiguous AmbiguousQName
ambD then Arg Type -> Bool -> QName -> TypeError
CannotEliminateWithProjection Arg Type
b Bool
True forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). MonadPretty m => QName -> m QName
dropTopLevelModule QName
d
                else forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ Arg Type -> Bool -> QName -> TypeError
CannotEliminateWithProjection Arg Type
b Bool
False QName
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 :: Bool
-> [Dom' Term QName]
-> QName
-> Args
-> QName
-> ExceptT
     TCErr (TCMT IO) (QName, (Arg Type, ArgInfo, Maybe TCState))
tryProj Bool
constraintsOk [Dom' Term QName]
fs QName
r Args
vs QName
d0 = forall (m :: * -> *).
HasConstInfo m =>
QName -> m (Maybe Projection)
isProjection QName
d0 forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
      -- Not a projection
      Maybe Projection
Nothing -> forall (m :: * -> *) a.
(MonadTCM m, MonadError TCErr m, ReadTCState m) =>
QName -> m a
wrongProj QName
d0
      Just Projection
proj -> do
        let d :: QName
d = Projection -> QName
projOrig Projection
proj

        -- Andreas, 2015-05-06 issue 1413 projProper=Nothing is not impossible
        QName
qr <- forall b a. b -> (a -> b) -> Maybe a -> b
maybe (forall (m :: * -> *) a.
(MonadTCM m, MonadError TCErr m, ReadTCState m) =>
QName -> m a
wrongProj QName
d) forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Projection -> Maybe QName
projProper Projection
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.
        forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (forall a. Null a => a -> Bool
null forall a b. (a -> b) -> a -> b
$ Projection -> ProjLams
projLams Projection
proj) forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a.
(MonadTCM m, MonadError TCErr m, ReadTCState m) =>
QName -> m a
wrongProj QName
d
        forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"tc.lhs.split" Int
90 [Char]
"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.
        forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.lhs.split" Int
20 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep
          [ forall (m :: * -> *). Applicative m => [Char] -> m Doc
text forall a b. (a -> b) -> a -> b
$ [Char]
"proj                  d0 = " forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> [Char]
prettyShow QName
d0
          , forall (m :: * -> *). Applicative m => [Char] -> m Doc
text forall a b. (a -> b) -> a -> b
$ [Char]
"original proj         d  = " forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> [Char]
prettyShow QName
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.
        Dom' Term QName
argd <- forall b a. b -> (a -> b) -> Maybe a -> b
maybe (forall (m :: * -> *) a.
(MonadTCM m, MonadError TCErr m, ReadTCState m) =>
QName -> m a
wrongProj QName
d) forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
List.find ((QName
d forall a. Eq a => a -> a -> Bool
==) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t e. Dom' t e -> e
unDom) [Dom' Term QName]
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 :: ArgInfo
ai = forall a. LensArgInfo a => a -> ArgInfo
getArgInfo Dom' Term QName
argd

        forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.lhs.split" Int
20 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
          [ forall (m :: * -> *). Applicative m => [Char] -> m Doc
text forall a b. (a -> b) -> a -> b
$ [Char]
"original proj relevance  = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show (forall a. LensRelevance a => a -> Relevance
getRelevance Dom' Term QName
argd)
          , forall (m :: * -> *). Applicative m => [Char] -> m Doc
text forall a b. (a -> b) -> a -> b
$ [Char]
"original proj quantity   = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show (forall a. LensQuantity a => a -> Quantity
getQuantity  Dom' Term QName
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.
        forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (forall a b. Maybe a -> b -> (a -> b) -> b
caseMaybe Maybe Hiding
h Bool
True forall a b. (a -> b) -> a -> b
$ forall a b. (LensHiding a, LensHiding b) => a -> b -> Bool
sameHiding forall a b. (a -> b) -> a -> b
$ Projection -> ArgInfo
projArgInfo Projection
proj) forall a b. (a -> b) -> a -> b
$
          forall (m :: * -> *) a.
(HasCallStack, ReadTCState m, MonadError TCErr m, MonadTCEnv m) =>
TypeError -> m a
softTypeError forall a b. (a -> b) -> a -> b
$ QName -> TypeError
WrongHidingInProjection QName
d

        -- Andreas, 2016-12-31, issue #1976: Check parameters.
        let chk :: TCMT IO ()
chk = forall (tcm :: * -> *).
MonadTCM tcm =>
QName -> QName -> Args -> tcm ()
checkParameters QName
qr QName
r Args
vs
        Maybe TCState
mst <- forall (m :: * -> *) a.
(MonadTCM m, MonadError TCErr m) =>
TCM a -> m a
suspendErrors forall a b. (a -> b) -> a -> b
$
          if Bool
constraintsOk then forall a. a -> Maybe a
Just forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> b
snd forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. TCM a -> TCM (a, TCState)
localTCStateSaving TCMT IO ()
chk
          else forall a. Maybe a
Nothing forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ forall (m :: * -> *) a.
(HasOptions m, MonadConstraint m, MonadDebug m, MonadError TCErr m,
 MonadFresh ProblemId m, MonadTCEnv m, MonadWarning m) =>
m a -> m a
nonConstraining TCMT IO ()
chk

        -- Get the type of projection d applied to "self"
        Type
dType <- forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM forall a b. (a -> b) -> a -> b
$ Definition -> Type
defType forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
d  -- full type!
        forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.lhs.split" Int
20 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep
          [ TCMT IO Doc
"we are being projected by dType = " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
dType
          ]
        Type
projType <- forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM forall a b. (a -> b) -> a -> b
$ Type
dType forall a (m :: * -> *).
(PiApplyM a, MonadReduce m, HasBuiltins m) =>
Type -> a -> m Type
`piApplyM` Args
vs
        forall (m :: * -> *) a. Monad m => a -> m a
return (QName
d0, (forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
ai Type
projType, Projection -> ArgInfo
projArgInfo Projection
proj, Maybe TCState
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 :: AmbiguousQName -> QName -> Args -> TCM (ConHead, Type)
disambiguateConstructor ambC :: AmbiguousQName
ambC@(AmbQ List1 QName
cs) QName
d Args
pars = do
  QName
d <- forall (m :: * -> *). HasConstInfo m => QName -> m QName
canonicalName QName
d
  [QName]
cons <- Definition -> Defn
theDef forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
d forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
    def :: Defn
def@Datatype{} -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Defn -> [QName]
dataCons Defn
def
    def :: Defn
def@Record{}   -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ [ConHead -> QName
conName forall a b. (a -> b) -> a -> b
$ Defn -> ConHead
recConHead Defn
def]
    Defn
_              -> forall a. HasCallStack => a
__IMPOSSIBLE__

  -- First, try do disambiguate with nonConstraining,
  -- if that fails, try again allowing constraint/solution generation.
  Bool
-> QName
-> [QName]
-> (([TCErr], [List1 (QName, ConHead, (Type, Maybe TCState))])
    -> TCM (ConHead, Type))
-> TCM (ConHead, Type)
tryDisambiguate Bool
False QName
d [QName]
cons forall a b. (a -> b) -> a -> b
$ \ ([TCErr], [List1 (QName, ConHead, (Type, Maybe TCState))])
_ ->
    Bool
-> QName
-> [QName]
-> (([TCErr], [List1 (QName, ConHead, (Type, Maybe TCState))])
    -> TCM (ConHead, Type))
-> TCM (ConHead, Type)
tryDisambiguate Bool
True QName
d [QName]
cons forall a b. (a -> b) -> a -> b
$ \case
        ([]   , [] ) -> forall a. HasCallStack => a
__IMPOSSIBLE__
        (TCErr
err:[TCErr]
_, [] ) -> forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError TCErr
err
        -- If all disambiguations point to the same original constructor
        -- meaning that only the parameters may differ,
        -- then throw more specific error.
        ([TCErr]
_    , [List1 (QName, ConHead, (Type, Maybe TCState))
_]) -> forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError forall a b. (a -> b) -> a -> b
$ QName -> List1 QName -> TypeError
CantResolveOverloadedConstructorsTargetingSameDatatype QName
d List1 QName
cs
        ([TCErr]
_    , disambs :: [List1 (QName, ConHead, (Type, Maybe TCState))]
disambs@(((QName
c,ConHead
_,(Type, Maybe TCState)
_) :| [(QName, ConHead, (Type, Maybe TCState))]
_) : [List1 (QName, ConHead, (Type, Maybe TCState))]
_)) -> forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError forall a b. (a -> b) -> a -> b
$
          QName -> [QName] -> TypeError
AmbiguousConstructor QName
c (forall a b. (a -> b) -> [a] -> [b]
map (ConHead -> QName
conName forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b c. (a, b, c) -> b
snd3) forall a b. (a -> b) -> a -> b
$ forall a. [List1 a] -> [a]
List1.concat [List1 (QName, ConHead, (Type, Maybe TCState))]
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 :: Bool
-> QName
-> [QName]
-> (([TCErr], [List1 (QName, ConHead, (Type, Maybe TCState))])
    -> TCM (ConHead, Type))
-> TCM (ConHead, Type)
tryDisambiguate Bool
constraintsOk QName
d [QName]
cons ([TCErr], [List1 (QName, ConHead, (Type, Maybe TCState))])
-> TCM (ConHead, Type)
failure = do
      forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.lhs.disamb" Int
30 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a. Foldable t => t [a] -> [a]
List.concat forall a b. (a -> b) -> a -> b
$
        [ [ TCMT IO Doc
"tryDisambiguate" ]
        , if Bool
constraintsOk then [ TCMT IO Doc
"(allowing new constraints)" ] else forall a. Null a => a
empty
        , forall a b. (a -> b) -> [a] -> [b]
map (forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty) forall a b. (a -> b) -> a -> b
$ forall l. IsList l => l -> [Item l]
List1.toList List1 QName
cs
        , [ TCMT IO Doc
"against" ]
        , forall a b. (a -> b) -> [a] -> [b]
map (forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty) [QName]
cons
        ]
      NonEmpty (Either TCErr (QName, ConHead, (Type, Maybe TCState)))
disambiguations <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
runExceptT forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bool
-> [QName]
-> QName
-> Args
-> QName
-> ExceptT TCErr (TCMT IO) (QName, ConHead, (Type, Maybe TCState))
tryCon Bool
constraintsOk [QName]
cons QName
d Args
pars) List1 QName
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 ([TCErr]
errs, [(QName, ConHead, (Type, Maybe TCState))]
fits0) = forall a b. List1 (Either a b) -> ([a], [b])
List1.partitionEithers NonEmpty (Either TCErr (QName, ConHead, (Type, Maybe TCState)))
disambiguations
      forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.lhs.disamb" Int
40 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat forall a b. (a -> b) -> a -> b
$ do
        let hideSt :: (a, b, (a, f b)) -> (a, b, (a, f [Char]))
hideSt (a
c0,b
c,(a
a,f b
mst)) = (a
c0, b
c, (a
a, ([Char]
"(state change)" :: String) forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ f b
mst))
        TCMT IO Doc
"remaining candidates: " forall a. a -> [a] -> [a]
: forall a b. (a -> b) -> [a] -> [b]
map (forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {f :: * -> *} {a} {b} {a} {b}.
Functor f =>
(a, b, (a, f b)) -> (a, b, (a, f [Char]))
hideSt) [(QName, ConHead, (Type, Maybe TCState))]
fits0
      forall a.
[(a, ConHead, (Type, Maybe TCState))]
-> TCM [List1 (a, ConHead, (Type, Maybe TCState))]
dedupCons [(QName, ConHead, (Type, Maybe TCState))]
fits0 forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case

        -- Single candidate remains.
        [ (QName
c0,ConHead
c,(Type
a,Maybe TCState
mst)) :| [] ] -> do
          forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.lhs.disamb" Int
30 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep forall a b. (a -> b) -> a -> b
$
            [ TCMT IO Doc
"tryDisambiguate suceeds with"
            , forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty QName
c0
            , TCMT IO Doc
":"
            , forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
a
            ]
          -- Andreas, 2020-06-16, issue #4135
          -- If disambiguation succeeded with new constraints/solutions,
          -- put them into action.
          forall (m :: * -> *) a. Monad m => Maybe a -> (a -> m ()) -> m ()
whenJust Maybe TCState
mst forall (m :: * -> *). MonadTCState m => TCState -> m ()
putTC
          -- If there are multiple candidates for the constructor pattern, exactly one of
          -- which type checks, remember our choice for highlighting info.
          forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (AmbiguousQName -> Bool
isAmbiguous AmbiguousQName
ambC) forall a b. (a -> b) -> a -> b
$ forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM forall a b. (a -> b) -> a -> b
$
            Induction -> QName -> TCMT IO ()
storeDisambiguatedConstructor (ConHead -> Induction
conInductive ConHead
c) QName
c0
          forall (m :: * -> *) a. Monad m => a -> m a
return (ConHead
c,Type
a)

        -- Either no candidate constructor in 'cs' type checks, or multiple candidates
        -- type check.
        [List1 (QName, ConHead, (Type, Maybe TCState))]
groups -> ([TCErr], [List1 (QName, ConHead, (Type, Maybe TCState))])
-> TCM (ConHead, Type)
failure ([TCErr]
errs, [List1 (QName, ConHead, (Type, Maybe TCState))]
groups)

    abstractConstructor :: QName -> m a
abstractConstructor QName
c = forall (m :: * -> *) a.
(HasCallStack, ReadTCState m, MonadError TCErr m, MonadTCEnv m) =>
TypeError -> m a
softTypeError forall a b. (a -> b) -> a -> b
$
      QName -> TypeError
AbstractConstructorNotInScope QName
c

    wrongDatatype :: QName -> QName -> m a
wrongDatatype QName
c QName
d = forall (m :: * -> *) a.
(HasCallStack, ReadTCState m, MonadError TCErr m, MonadTCEnv m) =>
TypeError -> m a
softTypeError forall a b. (a -> b) -> a -> b
$
      QName -> QName -> TypeError
ConstructorPatternInWrongDatatype QName
c QName
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 :: Bool
-> [QName]
-> QName
-> Args
-> QName
-> ExceptT TCErr (TCMT IO) (QName, ConHead, (Type, Maybe TCState))
tryCon Bool
constraintsOk [QName]
cons QName
d Args
pars QName
c = forall (m :: * -> *).
HasConstInfo m =>
QName -> m (Either SigError Definition)
getConstInfo' QName
c forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
      Left (SigUnknown [Char]
err)     -> forall a. HasCallStack => a
__IMPOSSIBLE__
      Left SigError
SigCubicalNotErasure -> forall a. HasCallStack => a
__IMPOSSIBLE__
      Left SigError
SigAbstract          -> forall {m :: * -> *} {a}.
(ReadTCState m, MonadError TCErr m, MonadTCEnv m) =>
QName -> m a
abstractConstructor QName
c
      Right Definition
def                 -> do
        let con :: ConHead
con = Defn -> ConHead
conSrcCon (Definition -> Defn
theDef Definition
def) forall t u. (SetRange t, HasRange u) => t -> u -> t
`withRangeOf` QName
c
        forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (ConHead -> QName
conName ConHead
con forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [QName]
cons) forall a b. (a -> b) -> a -> b
$ forall {m :: * -> *} {a}.
(ReadTCState m, MonadError TCErr m, MonadTCEnv m) =>
QName -> QName -> m a
wrongDatatype QName
c QName
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 :: TCMT IO ()
chk = forall (tcm :: * -> *).
MonadTCM tcm =>
QName -> QName -> Args -> tcm ()
checkConstructorParameters QName
c QName
d Args
pars
        Maybe TCState
mst <- forall (m :: * -> *) a.
(MonadTCM m, MonadError TCErr m) =>
TCM a -> m a
suspendErrors forall a b. (a -> b) -> a -> b
$
          if Bool
constraintsOk then forall a. a -> Maybe a
Just forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> b
snd forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. TCM a -> TCM (a, TCState)
localTCStateSaving TCMT IO ()
chk
          else forall a. Maybe a
Nothing forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ forall (m :: * -> *) a.
(HasOptions m, MonadConstraint m, MonadDebug m, MonadError TCErr m,
 MonadFresh ProblemId m, MonadTCEnv m, MonadWarning m) =>
m a -> m a
nonConstraining TCMT IO ()
chk

        -- Get the type from the original constructor.
        -- Andreas, 2020-06-17 TODO:
        -- Couldn't we return this type from checkConstructorParameters?
        Type
cType <- (Type -> Args -> Type
`piApply` Args
pars) forall b c a. (b -> c) -> (a -> b) -> a -> c
. Definition -> Type
defType forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasConstInfo m => ConHead -> m Definition
getConInfo ConHead
con

        forall (m :: * -> *) a. Monad m => a -> m a
return (QName
c, ConHead
con, (Type
cType, Maybe TCState
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 :: forall a.
[(a, ConHead, (Type, Maybe TCState))]
-> TCM [List1 (a, ConHead, (Type, Maybe TCState))]
dedupCons [(a, ConHead, (Type, Maybe TCState))]
cands = do
      -- Group candidates by original constructor name.
      let groups :: [List1 (a, ConHead, (Type, Maybe TCState))]
groups = forall (f :: * -> *) b a.
(Foldable f, Eq b) =>
(a -> b) -> f a -> [NonEmpty a]
List1.groupWith (ConHead -> QName
conName forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b c. (a, b, c) -> b
snd3) [(a, ConHead, (Type, Maybe TCState))]
cands
      -- Eliminate duplicates (same type) from groups.
      forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (forall (m :: * -> *) a.
Monad m =>
(a -> a -> m Bool) -> List1 a -> m (List1 a)
List1.nubM ((Type, Maybe TCState) -> (Type, Maybe TCState) -> TCMT IO Bool
cmpM forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` forall a b c. (a, b, c) -> c
thd3)) [List1 (a, ConHead, (Type, Maybe TCState))]
groups
      where
      -- The types come possibly with their own state.
      cmpM :: (Type, Maybe TCState) -> (Type, Maybe TCState) -> TCMT IO Bool
cmpM (Type
a1, Maybe TCState
mst1) (Type
a2, Maybe TCState
mst2) = do
        let cmpTypes :: TCMT IO Bool
cmpTypes = forall (m :: * -> *).
(MonadConstraint m, MonadWarning m, MonadError TCErr m,
 MonadFresh ProblemId m) =>
m () -> m Bool
tryConversion forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). MonadConversion m => Type -> Type -> m ()
equalType Type
a1 Type
a2
        case (Maybe TCState
mst1, Maybe TCState
mst2) of
          (Maybe TCState
Nothing, Maybe TCState
Nothing) -> TCMT IO Bool
cmpTypes
          (Just TCState
st, Maybe TCState
Nothing) -> forall {a}. TCState -> TCMT IO a -> TCMT IO a
inState TCState
st TCMT IO Bool
cmpTypes
          (Maybe TCState
Nothing, Just TCState
st) -> forall {a}. TCState -> TCMT IO a -> TCMT IO a
inState TCState
st TCMT IO Bool
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{})  -> forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
      inState :: TCState -> TCMT IO a -> TCMT IO a
inState TCState
st TCMT IO a
m = forall a. TCM a -> TCM a
localTCState forall a b. (a -> b) -> a -> b
$ do forall (m :: * -> *). MonadTCState m => TCState -> m ()
putTC TCState
st; TCMT IO a
m

-- | @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 :: forall (tcm :: * -> *).
MonadTCM tcm =>
QName -> QName -> Args -> tcm ()
checkConstructorParameters QName
c QName
d Args
pars = do
  QName
dc <- forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). HasConstInfo m => QName -> m QName
getConstructorData QName
c
  forall (tcm :: * -> *).
MonadTCM tcm =>
QName -> QName -> Args -> tcm ()
checkParameters QName
dc QName
d Args
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 :: forall (tcm :: * -> *).
MonadTCM tcm =>
QName -> QName -> Args -> tcm ()
checkParameters QName
dc QName
d Args
pars = forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM forall a b. (a -> b) -> a -> b
$ do
  Term
a  <- forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce (QName -> Elims -> Term
Def QName
dc [])
  case Term
a of
    Def QName
d0 Elims
es -> do -- compare parameters
      let vs :: Args
vs = forall a. a -> Maybe a -> a
fromMaybe forall a. HasCallStack => a
__IMPOSSIBLE__ forall a b. (a -> b) -> a -> b
$ forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims Elims
es
      forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.lhs.split" Int
40 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat forall a b. (a -> b) -> a -> b
$
        [ TCMT IO Doc
"checkParameters"
        , forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"d                   =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> (forall (m :: * -> *). Applicative m => [Char] -> m Doc
text forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Pretty a => a -> [Char]
prettyShow) QName
d
        , forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"d0 (should be == d) =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> (forall (m :: * -> *). Applicative m => [Char] -> m Doc
text forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Pretty a => a -> [Char]
prettyShow) QName
d0
        , forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"dc                  =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> (forall (m :: * -> *). Applicative m => [Char] -> m Doc
text forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Pretty a => a -> [Char]
prettyShow) QName
dc
        , forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"vs                  =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Args
vs
        , forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"pars                =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Args
pars
        ]
      -- when (d0 /= d) __IMPOSSIBLE__ -- d could have extra qualification
      Type
t <- forall (m :: * -> *).
(HasConstInfo m, ReadTCState m) =>
QName -> m Type
typeOfConst QName
d
      forall (m :: * -> *).
MonadConversion m =>
[Polarity] -> [IsForced] -> Type -> Term -> Args -> Args -> m ()
compareArgs [] [] Type
t (QName -> Elims -> Term
Def QName
d []) Args
vs (forall a. Int -> [a] -> [a]
take (forall (t :: * -> *) a. Foldable t => t a -> Int
length Args
vs) Args
pars)
    Term
_ -> forall a. HasCallStack => a
__IMPOSSIBLE__

checkSortOfSplitVar :: (MonadTCM m, PureTCM m, MonadError TCErr m,
                        LensSort a, PrettyTCM a, LensSort ty, PrettyTCM ty)
                    => DataOrRecord -> a -> Telescope -> Maybe ty -> m ()
checkSortOfSplitVar :: forall (m :: * -> *) a ty.
(MonadTCM m, PureTCM m, MonadError TCErr m, LensSort a,
 PrettyTCM a, LensSort ty, PrettyTCM ty) =>
DataOrRecord -> a -> Telescope -> Maybe ty -> m ()
checkSortOfSplitVar DataOrRecord
dr a
a Telescope
tel Maybe ty
mtarget = do
  forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce forall a b. (a -> b) -> a -> b
$ forall a. LensSort a => a -> Sort' Term
getSort a
a) forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
    Type{} -> forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
whenM forall (m :: * -> *). HasOptions m => m Bool
isTwoLevelEnabled m ()
checkFibrantSplit
    Prop{} -> m ()
checkPropSplit
    SSet{} -> forall (m :: * -> *) a. Monad m => a -> m a
return ()
    Inf Univ
u Integer
_ -> forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Univ -> IsFibrant
univFibrancy Univ
u forall a. Eq a => a -> a -> Bool
== IsFibrant
IsFibrant) forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
whenM forall (m :: * -> *). HasOptions m => m Bool
isTwoLevelEnabled m ()
checkFibrantSplit
    Sort' Term
sa      -> forall (m :: * -> *) a.
(HasCallStack, ReadTCState m, MonadError TCErr m, MonadTCEnv m) =>
TypeError -> m a
softTypeError forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< do
      forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM forall a b. (a -> b) -> a -> b
$ Maybe Blocker -> Doc -> TypeError
SortOfSplitVarError forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall t (m :: * -> *).
(Reduce t, IsMeta t, MonadReduce m) =>
t -> m (Maybe Blocker)
isBlocked Sort' Term
sa forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep
        [ TCMT IO Doc
"Cannot split on datatype in sort" , forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM (forall a. LensSort a => a -> Sort' Term
getSort a
a) ]

  where
    checkPropSplit :: m ()
checkPropSplit
      | IsRecord InductionAndEta { recordInduction :: InductionAndEta -> Maybe Induction
recordInduction=Maybe Induction
Nothing } <- DataOrRecord
dr = forall (m :: * -> *) a. Monad m => a -> m a
return ()
      | Just ty
target <- Maybe ty
mtarget = do
        forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.sort.check" Int
20 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"target prop:" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM ty
target
        ty -> m ()
checkIsProp ty
target
      | Bool
otherwise              = do
          forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.sort.check" Int
20 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"no target prop"
          forall {m :: * -> *} {a}.
(ReadTCState m, MonadError TCErr m, MonadTCEnv m) =>
DataOrRecord -> m a
splitOnPropError DataOrRecord
dr

    checkIsProp :: ty -> m ()
checkIsProp ty
t = forall (m :: * -> *) a.
Monad m =>
BlockT m a -> m (Either Blocker a)
runBlocked (forall a (m :: * -> *).
(LensSort a, PrettyTCM a, PureTCM m, MonadBlock m) =>
a -> m Bool
isPropM ty
t) forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
      Left Blocker
b      -> forall {m :: * -> *} {a}.
(ReadTCState m, MonadError TCErr m, MonadTCEnv m) =>
DataOrRecord -> m a
splitOnPropError DataOrRecord
dr -- TODO
      Right Bool
False -> forall {m :: * -> *} {a}.
(ReadTCState m, MonadError TCErr m, MonadTCEnv m) =>
DataOrRecord -> m a
splitOnPropError DataOrRecord
dr
      Right Bool
True  -> forall (m :: * -> *) a. Monad m => a -> m a
return ()

    checkFibrantSplit :: m ()
checkFibrantSplit
      | IsRecord InductionAndEta
_ <- DataOrRecord
dr       = forall (m :: * -> *) a. Monad m => a -> m a
return ()
      | Just ty
target <- Maybe ty
mtarget = do
          forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.sort.check" Int
20 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"target:" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM ty
target
          ty -> m ()
checkIsFibrant ty
target
          forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ (forall t. Tele (Dom t) -> [Dom ([Char], t)]
telToList Telescope
tel) forall a b. (a -> b) -> a -> b
$ \ Dom ([Char], Type)
d -> do
            let ty :: Type
ty = forall a b. (a, b) -> b
snd forall a b. (a -> b) -> a -> b
$ forall t e. Dom' t e -> e
unDom Dom ([Char], Type)
d
            Type -> m ()
checkIsCoFibrant Type
ty
      | Bool
otherwise              = do
          forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.sort.check" Int
20 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"no target"
          Maybe Blocker -> m ()
splitOnFibrantError forall a. Maybe a
Nothing

    -- Cofibrant types are those that could be the domain of a fibrant
    -- pi type. (Notion by C. Sattler).
    checkIsCoFibrant :: Type -> m ()
checkIsCoFibrant Type
t = forall (m :: * -> *) a.
Monad m =>
BlockT m a -> m (Either Blocker a)
runBlocked (forall a (m :: * -> *).
(LensSort a, PureTCM m, MonadBlock m) =>
a -> m Bool
isCoFibrantSort Type
t) forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
      Left Blocker
b      -> Type -> Maybe Blocker -> m ()
splitOnFibrantError' Type
t forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just Blocker
b
      Right Bool
False -> forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
unlessM (forall (m :: * -> *). (MonadTCM m, MonadReduce m) => Type -> m Bool
isInterval Type
t) forall a b. (a -> b) -> a -> b
$
                       Type -> Maybe Blocker -> m ()
splitOnFibrantError' Type
t forall a b. (a -> b) -> a -> b
$ forall a. Maybe a
Nothing
      Right Bool
True  -> forall (m :: * -> *) a. Monad m => a -> m a
return ()

    checkIsFibrant :: ty -> m ()
checkIsFibrant ty
t = forall (m :: * -> *) a.
Monad m =>
BlockT m a -> m (Either Blocker a)
runBlocked (forall a (m :: * -> *).
(LensSort a, PureTCM m, MonadBlock m) =>
a -> m Bool
isFibrant ty
t) forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
      Left Blocker
b      -> Maybe Blocker -> m ()
splitOnFibrantError forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just Blocker
b
      Right Bool
False -> Maybe Blocker -> m ()
splitOnFibrantError forall a. Maybe a
Nothing
      Right Bool
True  -> forall (m :: * -> *) a. Monad m => a -> m a
return ()

    splitOnPropError :: DataOrRecord -> m a
splitOnPropError DataOrRecord
dr = forall (m :: * -> *) a.
(HasCallStack, ReadTCState m, MonadError TCErr m, MonadTCEnv m) =>
TypeError -> m a
softTypeError forall a b. (a -> b) -> a -> b
$ DataOrRecord -> TypeError
SplitInProp DataOrRecord
dr

    splitOnFibrantError' :: Type -> Maybe Blocker -> m ()
splitOnFibrantError' Type
t Maybe Blocker
mb = forall (m :: * -> *) a.
(HasCallStack, ReadTCState m, MonadError TCErr m, MonadTCEnv m) =>
TypeError -> m a
softTypeError forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< do
      forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM forall a b. (a -> b) -> a -> b
$ Maybe Blocker -> Doc -> TypeError
SortOfSplitVarError Maybe Blocker
mb forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep
        [ TCMT IO Doc
"Cannot eliminate fibrant type" , forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM a
a
        , TCMT IO Doc
"unless context type", forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
t, TCMT IO Doc
"is also fibrant."
        ]

    splitOnFibrantError :: Maybe Blocker -> m ()
splitOnFibrantError Maybe Blocker
mb = forall (m :: * -> *) a.
(HasCallStack, ReadTCState m, MonadError TCErr m, MonadTCEnv m) =>
TypeError -> m a
softTypeError forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< do
      forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM forall a b. (a -> b) -> a -> b
$ Maybe Blocker -> Doc -> TypeError
SortOfSplitVarError Maybe Blocker
mb forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep
        [ TCMT IO Doc
"Cannot eliminate fibrant type" , forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM a
a
        , TCMT IO Doc
"unless target type is also fibrant"
        ]