{-# LANGUAGE NondecreasingIndentation #-}

module Agda.TypeChecking.Rules.Application
  ( checkArguments
  , checkArguments_
  , checkApplication
  , inferApplication
  , checkProjAppToKnownPrincipalArg
  ) where

import Prelude hiding ( null )

import Control.Applicative        ( (<|>) )
import Control.Monad              ( forM, forM_, guard, liftM2 )
import Control.Monad.Except
import Control.Monad.Trans
import Control.Monad.Trans.Maybe
import Control.Monad.Reader

import Data.Bifunctor
import Data.Maybe
import Data.Void
import qualified Data.Foldable as Fold
import qualified Data.IntSet   as IntSet

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

import qualified Agda.Syntax.Abstract as A
import Agda.Syntax.Abstract.Views as A
import qualified Agda.Syntax.Info as A
import Agda.Syntax.Concrete.Pretty () -- only Pretty instances
import Agda.Syntax.Common
import Agda.Syntax.Internal as I
import Agda.Syntax.Position

import Agda.TypeChecking.Conversion
import Agda.TypeChecking.Constraints
import Agda.TypeChecking.Datatypes
import Agda.TypeChecking.Free
import Agda.TypeChecking.Free.Lazy (VarMap, lookupVarMap)
import Agda.TypeChecking.Implicit
import Agda.TypeChecking.Injectivity
import Agda.TypeChecking.Irrelevance
import Agda.TypeChecking.InstanceArguments (postponeInstanceConstraints)
import Agda.TypeChecking.Level
import Agda.TypeChecking.MetaVars
import Agda.TypeChecking.Names
import Agda.TypeChecking.Pretty
import Agda.TypeChecking.Primitive hiding (Nat)
import Agda.TypeChecking.Monad
import Agda.TypeChecking.Records
import Agda.TypeChecking.Reduce
import Agda.TypeChecking.Rules.Def
import Agda.TypeChecking.Rules.Term
import Agda.TypeChecking.Substitute
import Agda.TypeChecking.Telescope

import Agda.Utils.Either
import Agda.Utils.Functor
import Agda.Utils.Lens
import Agda.Utils.List  ( (!!!), groupOn, initWithDefault )
import qualified Agda.Utils.List as List
import Agda.Utils.List1 ( List1, pattern (:|) )
import qualified Agda.Utils.List1 as List1
import Agda.Utils.Maybe
import Agda.Utils.Monad
import Agda.Utils.Null
import Agda.Utils.Pretty ( prettyShow )
import Agda.Utils.Size
import Agda.Utils.Tuple

import Agda.Utils.Impossible

-----------------------------------------------------------------------------
-- * Applications
-----------------------------------------------------------------------------

-- | Ranges of checked arguments, where present.
type MaybeRanges = [Maybe Range]

acHeadConstraints :: (Elims -> Term) -> ArgsCheckState a -> [Constraint]
acHeadConstraints :: forall a. (Elims -> Term) -> ArgsCheckState a -> [Constraint]
acHeadConstraints Elims -> Term
hd ACState{acElims :: forall a. ArgsCheckState a -> Elims
acElims = Elims
es, acConstraints :: forall a. ArgsCheckState a -> [Maybe (Abs Constraint)]
acConstraints = [Maybe (Abs Constraint)]
cs} = forall {a} {a}.
Subst a =>
([a] -> SubstArg a) -> [a] -> [Maybe (Abs a)] -> [a]
go Elims -> Term
hd Elims
es [Maybe (Abs Constraint)]
cs
  where
    go :: ([a] -> SubstArg a) -> [a] -> [Maybe (Abs a)] -> [a]
go [a] -> SubstArg a
hd [] [] = []
    go [a] -> SubstArg a
hd (a
e : [a]
es) (Maybe (Abs a)
c : [Maybe (Abs a)]
cs) = forall b a. b -> (a -> b) -> Maybe a -> b
maybe forall a. a -> a
id (\ Abs a
c -> (forall a. Subst a => Abs a -> SubstArg a -> a
lazyAbsApp Abs a
c ([a] -> SubstArg a
hd []) forall a. a -> [a] -> [a]
:)) Maybe (Abs a)
c forall a b. (a -> b) -> a -> b
$ ([a] -> SubstArg a) -> [a] -> [Maybe (Abs a)] -> [a]
go ([a] -> SubstArg a
hd forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a
e forall a. a -> [a] -> [a]
:)) [a]
es [Maybe (Abs a)]
cs
    go [a] -> SubstArg a
_  [] (Maybe (Abs a)
_:[Maybe (Abs a)]
_) = forall a. HasCallStack => a
__IMPOSSIBLE__
    go [a] -> SubstArg a
_  (a
_:[a]
_) [] = forall a. HasCallStack => a
__IMPOSSIBLE__

checkHeadConstraints :: (Elims -> Term) -> ArgsCheckState a -> TCM Term
checkHeadConstraints :: forall a. (Elims -> Term) -> ArgsCheckState a -> TCM Term
checkHeadConstraints Elims -> Term
hd ArgsCheckState a
st = do
  forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ Constraint -> TCM ()
solveConstraint_ (forall a. (Elims -> Term) -> ArgsCheckState a -> [Constraint]
acHeadConstraints Elims -> Term
hd ArgsCheckState a
st)
  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Elims -> Term
hd (forall a. ArgsCheckState a -> Elims
acElims ArgsCheckState a
st)


-- | @checkApplication hd args e t@ checks an application.
--   Precondition: @Application hs args = appView e@
--
--   @checkApplication@ disambiguates constructors
--   (and continues to 'checkConstructorApplication')
--   and resolves pattern synonyms.
checkApplication :: Comparison -> A.Expr -> A.Args -> A.Expr -> Type -> TCM Term
checkApplication :: Comparison -> Expr -> [NamedArg Expr] -> Expr -> Type -> TCM Term
checkApplication Comparison
cmp Expr
hd [NamedArg Expr]
args Expr
e Type
t =
  forall a. Expr -> TCM a -> TCM a
turnOffExpandLastIfExistingMeta Expr
hd forall a b. (a -> b) -> a -> b
$
  forall a. TCM a -> TCM a
postponeInstanceConstraints forall a b. (a -> b) -> a -> b
$ do
  forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.check.app" Nat
20 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
    [ TCMT IO Doc
"checkApplication"
    , forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
nest Nat
2 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"hd   = " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA Expr
hd
    , forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
nest Nat
2 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"args = " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep (forall a b. (a -> b) -> [a] -> [b]
map forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA [NamedArg Expr]
args)
    , forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
nest Nat
2 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"e    = " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA Expr
e
    , forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
nest Nat
2 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"t    = " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
t
    ]
  forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.check.app" Nat
70 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
    [ TCMT IO Doc
"checkApplication (raw)"
    , forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
nest Nat
2 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). Applicative m => [Char] -> m Doc
text forall a b. (a -> b) -> a -> b
$ [Char]
"hd   = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Expr
hd
    , forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
nest Nat
2 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). Applicative m => [Char] -> m Doc
text forall a b. (a -> b) -> a -> b
$ [Char]
"args = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show (forall a. ExprLike a => a -> a
deepUnscope [NamedArg Expr]
args)
    , forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
nest Nat
2 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). Applicative m => [Char] -> m Doc
text forall a b. (a -> b) -> a -> b
$ [Char]
"e    = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show (forall a. ExprLike a => a -> a
deepUnscope Expr
e)
    , forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
nest Nat
2 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). Applicative m => [Char] -> m Doc
text forall a b. (a -> b) -> a -> b
$ [Char]
"t    = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Type
t
    ]
  case Expr -> Expr
unScope Expr
hd of
    -- Subcase: unambiguous projection
    A.Proj ProjOrigin
o AmbiguousQName
p | Just QName
x <- AmbiguousQName -> Maybe QName
getUnambiguous AmbiguousQName
p -> do
      Comparison
-> Expr
-> Type
-> QName
-> ProjOrigin
-> Expr
-> [NamedArg Expr]
-> TCM Term
checkUnambiguousProjectionApplication Comparison
cmp Expr
e Type
t QName
x ProjOrigin
o Expr
hd [NamedArg Expr]
args

    -- Subcase: ambiguous projection
    A.Proj ProjOrigin
o AmbiguousQName
p -> do
      Comparison
-> Expr
-> ProjOrigin
-> List1 QName
-> [NamedArg Expr]
-> Type
-> TCM Term
checkProjApp Comparison
cmp Expr
e ProjOrigin
o (AmbiguousQName -> List1 QName
unAmbQ AmbiguousQName
p) [NamedArg Expr]
args Type
t

    -- Subcase: unambiguous constructor
    A.Con AmbiguousQName
ambC | Just QName
c <- AmbiguousQName -> Maybe QName
getUnambiguous AmbiguousQName
ambC -> do
      -- augment c with record fields, but do not revert to original name
      ConHead
con <- forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> m (Either a b) -> m b
fromRightM (forall a. ([Char] -> a) -> a -> SigError -> a
sigError forall (m :: * -> *) a.
(HasCallStack, MonadDebug m) =>
[Char] -> m a
__IMPOSSIBLE_VERBOSE__ (forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError forall a b. (a -> b) -> a -> b
$ QName -> TypeError
AbstractConstructorNotInScope QName
c)) forall a b. (a -> b) -> a -> b
$
        QName -> TCM (Either SigError ConHead)
getOrigConHead QName
c
      Comparison
-> Expr -> Type -> ConHead -> [NamedArg Expr] -> TCM Term
checkConstructorApplication Comparison
cmp Expr
e Type
t ConHead
con [NamedArg Expr]
args

    -- Subcase: ambiguous constructor
    A.Con (AmbQ List1 QName
cs0) -> List1 QName -> Type -> TCM (Either Blocker ConHead)
disambiguateConstructor List1 QName
cs0 Type
t forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \ case
      Left Blocker
unblock -> TypeCheckingProblem -> Blocker -> TCM Term
postponeTypeCheckingProblem (Comparison -> Expr -> Type -> TypeCheckingProblem
CheckExpr Comparison
cmp Expr
e Type
t) Blocker
unblock
      Right ConHead
c      -> Comparison
-> Expr -> Type -> ConHead -> [NamedArg Expr] -> TCM Term
checkConstructorApplication Comparison
cmp Expr
e Type
t ConHead
c [NamedArg Expr]
args

    -- Subcase: pattern synonym
    A.PatternSyn AmbiguousQName
n -> do
      ([Arg Name]
ns, Pattern' Void
p) <- AmbiguousQName -> TCM ([Arg Name], Pattern' Void)
lookupPatternSyn AmbiguousQName
n
      Pattern' Expr
p <- forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. SetRange a => Range -> a -> a
setRange (forall a. HasRange a => a -> Range
getRange AmbiguousQName
n) forall a b. (a -> b) -> a -> b
$ forall a. KillRange a => KillRangeT a
killRange forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a. Functor f => f Void -> f a
vacuous Pattern' Void
p   -- Pattern' Void -> Pattern' Expr
      -- Expand the pattern synonym by substituting for
      -- the arguments we have got and lambda-lifting
      -- over the ones we haven't.
      let meta :: Range -> Expr
meta Range
r = MetaInfo -> Expr
A.Underscore forall a b. (a -> b) -> a -> b
$ MetaInfo
A.emptyMetaInfo{ metaRange :: Range
A.metaRange = Range
r }   -- TODO: name suggestion
      case forall a.
HasRange a =>
(Range -> a)
-> Range
-> [Arg Name]
-> [NamedArg a]
-> Maybe ([(Name, a)], [Arg Name])
A.insertImplicitPatSynArgs Range -> Expr
meta (forall a. HasRange a => a -> Range
getRange AmbiguousQName
n) [Arg Name]
ns [NamedArg Expr]
args of
        Maybe ([(Name, Expr)], [Arg Name])
Nothing      -> forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError forall a b. (a -> b) -> a -> b
$ AmbiguousQName -> TypeError
BadArgumentsToPatternSynonym AmbiguousQName
n
        Just ([(Name, Expr)]
s, [Arg Name]
ns) -> do
          let p' :: Expr
p' = Pattern' Expr -> Expr
A.patternToExpr Pattern' Expr
p
              e' :: Expr
e' = [Name] -> Expr -> Expr
A.lambdaLiftExpr (forall a b. (a -> b) -> [a] -> [b]
map forall e. Arg e -> e
unArg [Arg Name]
ns) (forall a. SubstExpr a => [(Name, Expr)] -> a -> a
A.substExpr [(Name, Expr)]
s Expr
p')
          Comparison -> Expr -> Type -> TCM Term
checkExpr' Comparison
cmp Expr
e' Type
t

    -- Subcase: macro
    A.Macro QName
x -> do
      -- First go: no parameters
      TelV Tele (Dom Type)
tel Type
_ <- forall (m :: * -> *).
(MonadReduce m, MonadAddContext m) =>
Type -> m (TelV Type)
telView forall b c a. (b -> c) -> (a -> b) -> a -> c
. Definition -> Type
defType forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (m :: * -> *).
(Functor m, HasConstInfo m, HasOptions m, ReadTCState m,
 MonadTCEnv m, MonadDebug m) =>
Definition -> m Definition
instantiateDef forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
x

      Term
tTerm <- forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTerm
      Term
tName <- forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primQName

      -- Andreas, 2021-05-13, can we use @initWithDefault __IMPOSSIBLE__@ here?
      let argTel :: [Dom ([Char], Type)]
argTel   = forall a. [a] -> [a]
init forall a b. (a -> b) -> a -> b
$ forall t. Tele (Dom t) -> [Dom ([Char], t)]
telToList Tele (Dom Type)
tel -- last argument is the hole term

          -- inspect macro type to figure out if arguments need to be wrapped in quote/quoteTerm
          mkArg :: Type -> NamedArg A.Expr -> NamedArg A.Expr
          mkArg :: Type -> NamedArg Expr -> NamedArg Expr
mkArg Type
t NamedArg Expr
a | forall t a. Type'' t a -> a
unEl Type
t forall a. Eq a => a -> a -> Bool
== Term
tTerm =
            (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)
              (AppInfo -> Expr -> NamedArg Expr -> Expr
A.App (Range -> AppInfo
A.defaultAppInfo (forall a. HasRange a => a -> Range
getRange NamedArg Expr
a)) (ExprInfo -> Expr
A.QuoteTerm ExprInfo
A.exprNoRange) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. a -> NamedArg a
defaultNamedArg) NamedArg Expr
a
          mkArg Type
t NamedArg Expr
a | forall t a. Type'' t a -> a
unEl Type
t forall a. Eq a => a -> a -> Bool
== Term
tName =
            (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)
              (AppInfo -> Expr -> NamedArg Expr -> Expr
A.App (Range -> AppInfo
A.defaultAppInfo (forall a. HasRange a => a -> Range
getRange NamedArg Expr
a)) (ExprInfo -> Expr
A.Quote ExprInfo
A.exprNoRange) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. a -> NamedArg a
defaultNamedArg) NamedArg Expr
a
          mkArg Type
t NamedArg Expr
a | Bool
otherwise = NamedArg Expr
a

          makeArgs :: [Dom (String, Type)] -> [NamedArg A.Expr] -> ([NamedArg A.Expr], [NamedArg A.Expr])
          makeArgs :: [Dom ([Char], Type)]
-> [NamedArg Expr] -> ([NamedArg Expr], [NamedArg Expr])
makeArgs [] [NamedArg Expr]
args = ([], [NamedArg Expr]
args)
          makeArgs [Dom ([Char], Type)]
_  []   = ([], [])
          makeArgs tel :: [Dom ([Char], Type)]
tel@(Dom ([Char], Type)
d : [Dom ([Char], Type)]
tel1) (NamedArg Expr
arg : [NamedArg Expr]
args) =
            case forall e a. NamedArg e -> [Dom a] -> ImplicitInsertion
insertImplicit NamedArg Expr
arg [Dom ([Char], Type)]
tel of
              ImplicitInsertion
NoInsertNeeded -> forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first (Type -> NamedArg Expr -> NamedArg Expr
mkArg (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) NamedArg Expr
arg forall a. a -> [a] -> [a]
:) forall a b. (a -> b) -> a -> b
$ [Dom ([Char], Type)]
-> [NamedArg Expr] -> ([NamedArg Expr], [NamedArg Expr])
makeArgs [Dom ([Char], Type)]
tel1 [NamedArg Expr]
args
              ImpInsert [Dom ()]
is   -> [Dom ([Char], Type)]
-> [NamedArg Expr] -> ([NamedArg Expr], [NamedArg Expr])
makeArgs (forall a. Nat -> [a] -> [a]
drop (forall (t :: * -> *) a. Foldable t => t a -> Nat
length [Dom ()]
is) [Dom ([Char], Type)]
tel) (NamedArg Expr
arg forall a. a -> [a] -> [a]
: [NamedArg Expr]
args)
              ImplicitInsertion
BadImplicits   -> (NamedArg Expr
arg forall a. a -> [a] -> [a]
: [NamedArg Expr]
args, [])  -- fail later in checkHeadApplication
              NoSuchName{}   -> (NamedArg Expr
arg forall a. a -> [a] -> [a]
: [NamedArg Expr]
args, [])  -- ditto

          ([NamedArg Expr]
macroArgs, [NamedArg Expr]
otherArgs) = [Dom ([Char], Type)]
-> [NamedArg Expr] -> ([NamedArg Expr], [NamedArg Expr])
makeArgs [Dom ([Char], Type)]
argTel [NamedArg Expr]
args
          unq :: Expr -> Expr
unq = AppInfo -> Expr -> NamedArg Expr -> Expr
A.App (Range -> AppInfo
A.defaultAppInfo forall a b. (a -> b) -> a -> b
$ forall u t. (HasRange u, HasRange t) => u -> t -> Range
fuseRange QName
x [NamedArg Expr]
args) (ExprInfo -> Expr
A.Unquote ExprInfo
A.exprNoRange) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. a -> NamedArg a
defaultNamedArg

          desugared :: Expr
desugared = Expr -> [NamedArg Expr] -> Expr
A.app (Expr -> Expr
unq forall a b. (a -> b) -> a -> b
$ AppView -> Expr
unAppView forall a b. (a -> b) -> a -> b
$ forall arg. Expr -> [NamedArg arg] -> AppView' arg
Application (QName -> Expr
A.Def QName
x) forall a b. (a -> b) -> a -> b
$ [NamedArg Expr]
macroArgs) [NamedArg Expr]
otherArgs

      Comparison -> Expr -> Type -> TCM Term
checkExpr' Comparison
cmp Expr
desugared Type
t

    -- Subcase: unquote
    A.Unquote ExprInfo
_
      | [NamedArg Expr
arg] <- [NamedArg Expr]
args -> do
          (MetaId
_, Term
hole) <- forall (m :: * -> *).
MonadMetaSolver m =>
RunMetaOccursCheck -> Comparison -> Type -> m (MetaId, Term)
newValueMeta RunMetaOccursCheck
RunMetaOccursCheck Comparison
CmpLeq Type
t
          Expr -> Term -> Type -> TCM ()
unquoteM (forall a. NamedArg a -> a
namedArg NamedArg Expr
arg) Term
hole Type
t
          forall (m :: * -> *) a. Monad m => a -> m a
return Term
hole
      | NamedArg Expr
arg : [NamedArg Expr]
args <- [NamedArg Expr]
args -> do
          -- Example: unquote v a b : A
          --  Create meta H : (x : X) (y : Y x) → Z x y for the hole
          --  Check a : X, b : Y a
          --  Unify Z a b == A
          --  Run the tactic on H
          Tele (Dom Type)
tel    <- forall a. [Arg a] -> TCM (Tele (Dom Type))
metaTel [NamedArg Expr]
args                    -- (x : X) (y : Y x)
          Type
target <- forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Tele (Dom Type)
tel TCM Type
newTypeMeta_      -- Z x y
          let holeType :: Type
holeType = Tele (Dom Type) -> Type -> Type
telePi_ Tele (Dom Type)
tel Type
target         -- (x : X) (y : Y x) → Z x y
          (Just Args
vs, Tele (Dom Type)
EmptyTel) <- forall a c b. (a -> c) -> (a, b) -> (c, b)
mapFst forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Comparison
-> ExpandHidden
-> Range
-> [NamedArg Expr]
-> Tele (Dom Type)
-> TCM (Elims, Tele (Dom Type))
checkArguments_ Comparison
CmpLeq ExpandHidden
ExpandLast (forall a. HasRange a => a -> Range
getRange [NamedArg Expr]
args) [NamedArg Expr]
args Tele (Dom Type)
tel
                                                    -- a b : (x : X) (y : Y x)
          let rho :: Substitution' Term
rho = forall a. [a] -> [a]
reverse (forall a b. (a -> b) -> [a] -> [b]
map forall e. Arg e -> e
unArg Args
vs) forall a. DeBruijn a => [a] -> Substitution' a -> Substitution' a
++# forall a. Substitution' a
IdS  -- [x := a, y := b]
          forall (m :: * -> *). MonadConversion m => Type -> Type -> m ()
equalType (forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' Term
rho Type
target) Type
t       -- Z a b == A
          (MetaId
_, Term
hole) <- forall (m :: * -> *).
MonadMetaSolver m =>
RunMetaOccursCheck -> Comparison -> Type -> m (MetaId, Term)
newValueMeta RunMetaOccursCheck
RunMetaOccursCheck Comparison
CmpLeq Type
holeType
          Expr -> Term -> Type -> TCM ()
unquoteM (forall a. NamedArg a -> a
namedArg NamedArg Expr
arg) Term
hole Type
holeType
          forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall t. Apply t => t -> Args -> t
apply Term
hole Args
vs
      where
        metaTel :: [Arg a] -> TCM Telescope
        metaTel :: forall a. [Arg a] -> TCM (Tele (Dom Type))
metaTel []           = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a. Tele a
EmptyTel
        metaTel (Arg a
arg : [Arg a]
args) = do
          Type
a <- TCM Type
newTypeMeta_
          let dom :: Dom Type
dom = Type
a forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ forall a. Arg a -> Dom a
domFromArg Arg a
arg
          forall a. a -> Abs (Tele a) -> Tele a
ExtendTel Dom Type
dom forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. [Char] -> a -> Abs a
Abs [Char]
"x" forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
            forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext ([Char]
"x" :: String, Dom Type
dom) (forall a. [Arg a] -> TCM (Tele (Dom Type))
metaTel [Arg a]
args)

    -- Subcase: defined symbol or variable.
    Expr
_ -> do
      Term
v <- Comparison -> Expr -> Type -> Expr -> [NamedArg Expr] -> TCM Term
checkHeadApplication Comparison
cmp Expr
e Type
t Expr
hd [NamedArg Expr]
args
      forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.term.app" Nat
30 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
        [ TCMT IO Doc
"checkApplication: checkHeadApplication returned"
        , forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
nest Nat
2 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"v = " 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. Monad m => a -> m a
return Term
v

-- | Precondition: @Application hd args = appView e@.
inferApplication :: ExpandHidden -> A.Expr -> A.Args -> A.Expr -> TCM (Term, Type)
inferApplication :: ExpandHidden -> Expr -> [NamedArg Expr] -> Expr -> TCM (Term, Type)
inferApplication ExpandHidden
exh Expr
hd [NamedArg Expr]
args Expr
e | Bool -> Bool
not (Expr -> Bool
defOrVar Expr
hd) = do
  Type
t <- forall (m :: * -> *) a.
(MonadTCEnv m, HasOptions m, MonadDebug m) =>
m a -> m a
workOnTypes forall a b. (a -> b) -> a -> b
$ TCM Type
newTypeMeta_
  Term
v <- Comparison -> Expr -> Type -> TCM Term
checkExpr' Comparison
CmpEq Expr
e Type
t
  forall (m :: * -> *) a. Monad m => a -> m a
return (Term
v, Type
t)
inferApplication ExpandHidden
exh Expr
hd [NamedArg Expr]
args Expr
e = forall a. TCM a -> TCM a
postponeInstanceConstraints forall a b. (a -> b) -> a -> b
$ do
  SortKit{QName
IsFibrant -> QName
nameOfSetOmega :: SortKit -> IsFibrant -> QName
nameOfSSet :: SortKit -> QName
nameOfProp :: SortKit -> QName
nameOfSet :: SortKit -> QName
nameOfSetOmega :: IsFibrant -> QName
nameOfSSet :: QName
nameOfProp :: QName
nameOfSet :: QName
..} <- forall (m :: * -> *).
(HasBuiltins m, MonadTCError m, HasOptions m) =>
m SortKit
sortKit
  case Expr -> Expr
unScope Expr
hd of
    A.Proj ProjOrigin
o AmbiguousQName
p | AmbiguousQName -> Bool
isAmbiguous AmbiguousQName
p -> Expr
-> ProjOrigin -> List1 QName -> [NamedArg Expr] -> TCM (Term, Type)
inferProjApp Expr
e ProjOrigin
o (AmbiguousQName -> List1 QName
unAmbQ AmbiguousQName
p) [NamedArg Expr]
args
    A.Def' QName
x Suffix
s | QName
x forall a. Eq a => a -> a -> Bool
== QName
nameOfSet      -> Expr -> QName -> Suffix -> [NamedArg Expr] -> TCM (Term, Type)
inferSet Expr
e QName
x Suffix
s [NamedArg Expr]
args
    A.Def' QName
x Suffix
s | QName
x forall a. Eq a => a -> a -> Bool
== QName
nameOfProp     -> Expr -> QName -> Suffix -> [NamedArg Expr] -> TCM (Term, Type)
inferProp Expr
e QName
x Suffix
s [NamedArg Expr]
args
    A.Def' QName
x Suffix
s | QName
x forall a. Eq a => a -> a -> Bool
== QName
nameOfSSet     -> Expr -> QName -> Suffix -> [NamedArg Expr] -> TCM (Term, Type)
inferSSet Expr
e QName
x Suffix
s [NamedArg Expr]
args
    A.Def' QName
x Suffix
s | QName
x forall a. Eq a => a -> a -> Bool
== IsFibrant -> QName
nameOfSetOmega IsFibrant
IsFibrant -> Expr
-> QName
-> IsFibrant
-> Suffix
-> [NamedArg Expr]
-> TCM (Term, Type)
inferSetOmega Expr
e QName
x IsFibrant
IsFibrant Suffix
s [NamedArg Expr]
args
    A.Def' QName
x Suffix
s | QName
x forall a. Eq a => a -> a -> Bool
== IsFibrant -> QName
nameOfSetOmega IsFibrant
IsStrict  -> Expr
-> QName
-> IsFibrant
-> Suffix
-> [NamedArg Expr]
-> TCM (Term, Type)
inferSetOmega Expr
e QName
x IsFibrant
IsStrict Suffix
s [NamedArg Expr]
args
    Expr
_ -> do
      (Elims -> Term
f, Type
t0) <- Expr -> TCM (Elims -> Term, Type)
inferHead Expr
hd
      let r :: Range
r = forall a. HasRange a => a -> Range
getRange Expr
hd
      Either
  (ArgsCheckState [NamedArg Expr]) (ArgsCheckState CheckedTarget)
res <- forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
runExceptT forall a b. (a -> b) -> a -> b
$ Comparison
-> ExpandHidden
-> Range
-> [NamedArg Expr]
-> Type
-> Maybe Type
-> ExceptT
     (ArgsCheckState [NamedArg Expr])
     (TCMT IO)
     (ArgsCheckState CheckedTarget)
checkArgumentsE Comparison
CmpEq ExpandHidden
exh (forall a. HasRange a => a -> Range
getRange Expr
hd) [NamedArg Expr]
args Type
t0 forall a. Maybe a
Nothing
      case Either
  (ArgsCheckState [NamedArg Expr]) (ArgsCheckState CheckedTarget)
res of
        Right st :: ArgsCheckState CheckedTarget
st@(ACState{acType :: forall a. ArgsCheckState a -> Type
acType = Type
t1}) -> forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (,Type
t1) forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). PureTCM m => Term -> m Term
unfoldInlined forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall a. (Elims -> Term) -> ArgsCheckState a -> TCM Term
checkHeadConstraints Elims -> Term
f ArgsCheckState CheckedTarget
st
        Left ArgsCheckState [NamedArg Expr]
problem -> do
          Type
t <- forall (m :: * -> *) a.
(MonadTCEnv m, HasOptions m, MonadDebug m) =>
m a -> m a
workOnTypes forall a b. (a -> b) -> a -> b
$ TCM Type
newTypeMeta_
          Term
v <- ArgsCheckState [NamedArg Expr]
-> Comparison
-> ExpandHidden
-> Range
-> [NamedArg Expr]
-> Type
-> (ArgsCheckState CheckedTarget -> TCM Term)
-> TCM Term
postponeArgs ArgsCheckState [NamedArg Expr]
problem Comparison
CmpEq ExpandHidden
exh Range
r [NamedArg Expr]
args Type
t forall a b. (a -> b) -> a -> b
$ \ ArgsCheckState CheckedTarget
st -> forall (m :: * -> *). PureTCM m => Term -> m Term
unfoldInlined forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall a. (Elims -> Term) -> ArgsCheckState a -> TCM Term
checkHeadConstraints Elims -> Term
f ArgsCheckState CheckedTarget
st
          forall (m :: * -> *) a. Monad m => a -> m a
return (Term
v, Type
t)

-----------------------------------------------------------------------------
-- * Heads
-----------------------------------------------------------------------------

inferHeadDef :: ProjOrigin -> QName -> TCM (Elims -> Term, Type)
inferHeadDef :: ProjOrigin -> QName -> TCM (Elims -> Term, Type)
inferHeadDef ProjOrigin
o QName
x = do
  -- Andreas, 2022-03-07, issue #5809: don't drop parameters of irrelevant projections.
  Maybe Projection
proj <- forall (m :: * -> *).
HasConstInfo m =>
QName -> m (Maybe Projection)
isRelevantProjection QName
x
  Relevance
rel  <- forall a. LensRelevance a => a -> Relevance
getRelevance forall b c a. (b -> c) -> (a -> b) -> a -> c
. Definition -> ArgInfo
defArgInfo forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
x
  let app :: Args -> Term
app =
        case Maybe Projection
proj of
          Maybe Projection
Nothing -> \ Args
args -> QName -> Elims -> Term
Def QName
x forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall a. Arg a -> Elim' a
Apply Args
args
          Just Projection
p  -> \ Args
args -> Projection -> ProjOrigin -> Relevance -> Args -> Term
projDropParsApply Projection
p ProjOrigin
o Relevance
rel Args
args
  forall a c b. (a -> c) -> (a, b) -> (c, b)
mapFst forall t. Apply t => t -> Elims -> t
applyE forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Args -> Term) -> QName -> TCM (Term, Type)
inferDef Args -> Term
app QName
x

-- | Infer the type of a head thing (variable, function symbol, or constructor).
--   We return a function that applies the head to arguments.
--   This is because in case of a constructor we want to drop the parameters.
inferHead :: A.Expr -> TCM (Elims -> Term, Type)
inferHead :: Expr -> TCM (Elims -> Term, Type)
inferHead Expr
e = do
  case Expr
e of
    A.Var Name
x -> do -- traceCall (InferVar x) $ do
      (Term
u, Dom Type
a) <- forall (m :: * -> *).
(MonadFail m, MonadTCEnv m) =>
Name -> m (Term, Dom Type)
getVarInfo Name
x
      forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.term.var" Nat
20 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
hsep
        [ TCMT IO Doc
"variable" , forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Name
x
        , TCMT IO Doc
"(" , forall (m :: * -> *). Applicative m => [Char] -> m Doc
text (forall a. Show a => a -> [Char]
show Term
u) , TCMT IO Doc
")"
        , TCMT IO Doc
"has type:" , forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Dom Type
a
        ]
      forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (forall a. LensRelevance a => a -> Bool
usableRelevance Dom Type
a) 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 -> TypeError
VariableIsIrrelevant Name
x
      -- Andreas, 2019-06-18, LAIM 2019, issue #3855:
      -- Conor McBride style quantity judgement:
      -- The available quantity for variable x must be below
      -- the required quantity to construct the term x.
      -- Note: this whole thing does not work for linearity, where we need some actual arithmetics.
      forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
unlessM ((forall a. LensQuantity a => a -> Quantity
getQuantity Dom Type
a Quantity -> Quantity -> Bool
`moreQuantity`) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
asksTC forall a. LensQuantity a => a -> Quantity
getQuantity) 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 -> TypeError
VariableIsErased Name
x

      forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (forall a. LensCohesion a => a -> Bool
usableCohesion Dom Type
a) 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 -> Cohesion -> TypeError
VariableIsOfUnusableCohesion Name
x (forall a. LensCohesion a => a -> Cohesion
getCohesion Dom Type
a)

      forall (m :: * -> *) a. Monad m => a -> m a
return (forall t. Apply t => t -> Elims -> t
applyE Term
u, forall t e. Dom' t e -> e
unDom Dom Type
a)

    A.Def QName
x  -> ProjOrigin -> QName -> TCM (Elims -> Term, Type)
inferHeadDef ProjOrigin
ProjPrefix QName
x
    A.Def'{} -> forall a. HasCallStack => a
__IMPOSSIBLE__ -- handled in checkHeadApplication and inferApplication

    A.Proj ProjOrigin
o AmbiguousQName
ambP | Just QName
d <- AmbiguousQName -> Maybe QName
getUnambiguous AmbiguousQName
ambP -> ProjOrigin -> QName -> TCM (Elims -> Term, Type)
inferHeadDef ProjOrigin
o QName
d
    A.Proj{} -> forall a. HasCallStack => a
__IMPOSSIBLE__ -- inferHead will only be called on unambiguous projections

    A.Con AmbiguousQName
ambC | Just QName
c <- AmbiguousQName -> Maybe QName
getUnambiguous AmbiguousQName
ambC -> do

      -- Constructors are polymorphic internally.
      -- So, when building the constructor term
      -- we should throw away arguments corresponding to parameters.

      -- First, inferDef will try to apply the constructor
      -- to the free parameters of the current context. We ignore that.
      ConHead
con <- forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> m (Either a b) -> m b
fromRightM (forall a. ([Char] -> a) -> a -> SigError -> a
sigError forall (m :: * -> *) a.
(HasCallStack, MonadDebug m) =>
[Char] -> m a
__IMPOSSIBLE_VERBOSE__ (forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError forall a b. (a -> b) -> a -> b
$ QName -> TypeError
AbstractConstructorNotInScope QName
c)) forall a b. (a -> b) -> a -> b
$
        QName -> TCM (Either SigError ConHead)
getOrigConHead QName
c
      (Term
u, Type
a) <- (Args -> Term) -> QName -> TCM (Term, Type)
inferDef (\ Args
_ -> ConHead -> ConInfo -> Elims -> Term
Con ConHead
con ConInfo
ConOCon []) QName
c

      -- Next get the number of parameters in the current context.
      Constructor{conPars :: Defn -> Nat
conPars = Nat
n} <- Definition -> Defn
theDef forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall (m :: * -> *).
(Functor m, HasConstInfo m, HasOptions m, ReadTCState m,
 MonadTCEnv m, MonadDebug m) =>
Definition -> m Definition
instantiateDef forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
c)

      forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> [Char] -> m ()
reportSLn [Char]
"tc.term.con" Nat
7 forall a b. (a -> b) -> a -> b
$ [[Char]] -> [Char]
unwords [forall a. Pretty a => a -> [Char]
prettyShow QName
c, [Char]
"has", forall a. Show a => a -> [Char]
show Nat
n, [Char]
"parameters."]

      -- So when applying the constructor throw away the parameters.
      forall (m :: * -> *) a. Monad m => a -> m a
return (forall t. Apply t => t -> Elims -> t
applyE Term
u forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Nat -> [a] -> [a]
drop Nat
n, Type
a)
    A.Con{} -> forall a. HasCallStack => a
__IMPOSSIBLE__  -- inferHead will only be called on unambiguous constructors
    A.QuestionMark MetaInfo
i InteractionId
ii -> (Comparison -> Type -> TCM (MetaId, Term))
-> MetaInfo -> TCM (Elims -> Term, Type)
inferMeta (InteractionId -> Comparison -> Type -> TCM (MetaId, Term)
newQuestionMark InteractionId
ii) MetaInfo
i
    A.Underscore MetaInfo
i   -> (Comparison -> Type -> TCM (MetaId, Term))
-> MetaInfo -> TCM (Elims -> Term, Type)
inferMeta (forall (m :: * -> *).
MonadMetaSolver m =>
RunMetaOccursCheck -> Comparison -> Type -> m (MetaId, Term)
newValueMeta RunMetaOccursCheck
RunMetaOccursCheck) MetaInfo
i
    Expr
e -> do
      (Term
term, Type
t) <- Expr -> TCM (Term, Type)
inferExpr Expr
e
      forall (m :: * -> *) a. Monad m => a -> m a
return (forall t. Apply t => t -> Elims -> t
applyE Term
term, Type
t)

inferDef :: (Args -> Term) -> QName -> TCM (Term, Type)
inferDef :: (Args -> Term) -> QName -> TCM (Term, Type)
inferDef Args -> Term
mkTerm QName
x =
  forall (m :: * -> *) a. MonadTrace m => Call -> m a -> m a
traceCall (QName -> Call
InferDef QName
x) forall a b. (a -> b) -> a -> b
$ do
    -- getConstInfo retrieves the *absolute* (closed) type of x
    -- instantiateDef relativizes it to the current context
    Definition
d0 <- forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
x
    Definition
d  <- forall (m :: * -> *).
(Functor m, HasConstInfo m, HasOptions m, ReadTCState m,
 MonadTCEnv m, MonadDebug m) =>
Definition -> m Definition
instantiateDef Definition
d0
    forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.term.def" Nat
10 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"inferDef" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
x
    forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.term.def" Nat
30 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"  absolute type:    " 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 forall a b. (a -> b) -> a -> b
$ Definition -> Type
defType Definition
d0)
    forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.term.def" Nat
30 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"  instantiated type:" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM (Definition -> Type
defType Definition
d)
    -- Irrelevant defs are only allowed in irrelevant position.
    -- Erased defs are only allowed in erased position (see #3855).
    QName -> Definition -> TCM ()
checkModality QName
x Definition
d
    case Definition -> Defn
theDef Definition
d of
      GeneralizableVar{} -> do
        -- Generalizable variables corresponds to metas created
        -- at the point where they should be generalized. Module parameters
        -- have already been applied to the meta, so we don't have to do that
        -- here.
        GeneralizedValue
val <- forall a. a -> Maybe a -> a
fromMaybe forall a. HasCallStack => a
__IMPOSSIBLE__ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *) a. MonadTCEnv m => Lens' a TCEnv -> m a
viewTC (Lens' (Map QName GeneralizedValue) TCEnv
eGeneralizedVars forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k v. Ord k => k -> Lens' (Maybe v) (Map k v)
key QName
x)
        Substitution' Term
sub <- forall (tcm :: * -> *).
MonadTCEnv tcm =>
CheckpointId -> tcm (Substitution' Term)
checkpointSubstitution (GeneralizedValue -> CheckpointId
genvalCheckpoint GeneralizedValue
val)
        let (Term
v, Type
t) = forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' Term
sub (GeneralizedValue -> Term
genvalTerm GeneralizedValue
val, GeneralizedValue -> Type
genvalType GeneralizedValue
val)
        Args -> Type -> Term -> TCM ()
debug [] Type
t Term
v
        forall (m :: * -> *) a. Monad m => a -> m a
return (Term
v, Type
t)
      Defn
_ -> do
        -- since x is considered living in the top-level, we have to
        -- apply it to the current context
        Args
vs <- forall (m :: * -> *).
(Functor m, HasConstInfo m, HasOptions m, ReadTCState m,
 MonadTCEnv m, MonadDebug m) =>
QName -> m Args
freeVarsToApply QName
x
        forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.term.def" Nat
30 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"  free vars:" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) (t :: * -> *).
(Applicative m, Semigroup (m Doc), Foldable t) =>
t (m Doc) -> m Doc
prettyList_ (forall a b. (a -> b) -> [a] -> [b]
map forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Args
vs)
        let t :: Type
t = Definition -> Type
defType Definition
d
            v :: Term
v = Args -> Term
mkTerm Args
vs -- applies x to vs, dropping parameters

        -- Andrea 2019-07-16, Check that the supplied arguments
        -- respect the cohesion modalities of the current context.
        -- Cohesion is purely based on left-division, so it does not
        -- rely on "position" like Relevance/Quantity.
        Args -> TCM ()
checkCohesionArgs Args
vs

        Args -> Type -> Term -> TCM ()
debug Args
vs Type
t Term
v
        forall (m :: * -> *) a. Monad m => a -> m a
return (Term
v, Type
t)
  where
    debug :: Args -> Type -> Term -> TCM ()
    debug :: Args -> Type -> Term -> TCM ()
debug Args
vs Type
t Term
v = do
      forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.term.def" Nat
60 forall a b. (a -> b) -> a -> b
$
        TCMT IO Doc
"freeVarsToApply to def " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
hsep (forall a b. (a -> b) -> [a] -> [b]
map (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) Args
vs)
      forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.term.def" Nat
10 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
        [ TCMT IO Doc
"inferred def " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
x forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
hsep (forall a b. (a -> b) -> [a] -> [b]
map forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Args
vs)
        , forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
nest Nat
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
t
        , forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
nest Nat
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 ]

checkCohesionArgs :: Args -> TCM ()
checkCohesionArgs :: Args -> TCM ()
checkCohesionArgs Args
vs = do
  let
    vmap :: VarMap
    vmap :: VarMap
vmap = forall a c t. (IsVarSet a c, Singleton Nat c, Free t) => t -> c
freeVars Args
vs

  -- we iterate over all vars in the context and their ArgInfo,
  -- checking for each that "vs" uses them as allowed.
  Args
as <- forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Args
getContextArgs
  forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ Args
as forall a b. (a -> b) -> a -> b
$ \ (Arg ArgInfo
avail Term
t) -> do
    let m :: Maybe Modality
m = do
          Nat
v <- forall a. DeBruijn a => a -> Maybe Nat
deBruijnView Term
t
          forall a. VarOcc' a -> Modality
varModality forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. Nat -> VarMap' a -> Maybe (VarOcc' a)
lookupVarMap Nat
v VarMap
vmap
    forall (m :: * -> *) a. Monad m => Maybe a -> (a -> m ()) -> m ()
whenJust Maybe Modality
m forall a b. (a -> b) -> a -> b
$ \ Modality
used -> do
        forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (forall a. LensCohesion a => a -> Cohesion
getCohesion ArgInfo
avail Cohesion -> Cohesion -> Bool
`moreCohesion` forall a. LensCohesion a => a -> Cohesion
getCohesion Modality
used) 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
=<<) 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
$
                [TCMT IO Doc
"Variable" , forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
t]
             forall a. [a] -> [a] -> [a]
++ forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"is used as" forall a. [a] -> [a] -> [a]
++ [forall (m :: * -> *). Applicative m => [Char] -> m Doc
text forall a b. (a -> b) -> a -> b
$ forall a. Show a => a -> [Char]
show forall a b. (a -> b) -> a -> b
$ forall a. LensCohesion a => a -> Cohesion
getCohesion Modality
used]
             forall a. [a] -> [a] -> [a]
++ forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"but only available as" forall a. [a] -> [a] -> [a]
++ [forall (m :: * -> *). Applicative m => [Char] -> m Doc
text forall a b. (a -> b) -> a -> b
$ forall a. Show a => a -> [Char]
show forall a b. (a -> b) -> a -> b
$ forall a. LensCohesion a => a -> Cohesion
getCohesion ArgInfo
avail]

-- | The second argument is the definition of the first.
--   Returns 'Nothing' if ok, otherwise the error message.
checkRelevance' :: QName -> Definition -> TCM (Maybe TypeError)
checkRelevance' :: QName -> Definition -> TCM (Maybe TypeError)
checkRelevance' QName
x Definition
def = do
  case forall a. LensRelevance a => a -> Relevance
getRelevance Definition
def of
    Relevance
Relevant -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing -- relevance functions can be used in any context.
    Relevance
drel -> do
      -- Andreas,, 2018-06-09, issue #2170
      -- irrelevant projections are only allowed if --irrelevant-projections
      forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM (forall (m :: * -> *) a. Monad m => a -> m a
return (forall a. Maybe a -> Bool
isJust forall a b. (a -> b) -> a -> b
$ Defn -> Maybe Projection
isProjection_ forall a b. (a -> b) -> a -> b
$ Definition -> Defn
theDef Definition
def) forall (m :: * -> *). Monad m => m Bool -> m Bool -> m Bool
`and2M`
           (Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
.PragmaOptions -> Bool
optIrrelevantProjections forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasOptions m => m PragmaOptions
pragmaOptions)) {-then-} TCM (Maybe TypeError)
needIrrProj {-else-} forall a b. (a -> b) -> a -> b
$ do
        Relevance
rel <- forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
asksTC forall a. LensRelevance a => a -> Relevance
getRelevance
        forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.irr" Nat
50 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
          [ TCMT IO Doc
"declaration relevance =" 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 Relevance
drel)
          , TCMT IO Doc
"context     relevance =" 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 Relevance
rel)
          ]
        forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ if (Relevance
drel Relevance -> Relevance -> Bool
`moreRelevant` Relevance
rel) then forall a. Maybe a
Nothing else forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ QName -> TypeError
DefinitionIsIrrelevant QName
x
  where
  needIrrProj :: TCM (Maybe TypeError)
needIrrProj = forall a. a -> Maybe a
Just forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> TypeError
GenericDocError forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do
    forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep [ TCMT IO Doc
"Projection " , forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
x, TCMT IO Doc
" is irrelevant."
        , TCMT IO Doc
" Turn on option --irrelevant-projections to use it (unsafe)."
        ]

-- | The second argument is the definition of the first.
--   Returns 'Nothing' if ok, otherwise the error message.
checkQuantity' :: QName -> Definition -> TCM (Maybe TypeError)
checkQuantity' :: QName -> Definition -> TCM (Maybe TypeError)
checkQuantity' QName
x Definition
def = do
  case forall a. LensQuantity a => a -> Quantity
getQuantity Definition
def of
    dq :: Quantity
dq@Quantityω{} -> do
      forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.irr" Nat
50 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
        [ TCMT IO Doc
"declaration quantity =" 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 Quantity
dq)
        -- , "context     quantity =" <+> text (show q)
        ]
      forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing -- Abundant definitions can be used in any context.
    Quantity
dq -> do
      Quantity
q <- forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
asksTC forall a. LensQuantity a => a -> Quantity
getQuantity
      forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.irr" Nat
50 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
        [ TCMT IO Doc
"declaration quantity =" 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 Quantity
dq)
        , TCMT IO Doc
"context     quantity =" 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 Quantity
q)
        ]
      forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ if (Quantity
dq Quantity -> Quantity -> Bool
`moreQuantity` Quantity
q) then forall a. Maybe a
Nothing else forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ QName -> TypeError
DefinitionIsErased QName
x

-- | The second argument is the definition of the first.
checkModality' :: QName -> Definition -> TCM (Maybe TypeError)
checkModality' :: QName -> Definition -> TCM (Maybe TypeError)
checkModality' QName
x Definition
def = do
  QName -> Definition -> TCM (Maybe TypeError)
checkRelevance' QName
x Definition
def forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
    Maybe TypeError
Nothing    -> QName -> Definition -> TCM (Maybe TypeError)
checkQuantity' QName
x Definition
def
    err :: Maybe TypeError
err@Just{} -> forall (m :: * -> *) a. Monad m => a -> m a
return Maybe TypeError
err

-- | The second argument is the definition of the first.
checkModality :: QName -> Definition -> TCM ()
checkModality :: QName -> Definition -> TCM ()
checkModality QName
x Definition
def = forall {m :: * -> *}.
(MonadTCEnv m, ReadTCState m, MonadError TCErr m) =>
m (Maybe TypeError) -> m ()
justToError forall a b. (a -> b) -> a -> b
$ QName -> Definition -> TCM (Maybe TypeError)
checkModality' QName
x Definition
def
  where
  justToError :: m (Maybe TypeError) -> m ()
justToError m (Maybe TypeError)
m = forall b a. b -> (a -> b) -> Maybe a -> b
maybe (forall (m :: * -> *) a. Monad m => a -> m a
return ()) forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< m (Maybe TypeError)
m

-- | @checkHeadApplication e t hd args@ checks that @e@ has type @t@,
-- assuming that @e@ has the form @hd args@. The corresponding
-- type-checked term is returned.
--
-- If the head term @hd@ is a coinductive constructor, then a
-- top-level definition @fresh tel = hd args@ (where the clause is
-- delayed) is added, where @tel@ corresponds to the current
-- telescope. The returned term is @fresh tel@.
--
-- Precondition: The head @hd@ has to be unambiguous, and there should
-- not be any need to insert hidden lambdas.
checkHeadApplication :: Comparison -> A.Expr -> Type -> A.Expr -> [NamedArg A.Expr] -> TCM Term
checkHeadApplication :: Comparison -> Expr -> Type -> Expr -> [NamedArg Expr] -> TCM Term
checkHeadApplication Comparison
cmp Expr
e Type
t Expr
hd [NamedArg Expr]
args = do
  SortKit{QName
IsFibrant -> QName
nameOfSetOmega :: IsFibrant -> QName
nameOfSSet :: QName
nameOfProp :: QName
nameOfSet :: QName
nameOfSetOmega :: SortKit -> IsFibrant -> QName
nameOfSSet :: SortKit -> QName
nameOfProp :: SortKit -> QName
nameOfSet :: SortKit -> QName
..} <- forall (m :: * -> *).
(HasBuiltins m, MonadTCError m, HasOptions m) =>
m SortKit
sortKit
  Maybe QName
sharp <- forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap CoinductionKit -> QName
nameOfSharp forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCM (Maybe CoinductionKit)
coinductionKit
  Maybe QName
conId  <- forall (m :: * -> *). HasBuiltins m => [Char] -> m (Maybe QName)
getNameOfConstrained [Char]
builtinConId
  Maybe QName
pOr    <- forall (m :: * -> *). HasBuiltins m => [Char] -> m (Maybe QName)
getNameOfConstrained [Char]
builtinPOr
  Maybe QName
pComp  <- forall (m :: * -> *). HasBuiltins m => [Char] -> m (Maybe QName)
getNameOfConstrained [Char]
builtinComp
  Maybe QName
pHComp <- forall (m :: * -> *). HasBuiltins m => [Char] -> m (Maybe QName)
getNameOfConstrained [Char]
builtinHComp
  Maybe QName
pTrans <- forall (m :: * -> *). HasBuiltins m => [Char] -> m (Maybe QName)
getNameOfConstrained [Char]
builtinTrans
  Maybe QName
mglue  <- forall (m :: * -> *). HasBuiltins m => [Char] -> m (Maybe QName)
getNameOfConstrained [Char]
builtin_glue
  Maybe QName
mglueU  <- forall (m :: * -> *). HasBuiltins m => [Char] -> m (Maybe QName)
getNameOfConstrained [Char]
builtin_glueU
  case Expr
hd of
    A.Def' QName
c Suffix
s | QName
c forall a. Eq a => a -> a -> Bool
== QName
nameOfSet      -> Comparison
-> Expr -> Type -> QName -> Suffix -> [NamedArg Expr] -> TCM Term
checkSet Comparison
cmp Expr
e Type
t QName
c Suffix
s [NamedArg Expr]
args
    A.Def' QName
c Suffix
s | QName
c forall a. Eq a => a -> a -> Bool
== QName
nameOfProp     -> Comparison
-> Expr -> Type -> QName -> Suffix -> [NamedArg Expr] -> TCM Term
checkProp Comparison
cmp Expr
e Type
t QName
c Suffix
s [NamedArg Expr]
args
    A.Def' QName
c Suffix
s | QName
c forall a. Eq a => a -> a -> Bool
== QName
nameOfSSet     -> Comparison
-> Expr -> Type -> QName -> Suffix -> [NamedArg Expr] -> TCM Term
checkSSet Comparison
cmp Expr
e Type
t QName
c Suffix
s [NamedArg Expr]
args
    A.Def' QName
c Suffix
s | QName
c forall a. Eq a => a -> a -> Bool
== IsFibrant -> QName
nameOfSetOmega IsFibrant
IsFibrant -> Comparison
-> Expr
-> Type
-> QName
-> IsFibrant
-> Suffix
-> [NamedArg Expr]
-> TCM Term
checkSetOmega Comparison
cmp Expr
e Type
t QName
c IsFibrant
IsFibrant Suffix
s [NamedArg Expr]
args
    A.Def' QName
c Suffix
s | QName
c forall a. Eq a => a -> a -> Bool
== IsFibrant -> QName
nameOfSetOmega IsFibrant
IsStrict  -> Comparison
-> Expr
-> Type
-> QName
-> IsFibrant
-> Suffix
-> [NamedArg Expr]
-> TCM Term
checkSetOmega Comparison
cmp Expr
e Type
t QName
c IsFibrant
IsStrict Suffix
s [NamedArg Expr]
args

    -- Type checking #. The # that the user can write will be a Def, but the
    -- sharp we generate in the body of the wrapper is a Con.
    A.Def QName
c | forall a. a -> Maybe a
Just QName
c forall a. Eq a => a -> a -> Bool
== Maybe QName
sharp -> Expr -> Type -> QName -> [NamedArg Expr] -> TCM Term
checkSharpApplication Expr
e Type
t QName
c [NamedArg Expr]
args

    -- Cubical primitives
    A.Def QName
c | forall a. a -> Maybe a
Just QName
c forall a. Eq a => a -> a -> Bool
== Maybe QName
pComp -> Maybe (MaybeRanges -> Args -> Type -> TCM Args) -> TCM Term
defaultResult' forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ QName -> MaybeRanges -> Args -> Type -> TCM Args
checkPrimComp QName
c
    A.Def QName
c | forall a. a -> Maybe a
Just QName
c forall a. Eq a => a -> a -> Bool
== Maybe QName
pHComp -> Maybe (MaybeRanges -> Args -> Type -> TCM Args) -> TCM Term
defaultResult' forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ QName -> MaybeRanges -> Args -> Type -> TCM Args
checkPrimHComp QName
c
    A.Def QName
c | forall a. a -> Maybe a
Just QName
c forall a. Eq a => a -> a -> Bool
== Maybe QName
pTrans -> Maybe (MaybeRanges -> Args -> Type -> TCM Args) -> TCM Term
defaultResult' forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ QName -> MaybeRanges -> Args -> Type -> TCM Args
checkPrimTrans QName
c
    A.Def QName
c | forall a. a -> Maybe a
Just QName
c forall a. Eq a => a -> a -> Bool
== Maybe QName
conId -> Maybe (MaybeRanges -> Args -> Type -> TCM Args) -> TCM Term
defaultResult' forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ QName -> MaybeRanges -> Args -> Type -> TCM Args
checkConId QName
c
    A.Def QName
c | forall a. a -> Maybe a
Just QName
c forall a. Eq a => a -> a -> Bool
== Maybe QName
pOr   -> Maybe (MaybeRanges -> Args -> Type -> TCM Args) -> TCM Term
defaultResult' forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ QName -> MaybeRanges -> Args -> Type -> TCM Args
checkPOr QName
c
    A.Def QName
c | forall a. a -> Maybe a
Just QName
c forall a. Eq a => a -> a -> Bool
== Maybe QName
mglue -> Maybe (MaybeRanges -> Args -> Type -> TCM Args) -> TCM Term
defaultResult' forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ QName -> MaybeRanges -> Args -> Type -> TCM Args
check_glue QName
c
    A.Def QName
c | forall a. a -> Maybe a
Just QName
c forall a. Eq a => a -> a -> Bool
== Maybe QName
mglueU -> Maybe (MaybeRanges -> Args -> Type -> TCM Args) -> TCM Term
defaultResult' forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ QName -> MaybeRanges -> Args -> Type -> TCM Args
check_glueU QName
c

    Expr
_ -> TCM Term
defaultResult
  where
  defaultResult :: TCM Term
  defaultResult :: TCM Term
defaultResult = Maybe (MaybeRanges -> Args -> Type -> TCM Args) -> TCM Term
defaultResult' forall a. Maybe a
Nothing
  defaultResult' :: Maybe (MaybeRanges -> Args -> Type -> TCM Args) -> TCM Term
  defaultResult' :: Maybe (MaybeRanges -> Args -> Type -> TCM Args) -> TCM Term
defaultResult' Maybe (MaybeRanges -> Args -> Type -> TCM Args)
mk = do
    (Elims -> Term
f, Type
t0) <- Expr -> TCM (Elims -> Term, Type)
inferHead Expr
hd
    ExpandHidden
expandLast <- forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
asksTC TCEnv -> ExpandHidden
envExpandLast
    Comparison
-> ExpandHidden
-> Range
-> [NamedArg Expr]
-> Type
-> Type
-> (ArgsCheckState CheckedTarget -> TCM Term)
-> TCM Term
checkArguments Comparison
cmp ExpandHidden
expandLast (forall a. HasRange a => a -> Range
getRange Expr
hd) [NamedArg Expr]
args Type
t0 Type
t forall a b. (a -> b) -> a -> b
$ \ st :: ArgsCheckState CheckedTarget
st@(ACState MaybeRanges
rs Elims
vs [Maybe (Abs Constraint)]
_ Type
t1 CheckedTarget
checkedTarget) -> do
      let check :: Maybe (TCM Args)
check = do
           MaybeRanges -> Args -> Type -> TCM Args
k <- Maybe (MaybeRanges -> Args -> Type -> TCM Args)
mk
           Args
as <- forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims Elims
vs
           forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ MaybeRanges -> Args -> Type -> TCM Args
k MaybeRanges
rs Args
as Type
t1
      Elims
vs <- case Maybe (TCM Args)
check of
              Just TCM Args
ck -> do
                forall a b. (a -> b) -> [a] -> [b]
map forall a. Arg a -> Elim' a
Apply forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCM Args
ck
              Maybe (TCM Args)
Nothing -> do
                forall (m :: * -> *) a. Monad m => a -> m a
return Elims
vs
      Term
v <- forall (m :: * -> *). PureTCM m => Term -> m Term
unfoldInlined forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall a. (Elims -> Term) -> ArgsCheckState a -> TCM Term
checkHeadConstraints Elims -> Term
f (ArgsCheckState CheckedTarget
st { acElims :: Elims
acElims = Elims
vs })
      Comparison -> CheckedTarget -> Term -> Type -> Type -> TCM Term
coerce' Comparison
cmp CheckedTarget
checkedTarget Term
v Type
t1 Type
t

-- Issue #3019 and #4170: Don't insert trailing implicits when checking arguments to existing
-- metavariables.
turnOffExpandLastIfExistingMeta :: A.Expr -> TCM a -> TCM a
turnOffExpandLastIfExistingMeta :: forall a. Expr -> TCM a -> TCM a
turnOffExpandLastIfExistingMeta Expr
hd
  | Bool
isExistingMeta = forall a. TCM a -> TCM a
reallyDontExpandLast
  | Bool
otherwise      = forall a. a -> a
id
  where
    isExistingMeta :: Bool
isExistingMeta = forall a. Maybe a -> Bool
isJust forall a b. (a -> b) -> a -> b
$ MetaInfo -> Maybe MetaId
A.metaNumber forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Expr -> Maybe MetaInfo
metaInfo Expr
hd
    metaInfo :: Expr -> Maybe MetaInfo
metaInfo (A.QuestionMark MetaInfo
i InteractionId
_) = forall a. a -> Maybe a
Just MetaInfo
i
    metaInfo (A.Underscore MetaInfo
i)     = forall a. a -> Maybe a
Just MetaInfo
i
    metaInfo (A.ScopedExpr ScopeInfo
_ Expr
e)   = Expr -> Maybe MetaInfo
metaInfo Expr
e
    metaInfo Expr
_                    = forall a. Maybe a
Nothing

-----------------------------------------------------------------------------
-- * Spines
-----------------------------------------------------------------------------

traceCallE :: Call -> ExceptT e TCM r -> ExceptT e TCM r
traceCallE :: forall e r. Call -> ExceptT e (TCMT IO) r -> ExceptT e (TCMT IO) r
traceCallE Call
call ExceptT e (TCMT IO) r
m = do
  Either e r
z <- forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. MonadTrace m => Call -> m a -> m a
traceCall Call
call forall a b. (a -> b) -> a -> b
$ forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
runExceptT ExceptT e (TCMT IO) r
m
  case Either e r
z of
    Right r
e  -> forall (m :: * -> *) a. Monad m => a -> m a
return r
e
    Left e
err -> forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError e
err

-- | If we've already checked the target type we don't have to call coerce.
coerce' :: Comparison -> CheckedTarget -> Term -> Type -> Type -> TCM Term
coerce' :: Comparison -> CheckedTarget -> Term -> Type -> Type -> TCM Term
coerce' Comparison
cmp CheckedTarget
NotCheckedTarget           Term
v Type
inferred Type
expected = forall (m :: * -> *).
(MonadConversion m, MonadTCM m) =>
Comparison -> Term -> Type -> Type -> m Term
coerce Comparison
cmp Term
v Type
inferred Type
expected
coerce' Comparison
cmp (CheckedTarget Maybe ProblemId
Nothing)    Term
v Type
_        Type
_        = forall (m :: * -> *) a. Monad m => a -> m a
return Term
v
coerce' Comparison
cmp (CheckedTarget (Just ProblemId
pid)) Term
v Type
_        Type
expected = forall (m :: * -> *).
(MonadMetaSolver m, MonadFresh Nat m) =>
Type -> Term -> ProblemId -> m Term
blockTermOnProblem Type
expected Term
v ProblemId
pid

-- | Check a list of arguments: @checkArgs args t0 t1@ checks that
--   @t0 = Delta -> t0'@ and @args : Delta@. Inserts hidden arguments to
--   make this happen.  Returns the evaluated arguments @vs@, the remaining
--   type @t0'@ (which should be a subtype of @t1@) and any constraints @cs@
--   that have to be solved for everything to be well-formed.

checkArgumentsE :: Comparison -> ExpandHidden -> Range -> [NamedArg A.Expr] -> Type -> Maybe Type ->
                   ExceptT (ArgsCheckState [NamedArg A.Expr]) TCM (ArgsCheckState CheckedTarget)
checkArgumentsE :: Comparison
-> ExpandHidden
-> Range
-> [NamedArg Expr]
-> Type
-> Maybe Type
-> ExceptT
     (ArgsCheckState [NamedArg Expr])
     (TCMT IO)
     (ArgsCheckState CheckedTarget)
checkArgumentsE Comparison
sComp ExpandHidden
sExpand Range
sRange [NamedArg Expr]
sArgs Type
sFun Maybe Type
sApp = do
  Type -> PathView
sPathView <- forall (m :: * -> *). HasBuiltins m => m (Type -> PathView)
pathView'
  CheckArgumentsE'State
-> ExceptT
     (ArgsCheckState [NamedArg Expr])
     (TCMT IO)
     (ArgsCheckState CheckedTarget)
checkArgumentsE'
    S{ sChecked :: CheckedTarget
sChecked       = CheckedTarget
NotCheckedTarget
     , sArgs :: [(NamedArg Expr, Bool)]
sArgs          = forall a b. [a] -> [b] -> [(a, b)]
zip [NamedArg Expr]
sArgs forall a b. (a -> b) -> a -> b
$
                        forall a. (a -> Bool) -> [a] -> [Bool]
List.suffixesSatisfying forall a. LensHiding a => a -> Bool
visible [NamedArg Expr]
sArgs
     , sArgsLen :: Nat
sArgsLen       = forall (t :: * -> *) a. Foldable t => t a -> Nat
length [NamedArg Expr]
sArgs
     , sSizeLtChecked :: Bool
sSizeLtChecked = Bool
False
     , sSkipCheck :: SkipCheck
sSkipCheck     = SkipCheck
DontSkip
     , Maybe Type
Range
Comparison
Type
ExpandHidden
Type -> PathView
sPathView :: Type -> PathView
sApp :: Maybe Type
sFun :: Type
sRange :: Range
sExpand :: ExpandHidden
sComp :: Comparison
sPathView :: Type -> PathView
sApp :: Maybe Type
sFun :: Type
sRange :: Range
sExpand :: ExpandHidden
sComp :: Comparison
..
     }

-- | State used by 'checkArgumentsE''.

data CheckArgumentsE'State = S
  { CheckArgumentsE'State -> CheckedTarget
sChecked :: CheckedTarget
    -- ^ Have we already checked the target?
  , CheckArgumentsE'State -> Comparison
sComp :: Comparison
    -- ^ Comparison to use if checking the target type.
  , CheckArgumentsE'State -> ExpandHidden
sExpand :: ExpandHidden
    -- ^ Insert trailing hidden arguments?
  , CheckArgumentsE'State -> Range
sRange :: Range
    -- ^ Range of the function.
  , CheckArgumentsE'State -> [(NamedArg Expr, Bool)]
sArgs :: [(NamedArg A.Expr, Bool)]
    -- ^ Arguments, along with information about whether a given
    -- argument and all remaining arguments are 'visible'.
  , CheckArgumentsE'State -> Nat
sArgsLen :: !Nat
    -- ^ The length of 'sArgs'.
  , CheckArgumentsE'State -> Type
sFun :: Type
    -- ^ The function's type.
  , CheckArgumentsE'State -> Maybe Type
sApp :: Maybe Type
    -- ^ The type of the application.
  , CheckArgumentsE'State -> Bool
sSizeLtChecked :: !Bool
    -- ^ Have we checked if 'sApp' is 'BoundedLt'?
  , CheckArgumentsE'State -> SkipCheck
sSkipCheck :: !SkipCheck
    -- ^ Should the target type check be skipped?
  , CheckArgumentsE'State -> Type -> PathView
sPathView :: Type -> PathView
    -- ^ The function returned by 'pathView''.
  }

-- | Should the target type check in 'checkArgumentsE'' be skipped?

data SkipCheck
  = Skip
  | SkipNext !Nat
    -- ^ Skip the given number of checks.
  | DontSkip

checkArgumentsE'
  :: CheckArgumentsE'State
  -> ExceptT (ArgsCheckState [NamedArg A.Expr]) TCM (ArgsCheckState CheckedTarget)

-- Case: no arguments, do not insert trailing hidden arguments: We are done.
checkArgumentsE' :: CheckArgumentsE'State
-> ExceptT
     (ArgsCheckState [NamedArg Expr])
     (TCMT IO)
     (ArgsCheckState CheckedTarget)
checkArgumentsE' S{ sArgs :: CheckArgumentsE'State -> [(NamedArg Expr, Bool)]
sArgs = [], Bool
Nat
Maybe Type
Range
Comparison
Type
ExpandHidden
CheckedTarget
SkipCheck
Type -> PathView
sPathView :: Type -> PathView
sSkipCheck :: SkipCheck
sSizeLtChecked :: Bool
sApp :: Maybe Type
sFun :: Type
sArgsLen :: Nat
sRange :: Range
sExpand :: ExpandHidden
sComp :: Comparison
sChecked :: CheckedTarget
sPathView :: CheckArgumentsE'State -> Type -> PathView
sApp :: CheckArgumentsE'State -> Maybe Type
sFun :: CheckArgumentsE'State -> Type
sRange :: CheckArgumentsE'State -> Range
sExpand :: CheckArgumentsE'State -> ExpandHidden
sComp :: CheckArgumentsE'State -> Comparison
sSkipCheck :: CheckArgumentsE'State -> SkipCheck
sSizeLtChecked :: CheckArgumentsE'State -> Bool
sArgsLen :: CheckArgumentsE'State -> Nat
sChecked :: CheckArgumentsE'State -> CheckedTarget
.. }
  | ExpandHidden -> Bool
isDontExpandLast ExpandHidden
sExpand =
    forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ ACState
      { acRanges :: MaybeRanges
acRanges      = []
      , acElims :: Elims
acElims       = []
      , acConstraints :: [Maybe (Abs Constraint)]
acConstraints = []
      , acType :: Type
acType        = Type
sFun
      , acData :: CheckedTarget
acData        = CheckedTarget
sChecked
      }

-- Case: no arguments, but need to insert trailing hiddens.
checkArgumentsE' S{ sArgs :: CheckArgumentsE'State -> [(NamedArg Expr, Bool)]
sArgs = [], Bool
Nat
Maybe Type
Range
Comparison
Type
ExpandHidden
CheckedTarget
SkipCheck
Type -> PathView
sPathView :: Type -> PathView
sSkipCheck :: SkipCheck
sSizeLtChecked :: Bool
sApp :: Maybe Type
sFun :: Type
sArgsLen :: Nat
sRange :: Range
sExpand :: ExpandHidden
sComp :: Comparison
sChecked :: CheckedTarget
sPathView :: CheckArgumentsE'State -> Type -> PathView
sApp :: CheckArgumentsE'State -> Maybe Type
sFun :: CheckArgumentsE'State -> Type
sRange :: CheckArgumentsE'State -> Range
sExpand :: CheckArgumentsE'State -> ExpandHidden
sComp :: CheckArgumentsE'State -> Comparison
sSkipCheck :: CheckArgumentsE'State -> SkipCheck
sSizeLtChecked :: CheckArgumentsE'State -> Bool
sArgsLen :: CheckArgumentsE'State -> Nat
sChecked :: CheckArgumentsE'State -> CheckedTarget
.. } =
  forall e r. Call -> ExceptT e (TCMT IO) r -> ExceptT e (TCMT IO) r
traceCallE (Range -> [NamedArg Expr] -> Type -> Maybe Type -> Call
CheckArguments Range
sRange [] Type
sFun Maybe Type
sApp) forall a b. (a -> b) -> a -> b
$ forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ do
    Maybe Term
sApp    <- forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (forall t a. Type'' t a -> a
unEl forall (m :: * -> *) b c a.
Functor m =>
(b -> c) -> (a -> m b) -> a -> m c
<.> forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce) Maybe Type
sApp
    (Args
us, Type
t) <- forall (m :: * -> *).
(PureTCM m, MonadMetaSolver m, MonadTCM m) =>
Nat -> (Hiding -> Bool) -> Type -> m (Args, Type)
implicitArgs (-Nat
1) (Maybe Term -> Hiding -> Bool
expand Maybe Term
sApp) Type
sFun
    forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ ACState
      { acRanges :: MaybeRanges
acRanges      = forall a. Nat -> a -> [a]
replicate (forall (t :: * -> *) a. Foldable t => t a -> Nat
length Args
us) forall a. Maybe a
Nothing
      , acElims :: Elims
acElims       = forall a b. (a -> b) -> [a] -> [b]
map forall a. Arg a -> Elim' a
Apply Args
us
      , acConstraints :: [Maybe (Abs Constraint)]
acConstraints = forall a. Nat -> a -> [a]
replicate (forall (t :: * -> *) a. Foldable t => t a -> Nat
length Args
us) forall a. Maybe a
Nothing
      , acType :: Type
acType        = Type
t
      , acData :: CheckedTarget
acData        = CheckedTarget
sChecked
      }
  where
  expand :: Maybe Term -> Hiding -> Bool
expand (Just (Pi Dom Type
dom Abs Type
_)) Hiding
Hidden     = Bool -> Bool
not (forall a. LensHiding a => a -> Bool
hidden Dom Type
dom)
  expand Maybe Term
_                 Hiding
Hidden     = Bool
True
  expand (Just (Pi Dom Type
dom Abs Type
_)) Instance{} = Bool -> Bool
not (forall a. LensHiding a => a -> Bool
isInstance Dom Type
dom)
  expand Maybe Term
_                 Instance{} = Bool
True
  expand Maybe Term
_                 Hiding
NotHidden  = Bool
False

-- Case: argument given.
checkArgumentsE'
  s :: CheckArgumentsE'State
s@S{ sArgs :: CheckArgumentsE'State -> [(NamedArg Expr, Bool)]
sArgs = sArgs :: [(NamedArg Expr, Bool)]
sArgs@((arg :: NamedArg Expr
arg@(Arg ArgInfo
info Named_ Expr
e), Bool
sArgsVisible) : [(NamedArg Expr, Bool)]
args), Bool
Nat
Maybe Type
Range
Comparison
Type
ExpandHidden
CheckedTarget
SkipCheck
Type -> PathView
sPathView :: Type -> PathView
sSkipCheck :: SkipCheck
sSizeLtChecked :: Bool
sApp :: Maybe Type
sFun :: Type
sArgsLen :: Nat
sRange :: Range
sExpand :: ExpandHidden
sComp :: Comparison
sChecked :: CheckedTarget
sPathView :: CheckArgumentsE'State -> Type -> PathView
sApp :: CheckArgumentsE'State -> Maybe Type
sFun :: CheckArgumentsE'State -> Type
sRange :: CheckArgumentsE'State -> Range
sExpand :: CheckArgumentsE'State -> ExpandHidden
sComp :: CheckArgumentsE'State -> Comparison
sSkipCheck :: CheckArgumentsE'State -> SkipCheck
sSizeLtChecked :: CheckArgumentsE'State -> Bool
sArgsLen :: CheckArgumentsE'State -> Nat
sChecked :: CheckArgumentsE'State -> CheckedTarget
.. } =

    forall e r. Call -> ExceptT e (TCMT IO) r -> ExceptT e (TCMT IO) r
traceCallE (Range -> [NamedArg Expr] -> Type -> Maybe Type -> Call
CheckArguments Range
sRange (forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst [(NamedArg Expr, Bool)]
sArgs) Type
sFun Maybe Type
sApp) forall a b. (a -> b) -> a -> b
$ do
      forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.term.args" Nat
30 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep
        [ TCMT IO Doc
"checkArgumentsE"
--        , "  sArgs =" <+> prettyA sArgs
        , forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
nest Nat
2 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
          [ TCMT IO Doc
"e     =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA Named_ Expr
e
          , TCMT IO Doc
"sFun  =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
sFun
          , TCMT IO Doc
"sApp  =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall b a. b -> (a -> b) -> Maybe a -> b
maybe TCMT IO Doc
"Nothing" forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Maybe Type
sApp
          ]
        ]
      -- First, insert implicit arguments, depending on current argument @arg@.
      let hx :: Hiding
hx = forall a. LensHiding a => a -> Hiding
getHiding ArgInfo
info  -- hiding of current argument
          mx :: Maybe ArgName
          mx :: Maybe [Char]
mx = forall a. (LensNamed a, NameOf a ~ NamedName) => a -> Maybe [Char]
bareNameOf Named_ Expr
e    -- name of current argument
          -- do not insert visible arguments
          expand :: Hiding -> [Char] -> Bool
expand Hiding
NotHidden [Char]
y = Bool
False
          -- insert a hidden argument if arg is not hidden or has different name
          -- insert an instance argument if arg is not instance  or has different name
          expand Hiding
hy        [Char]
y = Bool -> Bool
not (forall a b. (LensHiding a, LensHiding b) => a -> b -> Bool
sameHiding Hiding
hy Hiding
hx) Bool -> Bool -> Bool
|| forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
False ([Char]
y forall a. Eq a => a -> a -> Bool
/=) Maybe [Char]
mx
      forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.term.args" Nat
30 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
        [ TCMT IO Doc
"calling implicitNamedArgs"
        , forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
nest Nat
2 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"sFun = " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
sFun
        , forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
nest Nat
2 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"hx   = " 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 Hiding
hx)
        , forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
nest Nat
2 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"mx   = " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall b a. b -> (a -> b) -> Maybe a -> b
maybe TCMT IO Doc
"nothing" forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Maybe [Char]
mx
        ]
      (NamedArgs
nargs, Type
sFun) <- forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
(PureTCM m, MonadMetaSolver m, MonadTCM m) =>
Nat -> (Hiding -> [Char] -> Bool) -> Type -> m (NamedArgs, Type)
implicitNamedArgs (-Nat
1) Hiding -> [Char] -> Bool
expand Type
sFun
      -- Separate names from args.
      let ([Maybe NamedName]
mxs, Elims
us) = forall a b. [(a, b)] -> ([a], [b])
unzip forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (\ (Arg ArgInfo
ai (Named Maybe NamedName
mx Term
u)) -> (Maybe NamedName
mx, forall a. Arg a -> Elim' a
Apply forall a b. (a -> b) -> a -> b
$ forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
ai Term
u)) NamedArgs
nargs
          xs :: [NamedName]
xs        = forall a. [Maybe a] -> [a]
catMaybes [Maybe NamedName]
mxs

      -- We need a function type here, but we don't know which kind
      -- (implicit/explicit). But it might be possible to use injectivity to
      -- force a pi.
      Type
sFun <- forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ Type -> TCM Type
forcePiUsingInjectivity Type
sFun

      -- We are done inserting implicit args.  Now, try to check @arg@.
      forall t (m :: * -> *) a.
(Reduce t, IsMeta t, MonadReduce m) =>
t -> (Blocker -> t -> m a) -> (NotBlocked -> t -> m a) -> m a
ifBlocked Type
sFun
        (\Blocker
_ Type
sFun -> forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError forall a b. (a -> b) -> a -> b
$ ACState
            { acRanges :: MaybeRanges
acRanges      = forall a. Nat -> a -> [a]
replicate (forall (t :: * -> *) a. Foldable t => t a -> Nat
length Elims
us) forall a. Maybe a
Nothing
            , acElims :: Elims
acElims       = Elims
us
            , acConstraints :: [Maybe (Abs Constraint)]
acConstraints = forall a. Nat -> a -> [a]
replicate (forall (t :: * -> *) a. Foldable t => t a -> Nat
length Elims
us) forall a. Maybe a
Nothing
            , acType :: Type
acType        = Type
sFun
            , acData :: [NamedArg Expr]
acData        = forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst [(NamedArg Expr, Bool)]
sArgs
            }) forall a b. (a -> b) -> a -> b
$ \NotBlocked
_ Type
sFun -> do

        -- What can go wrong?

        -- 1. We ran out of function types.
        let shouldBePi :: ExceptT
  (ArgsCheckState [NamedArg Expr])
  (TCMT IO)
  (ArgsCheckState CheckedTarget)
shouldBePi
              -- a) It is an explicit argument, but we ran out of function types.
              | forall a. LensHiding a => a -> Bool
visible ArgInfo
info = forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError forall a b. (a -> b) -> a -> b
$ Type -> TypeError
ShouldBePi Type
sFun
              -- b) It is an implicit argument, and we did not insert any implicits.
              --    Thus, the type was not a function type to start with.
              | forall a. Null a => a -> Bool
null [NamedName]
xs        = forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError forall a b. (a -> b) -> a -> b
$ Type -> TypeError
ShouldBePi Type
sFun
              -- c) We did insert implicits, but we ran out of implicit function types.
              --    Then, we should inform the user that we did not find his one.
              | Bool
otherwise      = forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError forall a b. (a -> b) -> a -> b
$ NamedArg Expr -> [NamedName] -> TypeError
WrongNamedArgument NamedArg Expr
arg [NamedName]
xs

        -- 2. We have a function type left, but it is the wrong one.
        --    Our argument must be implicit, case a) is impossible.
        --    (Otherwise we would have ran out of function types instead.)
        let wrongPi :: ExceptT
  (ArgsCheckState [NamedArg Expr])
  (TCMT IO)
  (ArgsCheckState CheckedTarget)
wrongPi
              -- b) We have not inserted any implicits.
              | forall a. Null a => a -> Bool
null [NamedName]
xs   = forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError forall a b. (a -> b) -> a -> b
$
                            Type -> TypeError
WrongHidingInApplication Type
sFun
              -- c) We inserted implicits, but did not find his one.
              | Bool
otherwise = forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError forall a b. (a -> b) -> a -> b
$ NamedArg Expr -> [NamedName] -> TypeError
WrongNamedArgument NamedArg Expr
arg [NamedName]
xs

        let (Bool
skip, SkipCheck
next) = case SkipCheck
sSkipCheck of
              SkipCheck
Skip       -> (Bool
True, SkipCheck
Skip)
              SkipCheck
DontSkip   -> (Bool
False, SkipCheck
DontSkip)
              SkipNext Nat
n -> case forall a. Ord a => a -> a -> Ordering
compare Nat
n Nat
1 of
                Ordering
LT -> (Bool
False, SkipCheck
DontSkip)
                Ordering
EQ -> (Bool
True,  SkipCheck
DontSkip)
                Ordering
GT -> (Bool
True,  Nat -> SkipCheck
SkipNext (Nat
n forall a. Num a => a -> a -> a
- Nat
1))

        CheckArgumentsE'State
s <- forall (m :: * -> *) a. Monad m => a -> m a
return CheckArgumentsE'State
s
          { sRange :: Range
sRange     = forall u t. (HasRange u, HasRange t) => u -> t -> Range
fuseRange Range
sRange Named_ Expr
e
          , sArgs :: [(NamedArg Expr, Bool)]
sArgs      = [(NamedArg Expr, Bool)]
args
          , sArgsLen :: Nat
sArgsLen   = Nat
sArgsLen forall a. Num a => a -> a -> a
- Nat
1
          , sFun :: Type
sFun       = Type
sFun
          , sSkipCheck :: SkipCheck
sSkipCheck = SkipCheck
next
          }

        -- Check the target type if we can get away with it.
        CheckArgumentsE'State
s <- forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$
          case (CheckedTarget
sChecked, Bool
skip, Maybe Type
sApp) of
            (CheckedTarget
NotCheckedTarget, Bool
False, Just Type
sApp) | Bool
sArgsVisible -> do
              -- How many visible Π's (up to at most sArgsLen) does
              -- sFun start with?
              TelV Tele (Dom Type)
tel Type
tgt <- forall (m :: * -> *).
(MonadReduce m, MonadAddContext m) =>
Nat -> (Dom Type -> Bool) -> Type -> m (TelV Type)
telViewUpTo' Nat
sArgsLen forall a. LensHiding a => a -> Bool
visible Type
sFun
              let visiblePis :: Nat
visiblePis = forall a. Sized a => a -> Nat
size Tele (Dom Type)
tel

                  -- The free variables less than visiblePis in tgt.
                  freeInTgt :: IntSet
freeInTgt =
                    forall a b. (a, b) -> a
fst forall a b. (a -> b) -> a -> b
$ Nat -> IntSet -> (IntSet, IntSet)
IntSet.split Nat
visiblePis forall a b. (a -> b) -> a -> b
$ forall a c t. (IsVarSet a c, Singleton Nat c, Free t) => t -> c
freeVars Type
tgt

              IsRigid
rigid <- CheckArgumentsE'State -> Type -> TCM IsRigid
isRigid CheckArgumentsE'State
s Type
tgt
              -- The target must be rigid.
              case IsRigid
rigid of
                IsNotRigid IsPermanent
reason ->
                      -- Skip the next visiblePis - 1 - k checks.
                  let skip :: Nat -> CheckArgumentsE'State
skip Nat
k   = CheckArgumentsE'State
s{ sSkipCheck :: SkipCheck
sSkipCheck =
                                    Nat -> SkipCheck
SkipNext forall a b. (a -> b) -> a -> b
$ Nat
visiblePis forall a. Num a => a -> a -> a
- Nat
1 forall a. Num a => a -> a -> a
- Nat
k
                                  }
                      dontSkip :: CheckArgumentsE'State
dontSkip = CheckArgumentsE'State
s
                  in forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ case IsPermanent
reason of
                    IsPermanent
Permanent   -> Nat -> CheckArgumentsE'State
skip Nat
0
                    IsPermanent
Unspecified -> CheckArgumentsE'State
dontSkip
                    AVar Nat
x      ->
                      if Nat
x Nat -> IntSet -> Bool
`IntSet.member` IntSet
freeInTgt
                      then Nat -> CheckArgumentsE'State
skip Nat
x
                      else Nat -> CheckArgumentsE'State
skip Nat
0
                IsRigid
IsRigid -> do

                      -- Is any free variable in tgt less than
                      -- visiblePis?
                  let dep :: Bool
dep = Bool -> Bool
not (IntSet -> Bool
IntSet.null IntSet
freeInTgt)
                  -- The target must be non-dependent.
                  if Bool
dep then forall (m :: * -> *) a. Monad m => a -> m a
return CheckArgumentsE'State
s else do

                  -- Andreas, 2019-03-28, issue #3248:
                  -- If the target type is SIZELT, we need coerce, leqType is insufficient.
                  -- For example, we have i : Size <= (Size< ↑ i), but not Size <= (Size< ↑ i).
                  (Bool
isSizeLt, Type
sApp, CheckArgumentsE'State
s) <-
                    if Bool
sSizeLtChecked
                    then forall (m :: * -> *) a. Monad m => a -> m a
return (Bool
False, Type
sApp, CheckArgumentsE'State
s)
                    else do
                      Type
sApp     <- forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce Type
sApp
                      Bool
isSizeLt <- forall a (m :: * -> *).
(IsSizeType a, HasOptions m, HasBuiltins m) =>
a -> m (Maybe BoundedSize)
isSizeType Type
sApp forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
<&> \case
                        Just (BoundedLt Term
_) -> Bool
True
                        Maybe BoundedSize
_                  -> Bool
False
                      forall (m :: * -> *) a. Monad m => a -> m a
return ( Bool
isSizeLt
                             , Type
sApp
                             , CheckArgumentsE'State
s{ sApp :: Maybe Type
sApp           = forall a. a -> Maybe a
Just Type
sApp
                                , sSizeLtChecked :: Bool
sSizeLtChecked = Bool
True
                                , sSkipCheck :: SkipCheck
sSkipCheck     =
                                    if Bool
isSizeLt then SkipCheck
Skip else SkipCheck
DontSkip
                                }
                             )
                  if Bool
isSizeLt then forall (m :: * -> *) a. Monad m => a -> m a
return CheckArgumentsE'State
s else do

                  let tgt1 :: Type
tgt1 = forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst
                               (forall a. Impossible -> Nat -> Substitution' a
strengthenS HasCallStack => Impossible
impossible Nat
visiblePis)
                               Type
tgt
                  forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.term.args.target" Nat
30 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
                    [ TCMT IO Doc
"Checking target types first"
                    , forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
nest Nat
2 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"inferred =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
tgt1
                    , forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
nest Nat
2 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"expected =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
sApp ]
                  CheckedTarget
chk <-
                    forall (m :: * -> *) a. MonadTrace m => Call -> m a -> m a
traceCall
                      (Range -> Type -> Type -> Call
CheckTargetType
                         (forall u t. (HasRange u, HasRange t) => u -> t -> Range
fuseRange Range
sRange [(NamedArg Expr, Bool)]
sArgs) Type
tgt1 Type
sApp) forall a b. (a -> b) -> a -> b
$
                      Maybe ProblemId -> CheckedTarget
CheckedTarget forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
                        forall a. TCM () -> TCM a -> (ProblemId -> TCM a) -> TCM a
ifNoConstraints_ (forall (m :: * -> *).
MonadConversion m =>
Comparison -> Type -> Type -> m ()
compareType Comparison
sComp Type
tgt1 Type
sApp)
                          (forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing) (forall (m :: * -> *) a. Monad m => a -> m a
return forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. a -> Maybe a
Just)
                  forall (m :: * -> *) a. Monad m => a -> m a
return CheckArgumentsE'State
s{ sChecked :: CheckedTarget
sChecked = CheckedTarget
chk }

            (CheckedTarget, Bool, Maybe Type)
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return CheckArgumentsE'State
s

        -- sFun <- lift $ forcePi (getHiding info)
        --                  (maybe "_" rangedThing $ nameOf e) sFun
        case forall t a. Type'' t a -> a
unEl Type
sFun of
          Pi (Dom{domInfo :: forall t e. Dom' t e -> ArgInfo
domInfo = ArgInfo
info', domName :: forall t e. Dom' t e -> Maybe NamedName
domName = Maybe NamedName
dname, unDom :: forall t e. Dom' t e -> e
unDom = Type
a}) Abs Type
b
            | let name :: [Char]
name = forall a.
(LensNamed a, NameOf a ~ NamedName) =>
[Char] -> a -> [Char]
bareNameWithDefault [Char]
"_" Maybe NamedName
dname,
              forall a b. (LensHiding a, LensHiding b) => a -> b -> Bool
sameHiding ArgInfo
info ArgInfo
info'
              Bool -> Bool -> Bool
&& (forall a. LensHiding a => a -> Bool
visible ArgInfo
info Bool -> Bool -> Bool
|| forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
True ([Char]
name forall a. Eq a => a -> a -> Bool
==) Maybe [Char]
mx) -> do
                Term
u <- forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ forall (tcm :: * -> *) m a.
(MonadTCEnv tcm, LensModality m) =>
m -> tcm a -> tcm a
applyModalityToContext ArgInfo
info' forall a b. (a -> b) -> a -> b
$ do
                 -- Andreas, 2014-05-30 experiment to check non-dependent arguments
                 -- after the spine has been processed.  Allows to propagate type info
                 -- from ascribed type into extended-lambdas.  Would solve issue 1159.
                 -- However, leaves unsolved type checking problems in the test suite.
                 -- I do not know what I am doing wrong here.
                 -- Could be extreme order-sensitivity or my abuse of the postponing
                 -- mechanism.
                 -- Andreas, 2016-02-02: Ulf says unless there is actually some meta
                 -- blocking a postponed type checking problem, we might never retry,
                 -- since the trigger for retrying constraints is solving a meta.
                 -- Thus, the following naive use violates some invariant.
                 -- if not $ isBinderUsed b
                 -- then postponeTypeCheckingProblem (CheckExpr (namedThing e) a) (return True) else
                  let e' :: Named_ Expr
e' = Named_ Expr
e { nameOf :: Maybe NamedName
nameOf = (forall name a. Named name a -> Maybe name
nameOf Named_ Expr
e) forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Maybe NamedName
dname }
                  NamedArg Expr -> Type -> TCM Term
checkNamedArg (forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
info' Named_ Expr
e') Type
a

                let c :: Maybe (Abs Constraint)
c | Lock
IsLock forall a. Eq a => a -> a -> Bool
== forall a. LensLock a => a -> Lock
getLock ArgInfo
info' =
                        forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall a. [Char] -> a -> Abs a
Abs [Char]
"t" forall a b. (a -> b) -> a -> b
$
                        Term -> Type -> Arg Term -> Type -> Constraint
CheckLockedVars (Nat -> Elims -> Term
Var Nat
0 []) (forall a. Subst a => Nat -> a -> a
raise Nat
1 Type
sFun)
                          (forall a. Subst a => Nat -> a -> a
raise Nat
1 forall a b. (a -> b) -> a -> b
$ forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
info' Term
u) (forall a. Subst a => Nat -> a -> a
raise Nat
1 Type
a)
                      | Bool
otherwise = forall a. Maybe a
Nothing
                forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.term.lock" Nat
40 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). Applicative m => [Char] -> m Doc
text [Char]
"lock =" 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. LensLock a => a -> Lock
getLock ArgInfo
info')
                forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.term.lock" Nat
40 forall a b. (a -> b) -> a -> b
$
                  forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext (forall a. a -> Dom a
defaultDom forall a b. (a -> b) -> a -> b
$ Type
sFun) forall a b. (a -> b) -> a -> b
$
                  forall b a. b -> (a -> b) -> Maybe a -> b
maybe (forall (m :: * -> *). Applicative m => [Char] -> m Doc
text [Char]
"nothing") forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM (forall a. Subst a => Abs a -> a
absBody forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe (Abs Constraint)
c)
                -- save relevance info' from domain in argument
                forall {a} {m :: * -> *} {a}.
MonadError (ArgsCheckState a) m =>
Elims
-> Range
-> Elim
-> Maybe (Abs Constraint)
-> m (ArgsCheckState a)
-> m (ArgsCheckState a)
addCheckedArgs Elims
us (forall a. HasRange a => a -> Range
getRange Named_ Expr
e) (forall a. Arg a -> Elim' a
Apply forall a b. (a -> b) -> a -> b
$ forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
info' Term
u) Maybe (Abs Constraint)
c forall a b. (a -> b) -> a -> b
$
                  CheckArgumentsE'State
-> ExceptT
     (ArgsCheckState [NamedArg Expr])
     (TCMT IO)
     (ArgsCheckState CheckedTarget)
checkArgumentsE' CheckArgumentsE'State
s{ sFun :: Type
sFun = forall a. Subst a => Abs a -> SubstArg a -> a
absApp Abs Type
b Term
u }
            | Bool
otherwise -> do
                forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"error" Nat
10 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
nest Nat
2 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]
"info      = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show ArgInfo
info
                  , forall (m :: * -> *). Applicative m => [Char] -> m Doc
text forall a b. (a -> b) -> a -> b
$ [Char]
"info'     = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show ArgInfo
info'
                  , forall (m :: * -> *). Applicative m => [Char] -> m Doc
text forall a b. (a -> b) -> a -> b
$ [Char]
"absName b = " forall a. [a] -> [a] -> [a]
++ forall a. Abs a -> [Char]
absName Abs Type
b
                  , forall (m :: * -> *). Applicative m => [Char] -> m Doc
text forall a b. (a -> b) -> a -> b
$ [Char]
"nameOf e  = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show (forall name a. Named name a -> Maybe name
nameOf Named_ Expr
e)
                  ]
                ExceptT
  (ArgsCheckState [NamedArg Expr])
  (TCMT IO)
  (ArgsCheckState CheckedTarget)
wrongPi
          Term
_
            | forall a. LensHiding a => a -> Bool
visible ArgInfo
info
            , PathType Sort
sort QName
_ Arg Term
_ Arg Term
bA Arg Term
x Arg Term
y <- Type -> PathView
sPathView Type
sFun -> do
                forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.term.args" Nat
30 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 Arg Term
bA
                Term
u <- forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ Expr -> Type -> TCM Term
checkExpr (forall name a. Named name a -> a
namedThing Named_ Expr
e) forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Type
primIntervalType
                forall {a} {m :: * -> *} {a}.
MonadError (ArgsCheckState a) m =>
Elims
-> Range
-> Elim
-> Maybe (Abs Constraint)
-> m (ArgsCheckState a)
-> m (ArgsCheckState a)
addCheckedArgs Elims
us (forall a. HasRange a => a -> Range
getRange Named_ Expr
e) (forall a. a -> a -> a -> Elim' a
IApply (forall e. Arg e -> e
unArg Arg Term
x) (forall e. Arg e -> e
unArg Arg Term
y) Term
u) forall a. Maybe a
Nothing forall a b. (a -> b) -> a -> b
$
                  CheckArgumentsE'State
-> ExceptT
     (ArgsCheckState [NamedArg Expr])
     (TCMT IO)
     (ArgsCheckState CheckedTarget)
checkArgumentsE'
                    CheckArgumentsE'State
s{ sChecked :: CheckedTarget
sChecked = CheckedTarget
NotCheckedTarget
                     , sFun :: Type
sFun     = forall t a. Sort' t -> a -> Type'' t a
El Sort
sort forall a b. (a -> b) -> a -> b
$ forall e. Arg e -> e
unArg Arg Term
bA forall t. Apply t => t -> Args -> t
`apply` [forall e. e -> Arg e
argN Term
u]
                     }
          Term
_ -> ExceptT
  (ArgsCheckState [NamedArg Expr])
  (TCMT IO)
  (ArgsCheckState CheckedTarget)
shouldBePi
  where
    -- Andrea: Here one would add constraints too.
    addCheckedArgs :: Elims
-> Range
-> Elim
-> Maybe (Abs Constraint)
-> m (ArgsCheckState a)
-> m (ArgsCheckState a)
addCheckedArgs Elims
us Range
r Elim
u Maybe (Abs Constraint)
c m (ArgsCheckState a)
rec = do
        st :: ArgsCheckState a
st@ACState{acRanges :: forall a. ArgsCheckState a -> MaybeRanges
acRanges = MaybeRanges
rs, acElims :: forall a. ArgsCheckState a -> Elims
acElims = Elims
vs} <- m (ArgsCheckState a)
rec
        let rs' :: MaybeRanges
rs' = forall a. Nat -> a -> [a]
replicate (forall (t :: * -> *) a. Foldable t => t a -> Nat
length Elims
us) forall a. Maybe a
Nothing forall a. [a] -> [a] -> [a]
++ forall a. a -> Maybe a
Just Range
r forall a. a -> [a] -> [a]
: MaybeRanges
rs
            cs' :: [Maybe (Abs Constraint)]
cs' = forall a. Nat -> a -> [a]
replicate (forall (t :: * -> *) a. Foldable t => t a -> Nat
length Elims
us) forall a. Maybe a
Nothing forall a. [a] -> [a] -> [a]
++ Maybe (Abs Constraint)
c forall a. a -> [a] -> [a]
: forall a. ArgsCheckState a -> [Maybe (Abs Constraint)]
acConstraints ArgsCheckState a
st
        forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ ArgsCheckState a
st { acRanges :: MaybeRanges
acRanges = MaybeRanges
rs', acElims :: Elims
acElims = Elims
us forall a. [a] -> [a] -> [a]
++ Elim
u forall a. a -> [a] -> [a]
: Elims
vs, acConstraints :: [Maybe (Abs Constraint)]
acConstraints = [Maybe (Abs Constraint)]
cs' }
      forall e (m :: * -> *) a.
MonadError e m =>
m a -> (e -> m a) -> m a
`catchError` \ st :: ArgsCheckState a
st@ACState{acRanges :: forall a. ArgsCheckState a -> MaybeRanges
acRanges = MaybeRanges
rs, acElims :: forall a. ArgsCheckState a -> Elims
acElims = Elims
vs} -> do
          let rs' :: MaybeRanges
rs' = forall a. Nat -> a -> [a]
replicate (forall (t :: * -> *) a. Foldable t => t a -> Nat
length Elims
us) forall a. Maybe a
Nothing forall a. [a] -> [a] -> [a]
++ forall a. a -> Maybe a
Just Range
r forall a. a -> [a] -> [a]
: MaybeRanges
rs
              cs' :: [Maybe (Abs Constraint)]
cs' = forall a. Nat -> a -> [a]
replicate (forall (t :: * -> *) a. Foldable t => t a -> Nat
length Elims
us) forall a. Maybe a
Nothing forall a. [a] -> [a] -> [a]
++ Maybe (Abs Constraint)
c forall a. a -> [a] -> [a]
: forall a. ArgsCheckState a -> [Maybe (Abs Constraint)]
acConstraints ArgsCheckState a
st
          forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError forall a b. (a -> b) -> a -> b
$ ArgsCheckState a
st { acRanges :: MaybeRanges
acRanges = MaybeRanges
rs', acElims :: Elims
acElims = Elims
us forall a. [a] -> [a] -> [a]
++ Elim
u forall a. a -> [a] -> [a]
: Elims
vs, acConstraints :: [Maybe (Abs Constraint)]
acConstraints = [Maybe (Abs Constraint)]
cs' }

-- | The result of 'isRigid'.

data IsRigid
  = IsRigid
    -- ^ The type is rigid.
  | IsNotRigid !IsPermanent
    -- ^ The type is not rigid. If the argument is 'Nothing', then
    -- this will not change. If the argument is @'Just' reason@, then
    -- this might change for the given @reason@.

-- | Is the result of 'isRigid' \"permanent\"?

data IsPermanent
  = Permanent
    -- ^ Yes.
  | AVar !Nat
    -- ^ The result does not change unless the given variable is
    -- instantiated.
  | Unspecified
    -- ^ Maybe, maybe not.

-- | Is the type \"rigid\"?

isRigid :: CheckArgumentsE'State -> Type -> TCM IsRigid
isRigid :: CheckArgumentsE'State -> Type -> TCM IsRigid
isRigid CheckArgumentsE'State
s Type
t | PathType{} <- CheckArgumentsE'State -> Type -> PathView
sPathView CheckArgumentsE'State
s Type
t =
  -- Path is not rigid.
  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ IsPermanent -> IsRigid
IsNotRigid IsPermanent
Permanent
isRigid CheckArgumentsE'State
_ (El Sort
_ Term
t) = case Term
t of
  Var Nat
x Elims
_    -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ IsPermanent -> IsRigid
IsNotRigid (Nat -> IsPermanent
AVar Nat
x)
  Lam{}      -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ IsPermanent -> IsRigid
IsNotRigid IsPermanent
Permanent
  Lit{}      -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ IsPermanent -> IsRigid
IsNotRigid IsPermanent
Permanent
  Con{}      -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ IsPermanent -> IsRigid
IsNotRigid IsPermanent
Permanent
  Pi Dom Type
dom Abs Type
_   -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$
                if forall a. LensHiding a => a -> Bool
visible Dom Type
dom then IsRigid
IsRigid else IsPermanent -> IsRigid
IsNotRigid IsPermanent
Permanent
  Sort{}     -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ IsPermanent -> IsRigid
IsNotRigid IsPermanent
Permanent
  Level{}    -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ IsPermanent -> IsRigid
IsNotRigid IsPermanent
Permanent
  MetaV{}    -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ IsPermanent -> IsRigid
IsNotRigid IsPermanent
Unspecified
  DontCare{} -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ IsPermanent -> IsRigid
IsNotRigid IsPermanent
Permanent
  Dummy{}    -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ IsPermanent -> IsRigid
IsNotRigid IsPermanent
Permanent
  Def QName
d Elims
_    -> forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
d forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
<&> Definition -> Defn
theDef forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
<&> \case
    Axiom{}                   -> IsRigid
IsRigid
    DataOrRecSig{}            -> IsRigid
IsRigid
    AbstractDefn{}            -> IsRigid
IsRigid
    Function{funClauses :: Defn -> [Clause]
funClauses = [Clause]
cs} -> if forall a. Null a => a -> Bool
null [Clause]
cs
                                 then IsRigid
IsRigid
                                 else IsPermanent -> IsRigid
IsNotRigid IsPermanent
Unspecified
                                      -- This Reason could perhaps be
                                      -- more precise (in some cases).
    Datatype{}                -> IsRigid
IsRigid
    Record{}                  -> IsRigid
IsRigid
    Constructor{}             -> forall a. HasCallStack => a
__IMPOSSIBLE__
    GeneralizableVar{}        -> forall a. HasCallStack => a
__IMPOSSIBLE__
    Primitive{}               -> IsPermanent -> IsRigid
IsNotRigid IsPermanent
Unspecified
    PrimitiveSort{}           -> IsPermanent -> IsRigid
IsNotRigid IsPermanent
Unspecified

-- | Check that a list of arguments fits a telescope.
--   Inserts hidden arguments as necessary.
--   Returns the type-checked arguments and the remaining telescope.
checkArguments_
  :: Comparison           -- ^ Comparison for target
  -> ExpandHidden         -- ^ Eagerly insert trailing hidden arguments?
  -> Range                -- ^ Range of application.
  -> [NamedArg A.Expr]    -- ^ Arguments to check.
  -> Telescope            -- ^ Telescope to check arguments against.
  -> TCM (Elims, Telescope)
     -- ^ Checked arguments and remaining telescope if successful.
checkArguments_ :: Comparison
-> ExpandHidden
-> Range
-> [NamedArg Expr]
-> Tele (Dom Type)
-> TCM (Elims, Tele (Dom Type))
checkArguments_ Comparison
cmp ExpandHidden
exh Range
r [NamedArg Expr]
args Tele (Dom Type)
tel = forall a. TCM a -> TCM a
postponeInstanceConstraints forall a b. (a -> b) -> a -> b
$ do
    Either
  (ArgsCheckState [NamedArg Expr]) (ArgsCheckState CheckedTarget)
z <- forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
runExceptT forall a b. (a -> b) -> a -> b
$
      Comparison
-> ExpandHidden
-> Range
-> [NamedArg Expr]
-> Type
-> Maybe Type
-> ExceptT
     (ArgsCheckState [NamedArg Expr])
     (TCMT IO)
     (ArgsCheckState CheckedTarget)
checkArgumentsE Comparison
cmp ExpandHidden
exh Range
r [NamedArg Expr]
args (Tele (Dom Type) -> Type -> Type
telePi Tele (Dom Type)
tel HasCallStack => Type
__DUMMY_TYPE__) forall a. Maybe a
Nothing
    case Either
  (ArgsCheckState [NamedArg Expr]) (ArgsCheckState CheckedTarget)
z of
      Right (ACState MaybeRanges
_ Elims
args [Maybe (Abs Constraint)]
cs Type
t CheckedTarget
_) | forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all forall a. Maybe a -> Bool
isNothing [Maybe (Abs Constraint)]
cs -> do
        let TelV Tele (Dom Type)
tel' Type
_ = Type -> TelV Type
telView' Type
t
        forall (m :: * -> *) a. Monad m => a -> m a
return (Elims
args, Tele (Dom Type)
tel')
                                    | Bool
otherwise -> do
        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]
"Head constraints are not (yet) supported in this position."
      Left ArgsCheckState [NamedArg Expr]
_ -> forall a. HasCallStack => a
__IMPOSSIBLE__  -- type cannot be blocked as it is generated by telePi

-- | @checkArguments cmp exph r args t0 t k@ tries @checkArgumentsE exph args t0 t@.
-- If it succeeds, it continues @k@ with the returned results.  If it fails,
-- it registers a postponed typechecking problem and returns the resulting new
-- meta variable.
--
-- Checks @e := ((_ : t0) args) : t@.
checkArguments ::
  Comparison -> ExpandHidden -> Range -> [NamedArg A.Expr] -> Type -> Type ->
  (ArgsCheckState CheckedTarget -> TCM Term) -> TCM Term
checkArguments :: Comparison
-> ExpandHidden
-> Range
-> [NamedArg Expr]
-> Type
-> Type
-> (ArgsCheckState CheckedTarget -> TCM Term)
-> TCM Term
checkArguments Comparison
cmp ExpandHidden
exph Range
r [NamedArg Expr]
args Type
t0 Type
t ArgsCheckState CheckedTarget -> TCM Term
k = forall a. TCM a -> TCM a
postponeInstanceConstraints forall a b. (a -> b) -> a -> b
$ do
  Either
  (ArgsCheckState [NamedArg Expr]) (ArgsCheckState CheckedTarget)
z <- forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
runExceptT forall a b. (a -> b) -> a -> b
$ Comparison
-> ExpandHidden
-> Range
-> [NamedArg Expr]
-> Type
-> Maybe Type
-> ExceptT
     (ArgsCheckState [NamedArg Expr])
     (TCMT IO)
     (ArgsCheckState CheckedTarget)
checkArgumentsE Comparison
cmp ExpandHidden
exph Range
r [NamedArg Expr]
args Type
t0 (forall a. a -> Maybe a
Just Type
t)
  case Either
  (ArgsCheckState [NamedArg Expr]) (ArgsCheckState CheckedTarget)
z of
    Right ArgsCheckState CheckedTarget
st -> ArgsCheckState CheckedTarget -> TCM Term
k ArgsCheckState CheckedTarget
st
      -- vs = evaluated args
      -- t1 = remaining type (needs to be subtype of t)
    Left ArgsCheckState [NamedArg Expr]
problem -> ArgsCheckState [NamedArg Expr]
-> Comparison
-> ExpandHidden
-> Range
-> [NamedArg Expr]
-> Type
-> (ArgsCheckState CheckedTarget -> TCM Term)
-> TCM Term
postponeArgs ArgsCheckState [NamedArg Expr]
problem Comparison
cmp ExpandHidden
exph Range
r [NamedArg Expr]
args Type
t ArgsCheckState CheckedTarget -> TCM Term
k
      -- if unsuccessful, postpone checking until t0 unblocks

postponeArgs :: (ArgsCheckState [NamedArg A.Expr]) -> Comparison -> ExpandHidden -> Range -> [NamedArg A.Expr] -> Type ->
                (ArgsCheckState CheckedTarget -> TCM Term) -> TCM Term
postponeArgs :: ArgsCheckState [NamedArg Expr]
-> Comparison
-> ExpandHidden
-> Range
-> [NamedArg Expr]
-> Type
-> (ArgsCheckState CheckedTarget -> TCM Term)
-> TCM Term
postponeArgs (ACState MaybeRanges
rs Elims
us [Maybe (Abs Constraint)]
cs Type
t0 [NamedArg Expr]
es) Comparison
cmp ExpandHidden
exph Range
r [NamedArg Expr]
args Type
t ArgsCheckState CheckedTarget -> TCM Term
k = do
  forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.term.expr.args" Nat
80 forall a b. (a -> b) -> a -> b
$
    forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep [ TCMT IO Doc
"postponed checking arguments"
        , forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
nest Nat
4 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Semigroup (m Doc), Foldable t) =>
t (m Doc) -> m Doc
prettyList (forall a b. (a -> b) -> [a] -> [b]
map (forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall name a. Named name a -> a
namedThing forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall e. Arg e -> e
unArg) [NamedArg Expr]
args)
        , forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
nest Nat
2 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"against"
        , forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
nest Nat
4 forall a b. (a -> b) -> a -> b
$ forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
t0 ] 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
"progress:"
        , forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
nest Nat
2 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"checked" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) (t :: * -> *).
(Applicative m, Semigroup (m Doc), Foldable t) =>
t (m Doc) -> m Doc
prettyList (forall a b. (a -> b) -> [a] -> [b]
map forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Elims
us)
        , forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
nest Nat
2 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"remaining" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep [ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Semigroup (m Doc), Foldable t) =>
t (m Doc) -> m Doc
prettyList (forall a b. (a -> b) -> [a] -> [b]
map (forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall name a. Named name a -> a
namedThing forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall e. Arg e -> e
unArg) [NamedArg Expr]
es)
                                            , forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
nest Nat
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
t0 ] ]
  TypeCheckingProblem -> TCM Term
postponeTypeCheckingProblem_ (Comparison
-> ExpandHidden
-> Range
-> [NamedArg Expr]
-> Type
-> Type
-> (ArgsCheckState CheckedTarget -> TCM Term)
-> TypeCheckingProblem
CheckArgs Comparison
cmp ExpandHidden
exph Range
r [NamedArg Expr]
es Type
t0 Type
t forall a b. (a -> b) -> a -> b
$ \ (ACState MaybeRanges
rs' Elims
vs [Maybe (Abs Constraint)]
cs' Type
t CheckedTarget
pid) -> ArgsCheckState CheckedTarget -> TCM Term
k forall a b. (a -> b) -> a -> b
$ forall a.
MaybeRanges
-> Elims
-> [Maybe (Abs Constraint)]
-> Type
-> a
-> ArgsCheckState a
ACState (MaybeRanges
rs forall a. [a] -> [a] -> [a]
++ MaybeRanges
rs') (Elims
us forall a. [a] -> [a] -> [a]
++ Elims
vs) ([Maybe (Abs Constraint)]
cs forall a. [a] -> [a] -> [a]
++ [Maybe (Abs Constraint)]
cs') Type
t CheckedTarget
pid)

-----------------------------------------------------------------------------
-- * Constructors
-----------------------------------------------------------------------------

-- | Check the type of a constructor application. This is easier than
--   a general application since the implicit arguments can be inserted
--   without looking at the arguments to the constructor.
checkConstructorApplication :: Comparison -> A.Expr -> Type -> ConHead -> [NamedArg A.Expr] -> TCM Term
checkConstructorApplication :: Comparison
-> Expr -> Type -> ConHead -> [NamedArg Expr] -> TCM Term
checkConstructorApplication Comparison
cmp Expr
org Type
t ConHead
c [NamedArg Expr]
args = do
  forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.term.con" Nat
50 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
    [ TCMT IO Doc
"entering checkConstructorApplication"
    , forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
nest Nat
2 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
      [ TCMT IO Doc
"org  =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Expr
org
      , TCMT IO Doc
"t    =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
t
      , 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
      , TCMT IO Doc
"args =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM [NamedArg Expr]
args
    ] ]

  Definition
cdef  <- forall (m :: * -> *). HasConstInfo m => ConHead -> m Definition
getConInfo ConHead
c

  QName -> Definition -> TCM ()
checkModality (ConHead -> QName
conName ConHead
c) Definition
cdef

  let paramsGiven :: Bool
paramsGiven = [NamedArg Expr] -> Bool
checkForParams [NamedArg Expr]
args
  if Bool
paramsGiven then TCM Term
fallback else do
    forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.term.con" Nat
50 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"checkConstructorApplication: no parameters explicitly supplied, continuing..."

    let Constructor{conData :: Defn -> QName
conData = QName
d, conPars :: Defn -> Nat
conPars = Nat
npars} = Definition -> Defn
theDef Definition
cdef
    forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.term.con" Nat
50 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
nest Nat
2 forall a b. (a -> b) -> a -> 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
d
    -- Issue 661: t maybe an evaluated form of d .., so we evaluate d
    -- as well and then check wether we deal with the same datatype
    Term
t0 <- forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce (QName -> Elims -> Term
Def QName
d [])
    Type
tReduced <- forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce Type
t
    case (Term
t0, forall t a. Type'' t a -> a
unEl Type
tReduced) of -- Only fully applied constructors get special treatment
      (Def QName
d0 Elims
_, Def QName
d' Elims
es) -> do
        let ~(Just Args
vs) = forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims Elims
es
        forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.term.con" Nat
50 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
nest Nat
2 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"d0   =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
d0
        forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.term.con" Nat
50 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
nest Nat
2 forall a b. (a -> b) -> a -> 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
d'
        forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.term.con" Nat
50 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
nest Nat
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
        if QName
d' forall a. Eq a => a -> a -> Bool
/= QName
d0 then TCM Term
fallback else do
         -- Issue 661: d' may take more parameters than d, in particular
         -- these additional parameters could be a module parameter telescope.
         -- Since we get the constructor type ctype from d but the parameters
         -- from t = Def d' vs, we drop the additional parameters.
         Maybe Nat
npars' <- forall (m :: * -> *). HasConstInfo m => QName -> m (Maybe Nat)
getNumberOfParameters QName
d'
         forall a b. Maybe a -> b -> (a -> b) -> b
caseMaybe (forall (t :: * -> *) (f :: * -> *) a.
(Traversable t, Applicative f) =>
t (f a) -> f (t a)
sequenceA forall a b. (a -> b) -> a -> b
$ forall a. a -> a -> Pair a
Pair (forall a. a -> Maybe a
Just Nat
npars) Maybe Nat
npars') TCM Term
fallback forall a b. (a -> b) -> a -> b
$ \ (Pair Nat
n Nat
n') -> do
           forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.term.con" Nat
50 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
nest Nat
2 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). Applicative m => [Char] -> m Doc
text forall a b. (a -> b) -> a -> b
$ [Char]
"n    = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Nat
n
           forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.term.con" Nat
50 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
nest Nat
2 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). Applicative m => [Char] -> m Doc
text forall a b. (a -> b) -> a -> b
$ [Char]
"n'   = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Nat
n'
           forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Nat
n forall a. Ord a => a -> a -> Bool
> Nat
n')  -- preprocessor does not like ', so put on next line
             forall a. HasCallStack => a
__IMPOSSIBLE__
           let ps :: Args
ps    = forall a. Nat -> [a] -> [a]
take Nat
n forall a b. (a -> b) -> a -> b
$ forall a. Nat -> [a] -> [a]
drop (Nat
n' forall a. Num a => a -> a -> a
- Nat
n) Args
vs
               ctype :: Type
ctype = Definition -> Type
defType Definition
cdef
           forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.term.con" Nat
20 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
             [ TCMT IO Doc
"special checking of constructor application of" 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 :: * -> *). Functor m => Nat -> m Doc -> m Doc
nest Nat
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 :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Args
ps
                             , TCMT IO Doc
"ctype  =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
ctype ] ]
           let ctype' :: Type
ctype' = Type
ctype Type -> Args -> Type
`piApply` Args
ps
           forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.term.con" Nat
20 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
nest Nat
2 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"ctype' =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
ctype'
           -- get the parameter names
           let TelV Tele (Dom Type)
ptel Type
_ = Nat -> Type -> TelV Type
telView'UpTo Nat
n Type
ctype
           let pnames :: [Dom' Term [Char]]
pnames = forall a b. (a -> b) -> [a] -> [b]
map (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a b. (a, b) -> a
fst) forall a b. (a -> b) -> a -> b
$ forall t. Tele (Dom t) -> [Dom ([Char], t)]
telToList Tele (Dom Type)
ptel
           -- drop the parameter arguments
               args' :: [NamedArg Expr]
args' = [Dom' Term [Char]] -> [NamedArg Expr] -> [NamedArg Expr]
dropArgs [Dom' Term [Char]]
pnames [NamedArg Expr]
args
           -- check the non-parameter arguments
           ExpandHidden
expandLast <- forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
asksTC TCEnv -> ExpandHidden
envExpandLast
           Comparison
-> ExpandHidden
-> Range
-> [NamedArg Expr]
-> Type
-> Type
-> (ArgsCheckState CheckedTarget -> TCM Term)
-> TCM Term
checkArguments Comparison
cmp ExpandHidden
expandLast (forall a. HasRange a => a -> Range
getRange ConHead
c) [NamedArg Expr]
args' Type
ctype' Type
t forall a b. (a -> b) -> a -> b
$ \ st :: ArgsCheckState CheckedTarget
st@(ACState MaybeRanges
_ Elims
_ [Maybe (Abs Constraint)]
_ Type
t' CheckedTarget
targetCheck) -> do
             forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.term.con" Nat
20 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
nest Nat
2 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 [Char]
"es     =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Elims
es
               , forall (m :: * -> *). Applicative m => [Char] -> m Doc
text [Char]
"t'     =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
t' ]
             Term
v <- forall a. (Elims -> Term) -> ArgsCheckState a -> TCM Term
checkHeadConstraints (ConHead -> ConInfo -> Elims -> Term
Con ConHead
c ConInfo
ConOCon) ArgsCheckState CheckedTarget
st
             Comparison -> CheckedTarget -> Term -> Type -> Type -> TCM Term
coerce' Comparison
cmp CheckedTarget
targetCheck Term
v Type
t' Type
t
      (Term, Term)
_ -> do
        forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.term.con" Nat
50 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
nest Nat
2 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"we are not at a datatype, falling back"
        TCM Term
fallback
  where
    fallback :: TCM Term
fallback = Comparison -> Expr -> Type -> Expr -> [NamedArg Expr] -> TCM Term
checkHeadApplication Comparison
cmp Expr
org Type
t (AmbiguousQName -> Expr
A.Con (QName -> AmbiguousQName
unambiguous forall a b. (a -> b) -> a -> b
$ ConHead -> QName
conName ConHead
c)) [NamedArg Expr]
args

    -- Check if there are explicitly given hidden arguments,
    -- in which case we fall back to default type checking.
    -- We could work harder, but let's not for now.
    --
    -- Andreas, 2012-04-18: if all inital args are underscores, ignore them
    checkForParams :: [NamedArg Expr] -> Bool
checkForParams [NamedArg Expr]
args =
      let ([NamedArg Expr]
hargs, [NamedArg Expr]
rest) = forall a. (a -> Bool) -> [a] -> ([a], [a])
break forall a. LensHiding a => a -> Bool
visible [NamedArg Expr]
args
          notUnderscore :: Expr -> Bool
notUnderscore A.Underscore{} = Bool
False
          notUnderscore Expr
_              = Bool
True
      in  forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (Expr -> Bool
notUnderscore forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expr -> Expr
unScope forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. NamedArg a -> a
namedArg) [NamedArg Expr]
hargs

    -- Drop the constructor arguments that correspond to parameters.
    dropArgs :: [Dom' Term [Char]] -> [NamedArg Expr] -> [NamedArg Expr]
dropArgs [] [NamedArg Expr]
args                = [NamedArg Expr]
args
    dropArgs [Dom' Term [Char]]
ps []                  = [NamedArg Expr]
args
    dropArgs [Dom' Term [Char]]
ps args :: [NamedArg Expr]
args@(NamedArg Expr
arg : [NamedArg Expr]
args')
      | Just [Char]
p   <- Maybe [Char]
name,
        Just [Dom' Term [Char]]
ps' <- forall {b} {t}. Eq b => b -> [Dom' t b] -> Maybe [Dom' t b]
namedPar [Char]
p [Dom' Term [Char]]
ps   = [Dom' Term [Char]] -> [NamedArg Expr] -> [NamedArg Expr]
dropArgs [Dom' Term [Char]]
ps' [NamedArg Expr]
args'
      | Maybe [Char]
Nothing  <- Maybe [Char]
name,
        Just [Dom' Term [Char]]
ps' <- forall {a} {t}.
(LensHiding a, LensHiding t) =>
a -> [t] -> Maybe [t]
unnamedPar Hiding
h [Dom' Term [Char]]
ps = [Dom' Term [Char]] -> [NamedArg Expr] -> [NamedArg Expr]
dropArgs [Dom' Term [Char]]
ps' [NamedArg Expr]
args'
      | Bool
otherwise                   = [NamedArg Expr]
args
      where
        name :: Maybe [Char]
name = forall a. (LensNamed a, NameOf a ~ NamedName) => a -> Maybe [Char]
bareNameOf NamedArg Expr
arg
        h :: Hiding
h    = forall a. LensHiding a => a -> Hiding
getHiding NamedArg Expr
arg

        namedPar :: b -> [Dom' t b] -> Maybe [Dom' t b]
namedPar   b
x = forall {t}. (t -> Bool) -> [t] -> Maybe [t]
dropPar ((b
x 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)
        unnamedPar :: a -> [t] -> Maybe [t]
unnamedPar a
h = forall {t}. (t -> Bool) -> [t] -> Maybe [t]
dropPar (forall a b. (LensHiding a, LensHiding b) => a -> b -> Bool
sameHiding a
h)

        dropPar :: (t -> Bool) -> [t] -> Maybe [t]
dropPar t -> Bool
this (t
p : [t]
ps) | t -> Bool
this t
p    = forall a. a -> Maybe a
Just [t]
ps
                              | Bool
otherwise = (t -> Bool) -> [t] -> Maybe [t]
dropPar t -> Bool
this [t]
ps
        dropPar t -> Bool
_ [] = forall a. Maybe a
Nothing

-- | Returns an unblocking action in case of failure.
disambiguateConstructor :: List1 QName -> Type -> TCM (Either Blocker ConHead)
disambiguateConstructor :: List1 QName -> Type -> TCM (Either Blocker ConHead)
disambiguateConstructor List1 QName
cs0 Type
t = do
  forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> [Char] -> m ()
reportSLn [Char]
"tc.check.term.con" Nat
40 forall a b. (a -> b) -> a -> b
$ [Char]
"Ambiguous constructor: " forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> [Char]
prettyShow List1 QName
cs0

  -- Get the datatypes of the various constructors
  let getData :: Defn -> QName
getData Constructor{conData :: Defn -> QName
conData = QName
d} = QName
d
      getData Defn
_                        = forall a. HasCallStack => a
__IMPOSSIBLE__
  forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> [Char] -> m ()
reportSLn [Char]
"tc.check.term.con" Nat
40 forall a b. (a -> b) -> a -> b
$ [Char]
"  ranges before: " forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> [Char]
prettyShow (forall a. HasRange a => a -> Range
getRange List1 QName
cs0)
  -- We use the reduced constructor when disambiguating, but
  -- the original constructor for type checking. This is important
  -- since they may have different types (different parameters).
  -- See issue 279.
  -- Andreas, 2017-08-13, issue #2686: ignore abstract constructors
  [(QName, ConHead)]
ccons  <- forall a b. List1 (Either a b) -> [b]
List1.rights forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do
     forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM List1 QName
cs0 forall a b. (a -> b) -> a -> b
$ \ QName
c -> forall b d a. (b -> d) -> Either a b -> Either a d
mapRight (QName
c,) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> TCM (Either SigError ConHead)
getConForm QName
c
  forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> [Char] -> m ()
reportSLn [Char]
"tc.check.term.con" Nat
40 forall a b. (a -> b) -> a -> b
$ [Char]
"  reduced: " forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> [Char]
prettyShow (forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> b
snd [(QName, ConHead)]
ccons)
  case [(QName, ConHead)]
ccons of
    []    -> forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError forall a b. (a -> b) -> a -> b
$ QName -> TypeError
AbstractConstructorNotInScope forall a b. (a -> b) -> a -> b
$ forall a. NonEmpty a -> a
List1.head List1 QName
cs0
    [(QName
c0,ConHead
con)] -> do
      let c :: ConHead
c = forall a. LensConName a => QName -> a -> a
setConName QName
c0 ConHead
con
      forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> [Char] -> m ()
reportSLn [Char]
"tc.check.term.con" Nat
40 forall a b. (a -> b) -> a -> b
$ [Char]
"  only one non-abstract constructor: " forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> [Char]
prettyShow ConHead
c
      Induction -> QName -> TCM ()
storeDisambiguatedConstructor (ConHead -> Induction
conInductive ConHead
c) (ConHead -> QName
conName ConHead
c)
      forall (m :: * -> *) a. Monad m => a -> m a
return (forall a b. b -> Either a b
Right ConHead
c)
    (QName
c0,ConHead
_):[(QName, ConHead)]
_   -> do
      [(QName, ConHead)]
dcs <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [(QName, ConHead)]
ccons forall a b. (a -> b) -> a -> b
$ \ (QName
c, ConHead
con) -> (, forall a. LensConName a => QName -> a -> a
setConName QName
c ConHead
con) forall b c a. (b -> c) -> (a -> b) -> a -> c
. Defn -> QName
getData 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 => ConHead -> m Definition
getConInfo ConHead
con
      -- Type error
      let badCon :: Type -> TCM (Either Blocker ConHead)
badCon Type
t = forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError forall a b. (a -> b) -> a -> b
$ QName -> Type -> TypeError
DoesNotConstructAnElementOf QName
c0 Type
t
      -- Lets look at the target type at this point
      TelV Tele (Dom Type)
tel Type
t1 <- forall (m :: * -> *). PureTCM m => Type -> m (TelV Type)
telViewPath Type
t
      forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Tele (Dom Type)
tel forall a b. (a -> b) -> a -> b
$ do
       forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.check.term.con" Nat
40 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
nest Nat
2 forall a b. (a -> b) -> a -> b
$
         TCMT IO Doc
"target type: " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
t1
       forall t (m :: * -> *) a.
(Reduce t, IsMeta t, MonadReduce m) =>
t -> (Blocker -> t -> m a) -> (NotBlocked -> t -> m a) -> m a
ifBlocked Type
t1 (\ Blocker
b Type
t -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a b. a -> Either a b
Left Blocker
b) forall a b. (a -> b) -> a -> b
$ \ NotBlocked
_ Type
t' ->
         forall (m :: * -> *) a b.
Monad m =>
m (Maybe a) -> m b -> (a -> m b) -> m b
caseMaybeM (Term -> TCMT IO (Maybe QName)
isDataOrRecord forall a b. (a -> b) -> a -> b
$ forall t a. Type'' t a -> a
unEl Type
t') (Type -> TCM (Either Blocker ConHead)
badCon Type
t') forall a b. (a -> b) -> a -> b
$ \ QName
d ->
           case [ ConHead
c | (QName
d', ConHead
c) <- [(QName, ConHead)]
dcs, QName
d forall a. Eq a => a -> a -> Bool
== QName
d' ] of
             [ConHead
c] -> do
               forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> [Char] -> m ()
reportSLn [Char]
"tc.check.term.con" Nat
40 forall a b. (a -> b) -> a -> b
$ [Char]
"  decided on: " forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> [Char]
prettyShow ConHead
c
               Induction -> QName -> TCM ()
storeDisambiguatedConstructor (ConHead -> Induction
conInductive ConHead
c) (ConHead -> QName
conName ConHead
c)
               forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a b. b -> Either a b
Right ConHead
c
             []  -> Type -> TCM (Either Blocker ConHead)
badCon forall a b. (a -> b) -> a -> b
$ Type
t' forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> QName -> Elims -> Term
Def QName
d []
             ConHead
c:[ConHead]
cs-> forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError forall a b. (a -> b) -> a -> b
$ QName -> List1 QName -> TypeError
CantResolveOverloadedConstructorsTargetingSameDatatype QName
d forall a b. (a -> b) -> a -> b
$
                      forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ConHead -> QName
conName forall a b. (a -> b) -> a -> b
$ ConHead
c forall a. a -> [a] -> NonEmpty a
:| [ConHead]
cs

---------------------------------------------------------------------------
-- * Projections
---------------------------------------------------------------------------

checkUnambiguousProjectionApplication :: Comparison -> A.Expr -> Type -> QName -> ProjOrigin -> A.Expr -> [NamedArg A.Expr] -> TCM Term
checkUnambiguousProjectionApplication :: Comparison
-> Expr
-> Type
-> QName
-> ProjOrigin
-> Expr
-> [NamedArg Expr]
-> TCM Term
checkUnambiguousProjectionApplication Comparison
cmp Expr
e Type
t QName
x ProjOrigin
o Expr
hd [NamedArg Expr]
args = do
  let fallback :: TCM Term
fallback = Comparison -> Expr -> Type -> Expr -> [NamedArg Expr] -> TCM Term
checkHeadApplication Comparison
cmp Expr
e Type
t Expr
hd [NamedArg Expr]
args
  -- Andreas, 2021-02-19, issue #3289
  -- If a postfix projection was moved to the head by appView,
  -- we have to patch the first argument with the correct hiding info.
  case (ProjOrigin
o, [NamedArg Expr]
args) of
    (ProjOrigin
ProjPostfix, NamedArg Expr
arg : [NamedArg Expr]
rest) -> do
      -- Andreas, 2021-11-19, issue #5657:
      -- If @x@ has been brought into scope by e.g. @open R r@, it is no longer
      -- a projection even though the scope checker labels it so.
      -- Thus, @isProjection@ may fail.
      forall (m :: * -> *) a b.
Monad m =>
m (Maybe a) -> m b -> (a -> m b) -> m b
caseMaybeM (forall (m :: * -> *).
HasConstInfo m =>
QName -> m (Maybe Projection)
isProjection QName
x) TCM Term
fallback forall a b. (a -> b) -> a -> b
$ \ Projection
pr -> do
        Comparison -> Expr -> Type -> Expr -> [NamedArg Expr] -> TCM Term
checkHeadApplication Comparison
cmp Expr
e Type
t Expr
hd (forall a. LensArgInfo a => ArgInfo -> a -> a
setArgInfo (Projection -> ArgInfo
projArgInfo Projection
pr) NamedArg Expr
arg forall a. a -> [a] -> [a]
: [NamedArg Expr]
rest)
    (ProjOrigin, [NamedArg Expr])
_ -> TCM Term
fallback

-- | Inferring the type of an overloaded projection application.
--   See 'inferOrCheckProjApp'.

inferProjApp :: A.Expr -> ProjOrigin -> List1 QName -> A.Args -> TCM (Term, Type)
inferProjApp :: Expr
-> ProjOrigin -> List1 QName -> [NamedArg Expr] -> TCM (Term, Type)
inferProjApp Expr
e ProjOrigin
o List1 QName
ds [NamedArg Expr]
args0 = do
  (Term
v, Type
t, CheckedTarget
_) <- Expr
-> ProjOrigin
-> List1 QName
-> [NamedArg Expr]
-> Maybe (Comparison, Type)
-> TCM (Term, Type, CheckedTarget)
inferOrCheckProjApp Expr
e ProjOrigin
o List1 QName
ds [NamedArg Expr]
args0 forall a. Maybe a
Nothing
  forall (m :: * -> *) a. Monad m => a -> m a
return (Term
v, Type
t)

-- | Checking the type of an overloaded projection application.
--   See 'inferOrCheckProjApp'.

checkProjApp  :: Comparison -> A.Expr -> ProjOrigin -> List1 QName -> A.Args -> Type -> TCM Term
checkProjApp :: Comparison
-> Expr
-> ProjOrigin
-> List1 QName
-> [NamedArg Expr]
-> Type
-> TCM Term
checkProjApp Comparison
cmp Expr
e ProjOrigin
o List1 QName
ds [NamedArg Expr]
args0 Type
t = do
  (Term
v, Type
ti, CheckedTarget
targetCheck) <- Expr
-> ProjOrigin
-> List1 QName
-> [NamedArg Expr]
-> Maybe (Comparison, Type)
-> TCM (Term, Type, CheckedTarget)
inferOrCheckProjApp Expr
e ProjOrigin
o List1 QName
ds [NamedArg Expr]
args0 (forall a. a -> Maybe a
Just (Comparison
cmp, Type
t))
  Comparison -> CheckedTarget -> Term -> Type -> Type -> TCM Term
coerce' Comparison
cmp CheckedTarget
targetCheck Term
v Type
ti Type
t

-- | Checking the type of an overloaded projection application.
--   See 'inferOrCheckProjAppToKnownPrincipalArg'.

checkProjAppToKnownPrincipalArg  :: Comparison -> A.Expr -> ProjOrigin -> List1 QName -> A.Args -> Type -> Int -> Term -> Type -> PrincipalArgTypeMetas -> TCM Term
checkProjAppToKnownPrincipalArg :: Comparison
-> Expr
-> ProjOrigin
-> List1 QName
-> [NamedArg Expr]
-> Type
-> Nat
-> Term
-> Type
-> PrincipalArgTypeMetas
-> TCM Term
checkProjAppToKnownPrincipalArg Comparison
cmp Expr
e ProjOrigin
o List1 QName
ds [NamedArg Expr]
args0 Type
t Nat
k Term
v0 Type
pt PrincipalArgTypeMetas
patm = do
  (Term
v, Type
ti, CheckedTarget
targetCheck) <- Expr
-> ProjOrigin
-> List1 QName
-> [NamedArg Expr]
-> Maybe (Comparison, Type)
-> Nat
-> Term
-> Type
-> Maybe PrincipalArgTypeMetas
-> TCM (Term, Type, CheckedTarget)
inferOrCheckProjAppToKnownPrincipalArg Expr
e ProjOrigin
o List1 QName
ds [NamedArg Expr]
args0 (forall a. a -> Maybe a
Just (Comparison
cmp, Type
t)) Nat
k Term
v0 Type
pt (forall a. a -> Maybe a
Just PrincipalArgTypeMetas
patm)
  Comparison -> CheckedTarget -> Term -> Type -> Type -> TCM Term
coerce' Comparison
cmp CheckedTarget
targetCheck Term
v Type
ti Type
t

-- | Inferring or Checking an overloaded projection application.
--
--   The overloaded projection is disambiguated by inferring the type of its
--   principal argument, which is the first visible argument.

inferOrCheckProjApp
  :: A.Expr
     -- ^ The whole expression which constitutes the application.
  -> ProjOrigin
     -- ^ The origin of the projection involved in this projection application.
  -> List1 QName
     -- ^ The projection name (potentially ambiguous).
  -> A.Args
     -- ^ The arguments to the projection.
  -> Maybe (Comparison, Type)
     -- ^ The expected type of the expression (if 'Nothing', infer it).
  -> TCM (Term, Type, CheckedTarget)
     -- ^ The type-checked expression and its type (if successful).
inferOrCheckProjApp :: Expr
-> ProjOrigin
-> List1 QName
-> [NamedArg Expr]
-> Maybe (Comparison, Type)
-> TCM (Term, Type, CheckedTarget)
inferOrCheckProjApp Expr
e ProjOrigin
o List1 QName
ds [NamedArg Expr]
args Maybe (Comparison, Type)
mt = do
  forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.proj.amb" Nat
20 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
    [ TCMT IO Doc
"checking ambiguous projection"
    , forall (m :: * -> *). Applicative m => [Char] -> m Doc
text forall a b. (a -> b) -> a -> b
$ [Char]
"  ds   = " forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> [Char]
prettyShow List1 QName
ds
    , forall (m :: * -> *). Applicative m => [Char] -> m Doc
text   [Char]
"  args = " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep (forall a b. (a -> b) -> [a] -> [b]
map forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM [NamedArg Expr]
args)
    , forall (m :: * -> *). Applicative m => [Char] -> m Doc
text   [Char]
"  t    = " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a b. Maybe a -> b -> (a -> b) -> b
caseMaybe Maybe (Comparison, Type)
mt TCMT IO Doc
"Nothing" forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM
    ]

  let cmp :: Comparison
cmp = forall a b. Maybe a -> b -> (a -> b) -> b
caseMaybe Maybe (Comparison, Type)
mt Comparison
CmpEq forall a b. (a, b) -> a
fst

      -- Postpone the whole type checking problem
      -- if type of principal argument (or the type where we get it from)
      -- is blocked by meta m.
      postpone :: Blocker -> TCM (Term, Type, CheckedTarget)
postpone Blocker
b = do
        Type
tc <- forall a b. Maybe a -> b -> (a -> b) -> b
caseMaybe Maybe (Comparison, Type)
mt TCM Type
newTypeMeta_ (forall (m :: * -> *) a. Monad m => a -> m a
return forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> b
snd)
        Term
v <- TypeCheckingProblem -> Blocker -> TCM Term
postponeTypeCheckingProblem (Comparison -> Expr -> Type -> TypeCheckingProblem
CheckExpr Comparison
cmp Expr
e Type
tc) Blocker
b
        forall (m :: * -> *) a. Monad m => a -> m a
return (Term
v, Type
tc, CheckedTarget
NotCheckedTarget)

  -- The following cases need to be considered:
  -- 1. No arguments to the projection.
  -- 2. Arguments (parameters), but not the principal argument.
  -- 3. Argument(s) including the principal argument.

  -- For now, we only allow ambiguous projections if the first visible
  -- argument is the record value.

  case forall a. (a -> Bool) -> [a] -> [a]
filter (forall a. LensHiding a => a -> Bool
visible forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> b
snd) forall a b. (a -> b) -> a -> b
$ forall a b. [a] -> [b] -> [(a, b)]
zip [Nat
0..] [NamedArg Expr]
args of

    -- Case: we have no visible argument to the projection.
    -- In inference mode, we really need the visible argument, postponing does not help
    [] -> forall a b. Maybe a -> b -> (a -> b) -> b
caseMaybe Maybe (Comparison, Type)
mt (forall a. List1 QName -> TCM a
refuseProjNotApplied List1 QName
ds) forall a b. (a -> b) -> a -> b
$ \ (Comparison
cmp , Type
t) -> do
      -- If we have the type, we can try to get the type of the principal argument.
      -- It is the first visible argument.
      TelV Tele (Dom Type)
_ptel Type
core <- forall (m :: * -> *).
(MonadReduce m, MonadAddContext m) =>
Nat -> (Dom Type -> Bool) -> Type -> m (TelV Type)
telViewUpTo' (-Nat
1) (Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. LensHiding a => a -> Bool
visible) Type
t
      forall t (m :: * -> *) a.
(Reduce t, IsMeta t, MonadReduce m) =>
t -> (Blocker -> t -> m a) -> (NotBlocked -> t -> m a) -> m a
ifBlocked Type
core (\ Blocker
m Type
_ -> Blocker -> TCM (Term, Type, CheckedTarget)
postpone Blocker
m) forall a b. (a -> b) -> a -> b
$ {-else-} \ NotBlocked
_ Type
core -> do
      forall (m :: * -> *) a.
MonadReduce m =>
Type -> (Type -> m a) -> (Dom Type -> Abs Type -> m a) -> m a
ifNotPiType Type
core (\ Type
_ -> forall a. List1 QName -> TCM a
refuseProjNotApplied List1 QName
ds) forall a b. (a -> b) -> a -> b
$ {-else-} \ Dom Type
dom Abs Type
_b -> do
      forall t (m :: * -> *) a.
(Reduce t, IsMeta t, MonadReduce m) =>
t -> (Blocker -> t -> m a) -> (NotBlocked -> t -> m a) -> m a
ifBlocked (forall t e. Dom' t e -> e
unDom Dom Type
dom) (\ Blocker
m Type
_ -> Blocker -> TCM (Term, Type, CheckedTarget)
postpone Blocker
m) forall a b. (a -> b) -> a -> b
$ {-else-} \ NotBlocked
_ Type
ta -> do
      forall (m :: * -> *) a b.
Monad m =>
m (Maybe a) -> m b -> (a -> m b) -> m b
caseMaybeM (forall (m :: * -> *).
PureTCM m =>
Type -> m (Maybe (QName, Args, Defn))
isRecordType Type
ta) (forall a. List1 QName -> TCM a
refuseProjNotRecordType List1 QName
ds) forall a b. (a -> b) -> a -> b
$ \ (QName
_q, Args
_pars, Defn
defn) -> do
      case Defn
defn of
        Record { recFields :: Defn -> [Dom QName]
recFields = [Dom QName]
fs } -> do
          case forall a b. [a] -> (a -> Maybe b) -> [b]
forMaybe [Dom QName]
fs forall a b. (a -> b) -> a -> b
$ \ Dom QName
f -> forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
Fold.find (forall t e. Dom' t e -> e
unDom Dom QName
f forall a. Eq a => a -> a -> Bool
==) List1 QName
ds of
            [] -> forall a. List1 QName -> TCM a
refuseProjNoMatching List1 QName
ds
            [QName
d] -> do
              QName -> TCM ()
storeDisambiguatedProjection QName
d
              -- checkHeadApplication will check the target type
              (, Type
t, Maybe ProblemId -> CheckedTarget
CheckedTarget forall a. Maybe a
Nothing) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
                Comparison -> Expr -> Type -> Expr -> [NamedArg Expr] -> TCM Term
checkHeadApplication Comparison
cmp Expr
e Type
t (ProjOrigin -> AmbiguousQName -> Expr
A.Proj ProjOrigin
o forall a b. (a -> b) -> a -> b
$ QName -> AmbiguousQName
unambiguous QName
d) [NamedArg Expr]
args
            [QName]
_ -> forall a. HasCallStack => a
__IMPOSSIBLE__
        Defn
_ -> forall a. HasCallStack => a
__IMPOSSIBLE__

    -- Case: we have a visible argument
    ((Nat
k, NamedArg Expr
arg) : [(Nat, NamedArg Expr)]
_) -> do
      (Term
v0, Type
ta) <- Expr -> TCM (Term, Type)
inferExpr forall a b. (a -> b) -> a -> b
$ forall a. NamedArg a -> a
namedArg NamedArg Expr
arg
      forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.proj.amb" Nat
25 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
        [ TCMT IO Doc
"  principal arg " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM NamedArg Expr
arg
        , TCMT IO Doc
"  has type "      forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
ta
        ]
      Expr
-> ProjOrigin
-> List1 QName
-> [NamedArg Expr]
-> Maybe (Comparison, Type)
-> Nat
-> Term
-> Type
-> Maybe PrincipalArgTypeMetas
-> TCM (Term, Type, CheckedTarget)
inferOrCheckProjAppToKnownPrincipalArg Expr
e ProjOrigin
o List1 QName
ds [NamedArg Expr]
args Maybe (Comparison, Type)
mt Nat
k Term
v0 Type
ta forall a. Maybe a
Nothing

-- | Same arguments 'inferOrCheckProjApp' above but also gets the position,
--   value and type of the principal argument.
inferOrCheckProjAppToKnownPrincipalArg
  :: A.Expr
     -- ^ The whole expression which constitutes the application.
  -> ProjOrigin
     -- ^ The origin of the projection involved in this projection application.
  -> List1 QName
     -- ^ The projection name (potentially ambiguous).
  -> A.Args
     -- ^ The arguments to the projection.
  -> Maybe (Comparison, Type)
     -- ^ The expected type of the expression (if 'Nothing', infer it).
  -> Int
     -- ^ The position of the principal argument.
  -> Term
     -- ^ The value of the principal argument.
  -> Type
     -- ^ The type of the principal argument.
  -> Maybe PrincipalArgTypeMetas
     -- ^ The metas previously created for the principal argument's type, when
     --   picking up a postponed problem. 'Nothing', otherwise.
  -> TCM (Term, Type, CheckedTarget)
     -- ^ The type-checked expression and its type (if successful).
inferOrCheckProjAppToKnownPrincipalArg :: Expr
-> ProjOrigin
-> List1 QName
-> [NamedArg Expr]
-> Maybe (Comparison, Type)
-> Nat
-> Term
-> Type
-> Maybe PrincipalArgTypeMetas
-> TCM (Term, Type, CheckedTarget)
inferOrCheckProjAppToKnownPrincipalArg Expr
e ProjOrigin
o List1 QName
ds [NamedArg Expr]
args Maybe (Comparison, Type)
mt Nat
k Term
v0 Type
ta Maybe PrincipalArgTypeMetas
mpatm = do
  let cmp :: Comparison
cmp = forall a b. Maybe a -> b -> (a -> b) -> b
caseMaybe Maybe (Comparison, Type)
mt Comparison
CmpEq forall a b. (a, b) -> a
fst
      postpone :: Blocker -> PrincipalArgTypeMetas -> TCM (Term, Type, CheckedTarget)
postpone Blocker
b PrincipalArgTypeMetas
patm = do
        Type
tc <- forall a b. Maybe a -> b -> (a -> b) -> b
caseMaybe Maybe (Comparison, Type)
mt TCM Type
newTypeMeta_ (forall (m :: * -> *) a. Monad m => a -> m a
return forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> b
snd)
        Term
v <- TypeCheckingProblem -> Blocker -> TCM Term
postponeTypeCheckingProblem (Comparison
-> Expr
-> ProjOrigin
-> List1 QName
-> [NamedArg Expr]
-> Type
-> Nat
-> Term
-> Type
-> PrincipalArgTypeMetas
-> TypeCheckingProblem
CheckProjAppToKnownPrincipalArg Comparison
cmp Expr
e ProjOrigin
o List1 QName
ds [NamedArg Expr]
args Type
tc Nat
k Term
v0 Type
ta PrincipalArgTypeMetas
patm) Blocker
b
        forall (m :: * -> *) a. Monad m => a -> m a
return (Term
v, Type
tc, CheckedTarget
NotCheckedTarget)
  -- ta should be a record type (after introducing the hidden args in v0)
  patm :: PrincipalArgTypeMetas
patm@(PrincipalArgTypeMetas Args
vargs Type
ta) <- case Maybe PrincipalArgTypeMetas
mpatm of
    -- keep using the previously created metas, when picking up a postponed
    -- problem - see #4924
    Just PrincipalArgTypeMetas
patm -> forall (m :: * -> *) a. Monad m => a -> m a
return PrincipalArgTypeMetas
patm
    -- create fresh metas
    Maybe PrincipalArgTypeMetas
Nothing -> forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Args -> Type -> PrincipalArgTypeMetas
PrincipalArgTypeMetas forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *).
(PureTCM m, MonadMetaSolver m, MonadTCM m) =>
Nat -> (Hiding -> Bool) -> Type -> m (Args, Type)
implicitArgs (-Nat
1) (Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. LensHiding a => a -> Bool
visible) Type
ta
  let v :: Term
v = Term
v0 forall t. Apply t => t -> Args -> t
`apply` Args
vargs
  forall t (m :: * -> *) a.
(Reduce t, IsMeta t, MonadReduce m) =>
t -> (Blocker -> t -> m a) -> (NotBlocked -> t -> m a) -> m a
ifBlocked Type
ta (\ Blocker
m Type
_ -> Blocker -> PrincipalArgTypeMetas -> TCM (Term, Type, CheckedTarget)
postpone Blocker
m PrincipalArgTypeMetas
patm) {-else-} forall a b. (a -> b) -> a -> b
$ \ NotBlocked
_ Type
ta -> do
  forall (m :: * -> *) a b.
Monad m =>
m (Maybe a) -> m b -> (a -> m b) -> m b
caseMaybeM (forall (m :: * -> *).
PureTCM m =>
Type -> m (Maybe (QName, Args, Defn))
isRecordType Type
ta) (forall a. List1 QName -> TCM a
refuseProjNotRecordType List1 QName
ds) forall a b. (a -> b) -> a -> b
$ \ (QName
q, Args
_pars0, Defn
_) -> do

      -- try to project it with all of the possible projections
      let try :: QName
-> MaybeT
     (TCMT IO) (QName, (QName, (Args, (Dom Type, Term, Type))))
try QName
d = do
            forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.proj.amb" Nat
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]
"trying projection " forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> [Char]
prettyShow QName
d
              , TCMT IO Doc
"  td  = " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) a b.
Monad m =>
m (Maybe a) -> m b -> (a -> m b) -> m b
caseMaybeM (forall (m :: * -> *). PureTCM m => QName -> Type -> m (Maybe Type)
getDefType QName
d Type
ta) TCMT IO Doc
"Nothing" forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM
              ]

            -- get the original projection name
            Definition
def <- forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
d
            let isP :: Maybe Projection
isP = Defn -> Maybe Projection
isProjection_ forall a b. (a -> b) -> a -> b
$ Definition -> Defn
theDef Definition
def
            forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.proj.amb" Nat
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
$
              forall (m :: * -> *). Applicative m => [Char] -> m Doc
text ( [Char]
"  isProjection = " forall a. [a] -> [a] -> [a]
++ forall a b. Maybe a -> b -> (a -> b) -> b
caseMaybe Maybe Projection
isP [Char]
"no" (forall a b. a -> b -> a
const [Char]
"yes")
                   ) forall a. a -> [a] -> [a]
: forall a b. Maybe a -> b -> (a -> b) -> b
caseMaybe Maybe Projection
isP [] (\ Projection{ projProper :: Projection -> Maybe QName
projProper = Maybe QName
proper, projOrig :: Projection -> QName
projOrig = QName
orig } ->
              [ forall (m :: * -> *). Applicative m => [Char] -> m Doc
text forall a b. (a -> b) -> a -> b
$ [Char]
"  proper       = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Maybe QName
proper
              , forall (m :: * -> *). Applicative m => [Char] -> m Doc
text forall a b. (a -> b) -> a -> b
$ [Char]
"  orig         = " forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> [Char]
prettyShow QName
orig
              ])

            -- Andreas, 2017-01-21, issue #2422
            -- The scope checker considers inherited projections (from nested records)
            -- as projections and allows overloading.  However, since they are defined
            -- as *composition* of projections, the type checker does *not* recognize them,
            -- and @isP@ will be @Nothing@.
            -- However, we can ignore this, as we only need the @orig@inal projection name
            -- for removing false ambiguity.  Thus, we skip these checks:

            -- Projection{ projProper = proper, projOrig = orig } <- MaybeT $ return isP
            -- guard $ isJust proper
            let orig :: QName
orig = forall a b. Maybe a -> b -> (a -> b) -> b
caseMaybe Maybe Projection
isP QName
d Projection -> QName
projOrig

            -- try to eliminate
            (Dom Type
dom, Term
u, Type
tb) <- forall (m :: * -> *) a. m (Maybe a) -> MaybeT m a
MaybeT (forall (m :: * -> *).
PureTCM m =>
Term
-> Type -> ProjOrigin -> QName -> m (Maybe (Dom Type, Term, Type))
projectTyped Term
v Type
ta ProjOrigin
o QName
d forall e (m :: * -> *) a.
MonadError e m =>
m a -> (e -> m a) -> m a
`catchError` \ TCErr
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing)
            forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.proj.amb" Nat
30 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
              [ TCMT IO Doc
"  dom = " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Dom Type
dom
              , TCMT IO Doc
"  u   = " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
u
              , TCMT IO Doc
"  tb  = " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
tb
              ]
            (QName
q', Args
pars, Defn
_) <- forall (m :: * -> *) a. m (Maybe a) -> MaybeT m a
MaybeT 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 t e. Dom' t e -> e
unDom Dom Type
dom
            forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.proj.amb" Nat
30 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
              [ TCMT IO Doc
"  q   = " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
q
              , TCMT IO Doc
"  q'  = " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
q'
              ]
            forall (f :: * -> *). Alternative f => Bool -> f ()
guard (QName
q forall a. Eq a => a -> a -> Bool
== QName
q')
            -- Get the type of the projection and check
            -- that the first visible argument is the record value.
            let tfull :: Type
tfull = Definition -> Type
defType Definition
def
            TelV Tele (Dom Type)
tel Type
_ <- forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
(MonadReduce m, MonadAddContext m) =>
Nat -> (Dom Type -> Bool) -> Type -> m (TelV Type)
telViewUpTo' (-Nat
1) (Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. LensHiding a => a -> Bool
visible) Type
tfull
            forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.proj.amb" Nat
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]
"  size tel  = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show (forall a. Sized a => a -> Nat
size Tele (Dom Type)
tel)
              , forall (m :: * -> *). Applicative m => [Char] -> m Doc
text forall a b. (a -> b) -> a -> b
$ [Char]
"  size pars = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show (forall a. Sized a => a -> Nat
size Args
pars)
              ]
            -- See issue 1960 for when the following assertion fails for
            -- the correct disambiguation.
            -- guard (size tel == size pars)

            forall (f :: * -> *). Alternative f => Bool -> f ()
guard forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< do forall a. Maybe a -> Bool
isNothing forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ QName -> Definition -> TCM (Maybe TypeError)
checkModality' QName
d Definition
def
            forall (m :: * -> *) a. Monad m => a -> m a
return (QName
orig, (QName
d, (Args
pars, (Dom Type
dom, Term
u, Type
tb))))

      [[(QName, (QName, (Args, (Dom Type, Term, Type))))]]
cands <- forall b a. Ord b => (a -> b) -> [a] -> [[a]]
groupOn forall a b. (a, b) -> a
fst forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. List1 (Maybe a) -> [a]
List1.catMaybes 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 (m :: * -> *) a. MaybeT m a -> m (Maybe a)
runMaybeT forall b c a. (b -> c) -> (a -> b) -> a -> c
. QName
-> MaybeT
     (TCMT IO) (QName, (QName, (Args, (Dom Type, Term, Type))))
try) List1 QName
ds
      case [[(QName, (QName, (Args, (Dom Type, Term, Type))))]]
cands of
        [] -> forall a. List1 QName -> TCM a
refuseProjNoMatching List1 QName
ds
        [[]] -> forall a. List1 QName -> TCM a
refuseProjNoMatching List1 QName
ds
        ([(QName, (QName, (Args, (Dom Type, Term, Type))))]
_:[(QName, (QName, (Args, (Dom Type, Term, Type))))]
_:[[(QName, (QName, (Args, (Dom Type, Term, Type))))]]
_) -> forall a. List1 QName -> [Char] -> TCM a
refuseProj List1 QName
ds forall a b. (a -> b) -> a -> b
$ [Char]
"several matching candidates found: "
             forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> [Char]
prettyShow (forall a b. (a -> b) -> [a] -> [b]
map (forall a b. (a, b) -> a
fst forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> b
snd) forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[(QName, (QName, (Args, (Dom Type, Term, Type))))]]
cands)
        -- case: just one matching projection d
        -- the term u = d v
        -- the type tb is the type of this application
        [ (QName
_orig, (QName
d, (Args
pars, (Dom Type
_dom,Term
u,Type
tb)))) : [(QName, (QName, (Args, (Dom Type, Term, Type))))]
_ ] -> do
          QName -> TCM ()
storeDisambiguatedProjection QName
d

          -- Check parameters
          Type
tfull <- forall (m :: * -> *).
(HasConstInfo m, ReadTCState m) =>
QName -> m Type
typeOfConst QName
d
          (Args
_,Type
_) <- [NamedArg Expr] -> Args -> Type -> TCM (Args, Type)
checkKnownArguments (forall a. Nat -> [a] -> [a]
take Nat
k [NamedArg Expr]
args) Args
pars Type
tfull

          -- Check remaining arguments
          let r :: Range
r     = forall a. HasRange a => a -> Range
getRange Expr
e
              args' :: [NamedArg Expr]
args' = forall a. Nat -> [a] -> [a]
drop (Nat
k forall a. Num a => a -> a -> a
+ Nat
1) [NamedArg Expr]
args
          Either
  (ArgsCheckState [NamedArg Expr]) (ArgsCheckState CheckedTarget)
z <- forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
runExceptT forall a b. (a -> b) -> a -> b
$ Comparison
-> ExpandHidden
-> Range
-> [NamedArg Expr]
-> Type
-> Maybe Type
-> ExceptT
     (ArgsCheckState [NamedArg Expr])
     (TCMT IO)
     (ArgsCheckState CheckedTarget)
checkArgumentsE Comparison
cmp ExpandHidden
ExpandLast Range
r [NamedArg Expr]
args' Type
tb (forall a b. (a, b) -> b
snd forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe (Comparison, Type)
mt)
          case Either
  (ArgsCheckState [NamedArg Expr]) (ArgsCheckState CheckedTarget)
z of
            Right st :: ArgsCheckState CheckedTarget
st@(ACState MaybeRanges
_ Elims
_ [Maybe (Abs Constraint)]
_ Type
trest CheckedTarget
targetCheck) -> do
              Term
v <- forall a. (Elims -> Term) -> ArgsCheckState a -> TCM Term
checkHeadConstraints (Term
u forall t. Apply t => t -> Elims -> t
`applyE`) ArgsCheckState CheckedTarget
st
              forall (m :: * -> *) a. Monad m => a -> m a
return (Term
v, Type
trest, CheckedTarget
targetCheck)
            Left ArgsCheckState [NamedArg Expr]
problem -> do
              -- In the inference case:
              -- To create a postponed type checking problem,
              -- we do not use typeDontCare, but create a meta.
              Type
tc <- forall a b. Maybe a -> b -> (a -> b) -> b
caseMaybe Maybe (Comparison, Type)
mt TCM Type
newTypeMeta_ (forall (m :: * -> *) a. Monad m => a -> m a
return forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> b
snd)
              Term
v  <- ArgsCheckState [NamedArg Expr]
-> Comparison
-> ExpandHidden
-> Range
-> [NamedArg Expr]
-> Type
-> (ArgsCheckState CheckedTarget -> TCM Term)
-> TCM Term
postponeArgs ArgsCheckState [NamedArg Expr]
problem Comparison
cmp ExpandHidden
ExpandLast Range
r [NamedArg Expr]
args' Type
tc forall a b. (a -> b) -> a -> b
$ \ st :: ArgsCheckState CheckedTarget
st@(ACState MaybeRanges
_ Elims
_ [Maybe (Abs Constraint)]
_ Type
trest CheckedTarget
targetCheck) -> do
                      Term
v <- forall a. (Elims -> Term) -> ArgsCheckState a -> TCM Term
checkHeadConstraints (Term
u forall t. Apply t => t -> Elims -> t
`applyE`) ArgsCheckState CheckedTarget
st
                      Comparison -> CheckedTarget -> Term -> Type -> Type -> TCM Term
coerce' Comparison
cmp CheckedTarget
targetCheck Term
v Type
trest Type
tc

              forall (m :: * -> *) a. Monad m => a -> m a
return (Term
v, Type
tc, CheckedTarget
NotCheckedTarget)

refuseProj :: List1 QName -> String -> TCM a
refuseProj :: forall a. List1 QName -> [Char] -> TCM a
refuseProj List1 QName
ds [Char]
reason = 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 resolve overloaded projection "
        forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> [Char]
prettyShow (Name -> Name
A.nameConcrete forall a b. (a -> b) -> a -> b
$ QName -> Name
A.qnameName forall a b. (a -> b) -> a -> b
$ forall a. NonEmpty a -> a
List1.head List1 QName
ds)
        forall a. [a] -> [a] -> [a]
++ [Char]
" because " forall a. [a] -> [a] -> [a]
++ [Char]
reason

refuseProjNotApplied, refuseProjNoMatching, refuseProjNotRecordType :: List1 QName -> TCM a
refuseProjNotApplied :: forall a. List1 QName -> TCM a
refuseProjNotApplied    List1 QName
ds = forall a. List1 QName -> [Char] -> TCM a
refuseProj List1 QName
ds [Char]
"it is not applied to a visible argument"
refuseProjNoMatching :: forall a. List1 QName -> TCM a
refuseProjNoMatching    List1 QName
ds = forall a. List1 QName -> [Char] -> TCM a
refuseProj List1 QName
ds [Char]
"no matching candidate found"
refuseProjNotRecordType :: forall a. List1 QName -> TCM a
refuseProjNotRecordType List1 QName
ds = forall a. List1 QName -> [Char] -> TCM a
refuseProj List1 QName
ds [Char]
"principal argument is not of record type"

-----------------------------------------------------------------------------
-- * Sorts
-----------------------------------------------------------------------------

checkSet
  :: Comparison -> A.Expr -> Type
  -> QName -> Suffix -> [NamedArg A.Expr] -> TCM Term
checkSet :: Comparison
-> Expr -> Type -> QName -> Suffix -> [NamedArg Expr] -> TCM Term
checkSet = (Level -> Sort)
-> Comparison
-> Expr
-> Type
-> QName
-> Suffix
-> [NamedArg Expr]
-> TCM Term
checkSetOrProp forall t. Level' t -> Sort' t
Type

checkProp
  :: Comparison -> A.Expr -> Type
  -> QName -> Suffix -> [NamedArg A.Expr] -> TCM Term
checkProp :: Comparison
-> Expr -> Type -> QName -> Suffix -> [NamedArg Expr] -> TCM Term
checkProp Comparison
cmp Expr
e Type
t QName
q Suffix
s [NamedArg Expr]
args = do
  forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
unlessM forall (m :: * -> *). HasOptions m => m Bool
isPropEnabled forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError TypeError
NeedOptionProp
  (Level -> Sort)
-> Comparison
-> Expr
-> Type
-> QName
-> Suffix
-> [NamedArg Expr]
-> TCM Term
checkSetOrProp forall t. Level' t -> Sort' t
Prop Comparison
cmp Expr
e Type
t QName
q Suffix
s [NamedArg Expr]
args

checkSSet
  :: Comparison -> A.Expr -> Type
  -> QName -> Suffix -> [NamedArg A.Expr] -> TCM Term
checkSSet :: Comparison
-> Expr -> Type -> QName -> Suffix -> [NamedArg Expr] -> TCM Term
checkSSet Comparison
cmp Expr
e Type
t QName
q Suffix
s [NamedArg Expr]
args = do
  forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
unlessM forall (m :: * -> *). HasOptions m => m Bool
isTwoLevelEnabled forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError TypeError
NeedOptionTwoLevel
  (Level -> Sort)
-> (Level -> Sort)
-> Comparison
-> Expr
-> Type
-> QName
-> Suffix
-> [NamedArg Expr]
-> TCM Term
checkLeveledSort forall t. Level' t -> Sort' t
SSet forall t. Level' t -> Sort' t
SSet Comparison
cmp Expr
e Type
t QName
q Suffix
s [NamedArg Expr]
args

checkSetOrProp
  :: (Level -> Sort) -> Comparison -> A.Expr -> Type
  -> QName -> Suffix -> [NamedArg A.Expr] -> TCM Term
checkSetOrProp :: (Level -> Sort)
-> Comparison
-> Expr
-> Type
-> QName
-> Suffix
-> [NamedArg Expr]
-> TCM Term
checkSetOrProp Level -> Sort
mkSort Comparison
cmp Expr
e Type
t QName
q Suffix
suffix [NamedArg Expr]
args = do
  (Level -> Sort)
-> (Level -> Sort)
-> Comparison
-> Expr
-> Type
-> QName
-> Suffix
-> [NamedArg Expr]
-> TCM Term
checkLeveledSort Level -> Sort
mkSort forall t. Level' t -> Sort' t
Type Comparison
cmp Expr
e Type
t QName
q Suffix
suffix [NamedArg Expr]
args

checkLeveledSort
  :: (Level -> Sort) -> (Level -> Sort) -> Comparison -> A.Expr -> Type
  -> QName -> Suffix -> [NamedArg A.Expr] -> TCM Term
checkLeveledSort :: (Level -> Sort)
-> (Level -> Sort)
-> Comparison
-> Expr
-> Type
-> QName
-> Suffix
-> [NamedArg Expr]
-> TCM Term
checkLeveledSort Level -> Sort
mkSort Level -> Sort
mkSortOfSort Comparison
cmp Expr
e Type
t QName
q Suffix
suffix [NamedArg Expr]
args = do
  (Term
v, Type
t0) <- (Level -> Sort)
-> (Level -> Sort)
-> Expr
-> QName
-> Suffix
-> [NamedArg Expr]
-> TCM (Term, Type)
inferLeveledSort Level -> Sort
mkSort Level -> Sort
mkSortOfSort Expr
e QName
q Suffix
suffix [NamedArg Expr]
args
  forall (m :: * -> *).
(MonadConversion m, MonadTCM m) =>
Comparison -> Term -> Type -> Type -> m Term
coerce Comparison
cmp Term
v Type
t0 Type
t

inferSet :: A.Expr -> QName -> Suffix -> [NamedArg A.Expr] -> TCM (Term, Type)
inferSet :: Expr -> QName -> Suffix -> [NamedArg Expr] -> TCM (Term, Type)
inferSet = (Level -> Sort)
-> Expr -> QName -> Suffix -> [NamedArg Expr] -> TCM (Term, Type)
inferSetOrProp forall t. Level' t -> Sort' t
Type

inferProp :: A.Expr -> QName -> Suffix -> [NamedArg A.Expr] -> TCM (Term, Type)
inferProp :: Expr -> QName -> Suffix -> [NamedArg Expr] -> TCM (Term, Type)
inferProp Expr
e QName
q Suffix
s [NamedArg Expr]
args = do
  forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
unlessM forall (m :: * -> *). HasOptions m => m Bool
isPropEnabled forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError TypeError
NeedOptionProp
  (Level -> Sort)
-> Expr -> QName -> Suffix -> [NamedArg Expr] -> TCM (Term, Type)
inferSetOrProp forall t. Level' t -> Sort' t
Prop Expr
e QName
q Suffix
s [NamedArg Expr]
args

inferSSet :: A.Expr -> QName -> Suffix -> [NamedArg A.Expr] -> TCM (Term, Type)
inferSSet :: Expr -> QName -> Suffix -> [NamedArg Expr] -> TCM (Term, Type)
inferSSet Expr
e QName
q Suffix
s [NamedArg Expr]
args = do
  forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
unlessM forall (m :: * -> *). HasOptions m => m Bool
isTwoLevelEnabled forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError TypeError
NeedOptionTwoLevel
  (Level -> Sort)
-> (Level -> Sort)
-> Expr
-> QName
-> Suffix
-> [NamedArg Expr]
-> TCM (Term, Type)
inferLeveledSort forall t. Level' t -> Sort' t
SSet forall t. Level' t -> Sort' t
SSet Expr
e QName
q Suffix
s [NamedArg Expr]
args

inferSetOrProp
  :: (Level -> Sort) -> A.Expr
  -> QName -> Suffix -> [NamedArg A.Expr] -> TCM (Term, Type)
inferSetOrProp :: (Level -> Sort)
-> Expr -> QName -> Suffix -> [NamedArg Expr] -> TCM (Term, Type)
inferSetOrProp Level -> Sort
mkSort Expr
e QName
q Suffix
suffix [NamedArg Expr]
args = (Level -> Sort)
-> (Level -> Sort)
-> Expr
-> QName
-> Suffix
-> [NamedArg Expr]
-> TCM (Term, Type)
inferLeveledSort Level -> Sort
mkSort forall t. Level' t -> Sort' t
Type Expr
e QName
q Suffix
suffix [NamedArg Expr]
args

inferLeveledSort
  :: (Level -> Sort) -> (Level -> Sort) -> A.Expr
  -> QName -> Suffix -> [NamedArg A.Expr] -> TCM (Term, Type)
inferLeveledSort :: (Level -> Sort)
-> (Level -> Sort)
-> Expr
-> QName
-> Suffix
-> [NamedArg Expr]
-> TCM (Term, Type)
inferLeveledSort Level -> Sort
mkSort Level -> Sort
mkSortOfSort Expr
e QName
q Suffix
suffix [NamedArg Expr]
args = case [NamedArg Expr]
args of
  [] -> do
    let n :: Integer
n = case Suffix
suffix of
              Suffix
NoSuffix -> Integer
0
              Suffix Integer
n -> Integer
n
    forall (m :: * -> *) a. Monad m => a -> m a
return (Sort -> Term
Sort (Level -> Sort
mkSort forall a b. (a -> b) -> a -> b
$ Integer -> Level
ClosedLevel Integer
n) , Sort -> Type
sort (Level -> Sort
mkSortOfSort forall a b. (a -> b) -> a -> b
$ Integer -> Level
ClosedLevel forall a b. (a -> b) -> a -> b
$ Integer
n forall a. Num a => a -> a -> a
+ Integer
1))
  [NamedArg Expr
arg] -> do
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (forall a. LensHiding a => a -> Bool
visible NamedArg Expr
arg) forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError forall a b. (a -> b) -> a -> b
$ Type -> TypeError
WrongHidingInApplication forall a b. (a -> b) -> a -> b
$ Sort -> Type
sort forall a b. (a -> b) -> a -> b
$ Level -> Sort
mkSort forall a b. (a -> b) -> a -> b
$ Integer -> Level
ClosedLevel Integer
0
    forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
unlessM forall (m :: * -> *). HasOptions m => m Bool
hasUniversePolymorphism forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
[Char] -> m a
genericError
      [Char]
"Use --universe-polymorphism to enable level arguments to Set"
    Level
l <- forall (tcm :: * -> *) r a.
(MonadTCEnv tcm, LensRelevance r) =>
r -> tcm a -> tcm a
applyRelevanceToContext Relevance
NonStrict forall a b. (a -> b) -> a -> b
$ NamedArg Expr -> TCMT IO Level
checkLevel NamedArg Expr
arg
    forall (m :: * -> *) a. Monad m => a -> m a
return (Sort -> Term
Sort forall a b. (a -> b) -> a -> b
$ Level -> Sort
mkSort Level
l , Sort -> Type
sort (Level -> Sort
mkSortOfSort forall a b. (a -> b) -> a -> b
$ Level -> Level
levelSuc Level
l))
  NamedArg Expr
arg : [NamedArg Expr]
_ -> 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
fsep
    [ forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
q , TCMT IO Doc
"cannot be applied to more than one argument" ]

checkSetOmega :: Comparison -> A.Expr -> Type -> QName -> IsFibrant -> Suffix -> [NamedArg A.Expr] -> TCM Term
checkSetOmega :: Comparison
-> Expr
-> Type
-> QName
-> IsFibrant
-> Suffix
-> [NamedArg Expr]
-> TCM Term
checkSetOmega Comparison
cmp Expr
e Type
t QName
q IsFibrant
f Suffix
s [NamedArg Expr]
args = do
  (Term
v, Type
t0) <- Expr
-> QName
-> IsFibrant
-> Suffix
-> [NamedArg Expr]
-> TCM (Term, Type)
inferSetOmega Expr
e QName
q IsFibrant
f Suffix
s [NamedArg Expr]
args
  forall (m :: * -> *).
(MonadConversion m, MonadTCM m) =>
Comparison -> Term -> Type -> Type -> m Term
coerce Comparison
cmp Term
v Type
t0 Type
t

inferSetOmega :: A.Expr -> QName -> IsFibrant -> Suffix -> [NamedArg A.Expr] -> TCM (Term, Type)
inferSetOmega :: Expr
-> QName
-> IsFibrant
-> Suffix
-> [NamedArg Expr]
-> TCM (Term, Type)
inferSetOmega Expr
e QName
q IsFibrant
f Suffix
suffix [NamedArg Expr]
args = do
  forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (IsFibrant
f forall a. Eq a => a -> a -> Bool
== IsFibrant
IsStrict) forall a b. (a -> b) -> a -> b
$
    forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
unlessM forall (m :: * -> *). HasOptions m => m Bool
isTwoLevelEnabled forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError TypeError
NeedOptionTwoLevel
  let n :: Integer
n = case Suffix
suffix of
            Suffix
NoSuffix -> Integer
0
            Suffix Integer
n -> Integer
n
  case [NamedArg Expr]
args of
    [] -> forall (m :: * -> *) a. Monad m => a -> m a
return (Sort -> Term
Sort (forall t. IsFibrant -> Integer -> Sort' t
Inf IsFibrant
f Integer
n) , Sort -> Type
sort (forall t. IsFibrant -> Integer -> Sort' t
Inf IsFibrant
f forall a b. (a -> b) -> a -> b
$ Integer
1 forall a. Num a => a -> a -> a
+ Integer
n))
    NamedArg Expr
arg : [NamedArg Expr]
_ -> 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
fsep
        [ forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
q , TCMT IO Doc
"cannot be applied to an argument" ]

-----------------------------------------------------------------------------
-- * Coinduction
-----------------------------------------------------------------------------

checkSharpApplication :: A.Expr -> Type -> QName -> [NamedArg A.Expr] -> TCM Term
checkSharpApplication :: Expr -> Type -> QName -> [NamedArg Expr] -> TCM Term
checkSharpApplication Expr
e Type
t QName
c [NamedArg Expr]
args = do
  Expr
arg <- case [NamedArg Expr]
args of
           [NamedArg Expr
a] | forall a. LensHiding a => a -> Bool
visible NamedArg Expr
a -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. NamedArg a -> a
namedArg NamedArg Expr
a
           [NamedArg Expr]
_ -> 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
$ forall a. Pretty a => a -> [Char]
prettyShow QName
c forall a. [a] -> [a] -> [a]
++ [Char]
" must be applied to exactly one argument."

  -- The name of the fresh function.
  Nat
i <- forall i (m :: * -> *). MonadFresh i m => m i
fresh :: TCM Int
  let name :: [Char]
name = forall a. (a -> Bool) -> [a] -> [a]
filter (forall a. Eq a => a -> a -> Bool
/= Char
'_') (forall a. Pretty a => a -> [Char]
prettyShow forall a b. (a -> b) -> a -> b
$ Name -> Name
A.nameConcrete forall a b. (a -> b) -> a -> b
$ QName -> Name
A.qnameName QName
c) forall a. [a] -> [a] -> [a]
++ [Char]
"-" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Nat
i

  CoinductionKit
kit <- TCM CoinductionKit
coinductionKit'
  let flat :: QName
flat = CoinductionKit -> QName
nameOfFlat CoinductionKit
kit
      inf :: QName
inf  = CoinductionKit -> QName
nameOfInf  CoinductionKit
kit

  -- Add the type signature of the fresh function to the
  -- signature.
  -- To make sure we can type check the generated function we have to make
  -- sure that its type is \inf. The reason for this is that we don't yet
  -- postpone checking of patterns when we don't know their types (Issue480).
  Type
forcedType <- do
    Type
lvl <- forall (m :: * -> *). (HasBuiltins m, MonadTCError m) => m Type
levelType
    (MetaId
_, Term
l) <- forall (m :: * -> *).
MonadMetaSolver m =>
RunMetaOccursCheck -> Comparison -> Type -> m (MetaId, Term)
newValueMeta RunMetaOccursCheck
RunMetaOccursCheck Comparison
CmpLeq Type
lvl
    Level
lv  <- forall (m :: * -> *). PureTCM m => Term -> m Level
levelView Term
l
    (MetaId
_, Term
a) <- forall (m :: * -> *).
MonadMetaSolver m =>
RunMetaOccursCheck -> Comparison -> Type -> m (MetaId, Term)
newValueMeta RunMetaOccursCheck
RunMetaOccursCheck Comparison
CmpEq (Sort -> Type
sort forall a b. (a -> b) -> a -> b
$ forall t. Level' t -> Sort' t
Type Level
lv)
    forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall t a. Sort' t -> a -> Type'' t a
El (forall t. Level' t -> Sort' t
Type Level
lv) forall a b. (a -> b) -> a -> b
$ QName -> Elims -> Term
Def QName
inf [forall a. Arg a -> Elim' a
Apply forall a b. (a -> b) -> a -> b
$ forall a. LensHiding a => Hiding -> a -> a
setHiding Hiding
Hidden forall a b. (a -> b) -> a -> b
$ forall e. e -> Arg e
defaultArg Term
l, forall a. Arg a -> Elim' a
Apply forall a b. (a -> b) -> a -> b
$ forall e. e -> Arg e
defaultArg Term
a]

  QName
wrapper <- forall a. TCM a -> TCM a
inFreshModuleIfFreeParams forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a.
MonadTCEnv m =>
(TCEnv -> TCEnv) -> m a -> m a
localTC (forall i o. Lens' i o -> LensSet i o
set Lens' Quantity TCEnv
eQuantity Quantity
topQuantity) forall a b. (a -> b) -> a -> b
$ do
    -- Andreas, 2019-10-12: create helper functions in non-erased mode.
    -- Otherwise, they are not usable in meta-solutions in the term world.
    QName
c' <- forall a. SetRange a => Range -> a -> a
setRange (forall a. HasRange a => a -> Range
getRange QName
c) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
            forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 ModuleName -> Name -> QName
qualify (forall a. KillRange a => KillRangeT a
killRange forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). MonadTCEnv m => m ModuleName
currentModule)
                           (forall a (m :: * -> *).
(FreshName a, MonadFresh NameId m) =>
a -> m Name
freshName_ [Char]
name)

    -- Define and type check the fresh function.
    Modality
mod <- forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
asksTC forall a. LensModality a => a -> Modality
getModality
    IsAbstract
abs <- forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
asksTC (forall o i. o -> Lens' i o -> i
^. forall a. LensIsAbstract a => Lens' IsAbstract a
lensIsAbstract)
    let info :: DefInfo' Expr
info   = forall t.
Name -> Fixity' -> Access -> IsAbstract -> Range -> DefInfo' t
A.mkDefInfo (Name -> Name
A.nameConcrete forall a b. (a -> b) -> a -> b
$ QName -> Name
A.qnameName QName
c') Fixity'
noFixity'
                             Access
PublicAccess IsAbstract
abs forall a. Range' a
noRange
        core :: LHSCore' Expr
core   = A.LHSProj { lhsDestructor :: AmbiguousQName
A.lhsDestructor = QName -> AmbiguousQName
unambiguous QName
flat
                           , lhsFocus :: NamedArg (LHSCore' Expr)
A.lhsFocus      = forall a. a -> NamedArg a
defaultNamedArg forall a b. (a -> b) -> a -> b
$ forall e. QName -> [NamedArg (Pattern' e)] -> LHSCore' e
A.LHSHead QName
c' []
                           , lhsPats :: [NamedArg (Pattern' Expr)]
A.lhsPats       = [] }
        clause :: Clause' LHS
clause = forall lhs.
lhs
-> [ProblemEq] -> RHS -> WhereDeclarations -> Bool -> Clause' lhs
A.Clause (LHSInfo -> LHSCore' Expr -> LHS
A.LHS forall a. Null a => a
empty LHSCore' Expr
core) []
                          (Expr -> Maybe Expr -> RHS
A.RHS Expr
arg forall a. Maybe a
Nothing)
                          WhereDeclarations
A.noWhereDecls Bool
False

    MutualId
i <- TCM MutualId
currentOrFreshMutualBlock

    -- If we are in irrelevant position, add definition irrelevantly.
    -- If we are in erased position, add definition as erased.
    -- TODO: is this sufficient?
    QName -> Definition -> TCM ()
addConstant QName
c' forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< do
      let ai :: ArgInfo
ai = forall a. LensModality a => Modality -> a -> a
setModality Modality
mod ArgInfo
defaultArgInfo
      Language
lang <- forall (m :: * -> *). HasOptions m => m Language
getLanguage
      Definition -> TCMT IO Definition
useTerPragma forall a b. (a -> b) -> a -> b
$
        (ArgInfo -> QName -> Type -> Language -> Defn -> Definition
defaultDefn ArgInfo
ai QName
c' Type
forcedType Language
lang Defn
emptyFunction)
        { defMutual :: MutualId
defMutual = MutualId
i }

    Delayed -> DefInfo' Expr -> QName -> [Clause' LHS] -> TCM ()
checkFunDef Delayed
NotDelayed DefInfo' Expr
info QName
c' [Clause' LHS
clause]

    forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.term.expr.coind" Nat
15 forall a b. (a -> b) -> a -> b
$ do
      Defn
def <- Definition -> Defn
theDef forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
c'
      forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat forall a b. (a -> b) -> a -> b
$
        [ TCMT IO Doc
"The coinductive wrapper"
        , forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
nest Nat
2 forall a b. (a -> b) -> a -> b
$ forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Modality
mod forall a. Semigroup a => a -> a -> a
<> (forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
c' forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
":")
        , forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
nest Nat
4 forall a b. (a -> b) -> a -> b
$ forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
t
        , forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
nest Nat
2 forall a b. (a -> b) -> a -> b
$ forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA Clause' LHS
clause
        , (TCMT IO Doc
"The definition is" 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
$ Defn -> Delayed
funDelayed Defn
def)) forall a. Semigroup a => a -> a -> a
<>
          TCMT IO Doc
"."
        ]
    forall (m :: * -> *) a. Monad m => a -> m a
return QName
c'

  -- The application of the fresh function to the relevant
  -- arguments.
  Term
e' <- QName -> Elims -> Term
Def QName
wrapper forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map forall a. Arg a -> Elim' a
Apply forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Args
getContextArgs

  forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.term.expr.coind" Nat
15 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
"The coinductive constructor application"
      , forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
nest Nat
2 forall a b. (a -> b) -> a -> b
$ forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Expr
e
      , TCMT IO Doc
"was translated into the application"
      , forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
nest Nat
2 forall a b. (a -> b) -> a -> b
$ forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
e'
      ]

  forall (m :: * -> *).
(MonadMetaSolver m, MonadConstraint m, MonadFresh Nat m,
 MonadFresh ProblemId m) =>
Type -> m Term -> m Term
blockTerm Type
t forall a b. (a -> b) -> a -> b
$ Term
e' forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ forall (m :: * -> *) a.
(MonadTCEnv m, HasOptions m, MonadDebug m) =>
m a -> m a
workOnTypes (forall (m :: * -> *). MonadConversion m => Type -> Type -> m ()
leqType Type
forcedType Type
t)

-----------------------------------------------------------------------------
-- * Cubical
-----------------------------------------------------------------------------

-- | "pathAbs (PathView s _ l a x y) t" builds "(\ t) : pv"
--   Preconditions: PathView is PathType, and t[i0] = x, t[i1] = y
pathAbs :: PathView -> Abs Term -> TCM Term
pathAbs :: PathView -> Abs Term -> TCM Term
pathAbs (OType Type
_) Abs Term
t = forall a. HasCallStack => a
__IMPOSSIBLE__
pathAbs (PathType Sort
s QName
path Arg Term
l Arg Term
a Arg Term
x Arg Term
y) Abs Term
t = do
  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ ArgInfo -> Abs Term -> Term
Lam ArgInfo
defaultArgInfo Abs Term
t

-- | @primComp : ∀ {ℓ} (A : (i : I) → Set (ℓ i)) (φ : I) (u : ∀ i → Partial φ (A i)) (a : A i0) → A i1@
--
--   Check:  @u i0 = (λ _ → a) : Partial φ (A i0)@.
--
checkPrimComp :: QName -> MaybeRanges -> Args -> Type -> TCM Args
checkPrimComp :: QName -> MaybeRanges -> Args -> Type -> TCM Args
checkPrimComp QName
c MaybeRanges
rs Args
vs Type
_ = do
  case Args
vs of
    -- WAS: [l, a, phi, u, a0] -> do
    Arg Term
l : Arg Term
a : Arg Term
phi : Arg Term
u : Arg Term
a0 : Args
rest -> do
      Arg Term
iz <- forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
defaultArgInfo forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasBuiltins m => IntervalView -> m Term
intervalUnview IntervalView
IZero
      let lz :: Term
lz = forall e. Arg e -> e
unArg Arg Term
l forall t. Apply t => t -> Args -> t
`apply` [Arg Term
iz]
          az :: Term
az = forall e. Arg e -> e
unArg Arg Term
a forall t. Apply t => t -> Args -> t
`apply` [Arg Term
iz]
      Type
ty <- forall (m :: * -> *). Applicative m => m Term -> m Term -> m Type
el's (forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall e. Arg e -> e
unArg Arg Term
l forall t. Apply t => t -> Args -> t
`apply` [Arg Term
iz])) forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primPartial forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall e. Arg e -> e
unArg Arg Term
l forall t. Apply t => t -> Args -> t
`apply` [Arg Term
iz]) forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall e. Arg e -> e
unArg Arg Term
phi) forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall e. Arg e -> e
unArg Arg Term
a forall t. Apply t => t -> Args -> t
`apply` [Arg Term
iz])
      Type
bAz <- forall (m :: * -> *). Applicative m => m Term -> m Term -> m Type
el' (forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ Term
lz) (forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ Term
az)
      Arg Term
a0 <- forall r.
HasRange r =>
Type -> r -> Arg Term -> TCM () -> TCMT IO (Arg Term)
blockArg Type
bAz (MaybeRanges
rs forall a. [a] -> Nat -> Maybe a
!!! Nat
4) Arg Term
a0 forall a b. (a -> b) -> a -> b
$ do
        forall (m :: * -> *).
MonadConversion m =>
Type -> Term -> Term -> m ()
equalTerm Type
ty -- (El (getSort t1) (apply (unArg a) [iz]))
          (ArgInfo -> Abs Term -> Term
Lam ArgInfo
defaultArgInfo forall a b. (a -> b) -> a -> b
$ forall a. [Char] -> a -> Abs a
NoAbs [Char]
"_" forall a b. (a -> b) -> a -> b
$ forall e. Arg e -> e
unArg Arg Term
a0)
          (forall t. Apply t => t -> Args -> t
apply (forall e. Arg e -> e
unArg Arg Term
u) [Arg Term
iz])
      forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Arg Term
l forall a. a -> [a] -> [a]
: Arg Term
a forall a. a -> [a] -> [a]
: Arg Term
phi forall a. a -> [a] -> [a]
: Arg Term
u forall a. a -> [a] -> [a]
: Arg Term
a0 forall a. a -> [a] -> [a]
: Args
rest
    Args
_ -> 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 a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
c forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
"must be fully applied"

-- | @primHComp : ∀ {ℓ} {A : Set ℓ} {φ : I} (u : ∀ i → Partial φ A) (a : A) → A@
--
--   Check:  @u i0 = (λ _ → a) : Partial φ A@.
--
checkPrimHComp :: QName -> MaybeRanges -> Args -> Type -> TCM Args
checkPrimHComp :: QName -> MaybeRanges -> Args -> Type -> TCM Args
checkPrimHComp QName
c MaybeRanges
rs Args
vs Type
_ = do
  case Args
vs of
    -- WAS: [l, a, phi, u, a0] -> do
    Arg Term
l : Arg Term
a : Arg Term
phi : Arg Term
u : Arg Term
a0 : Args
rest -> do
      -- iz = i0
      Arg Term
iz <- forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
defaultArgInfo forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasBuiltins m => IntervalView -> m Term
intervalUnview IntervalView
IZero
      -- ty = Partial φ A
      Type
ty <- forall (m :: * -> *). Applicative m => m Term -> m Term -> m Type
el's (forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall e. Arg e -> e
unArg Arg Term
l)) forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primPartial forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall e. Arg e -> e
unArg Arg Term
l) forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall e. Arg e -> e
unArg Arg Term
phi) forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall e. Arg e -> e
unArg Arg Term
a)
      -- (λ _ → a) = u i0 : ty
      Type
bA <- forall (m :: * -> *). Applicative m => m Term -> m Term -> m Type
el' (forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall e. Arg e -> e
unArg Arg Term
l) (forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall e. Arg e -> e
unArg Arg Term
a)
      Arg Term
a0 <- forall r.
HasRange r =>
Type -> r -> Arg Term -> TCM () -> TCMT IO (Arg Term)
blockArg Type
bA (MaybeRanges
rs forall a. [a] -> Nat -> Maybe a
!!! Nat
4) Arg Term
a0 forall a b. (a -> b) -> a -> b
$ do
        forall (m :: * -> *).
MonadConversion m =>
Type -> Term -> Term -> m ()
equalTerm Type
ty -- (El (getSort t1) (apply (unArg a) [iz]))
            (ArgInfo -> Abs Term -> Term
Lam ArgInfo
defaultArgInfo forall a b. (a -> b) -> a -> b
$ forall a. [Char] -> a -> Abs a
NoAbs [Char]
"_" forall a b. (a -> b) -> a -> b
$ forall e. Arg e -> e
unArg Arg Term
a0)
            (forall t. Apply t => t -> Args -> t
apply (forall e. Arg e -> e
unArg Arg Term
u) [Arg Term
iz])
      forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Arg Term
l forall a. a -> [a] -> [a]
: Arg Term
a forall a. a -> [a] -> [a]
: Arg Term
phi forall a. a -> [a] -> [a]
: Arg Term
u forall a. a -> [a] -> [a]
: Arg Term
a0 forall a. a -> [a] -> [a]
: Args
rest
    Args
_ -> 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 a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
c forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
"must be fully applied"

-- | @transp : ∀{ℓ} (A : (i : I) → Set (ℓ i)) (φ : I) (a0 : A i0) → A i1@
--
--   Check:  If φ, then @A i = A i0 : Set (ℓ i)@ must hold for all @i : I@.
--
checkPrimTrans :: QName -> MaybeRanges -> Args -> Type -> TCM Args
checkPrimTrans :: QName -> MaybeRanges -> Args -> Type -> TCM Args
checkPrimTrans QName
c MaybeRanges
rs Args
vs Type
_ = do
  case Args
vs of
    -- Andreas, 2019-03-02, issue #3601, why exactly 4 arguments?
    -- Only 3 are needed to check the side condition.
    -- WAS:
    -- [l, a, phi, a0] -> do
    Arg Term
l : Arg Term
a : Arg Term
phi : Args
rest -> do
      Arg Term
iz <- forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
defaultArgInfo forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasBuiltins m => IntervalView -> m Term
intervalUnview IntervalView
IZero
      -- ty = (i : I) -> Set (l i)
      Type
ty <- forall (m :: * -> *) a. [[Char]] -> NamesT m a -> m a
runNamesT [] forall a b. (a -> b) -> a -> b
$ do
        NamesT (TCMT IO) Term
l <- forall (m :: * -> *) a.
(MonadFail m, Subst a) =>
a -> NamesT m (NamesT m a)
open forall a b. (a -> b) -> a -> b
$ forall e. Arg e -> e
unArg Arg Term
l
        forall (m :: * -> *).
(MonadFail m, MonadAddContext m, MonadDebug m) =>
[Char]
-> NamesT m Type
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
nPi' [Char]
"i" forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Type
primIntervalType forall a b. (a -> b) -> a -> b
$ \ NamesT (TCMT IO) Term
i -> (Sort -> Type
sort forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term -> Sort
tmSort forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (NamesT (TCMT IO) Term
l forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT (TCMT IO) Term
i))
      Arg Term
a <- forall r.
HasRange r =>
Type -> r -> Arg Term -> TCM () -> TCMT IO (Arg Term)
blockArg Type
ty (MaybeRanges
rs forall a. [a] -> Nat -> Maybe a
!!! Nat
1) Arg Term
a forall a b. (a -> b) -> a -> b
$ do
        forall (m :: * -> *).
MonadConversion m =>
Term -> Type -> Term -> Term -> m ()
equalTermOnFace (forall e. Arg e -> e
unArg Arg Term
phi) Type
ty
          (forall e. Arg e -> e
unArg Arg Term
a)
          (ArgInfo -> Abs Term -> Term
Lam ArgInfo
defaultArgInfo forall a b. (a -> b) -> a -> b
$ forall a. [Char] -> a -> Abs a
NoAbs [Char]
"_" forall a b. (a -> b) -> a -> b
$ forall t. Apply t => t -> Args -> t
apply (forall e. Arg e -> e
unArg Arg Term
a) [Arg Term
iz])
      forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Arg Term
l forall a. a -> [a] -> [a]
: Arg Term
a forall a. a -> [a] -> [a]
: Arg Term
phi forall a. a -> [a] -> [a]
: Args
rest
    Args
_ -> 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 a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
c forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
"must be fully applied"

blockArg :: HasRange r => Type -> r -> Arg Term -> TCM () -> TCM (Arg Term)
blockArg :: forall r.
HasRange r =>
Type -> r -> Arg Term -> TCM () -> TCMT IO (Arg Term)
blockArg Type
t r
r Arg Term
a TCM ()
m =
  forall (m :: * -> *) x a.
(MonadTrace m, HasRange x) =>
x -> m a -> m a
setCurrentRange (forall a. HasRange a => a -> Range
getRange forall a b. (a -> b) -> a -> b
$ r
r) forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Arg Term
a forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$>) forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
(MonadMetaSolver m, MonadConstraint m, MonadFresh Nat m,
 MonadFresh ProblemId m) =>
Type -> m Term -> m Term
blockTerm Type
t forall a b. (a -> b) -> a -> b
$ TCM ()
m forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall (m :: * -> *) a. Monad m => a -> m a
return (forall e. Arg e -> e
unArg Arg Term
a)

checkConId :: QName -> MaybeRanges -> Args -> Type -> TCM Args
checkConId :: QName -> MaybeRanges -> Args -> Type -> TCM Args
checkConId QName
c MaybeRanges
rs Args
vs Type
t1 = do
  case Args
vs of
   args :: Args
args@[Arg Term
_, Arg Term
_, Arg Term
_, Arg Term
_, Arg Term
phi, Arg Term
p] -> do
      iv :: PathView
iv@(PathType Sort
s QName
_ Arg Term
l Arg Term
a Arg Term
x Arg Term
y) <- forall (m :: * -> *). HasBuiltins m => Type -> m PathView
idViewAsPath Type
t1
      let ty :: Type
ty = PathView -> Type
pathUnview PathView
iv
      -- the following duplicates reduction of phi
      Term
const_x <- forall (m :: * -> *).
(MonadMetaSolver m, MonadConstraint m, MonadFresh Nat m,
 MonadFresh ProblemId m) =>
Type -> m Term -> m Term
blockTerm Type
ty forall a b. (a -> b) -> a -> b
$ do
          forall (m :: * -> *).
MonadConversion m =>
Term -> Type -> Term -> Term -> m ()
equalTermOnFace (forall e. Arg e -> e
unArg Arg Term
phi) (forall t a. Sort' t -> a -> Type'' t a
El Sort
s (forall e. Arg e -> e
unArg Arg Term
a)) (forall e. Arg e -> e
unArg Arg Term
x) (forall e. Arg e -> e
unArg Arg Term
y)
          PathView -> Abs Term -> TCM Term
pathAbs PathView
iv (forall a. [Char] -> a -> Abs a
NoAbs ([Char] -> [Char]
stringToArgName [Char]
"_") (forall e. Arg e -> e
unArg Arg Term
x))
      Arg Term
p <- forall r.
HasRange r =>
Type -> r -> Arg Term -> TCM () -> TCMT IO (Arg Term)
blockArg Type
ty (MaybeRanges
rs forall a. [a] -> Nat -> Maybe a
!!! Nat
5) Arg Term
p forall a b. (a -> b) -> a -> b
$ do
        forall (m :: * -> *).
MonadConversion m =>
Term -> Type -> Term -> Term -> m ()
equalTermOnFace (forall e. Arg e -> e
unArg Arg Term
phi) Type
ty (forall e. Arg e -> e
unArg Arg Term
p) Term
const_x   -- G, phi |- p = \ i . x
      forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. [a] -> [a] -> [a]
initWithDefault forall a. HasCallStack => a
__IMPOSSIBLE__ Args
args forall a. [a] -> [a] -> [a]
++ [Arg Term
p]
      -- phi <- reduce phi
      -- forallFaceMaps (unArg phi) $ \ alpha -> do
      --   iv@(PathType s _ l a x y) <- idViewAsPath (applySubst alpha t1)
      --   let ty = pathUnview iv
      --   equalTerm (El s (unArg a)) (unArg x) (unArg y) -- precondition for cx being well-typed at ty
      --   cx <- pathAbs iv (NoAbs (stringToArgName "_") (applySubst alpha (unArg x)))
      --   equalTerm ty (applySubst alpha (unArg p)) cx   -- G, phi |- p = \ i . x
   Args
_ -> 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 a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
c forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
"must be fully applied"


-- The following comment contains silly ' escapes to calm CPP about ∨ (\vee).
-- May not be haddock-parseable.

-- ' @primPOr : ∀ {ℓ} (φ₁ φ₂ : I) {A : Partial (φ₁ ∨ φ₂) (Set ℓ)}
-- '         → (u : PartialP φ₁ (λ (o : IsOne φ₁) → A (IsOne1 φ₁ φ₂ o)))
-- '         → (v : PartialP φ₂ (λ (o : IsOne φ₂) → A (IsOne2 φ₁ φ₂ o)))
-- '         → PartialP (φ₁ ∨ φ₂) A@
-- '
-- ' Checks: @u = v : PartialP (φ₁ ∨ φ₂) A@ whenever @IsOne (φ₁ ∧ φ₂)@.
checkPOr :: QName -> MaybeRanges -> Args -> Type -> TCM Args
checkPOr :: QName -> MaybeRanges -> Args -> Type -> TCM Args
checkPOr QName
c MaybeRanges
rs Args
vs Type
_ = do
  case Args
vs of
   Arg Term
l : Arg Term
phi1 : Arg Term
phi2 : Arg Term
a : Arg Term
u : Arg Term
v : Args
rest -> do
      Term
phi <- forall (m :: * -> *). HasBuiltins m => IntervalView -> m Term
intervalUnview (Arg Term -> Arg Term -> IntervalView
IMin Arg Term
phi1 Arg Term
phi2)
      forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.term.por" Nat
10 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). Applicative m => [Char] -> m Doc
text (forall a. Show a => a -> [Char]
show Term
phi)
      -- phi <- reduce phi
      -- alphas <- toFaceMaps phi
      -- reportSDoc "tc.term.por" 10 $ text (show alphas)
      Type
t1 <- forall (m :: * -> *) a. [[Char]] -> NamesT m a -> m a
runNamesT [] forall a b. (a -> b) -> a -> b
$ do
             [NamesT (TCMT IO) Term
l,NamesT (TCMT IO) Term
a] <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (forall (m :: * -> *) a.
(MonadFail m, Subst a) =>
a -> NamesT m (NamesT m a)
open forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall e. Arg e -> e
unArg) [Arg Term
l,Arg Term
a]
             NamesT (TCMT IO) Term
psi <- forall (m :: * -> *) a.
(MonadFail m, Subst a) =>
a -> NamesT m (NamesT m a)
open forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (m :: * -> *). HasBuiltins m => IntervalView -> m Term
intervalUnview (Arg Term -> Arg Term -> IntervalView
IMax Arg Term
phi1 Arg Term
phi2)
             forall (m :: * -> *).
(MonadAddContext m, HasBuiltins m, MonadDebug m) =>
[Char]
-> NamesT m Term
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
pPi' [Char]
"o" NamesT (TCMT IO) Term
psi forall a b. (a -> b) -> a -> b
$ \ NamesT (TCMT IO) Term
o -> forall (m :: * -> *). Applicative m => m Term -> m Term -> m Type
el' NamesT (TCMT IO) Term
l (NamesT (TCMT IO) Term
a forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<..> NamesT (TCMT IO) Term
o)
      Type
tv <- forall (m :: * -> *) a. [[Char]] -> NamesT m a -> m a
runNamesT [] forall a b. (a -> b) -> a -> b
$ do
             [NamesT (TCMT IO) Term
l,NamesT (TCMT IO) Term
a,NamesT (TCMT IO) Term
phi1,NamesT (TCMT IO) Term
phi2] <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (forall (m :: * -> *) a.
(MonadFail m, Subst a) =>
a -> NamesT m (NamesT m a)
open forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall e. Arg e -> e
unArg) [Arg Term
l,Arg Term
a,Arg Term
phi1,Arg Term
phi2]
             forall (m :: * -> *).
(MonadAddContext m, HasBuiltins m, MonadDebug m) =>
[Char]
-> NamesT m Term
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
pPi' [Char]
"o" NamesT (TCMT IO) Term
phi2 forall a b. (a -> b) -> a -> b
$ \ NamesT (TCMT IO) Term
o -> forall (m :: * -> *). Applicative m => m Term -> m Term -> m Type
el' NamesT (TCMT IO) Term
l (NamesT (TCMT IO) Term
a forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<..> (forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primIsOne2 forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT (TCMT IO) Term
phi1 forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT (TCMT IO) Term
phi2 forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT (TCMT IO) Term
o))
      Arg Term
v <- forall r.
HasRange r =>
Type -> r -> Arg Term -> TCM () -> TCMT IO (Arg Term)
blockArg Type
tv (MaybeRanges
rs forall a. [a] -> Nat -> Maybe a
!!! Nat
5) Arg Term
v forall a b. (a -> b) -> a -> b
$ do
        -- ' φ₁ ∧ φ₂  ⊢ u , v : PartialP (φ₁ ∨ φ₂) \ o → a o
        forall (m :: * -> *).
MonadConversion m =>
Term -> Type -> Term -> Term -> m ()
equalTermOnFace Term
phi Type
t1 (forall e. Arg e -> e
unArg Arg Term
u) (forall e. Arg e -> e
unArg Arg Term
v)
      forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Arg Term
l forall a. a -> [a] -> [a]
: Arg Term
phi1 forall a. a -> [a] -> [a]
: Arg Term
phi2 forall a. a -> [a] -> [a]
: Arg Term
a forall a. a -> [a] -> [a]
: Arg Term
u forall a. a -> [a] -> [a]
: Arg Term
v forall a. a -> [a] -> [a]
: Args
rest
   Args
_ -> 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 a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
c forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
"must be fully applied"

-- | @prim^glue : ∀ {ℓ ℓ'} {A : Set ℓ} {φ : I}
--              → {T : Partial φ (Set ℓ')} → {e : PartialP φ (λ o → T o ≃ A)}
--              → (t : PartialP φ T) → (a : A) → primGlue A T e@
--
--   Check   @φ ⊢ a = e 1=1 (t 1=1)@  or actually the equivalent:  @(\ _ → a) = (\ o -> e o (t o)) : PartialP φ A@
check_glue :: QName -> MaybeRanges -> Args -> Type -> TCM Args
check_glue :: QName -> MaybeRanges -> Args -> Type -> TCM Args
check_glue QName
c MaybeRanges
rs Args
vs Type
_ = do
  case Args
vs of
   -- WAS: [la, lb, bA, phi, bT, e, t, a] -> do
   Arg Term
la : Arg Term
lb : Arg Term
bA : Arg Term
phi : Arg Term
bT : Arg Term
e : Arg Term
t : Arg Term
a : Args
rest -> do
      let iinfo :: ArgInfo
iinfo = forall a. LensRelevance a => Relevance -> a -> a
setRelevance Relevance
Irrelevant ArgInfo
defaultArgInfo
      Term
v <- forall (m :: * -> *) a. [[Char]] -> NamesT m a -> m a
runNamesT [] forall a b. (a -> b) -> a -> b
$ do
            [NamesT (TCMT IO) Term
lb, NamesT (TCMT IO) Term
la, NamesT (TCMT IO) Term
bA, NamesT (TCMT IO) Term
phi, NamesT (TCMT IO) Term
bT, NamesT (TCMT IO) Term
e, NamesT (TCMT IO) Term
t] <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (forall (m :: * -> *) a.
(MonadFail m, Subst a) =>
a -> NamesT m (NamesT m a)
open forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall e. Arg e -> e
unArg) [Arg Term
lb, Arg Term
la, Arg Term
bA, Arg Term
phi, Arg Term
bT, Arg Term
e, Arg Term
t]
            let f :: NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
f NamesT (TCMT IO) Term
o = forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primEquivFun forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> NamesT (TCMT IO) Term
lb forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> NamesT (TCMT IO) Term
la forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> (NamesT (TCMT IO) Term
bT forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<..> NamesT (TCMT IO) Term
o) forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> NamesT (TCMT IO) Term
bA forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> (NamesT (TCMT IO) Term
e forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<..> NamesT (TCMT IO) Term
o)
            forall (m :: * -> *).
MonadFail m =>
ArgInfo
-> [Char] -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
glam ArgInfo
iinfo [Char]
"o" forall a b. (a -> b) -> a -> b
$ \ NamesT (TCMT IO) Term
o -> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
f NamesT (TCMT IO) Term
o forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> (NamesT (TCMT IO) Term
t forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<..> NamesT (TCMT IO) Term
o)
      Type
ty <- forall (m :: * -> *) a. [[Char]] -> NamesT m a -> m a
runNamesT [] forall a b. (a -> b) -> a -> b
$ do
            [NamesT (TCMT IO) Term
lb, NamesT (TCMT IO) Term
phi, NamesT (TCMT IO) Term
bA] <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (forall (m :: * -> *) a.
(MonadFail m, Subst a) =>
a -> NamesT m (NamesT m a)
open forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall e. Arg e -> e
unArg) [Arg Term
lb, Arg Term
phi, Arg Term
bA]
            forall (m :: * -> *). Applicative m => m Term -> m Term -> m Type
el's NamesT (TCMT IO) Term
lb forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primPartialP forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> NamesT (TCMT IO) Term
lb forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT (TCMT IO) Term
phi forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> forall (m :: * -> *).
MonadFail m =>
ArgInfo
-> [Char] -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
glam ArgInfo
iinfo [Char]
"o" (\ NamesT (TCMT IO) Term
_ -> NamesT (TCMT IO) Term
bA)
      let a' :: Term
a' = ArgInfo -> Abs Term -> Term
Lam ArgInfo
iinfo (forall a. [Char] -> a -> Abs a
NoAbs [Char]
"o" forall a b. (a -> b) -> a -> b
$ forall e. Arg e -> e
unArg Arg Term
a)
      Type
ta <- forall (m :: * -> *). Applicative m => m Term -> m Term -> m Type
el' (forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall e. Arg e -> e
unArg Arg Term
la) (forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall e. Arg e -> e
unArg Arg Term
bA)
      Arg Term
a <- forall r.
HasRange r =>
Type -> r -> Arg Term -> TCM () -> TCMT IO (Arg Term)
blockArg Type
ta (MaybeRanges
rs forall a. [a] -> Nat -> Maybe a
!!! Nat
7) Arg Term
a forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
MonadConversion m =>
Type -> Term -> Term -> m ()
equalTerm Type
ty Term
a' Term
v
      forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Arg Term
la forall a. a -> [a] -> [a]
: Arg Term
lb forall a. a -> [a] -> [a]
: Arg Term
bA forall a. a -> [a] -> [a]
: Arg Term
phi forall a. a -> [a] -> [a]
: Arg Term
bT forall a. a -> [a] -> [a]
: Arg Term
e forall a. a -> [a] -> [a]
: Arg Term
t forall a. a -> [a] -> [a]
: Arg Term
a forall a. a -> [a] -> [a]
: Args
rest
   Args
_ -> 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 a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
c forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
"must be fully applied"


-- | @prim^glueU : ∀ {ℓ} {φ : I}
--              → {T : I → Partial φ (Set ℓ)} → {A : Set ℓ [ φ ↦ T i0 ]}
--              → (t : PartialP φ (T i1)) → (a : outS A) → hcomp T (outS A)@
--
--   Check   @φ ⊢ a = transp (\ i -> T 1=1 (~ i)) i0 (t 1=1)@  or actually the equivalent:
--           @(\ _ → a) = (\o -> transp (\ i -> T o (~ i)) i0 (t o)) : PartialP φ (T i0)@
check_glueU :: QName -> MaybeRanges -> Args -> Type -> TCM Args
check_glueU :: QName -> MaybeRanges -> Args -> Type -> TCM Args
check_glueU QName
c MaybeRanges
rs Args
vs Type
_ = do
  case Args
vs of
   -- WAS: [la, lb, bA, phi, bT, e, t, a] -> do
   Arg Term
la : Arg Term
phi : Arg Term
bT : Arg Term
bA : Arg Term
t : Arg Term
a : Args
rest -> do
      let iinfo :: ArgInfo
iinfo = forall a. LensRelevance a => Relevance -> a -> a
setRelevance Relevance
Irrelevant ArgInfo
defaultArgInfo
      Term
v <- forall (m :: * -> *) a. [[Char]] -> NamesT m a -> m a
runNamesT [] forall a b. (a -> b) -> a -> b
$ do
            [NamesT (TCMT IO) Term
la, NamesT (TCMT IO) Term
phi, NamesT (TCMT IO) Term
bT, NamesT (TCMT IO) Term
bA, NamesT (TCMT IO) Term
t] <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (forall (m :: * -> *) a.
(MonadFail m, Subst a) =>
a -> NamesT m (NamesT m a)
open forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall e. Arg e -> e
unArg) [Arg Term
la, Arg Term
phi, Arg Term
bT, Arg Term
bA, Arg Term
t]
            let f :: NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
f NamesT (TCMT IO) Term
o = forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primTrans forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> forall (m :: * -> *).
MonadFail m =>
[Char] -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
lam [Char]
"i" (forall a b. a -> b -> a
const NamesT (TCMT IO) Term
la) forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> forall (m :: * -> *).
MonadFail m =>
[Char] -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
lam [Char]
"i" (\ NamesT (TCMT IO) Term
i -> NamesT (TCMT IO) Term
bT forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> (forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primINeg forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT (TCMT IO) Term
i) forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<..> NamesT (TCMT IO) Term
o) forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primIZero
            forall (m :: * -> *).
MonadFail m =>
ArgInfo
-> [Char] -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
glam ArgInfo
iinfo [Char]
"o" forall a b. (a -> b) -> a -> b
$ \ NamesT (TCMT IO) Term
o -> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
f NamesT (TCMT IO) Term
o forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> (NamesT (TCMT IO) Term
t forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<..> NamesT (TCMT IO) Term
o)
      Type
ty <- forall (m :: * -> *) a. [[Char]] -> NamesT m a -> m a
runNamesT [] forall a b. (a -> b) -> a -> b
$ do
            [NamesT (TCMT IO) Term
la, NamesT (TCMT IO) Term
phi, NamesT (TCMT IO) Term
bT] <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (forall (m :: * -> *) a.
(MonadFail m, Subst a) =>
a -> NamesT m (NamesT m a)
open forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall e. Arg e -> e
unArg) [Arg Term
la, Arg Term
phi, Arg Term
bT]
            forall (m :: * -> *).
(MonadAddContext m, HasBuiltins m, MonadDebug m) =>
[Char]
-> NamesT m Term
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
pPi' [Char]
"o" NamesT (TCMT IO) Term
phi forall a b. (a -> b) -> a -> b
$ \ NamesT (TCMT IO) Term
o -> forall (m :: * -> *). Applicative m => m Term -> m Term -> m Type
el' NamesT (TCMT IO) Term
la (NamesT (TCMT IO) Term
bT forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primIZero forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<..> NamesT (TCMT IO) Term
o)
      let a' :: Term
a' = ArgInfo -> Abs Term -> Term
Lam ArgInfo
iinfo (forall a. [Char] -> a -> Abs a
NoAbs [Char]
"o" forall a b. (a -> b) -> a -> b
$ forall e. Arg e -> e
unArg Arg Term
a)
      Type
ta <- forall (m :: * -> *) a. [[Char]] -> NamesT m a -> m a
runNamesT [] forall a b. (a -> b) -> a -> b
$ do
            [NamesT (TCMT IO) Term
la, NamesT (TCMT IO) Term
phi, NamesT (TCMT IO) Term
bT, NamesT (TCMT IO) Term
bA] <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (forall (m :: * -> *) a.
(MonadFail m, Subst a) =>
a -> NamesT m (NamesT m a)
open forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall e. Arg e -> e
unArg) [Arg Term
la, Arg Term
phi, Arg Term
bT, Arg Term
bA]
            forall (m :: * -> *). Applicative m => m Term -> m Term -> m Type
el' NamesT (TCMT IO) Term
la (forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primSubOut forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> (forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primLevelSuc forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT (TCMT IO) Term
la) forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> (Sort -> Term
Sort forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term -> Sort
tmSort forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> NamesT (TCMT IO) Term
la) forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> NamesT (TCMT IO) Term
phi forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> (NamesT (TCMT IO) Term
bT forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primIZero) forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT (TCMT IO) Term
bA)
      Arg Term
a <- forall r.
HasRange r =>
Type -> r -> Arg Term -> TCM () -> TCMT IO (Arg Term)
blockArg Type
ta (MaybeRanges
rs forall a. [a] -> Nat -> Maybe a
!!! Nat
5) Arg Term
a forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
MonadConversion m =>
Type -> Term -> Term -> m ()
equalTerm Type
ty Term
a' Term
v
      forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Arg Term
la forall a. a -> [a] -> [a]
: Arg Term
phi forall a. a -> [a] -> [a]
: Arg Term
bT forall a. a -> [a] -> [a]
: Arg Term
bA forall a. a -> [a] -> [a]
: Arg Term
t forall a. a -> [a] -> [a]
: Arg Term
a forall a. a -> [a] -> [a]
: Args
rest
   Args
_ -> 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 a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
c forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
"must be fully applied"