{-# LANGUAGE NondecreasingIndentation #-}

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

import Prelude hiding ( null )

import Data.Function (on)
import Data.Maybe

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

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

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

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

import Agda.TypeChecking.Monad

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

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

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

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

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

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

  isFlexiblePattern :: (HasConstInfo m, MonadDebug m) => a -> m Bool
  isFlexiblePattern 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' i o -> i
^. forall a. Lens' Telescope (LHSState a)
lhsTel
      problem :: Problem a
problem = LHSState a
st forall o i. o -> Lens' i o -> i
^. forall a. Lens' (Problem a) (LHSState 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' i o -> i
^. forall a. Lens' [ProblemEq] (Problem a)
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 i o. Lens' i o -> LensSet i o
set forall a. Lens' Telescope (LHSState a)
lhsTel Telescope
tel' forall a b. (a -> b) -> a -> b
$ forall i o. Lens' i o -> LensSet i o
set (forall a. Lens' (Problem a) (LHSState a)
lhsProblem forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Lens' [ProblemEq] (Problem a)
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' Term Type
_) = forall (m :: * -> *) a. Monad m => a -> m a
return []
    update eq :: ProblemEq
eq@(ProblemEq p :: Pattern
p@A.ProjP{} Term
_ Dom' Term Type
_) = forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError forall a b. (a -> b) -> a -> b
$ Pattern -> TypeError
IllformedProjectionPattern Pattern
p
    update eq :: ProblemEq
eq@(ProblemEq p :: Pattern
p@(A.AsP PatInfo
info BindName
x Pattern
p') Term
v Dom' Term Type
a) =
      (Pattern -> Term -> Dom' Term Type -> ProblemEq
ProblemEq (forall e. BindName -> Pattern' e
A.VarP BindName
x) Term
v Dom' Term 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' Term Type -> ProblemEq
ProblemEq Pattern
p' Term
v Dom' Term Type
a)

    update eq :: ProblemEq
eq@(ProblemEq p :: Pattern
p@(A.AnnP PatInfo
_ Expr
_ A.WildP{}) Term
v Dom' Term 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' Term Type
a) =
      (Pattern -> Term -> Dom' Term 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' Term 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' Term Type -> ProblemEq
ProblemEq Pattern
p' Term
v Dom' Term Type
a)

    update eq :: ProblemEq
eq@(ProblemEq Pattern
p Term
v Dom' Term 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' Term 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' Term 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' Term Type]
bs = Telescope -> [Term] -> [Dom' Term 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 -> TCMT IO ()
checkArgs [] [] = forall (m :: * -> *) a. Monad m => a -> m a
return ()
                checkArgs (NamedArg Pattern
p : [NamedArg Pattern]
ps) (Arg Term
v : Args
vs)
                  | 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 -> TCMT IO ()
checkArgs [NamedArg Pattern]
ps Args
vs
                  | 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) =>
Doc -> m a
genericDocError forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< do
                      forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords ([Char]
"Expected an " forall a. [a] -> [a] -> [a]
++ forall {a}. IsString a => Hiding -> a
which (forall a. LensHiding a => a -> Hiding
getHiding Arg Term
v) forall a. [a] -> [a] -> [a]
++ [Char]
" argument " forall a. [a] -> [a] -> [a]
++
                                     [Char]
"instead of "  forall a. [a] -> [a] -> [a]
++ forall {a}. IsString a => Hiding -> a
which (forall a. LensHiding a => a -> Hiding
getHiding NamedArg Pattern
p) forall a. [a] -> [a] -> [a]
++ [Char]
" argument") forall a. [a] -> [a] -> [a]
++
                             [ forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA NamedArg Pattern
p ]
                  where which :: Hiding -> a
which Hiding
NotHidden  = a
"explicit"
                        which Hiding
Hidden     = a
"implicit"
                        which Instance{} = a
"instance"
                checkArgs [] Args
vs = forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
Doc -> m a
genericDocError forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< do
                    forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"Too few arguments to constructor" forall a. [a] -> [a] -> [a]
++ [forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM ConHead
c forall a. Semigroup a => a -> a -> a
<> TCMT IO Doc
","] forall a. [a] -> [a] -> [a]
++
                           forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords ([Char]
"expected " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Int
n forall a. [a] -> [a] -> [a]
++ [Char]
" more explicit "  forall a. [a] -> [a] -> [a]
++ [Char]
arguments)
                  where n :: Int
n = forall (t :: * -> *) a. Foldable t => t a -> Int
length (forall a. (a -> Bool) -> [a] -> [a]
filter forall a. LensHiding a => a -> Bool
visible Args
vs)
                        arguments :: [Char]
arguments | Int
n forall a. Eq a => a -> a -> Bool
== Int
1    = [Char]
"argument"
                                  | Bool
otherwise = [Char]
"arguments"
                checkArgs (NamedArg Pattern
p : [NamedArg Pattern]
_) [] = 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) =>
Doc -> m a
genericDocError forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< do
                  forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"Too many arguments to constructor" forall a. [a] -> [a] -> [a]
++ [forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM ConHead
c]
            [NamedArg Pattern] -> Args -> TCMT IO ()
checkArgs [NamedArg Pattern]
ps Args
vs

            [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' Term 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' Term 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' Term 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' Term 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' Term 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' Term Type]
instTel Telescope
EmptyTel [Term]
_                   = []
    instTel (ExtendTel Dom' Term Type
arg Abs Telescope
tel) (Term
u : [Term]
us) = Dom' Term Type
arg forall a. a -> [a] -> [a]
: Telescope -> [Term] -> [Dom' Term 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' i o -> i
^. forall a. Lens' [NamedArg Pattern] (Problem a)
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' i o -> i
^. forall a. Lens' [NamedArg Pattern] (Problem a)
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' SrcFile
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
    Term
a <- forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce Term
a
    case Term
a of
      Def QName
t Elims
_ -> do
        Defn
d <- Definition -> Defn
theDef forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
t
        case Defn
d of
          Datatype { dataCons :: Defn -> [QName]
dataCons = [QName]
cs } -> do
            case forall a. (a -> Bool) -> [a] -> [a]
filter ((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 of
              []      -> forall (m :: * -> *) a. Monad m => a -> m a
return ()
              (QName
c : [QName]
_) -> 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 :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError forall a b. (a -> b) -> a -> b
$ Name -> QName -> TypeError
PatternShadowsConstructor (Name -> Name
nameConcrete Name
x) QName
c
          AbstractDefn{} -> forall (m :: * -> *) a. Monad m => a -> m a
return ()
            -- Abstract constructors cannot be brought into scope,
            -- even by a bigger import list.
            -- Thus, they cannot be confused with variables.
            -- Alternatively, we could do getConstInfo in ignoreAbstractMode,
            -- then Agda would complain if a variable shadowed an abstract constructor.
          Axiom       {} -> forall (m :: * -> *) a. Monad m => a -> m a
return ()
          DataOrRecSig{} -> forall (m :: * -> *) a. Monad m => a -> m a
return ()
          Function    {} -> forall (m :: * -> *) a. Monad m => a -> m a
return ()
          Record      {} -> forall (m :: * -> *) a. Monad m => a -> m a
return ()
          Constructor {} -> forall a. HasCallStack => a
__IMPOSSIBLE__
          GeneralizableVar{} -> forall a. HasCallStack => a
__IMPOSSIBLE__
          -- TODO: in the future some stuck primitives might allow constructors
          Primitive   {} -> forall (m :: * -> *) a. Monad m => a -> m a
return ()
          PrimitiveSort{} -> forall (m :: * -> *) a. Monad m => a -> m a
return ()
      Var   {} -> forall (m :: * -> *) a. Monad m => a -> m a
return ()
      Pi    {} -> forall (m :: * -> *) a. Monad m => a -> m a
return ()
      Sort  {} -> forall (m :: * -> *) a. Monad m => a -> m a
return ()
      MetaV {} -> forall (m :: * -> *) a. Monad m => a -> m a
return ()
      -- TODO: If the type is a meta-variable, should the test be
      -- postponed? If there is a problem, then it will be caught when
      -- the completed module is type checked, so it is safe to skip
      -- the test here. However, users may be annoyed if they get an
      -- error in code which has already passed the type checker.
      Lam   {} -> forall a. HasCallStack => a
__IMPOSSIBLE__
      Lit   {} -> forall a. HasCallStack => a
__IMPOSSIBLE__
      Level {} -> forall a. HasCallStack => a
__IMPOSSIBLE__
      Con   {} -> 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

-- | 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' SrcFile
r Type
a) = Range' SrcFile -> Type -> TCMT IO ()
ensureEmptyType Range' SrcFile
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' Term 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' Term 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' Term 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' Term 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' Term 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' Term Type -> ProblemEq
ProblemEq (forall e. BindName -> Pattern' e
A.VarP BindName
x) Term
u Dom' Term Type
a, Pattern -> Term -> Dom' Term Type -> ProblemEq
ProblemEq Pattern
p Term
u Dom' Term 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' Term 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' Term 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' Term Type -> ProblemEq
ProblemEq Pattern
p Term
u Dom' Term 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 -> Name -> Term -> Type -> m a -> m a
addLetBinding (forall a. LensModality a => Modality -> a -> a
setModality Modality
m ArgInfo
defaultArgInfo) 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' Term Type
a) = forall (m :: * -> *).
MonadCheckInternal m =>
Term -> Comparison -> Type -> m ()
checkInternal Term
v Comparison
CmpLeq (forall t e. Dom' t e -> e
unDom Dom' Term 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 b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> TypeError
GenericDocError forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
    [ TCMT IO Doc
"Ill-typed pattern after with abstraction: " 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
    , TCMT IO Doc
"(perhaps you can replace it by `_`?)"
    ]

-- | 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' Term 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' i o -> i
^. forall a. Lens' Telescope (LHSState a)
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 i o. Lens' i o -> LensMap i o
over (forall a. Lens' (Problem a) (LHSState a)
lhsProblem forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Lens' [ProblemEq] (Problem a)
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 = 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
    , 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
      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
      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)
        Name
argn <- Int -> TCMT IO Name
name Int
arg
        forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (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 a b. (a, b) -> b
snd forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Dom ([Char], Type)
d) Bool -> Bool -> Bool
&& Int
arg forall a. Eq a => a -> a -> Bool
/= Int
blocking) 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 (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))))
    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' Term 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 i o. Lens' i o -> LensMap i o
over (forall a. Lens' Telescope (LHSState a)
lhsTel forall b c a. (b -> c) -> (a -> b) -> a -> c
. Lens' [Dom ([Char], Type)] Telescope
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' i o -> i
^. forall a. Lens' (LHSState a -> TCM a) (Problem 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' i o -> i
^. forall a. Lens' [ProblemEq] (Problem a)
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' i o -> i
^. forall a. Lens' [NamedArg Pattern] (Problem a)
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
iforall a. Num a => a -> a -> a
+Int
1)
          (Telescope
delta1, tel' :: Telescope
tel'@(ExtendTel Dom' Term 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' Term Type
-> Abs Telescope
-> Literal
-> ExceptT TCErr tcm (LHSState a)
splitLit Telescope
delta1 Dom' Term Type
dom Abs Telescope
adelta2 Literal
l
            p :: Pattern
p@A.RecP{}        -> Telescope
-> Dom' Term Type
-> Abs Telescope
-> Pattern
-> Maybe AmbiguousQName
-> ExceptT TCErr tcm (LHSState a)
splitCon Telescope
delta1 Dom' Term 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' Term Type
-> Abs Telescope
-> Pattern
-> Maybe AmbiguousQName
-> ExceptT TCErr tcm (LHSState a)
splitCon Telescope
delta1 Dom' Term 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' Term Type
-> Abs Telescope
-> [(Expr, Expr)]
-> ExceptT TCErr tcm (LHSState a)
splitPartial Telescope
delta1 Dom' Term 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 b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> TypeError
GenericDocError 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
$ TCMT IO Doc
"Copattern matching is disabled for record" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM 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 a. Bool -> (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 i o. Lens' i o -> LensMap i o
over forall a. Lens' [NamedArg Pattern] (Problem a)
problemRestPats forall a. [a] -> [a]
tail 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' Term Type
-> Abs Telescope
-> [(Expr, Expr)]
-> ExceptT TCErr tcm (LHSState a)
splitPartial Telescope
delta1 Dom' Term 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' Term 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 b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> TypeError
GenericDocError forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<<
        forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat [ TCMT IO Doc
"Splitting on partial elements is only allowed at the type Partial, but the domain here is" , forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM forall a b. (a -> b) -> a -> b
$ forall t e. Dom' t e -> e
unDom Dom' Term 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' i o -> i
^. forall a. Lens' [ProblemEq] (Problem a)
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' Term 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 => [Char] -> m (Maybe QName)
getBuiltinName' [Char]
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 b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> TypeError
GenericDocError forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< do
                         forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
a forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
" is not IsOne."

                   [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' i o -> i
^. forall a. Lens' [ProblemEq] (Problem a)
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 i o. Lens' i o -> LensSet i o
set forall a. Lens' [ProblemEq] (Problem a)
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' Term Type
-> Abs Telescope
-> Literal
-> ExceptT TCErr tcm (LHSState a)
splitLit Telescope
delta1 dom :: Dom' Term 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' i o -> i
^. forall a. Lens' [ProblemEq] (Problem a)
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' Term Type -> TypeError
SplitOnIrrelevant Dom' Term 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' Term Type -> TypeError
SplitOnUnusableCohesion Dom' Term 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 i o. Lens' i o -> LensSet i o
set forall a. Lens' [ProblemEq] (Problem a)
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' Term Type
-> Abs Telescope
-> Pattern
-> Maybe AmbiguousQName
-> ExceptT TCErr tcm (LHSState a)
splitCon Telescope
delta1 dom :: Dom' Term 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' Term 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' Term Type -> TypeError
SplitOnIrrelevant Dom' Term 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' Term Type -> TypeError
SplitOnUnusableCohesion Dom' Term 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 (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
        SSet{} -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a b.
MonadTCEnv m =>
Lens' a TCEnv -> (a -> a) -> m b -> m b
locallyTC Lens' Bool TCEnv
eSplitOnStrict forall a b. (a -> b) -> a -> b
$ forall a b. a -> b -> a
const Bool
True
        Sort' Term
_      -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a. a -> a
id

      -- 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' a TCEnv -> m a
viewTC Lens' Bool TCEnv
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' i o -> i
^. forall a. Lens' [ProblemEq] (Problem a)
problemEqs
              problem' :: Problem a
problem' = forall i o. Lens' i o -> LensSet i o
set forall a. Lens' [ProblemEq] (Problem a)
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 <- forall (b :: Bool). KnownBool b => WithDefault b -> Bool
collapseDefault forall b c a. (b -> c) -> (a -> b) -> a -> c
. PragmaOptions -> WithDefault 'False
optWithoutK forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasOptions m => m PragmaOptions
pragmaOptions
            Bool
cubical <- forall (b :: Bool). KnownBool b => WithDefault b -> Bool
collapseDefault forall b c a. (b -> c) -> (a -> b) -> a -> c
. PragmaOptions -> WithDefault 'False
optCubicalCompatible forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasOptions m => m PragmaOptions
pragmaOptions
            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 (forall a. LensModality a => a -> Modality
getModality Arg Type
target) 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' i o -> i
^. forall a. Lens' Telescope (LHSState a)
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' i o -> i
^. forall a. Lens' Telescope (LHSState a)
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' i o -> i
^. (forall a. Lens' (Problem a) (LHSState a)
lhsProblem forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Lens' [ProblemEq] (Problem a)
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' i o -> i
^. forall a. Lens' Telescope (LHSState a)
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' i o -> i
^. forall a. Lens' [NamedArg DeBruijnPattern] (LHSState a)
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 Maybe Induction
ind 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

data DataOrRecord
  = IsData
  | IsRecord
    { DataOrRecord -> Maybe Induction
recordInduction   :: Maybe Induction
    , DataOrRecord -> EtaEquality
recordEtaEquality :: EtaEquality
    }
  deriving (Int -> DataOrRecord -> [Char] -> [Char]
[DataOrRecord] -> [Char] -> [Char]
DataOrRecord -> [Char]
forall a.
(Int -> a -> [Char] -> [Char])
-> (a -> [Char]) -> ([a] -> [Char] -> [Char]) -> Show a
showList :: [DataOrRecord] -> [Char] -> [Char]
$cshowList :: [DataOrRecord] -> [Char] -> [Char]
show :: DataOrRecord -> [Char]
$cshow :: DataOrRecord -> [Char]
showsPrec :: Int -> DataOrRecord -> [Char] -> [Char]
$cshowsPrec :: Int -> DataOrRecord -> [Char] -> [Char]
Show)

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

isDataOrRecordType :: 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 (DataOrRecord
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 (Maybe Induction -> EtaEquality -> DataOrRecord
IsRecord Maybe Induction
recInduction 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 b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> TypeError
GenericDocError 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
$ TCMT IO Doc
"Cannot split on abstract data type" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM 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 b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> TypeError
GenericDocError 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
$ TCMT IO Doc
"Cannot split on data type" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
d forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
"whose definition has not yet been checked"

      -- Issue #2997: the type could be a Def that does not reduce for some reason
      -- (abstract, failed termination checking, NON_TERMINATING, ...)
      Function{}    -> 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 b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> TypeError
GenericDocError forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
              [ TCMT IO Doc
"Ambiguous projection " forall a. Semigroup a => a -> a -> a
<> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
d forall a. Semigroup a => a -> a -> a
<> TCMT IO Doc
"."
              , TCMT IO Doc
"It could refer to any of"
              , 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 forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (QName -> TCMT IO Doc
prettyDisambProj forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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
$ Doc -> TypeError
GenericDocError forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep
        [ TCMT IO Doc
"Cannot eliminate type "
        , forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM (forall e. Arg e -> e
unArg Arg Type
b)
        , TCMT IO Doc
" with projection "
        , if AmbiguousQName -> Bool
isAmbiguous AmbiguousQName
ambD then
            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 forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< QName -> TCMT IO QName
dropTopLevelModule QName
d
          else
            forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
d
        ]

    wrongHiding :: (MonadTCM m, MonadError TCErr m, ReadTCState m) => QName -> m a
    wrongHiding :: forall (m :: * -> *) a.
(MonadTCM m, MonadError TCErr m, ReadTCState m) =>
QName -> m a
wrongHiding 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
$ Doc -> TypeError
GenericDocError forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep
        [ TCMT IO Doc
"Wrong hiding used for projection " , forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM 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.
(MonadTCM m, MonadError TCErr m, ReadTCState m) =>
QName -> m a
wrongHiding 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 b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> TypeError
GenericDocError forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
          [ TCMT IO Doc
"Ambiguous constructor " forall a. Semigroup a => a -> a -> a
<> forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty (QName -> Name
qnameName QName
c) forall a. Semigroup a => a -> a -> a
<> TCMT IO Doc
"."
          , TCMT IO Doc
"It could refer to any of"
          , 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 forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (QName -> TCMT IO Doc
prettyDisambCons forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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
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


prettyDisamb :: (QName -> Maybe (Range' SrcFile)) -> QName -> TCM Doc
prettyDisamb :: (QName -> Maybe (Range' SrcFile)) -> QName -> TCMT IO Doc
prettyDisamb QName -> Maybe (Range' SrcFile)
f QName
x = do
  let d :: TCMT IO Doc
d  = forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< QName -> TCMT IO QName
dropTopLevelModule QName
x
  forall a b. Maybe a -> b -> (a -> b) -> b
caseMaybe (QName -> Maybe (Range' SrcFile)
f QName
x) TCMT IO Doc
d forall a b. (a -> b) -> a -> b
$ \ Range' SrcFile
r -> TCMT IO Doc
d forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> (TCMT IO Doc
"(introduced at " forall a. Semigroup a => a -> a -> a
<> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Range' SrcFile
r forall a. Semigroup a => a -> a -> a
<> TCMT IO Doc
")")

-- | For Ambiguous Projection errors, print the last range in 'qnameModule'.
--   For Ambiguous Constructor errors, print the range in 'qnameName'. This fixes the bad
--   error message in #4130.
prettyDisambProj, prettyDisambCons :: QName -> TCM Doc
prettyDisambProj :: QName -> TCMT IO Doc
prettyDisambProj = (QName -> Maybe (Range' SrcFile)) -> QName -> TCMT IO Doc
prettyDisamb forall a b. (a -> b) -> a -> b
$ forall a. [a] -> Maybe a
lastMaybe forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. (a -> Bool) -> [a] -> [a]
filter (forall a. Range' a
noRange forall a. Eq a => a -> a -> Bool
/=) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map Name -> Range' SrcFile
nameBindingSite forall b c a. (b -> c) -> (a -> b) -> a -> c
. ModuleName -> [Name]
mnameToList forall b c a. (b -> c) -> (a -> b) -> a -> c
. QName -> ModuleName
qnameModule
prettyDisambCons :: QName -> TCMT IO Doc
prettyDisambCons = (QName -> Maybe (Range' SrcFile)) -> QName -> TCMT IO Doc
prettyDisamb forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> Range' SrcFile
nameBindingSite forall b c a. (b -> c) -> (a -> b) -> a -> c
. QName -> Name
qnameName

-- | @checkConstructorParameters c d pars@ checks that the data/record type
--   behind @c@ is has initial parameters (coming e.g. from a module instantiation)
--   that coincide with an prefix of @pars@.
checkConstructorParameters :: MonadTCM tcm => QName -> QName -> Args -> tcm ()
checkConstructorParameters :: 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
    sa :: Sort' Term
sa@Type{} -> forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
whenM forall (m :: * -> *). HasOptions m => m Bool
isTwoLevelEnabled m ()
checkFibrantSplit
    Prop{} -> m ()
checkPropSplit
    Inf IsFibrant
IsFibrant Integer
_ -> forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
whenM forall (m :: * -> *). HasOptions m => m Bool
isTwoLevelEnabled m ()
checkFibrantSplit
    Inf IsFibrant
IsStrict Integer
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return ()
    SSet{} -> forall (m :: * -> *) a. Monad m => a -> m a
return ()
    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 Maybe Induction
Nothing EtaEquality
_ <- 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 :: * -> *} {b}.
(ReadTCState m, MonadError TCErr m, MonadTCM m) =>
DataOrRecord -> m b
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 :: * -> *} {b}.
(ReadTCState m, MonadError TCErr m, MonadTCM m) =>
DataOrRecord -> m b
splitOnPropError DataOrRecord
dr -- TODO
      Right Bool
False -> forall {m :: * -> *} {b}.
(ReadTCState m, MonadError TCErr m, MonadTCM m) =>
DataOrRecord -> m b
splitOnPropError DataOrRecord
dr
      Right Bool
True  -> forall (m :: * -> *) a. Monad m => a -> m a
return ()

    checkFibrantSplit :: m ()
checkFibrantSplit
      | IsRecord Maybe Induction
_ EtaEquality
_ <- 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 b
splitOnPropError DataOrRecord
dr = 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
$ Doc -> TypeError
GenericDocError forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
        (TCMT IO Doc
"Cannot split on" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> DataOrRecord -> TCMT IO Doc
kindOfData DataOrRecord
dr forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
"in Prop unless target is in Prop")
      where
        kindOfData :: DataOrRecord -> TCM Doc
        kindOfData :: DataOrRecord -> TCMT IO Doc
kindOfData DataOrRecord
IsData                          = TCMT IO Doc
"datatype"
        kindOfData (IsRecord Maybe Induction
Nothing EtaEquality
_)            = TCMT IO Doc
"record type"
        kindOfData (IsRecord (Just Induction
Inductive) EtaEquality
_)   = TCMT IO Doc
"inductive record type"
        kindOfData (IsRecord (Just Induction
CoInductive) EtaEquality
_) = TCMT IO Doc
"coinductive record type"

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