{-# LANGUAGE NondecreasingIndentation #-}

module Agda.TypeChecking.Rules.Application
  ( checkArguments
  , checkArguments_
  , checkApplication
  , inferApplication
  , checkProjAppToKnownPrincipalArg
  , disambiguateConstructor'
  , univChecks
  , suffixToLevel
  ) where

import Prelude hiding ( null )

import Control.Applicative        ( (<|>) )
import Control.Monad.Except       ( ExceptT, runExceptT, MonadError, catchError, throwError )
import Control.Monad.Trans.Maybe

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 qualified Agda.Syntax.Abstract as A
import Agda.Syntax.Abstract.Pattern (patternToExpr)
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.Implicit
import Agda.TypeChecking.Injectivity
import Agda.TypeChecking.InstanceArguments (postponeInstanceConstraints)
import Agda.TypeChecking.Level
import Agda.TypeChecking.MetaVars
import Agda.TypeChecking.Modalities
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.TypeChecking.Warnings (warning)

import Agda.Utils.Either
import Agda.Utils.Function
import Agda.Utils.Functor
import Agda.Utils.Lens
import Agda.Utils.List hiding (Suffix)
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.Syntax.Common.Pretty ( prettyShow )
import Agda.Utils.Size
import Agda.Utils.Tuple
import qualified Agda.Utils.VarSet as VarSet

import Agda.Utils.Impossible
import Agda.Utils.Singleton (singleton)

---------------------------------------------------------------------------
-- * Data structures for checking arguments
---------------------------------------------------------------------------

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

setACElims :: [Elim] -> ArgsCheckState a -> ArgsCheckState a
setACElims :: forall a. [Elim' Term] -> ArgsCheckState a -> ArgsCheckState a
setACElims [Elim' Term]
es ArgsCheckState a
st = ArgsCheckState a
st{ acCheckedArgs = go es (acCheckedArgs st) }
  where
    go :: [Elim' Term] -> [CheckedArg] -> [CheckedArg]
go [] [] = []
    go (Elim' Term
e : [Elim' Term]
es) (CheckedArg
ca : [CheckedArg]
cas) = CheckedArg
ca{ caElim = e } CheckedArg -> [CheckedArg] -> [CheckedArg]
forall a. a -> [a] -> [a]
: [Elim' Term] -> [CheckedArg] -> [CheckedArg]
go [Elim' Term]
es [CheckedArg]
cas
    go [Elim' Term]
_ [CheckedArg]
_ = [CheckedArg]
forall a. HasCallStack => a
__IMPOSSIBLE__

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

-- | Extract the "head constraints" (currently lock constraints 'CheckLockedVars')
--   from the application checker (final) state.
acHeadConstraints :: (Elims -> Term) -> ArgsCheckState a -> [Constraint]
acHeadConstraints :: forall a.
([Elim' Term] -> Term) -> ArgsCheckState a -> [Constraint]
acHeadConstraints [Elim' Term] -> Term
hd = ([Elim' Term] -> Term) -> [CheckedArg] -> [Constraint]
go [Elim' Term] -> Term
hd ([CheckedArg] -> [Constraint])
-> (ArgsCheckState a -> [CheckedArg])
-> ArgsCheckState a
-> [Constraint]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ArgsCheckState a -> [CheckedArg]
forall a. ArgsCheckState a -> [CheckedArg]
acCheckedArgs
  where
    go :: (Elims -> Term) -> [CheckedArg] -> [Constraint]
    go :: ([Elim' Term] -> Term) -> [CheckedArg] -> [Constraint]
go [Elim' Term] -> Term
hd = \case
      [] -> []
      CheckedArg Elim' Term
e Range
_ Maybe (Abs Constraint)
mc : [CheckedArg]
cas -> Maybe (Abs Constraint)
-> (Abs Constraint -> [Constraint] -> [Constraint])
-> [Constraint]
-> [Constraint]
forall b a. Maybe b -> (b -> a -> a) -> a -> a
applyWhenJust Maybe (Abs Constraint)
mc (\ Abs Constraint
c -> (Abs Constraint -> SubstArg Constraint -> Constraint
forall a. Subst a => Abs a -> SubstArg a -> a
lazyAbsApp Abs Constraint
c ([Elim' Term] -> Term
hd []) Constraint -> [Constraint] -> [Constraint]
forall a. a -> [a] -> [a]
:)) ([Constraint] -> [Constraint]) -> [Constraint] -> [Constraint]
forall a b. (a -> b) -> a -> b
$
        ([Elim' Term] -> Term) -> [CheckedArg] -> [Constraint]
go ([Elim' Term] -> Term
hd ([Elim' Term] -> Term)
-> ([Elim' Term] -> [Elim' Term]) -> [Elim' Term] -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Elim' Term
e Elim' Term -> [Elim' Term] -> [Elim' Term]
forall a. a -> [a] -> [a]
:)) [CheckedArg]
cas

-- | Check the "head constraints" (currently lock constraints 'CheckLockedVars')
--   accumulated during checking of an application.
checkHeadConstraints :: (Elims -> Term) -> ArgsCheckState a -> TCM Term
checkHeadConstraints :: forall a. ([Elim' Term] -> Term) -> ArgsCheckState a -> TCM Term
checkHeadConstraints [Elim' Term] -> Term
hd ArgsCheckState a
st = do
  (Constraint -> TCMT IO ()) -> [Constraint] -> TCMT IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ Constraint -> TCMT IO ()
solveConstraint_ ([Constraint] -> TCMT IO ()) -> [Constraint] -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ ([Elim' Term] -> Term) -> ArgsCheckState a -> [Constraint]
forall a.
([Elim' Term] -> Term) -> ArgsCheckState a -> [Constraint]
acHeadConstraints [Elim' Term] -> Term
hd ArgsCheckState a
st
  Term -> TCM Term
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> TCM Term) -> Term -> TCM Term
forall a b. (a -> b) -> a -> b
$ [Elim' Term] -> Term
hd ([Elim' Term] -> Term) -> [Elim' Term] -> Term
forall a b. (a -> b) -> a -> b
$ (CheckedArg -> Elim' Term) -> [CheckedArg] -> [Elim' Term]
forall a b. (a -> b) -> [a] -> [b]
map' CheckedArg -> Elim' Term
caElim ([CheckedArg] -> [Elim' Term]) -> [CheckedArg] -> [Elim' Term]
forall a b. (a -> b) -> a -> b
$ ArgsCheckState a -> [CheckedArg]
forall a. ArgsCheckState a -> [CheckedArg]
acCheckedArgs 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
-> [Arg (Named_ Expr)]
-> Expr
-> Type'' Term Term
-> TCM Term
checkApplication Comparison
cmp Expr
hd [Arg (Named_ Expr)]
args Expr
e Type'' Term Term
t =
  Expr -> TCM Term -> TCM Term
forall a. Expr -> TCM a -> TCM a
turnOffExpandLastIfExistingMeta Expr
hd (TCM Term -> TCM Term) -> TCM Term -> TCM Term
forall a b. (a -> b) -> a -> b
$
  TCM Term -> TCM Term
forall a. TCM a -> TCM a
postponeInstanceConstraints (TCM Term -> TCM Term) -> TCM Term -> TCM Term
forall a b. (a -> b) -> a -> b
$ do
  [Char] -> Int -> TCMT IO Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.check.app" Int
20 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
    [ TCMT IO Doc
"checkApplication"
    , Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"hd   = " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Expr -> TCMT IO Doc
forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA Expr
hd
    , Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"args = " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> do [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
prettyList ([TCMT IO Doc] -> TCMT IO Doc) -> [TCMT IO Doc] -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ (Arg (Named_ Expr) -> TCMT IO Doc)
-> [Arg (Named_ Expr)] -> [TCMT IO Doc]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Arg (Named_ Expr) -> TCMT IO Doc
forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA [Arg (Named_ Expr)]
args
    , Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"e    = " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Expr -> TCMT IO Doc
forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA Expr
e
    , Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"t    = " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Type'' Term Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type'' Term Term -> m Doc
prettyTCM Type'' Term Term
t
    ]
  [Char] -> Int -> TCMT IO Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.check.app" Int
70 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
    [ TCMT IO Doc
"checkApplication (raw)"
    , Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ [Char] -> TCMT IO Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text ([Char] -> TCMT IO Doc) -> [Char] -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ [Char]
"hd   = " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++! Expr -> [Char]
forall a. Show a => a -> [Char]
show Expr
hd
    , Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ [Char] -> TCMT IO Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text ([Char] -> TCMT IO Doc) -> [Char] -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ [Char]
"args = " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++! [Arg (Named_ Expr)] -> [Char]
forall a. Show a => a -> [Char]
show ([Arg (Named_ Expr)] -> [Arg (Named_ Expr)]
forall a. ExprLike a => a -> a
deepUnscope [Arg (Named_ Expr)]
args)
    , Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ [Char] -> TCMT IO Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text ([Char] -> TCMT IO Doc) -> [Char] -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ [Char]
"e    = " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++! Expr -> [Char]
forall a. Show a => a -> [Char]
show (Expr -> Expr
forall a. ExprLike a => a -> a
deepUnscope Expr
e)
    , Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ [Char] -> TCMT IO Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text ([Char] -> TCMT IO Doc) -> [Char] -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ [Char]
"t    = " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++! Type'' Term Term -> [Char]
forall a. Show a => a -> [Char]
show Type'' Term Term
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'' Term Term
-> QName
-> ProjOrigin
-> Expr
-> [Arg (Named_ Expr)]
-> TCM Term
checkUnambiguousProjectionApplication Comparison
cmp Expr
e Type'' Term Term
t QName
x ProjOrigin
o Expr
hd [Arg (Named_ Expr)]
args

    -- Subcase: ambiguous projection
    A.Proj ProjOrigin
o AmbiguousQName
p -> do
      Comparison
-> Expr
-> ProjOrigin
-> AmbiguousQName
-> Expr
-> [Arg (Named_ Expr)]
-> Type'' Term Term
-> TCM Term
checkProjApp Comparison
cmp Expr
e ProjOrigin
o AmbiguousQName
p Expr
hd [Arg (Named_ Expr)]
args Type'' Term Term
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
      con <- HasCallStack => QName -> TCM ConHead
QName -> TCM ConHead
getOrigConHead QName
c
      checkConstructorApplication cmp e t con hd args

    -- Subcase: ambiguous constructor
    A.Con AmbiguousQName
ambC -> do
      let cont :: ConHead -> TCM Term
cont ConHead
c = Comparison
-> Expr
-> Type'' Term Term
-> ConHead
-> Expr
-> [Arg (Named_ Expr)]
-> TCM Term
checkConstructorApplication Comparison
cmp Expr
e Type'' Term Term
t ConHead
c Expr
hd [Arg (Named_ Expr)]
args
      (ConHead -> TCM Term) -> DisambiguateConstructor -> TCM Term
afterDisambiguation ConHead -> TCM Term
cont (DisambiguateConstructor -> TCM Term)
-> DisambiguateConstructor -> TCM Term
forall a b. (a -> b) -> a -> b
$ AmbiguousQName
-> [Arg (Named_ Expr)]
-> Type'' Term Term
-> DisambiguateConstructor
disambiguateConstructor AmbiguousQName
ambC [Arg (Named_ Expr)]
args Type'' Term Term
t

    -- Subcase: pattern synonym
    A.PatternSyn AmbiguousQName
n -> do
      A.PatternSynDefn ns p0 <- AmbiguousQName -> TCM PatternSynDefn
lookupPatternSyn AmbiguousQName
n
      let p = Range -> Pattern' Expr -> Pattern' Expr
forall a. SetRange a => Range -> a -> a
setRange (AmbiguousQName -> Range
forall a. HasRange a => a -> Range
getRange AmbiguousQName
n) (Pattern' Expr -> Pattern' Expr) -> Pattern' Expr -> Pattern' Expr
forall a b. (a -> b) -> a -> b
$ Pattern' Expr -> Pattern' Expr
forall a. KillRange a => KillRangeT a
killRange (Pattern' Expr -> Pattern' Expr) -> Pattern' Expr -> Pattern' Expr
forall a b. (a -> b) -> a -> b
$ Pattern' Void -> Pattern' Expr
forall (f :: * -> *) a. Functor f => f Void -> f a
vacuous Pattern' Void
p0   -- 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 Hiding
h Range
r = MetaInfo -> Expr
A.Underscore (MetaInfo -> Expr) -> MetaInfo -> Expr
forall a b. (a -> b) -> a -> b
$ MetaInfo
A.emptyMetaInfo{ A.metaRange = r, A.metaKind = A.hidingToMetaKind h }   -- TODO: name suggestion
      case A.insertImplicitPatSynArgs meta (getRange n) ns args of
        Maybe ([(Name, Expr)], [WithHiding Name])
Nothing      -> TypeError -> TCM Term
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> TCM Term) -> TypeError -> TCM Term
forall a b. (a -> b) -> a -> b
$ AmbiguousQName -> TypeError
BadArgumentsToPatternSynonym AmbiguousQName
n
        Just ([(Name, Expr)]
s, [WithHiding Name]
ns) -> do
          let p' :: Expr
p' = Pattern' Expr -> Expr
patternToExpr Pattern' Expr
p
              e' :: Expr
e' = [WithHiding Name] -> Expr -> Expr
A.lambdaLiftExpr [WithHiding Name]
ns ([(Name, Expr)] -> Expr -> Expr
forall a. SubstExpr a => [(Name, Expr)] -> a -> a
A.substExpr [(Name, Expr)]
s Expr
p')
          Comparison -> Expr -> Type'' Term Term -> TCM Term
checkExpr' Comparison
cmp Expr
e' Type'' Term Term
t

    -- Subcase: macro
    A.Macro QName
x -> do
      -- First go: no parameters
      TelV tel _ <- Type'' Term Term -> TCMT IO (TelV (Type'' Term Term))
forall (m :: * -> *).
(MonadReduce m, MonadAddContext m) =>
Type'' Term Term -> m (TelV (Type'' Term Term))
telView (Type'' Term Term -> TCMT IO (TelV (Type'' Term Term)))
-> (Definition -> Type'' Term Term)
-> Definition
-> TCMT IO (TelV (Type'' Term Term))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Definition -> Type'' Term Term
defType (Definition -> TCMT IO (TelV (Type'' Term Term)))
-> TCMT IO Definition -> TCMT IO (TelV (Type'' Term Term))
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Definition -> TCMT IO Definition
forall (m :: * -> *).
(HasConstInfo m, ReadTCState m) =>
Definition -> m Definition
instantiateDef (Definition -> TCMT IO Definition)
-> TCMT IO Definition -> TCMT IO Definition
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< QName -> TCMT IO Definition
forall (m :: * -> *).
(HasConstInfo m, HasCallStack) =>
QName -> m Definition
getConstInfo QName
x

      tTerm <- primAgdaTerm
      tName <- primQName

      -- Andreas, 2021-05-13, can we use @initWithDefault __IMPOSSIBLE__@ here?
      let argTel   = [Dom' Term ([Char], Type'' Term Term)]
-> [Dom' Term ([Char], Type'' Term Term)]
forall a. HasCallStack => [a] -> [a]
init ([Dom' Term ([Char], Type'' Term Term)]
 -> [Dom' Term ([Char], Type'' Term Term)])
-> [Dom' Term ([Char], Type'' Term Term)]
-> [Dom' Term ([Char], Type'' Term Term)]
forall a b. (a -> b) -> a -> b
$ Tele (Dom' Term (Type'' Term Term))
-> [Dom' Term ([Char], Type'' Term Term)]
forall t. Tele (Dom t) -> [Dom ([Char], t)]
telToList Tele (Dom' Term (Type'' Term Term))
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'' Term Term
t Arg (Named_ Expr)
a | Type'' Term Term -> Term
forall t a. Type'' t a -> a
unEl Type'' Term Term
t Term -> Term -> Bool
forall a. Eq a => a -> a -> Bool
== Term
tTerm =
            ((Named_ Expr -> Named_ Expr)
-> Arg (Named_ Expr) -> Arg (Named_ Expr)
forall a b. (a -> b) -> Arg a -> Arg b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Named_ Expr -> Named_ Expr)
 -> Arg (Named_ Expr) -> Arg (Named_ Expr))
-> ((Expr -> Expr) -> Named_ Expr -> Named_ Expr)
-> (Expr -> Expr)
-> Arg (Named_ Expr)
-> Arg (Named_ Expr)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Expr -> Expr) -> Named_ Expr -> Named_ Expr
forall a b. (a -> b) -> Named NamedName a -> Named NamedName b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap)
              (AppInfo -> Expr -> Arg (Named_ Expr) -> Expr
A.App (Range -> AppInfo
A.defaultAppInfo (Arg (Named_ Expr) -> Range
forall a. HasRange a => a -> Range
getRange Arg (Named_ Expr)
a)) (ExprInfo -> Expr
A.QuoteTerm ExprInfo
A.exprNoRange) (Arg (Named_ Expr) -> Expr)
-> (Expr -> Arg (Named_ Expr)) -> Expr -> Expr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expr -> Arg (Named_ Expr)
forall a. a -> NamedArg a
defaultNamedArg) Arg (Named_ Expr)
a
          mkArg Type'' Term Term
t Arg (Named_ Expr)
a | Type'' Term Term -> Term
forall t a. Type'' t a -> a
unEl Type'' Term Term
t Term -> Term -> Bool
forall a. Eq a => a -> a -> Bool
== Term
tName =
            ((Named_ Expr -> Named_ Expr)
-> Arg (Named_ Expr) -> Arg (Named_ Expr)
forall a b. (a -> b) -> Arg a -> Arg b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Named_ Expr -> Named_ Expr)
 -> Arg (Named_ Expr) -> Arg (Named_ Expr))
-> ((Expr -> Expr) -> Named_ Expr -> Named_ Expr)
-> (Expr -> Expr)
-> Arg (Named_ Expr)
-> Arg (Named_ Expr)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Expr -> Expr) -> Named_ Expr -> Named_ Expr
forall a b. (a -> b) -> Named NamedName a -> Named NamedName b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap)
              (AppInfo -> Expr -> Arg (Named_ Expr) -> Expr
A.App (Range -> AppInfo
A.defaultAppInfo (Arg (Named_ Expr) -> Range
forall a. HasRange a => a -> Range
getRange Arg (Named_ Expr)
a)) (ExprInfo -> Expr
A.Quote ExprInfo
A.exprNoRange) (Arg (Named_ Expr) -> Expr)
-> (Expr -> Arg (Named_ Expr)) -> Expr -> Expr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expr -> Arg (Named_ Expr)
forall a. a -> NamedArg a
defaultNamedArg) Arg (Named_ Expr)
a
          mkArg Type'' Term Term
t Arg (Named_ Expr)
a | Bool
otherwise = Arg (Named_ Expr)
a

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

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

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

      checkExpr' cmp desugared t

    -- Subcase: unquote
    A.Unquote ExprInfo
_
      | [Arg (Named_ Expr)
arg] <- [Arg (Named_ Expr)]
args -> do
          (_, hole) <- RunMetaOccursCheck
-> Comparison -> Type'' Term Term -> TCM (MetaId, Term)
newValueMeta RunMetaOccursCheck
RunMetaOccursCheck Comparison
CmpLeq Type'' Term Term
t
          unquoteM (namedArg arg) hole t
          return hole
      | Arg (Named_ Expr)
arg : [Arg (Named_ Expr)]
args <- [Arg (Named_ 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
          --  Run the tactic on H
          --  Check H a b : A
          tel    <- [Arg (Named_ Expr)] -> TCM (Tele (Dom' Term (Type'' Term Term)))
forall a. [Arg a] -> TCM (Tele (Dom' Term (Type'' Term Term)))
metaTel [Arg (Named_ Expr)]
args                    -- (x : X) (y : Y x)
          target <- addContext tel newTypeMeta_     -- Z x y
          let holeType = Tele (Dom' Term (Type'' Term Term))
-> Type'' Term Term -> Type'' Term Term
telePi_ Tele (Dom' Term (Type'' Term Term))
tel Type'' Term Term
target         -- (x : X) (y : Y x) → Z x y
          let hd       = Arg (Named_ Expr) -> Expr
forall a. NamedArg a -> a
namedArg Arg (Named_ Expr)
arg
          (Just vs, EmptyTel) <- first allApplyElims <$> checkArguments_ CmpLeq ExpandLast hd args tel
                                                    -- a b : (x : X) (y : Y x)
          (_, hole) <- newValueMeta RunMetaOccursCheck CmpLeq holeType
          unquoteM hd hole holeType
          let rho = [Term] -> [Term]
forall a. [a] -> [a]
reverse ((Arg Term -> Term) -> [Arg Term] -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map' Arg Term -> Term
forall e. Arg e -> e
unArg [Arg Term]
vs) [Term] -> Substitution' Term -> Substitution' Term
forall a. DeBruijn a => [a] -> Substitution' a -> Substitution' a
++# Substitution' Term
forall a. Substitution' a
IdS  -- [x := a, y := b]
          coerce CmpEq (apply hole vs) (applySubst rho target) t -- H a b : A
      where
        metaTel :: [Arg a] -> TCM Telescope
        metaTel :: forall a. [Arg a] -> TCM (Tele (Dom' Term (Type'' Term Term)))
metaTel []           = Tele (Dom' Term (Type'' Term Term))
-> TCM (Tele (Dom' Term (Type'' Term Term)))
forall a. a -> TCMT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Tele (Dom' Term (Type'' Term Term))
forall a. Tele a
EmptyTel
        metaTel (Arg a
arg : [Arg a]
args) = do
          a <- TCMT IO (Type'' Term Term)
newTypeMeta_
          let dom = Type'' Term Term
a Type'' Term Term -> Dom' Term a -> Dom' Term (Type'' Term Term)
forall a b. a -> Dom' Term b -> Dom' Term a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Arg a -> Dom' Term a
forall a. Arg a -> Dom a
domFromArg Arg a
arg
          ExtendTel dom . Abs "x" <$>
            addContext ("x" :: String, dom) (metaTel args)

    -- Subcase: defined symbol or variable.
    Expr
_ -> do
      v <- Comparison
-> Expr
-> Type'' Term Term
-> Expr
-> [Arg (Named_ Expr)]
-> TCM Term
checkHeadApplication Comparison
cmp Expr
e Type'' Term Term
t Expr
hd [Arg (Named_ Expr)]
args
      reportSDoc "tc.term.app" 30 $ vcat
        [ "checkApplication: checkHeadApplication returned"
        , nest 2 $ "v = " <+> prettyTCM v
        ]
      return v

-- | Precondition: @Application hd args = appView e@.
inferApplication :: ExpandHidden -> A.Expr -> A.Args -> A.Expr -> TCM (Term, Type)
inferApplication :: ExpandHidden
-> Expr
-> [Arg (Named_ Expr)]
-> Expr
-> TCM (Term, Type'' Term Term)
inferApplication ExpandHidden
exh Expr
hd [Arg (Named_ Expr)]
args Expr
e | Bool -> Bool
not (Expr -> Bool
defOrVar Expr
hd) = do
  t <- TCMT IO (Type'' Term Term) -> TCMT IO (Type'' Term Term)
forall (m :: * -> *) a.
(MonadTCEnv m, HasOptions m, MonadDebug m) =>
m a -> m a
workOnTypes (TCMT IO (Type'' Term Term) -> TCMT IO (Type'' Term Term))
-> TCMT IO (Type'' Term Term) -> TCMT IO (Type'' Term Term)
forall a b. (a -> b) -> a -> b
$ TCMT IO (Type'' Term Term)
newTypeMeta_
  v <- checkExpr' CmpEq e t
  return (v, t)
inferApplication ExpandHidden
exh Expr
hd [Arg (Named_ Expr)]
args Expr
e = TCM (Term, Type'' Term Term) -> TCM (Term, Type'' Term Term)
forall a. TCM a -> TCM a
postponeInstanceConstraints (TCM (Term, Type'' Term Term) -> TCM (Term, Type'' Term Term))
-> TCM (Term, Type'' Term Term) -> TCM (Term, Type'' Term Term)
forall a b. (a -> b) -> a -> b
$ do
  SortKit{ isNameOfUniv } <- TCMT IO SortKit
forall (m :: * -> *). (HasBuiltins m, MonadTCError m) => m SortKit
sortKit
  case unScope hd of
    A.Proj ProjOrigin
o AmbiguousQName
p | AmbiguousQName -> Bool
isAmbiguous AmbiguousQName
p -> Expr
-> ProjOrigin
-> AmbiguousQName
-> Expr
-> [Arg (Named_ Expr)]
-> TCM (Term, Type'' Term Term)
inferProjApp Expr
e ProjOrigin
o AmbiguousQName
p Expr
hd [Arg (Named_ Expr)]
args
    A.Def' QName
x Suffix
s | Just (UnivSize
sz, Univ
u) <- QName -> Maybe (UnivSize, Univ)
isNameOfUniv QName
x -> UnivSize
-> Univ
-> Expr
-> QName
-> Suffix
-> [Arg (Named_ Expr)]
-> TCM (Term, Type'' Term Term)
inferUniv UnivSize
sz Univ
u Expr
e QName
x Suffix
s [Arg (Named_ Expr)]
args
    Expr
_ -> do
      (f, t0) <- Expr -> TCM ([Elim' Term] -> Term, Type'' Term Term)
inferHead Expr
hd
      res <- runExceptT $ checkArgumentsE CmpEq exh hd args t0 Nothing
      case res of
        Right st :: ArgsCheckState CheckedTarget
st@(ACState{acType :: forall a. ArgsCheckState a -> Type'' Term Term
acType = Type'' Term Term
t1}) -> (Term -> (Term, Type'' Term Term))
-> TCM Term -> TCM (Term, Type'' Term Term)
forall a b. (a -> b) -> TCMT IO a -> TCMT IO b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (,Type'' Term Term
t1) (TCM Term -> TCM (Term, Type'' Term Term))
-> TCM Term -> TCM (Term, Type'' Term Term)
forall a b. (a -> b) -> a -> b
$ Term -> TCM Term
forall (m :: * -> *). PureTCM m => Term -> m Term
unfoldInlined (Term -> TCM Term) -> TCM Term -> TCM Term
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< ([Elim' Term] -> Term) -> ArgsCheckState CheckedTarget -> TCM Term
forall a. ([Elim' Term] -> Term) -> ArgsCheckState a -> TCM Term
checkHeadConstraints [Elim' Term] -> Term
f ArgsCheckState CheckedTarget
st
        Left ArgsCheckState [Arg (Named_ Expr)]
problem -> do
          t <- TCMT IO (Type'' Term Term) -> TCMT IO (Type'' Term Term)
forall (m :: * -> *) a.
(MonadTCEnv m, HasOptions m, MonadDebug m) =>
m a -> m a
workOnTypes (TCMT IO (Type'' Term Term) -> TCMT IO (Type'' Term Term))
-> TCMT IO (Type'' Term Term) -> TCMT IO (Type'' Term Term)
forall a b. (a -> b) -> a -> b
$ TCMT IO (Type'' Term Term)
newTypeMeta_
          v <- postponeArgs problem CmpEq exh hd args t0 t $ \ ArgsCheckState CheckedTarget
st -> Term -> TCM Term
forall (m :: * -> *). PureTCM m => Term -> m Term
unfoldInlined (Term -> TCM Term) -> TCM Term -> TCM Term
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< ([Elim' Term] -> Term) -> ArgsCheckState CheckedTarget -> TCM Term
forall a. ([Elim' Term] -> Term) -> ArgsCheckState a -> TCM Term
checkHeadConstraints [Elim' Term] -> Term
f ArgsCheckState CheckedTarget
st
          return (v, t)

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

inferHeadDef :: ProjOrigin -> QName -> TCM (Elims -> Term, Type)
inferHeadDef :: ProjOrigin -> QName -> TCM ([Elim' Term] -> Term, Type'' Term Term)
inferHeadDef ProjOrigin
o QName
x = do
  -- Andreas, 2022-03-07, issue #5809: don't drop parameters of irrelevant projections.
  proj <- QName -> TCMT IO (Maybe Projection)
forall (m :: * -> *).
HasConstInfo m =>
QName -> m (Maybe Projection)
isRelevantProjection QName
x
  rel  <- getRelevance . defArgInfo <$> getConstInfo x
  let app =
        case Maybe Projection
proj of
          Maybe Projection
Nothing -> \ [Arg Term]
args -> QName -> [Elim' Term] -> Term
Def QName
x ([Elim' Term] -> Term) -> [Elim' Term] -> Term
forall a b. (a -> b) -> a -> b
$ (Arg Term -> Elim' Term) -> [Arg Term] -> [Elim' Term]
forall a b. (a -> b) -> [a] -> [b]
map' Arg Term -> Elim' Term
forall a. Arg a -> Elim' a
Apply [Arg Term]
args
          Just Projection
p  -> \ [Arg Term]
args -> Projection -> ProjOrigin -> Relevance -> [Arg Term] -> Term
projDropParsApply Projection
p ProjOrigin
o Relevance
rel [Arg Term]
args
  first applyE <$> inferDef app 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 ([Elim' Term] -> Term, Type'' Term Term)
inferHead Expr
e = do
  case Expr
e of
    A.Var Name
x -> do -- traceCall (InferVar x) $ do
      (u, a) <- Name -> TCMT IO (Term, Dom' Term (Type'' Term Term))
forall (m :: * -> *).
(MonadDebug m, MonadFail m, MonadTCEnv m) =>
Name -> m (Term, Dom' Term (Type'' Term Term))
getVarInfo Name
x
      reportSDoc "tc.term.var" 20 $ hsep
        [ "variable" , prettyTCM x
        , "(" , text (show u) , ")"
        , "has type:" , prettyTCM a
        ]
      unless (usableRelevance a) $
        typeError $ VariableIsIrrelevant 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.
      unlessM ((getQuantity a `moreQuantity`) <$> viewTC eQuantity) $
        typeError $ VariableIsErased x

      unless (usableCohesion a) $
        typeError $ VariableIsOfUnusableCohesion x (getCohesion a)

      unless (usablePolarity a) $
        typeError $ VariableIsOfUnusablePolarity x (getModalPolarity a)

      return (applyE u, unDom a)

    A.Def QName
x  -> ProjOrigin -> QName -> TCM ([Elim' Term] -> Term, Type'' Term Term)
inferHeadDef ProjOrigin
ProjPrefix QName
x
    A.Def'{} -> TCM ([Elim' Term] -> Term, Type'' Term Term)
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 ([Elim' Term] -> Term, Type'' Term Term)
inferHeadDef ProjOrigin
o QName
d
    A.Proj{} -> TCM ([Elim' Term] -> Term, Type'' Term Term)
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.
      con <- HasCallStack => QName -> TCM ConHead
QName -> TCM ConHead
getOrigConHead QName
c
      (u, a) <- inferDef (\ [Arg Term]
_ -> ConHead -> ConInfo -> [Elim' Term] -> Term
Con ConHead
con ConInfo
ConOCon []) c

      -- Next get the number of parameters in the current context.
      Constructor{conPars = n} <- theDef <$> (instantiateDef =<< getConstInfo c)

      reportSLn "tc.term.con" 7 $ unwords [prettyShow c, "has", show n, "parameters."]

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

inferDef :: (Args -> Term) -> QName -> TCM (Term, Type)
inferDef :: ([Arg Term] -> Term) -> QName -> TCM (Term, Type'' Term Term)
inferDef [Arg Term] -> Term
mkTerm QName
x =
  Call
-> TCM (Term, Type'' Term Term) -> TCM (Term, Type'' Term Term)
forall a. Call -> TCMT IO a -> TCMT IO a
forall (m :: * -> *) a. MonadTrace m => Call -> m a -> m a
traceCall (QName -> Call
InferDef QName
x) (TCM (Term, Type'' Term Term) -> TCM (Term, Type'' Term Term))
-> TCM (Term, Type'' Term Term) -> TCM (Term, Type'' Term Term)
forall a b. (a -> b) -> a -> b
$ do
    -- getConstInfo retrieves the *absolute* (closed) type of x
    -- instantiateDef relativizes it to the current context
    d0 <- QName -> TCMT IO Definition
forall (m :: * -> *).
(HasConstInfo m, HasCallStack) =>
QName -> m Definition
getConstInfo QName
x
    d  <- instantiateDef d0
    reportSDoc "tc.term.def" 10 $ "inferDef" <+> prettyTCM x
    reportSDoc "tc.term.def" 30 $ "  absolute type:    " <+> inTopContext (prettyTCM $ defType d0)
    reportSDoc "tc.term.def" 30 $ "  instantiated type:" <+> prettyTCM (defType d)
    -- Irrelevant defs are only allowed in irrelevant position.
    -- Erased defs are only allowed in erased position (see #3855).
    checkModality x d
    reportSDoc "tc.term.def" 30 $ "  checked modality!"
    case theDef d of
      GeneralizableVar{} -> do
        [Char] -> Int -> TCMT IO Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.term.def" Int
30 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"  we are a GeneralizableVar"
        -- 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.
        val <- GeneralizedValue -> Maybe GeneralizedValue -> GeneralizedValue
forall a. a -> Maybe a -> a
fromMaybe GeneralizedValue
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe GeneralizedValue -> GeneralizedValue)
-> TCMT IO (Maybe GeneralizedValue) -> TCMT IO GeneralizedValue
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Lens' TCEnv (Maybe GeneralizedValue)
-> TCMT IO (Maybe GeneralizedValue)
forall (m :: * -> *) a. MonadTCEnv m => Lens' TCEnv a -> m a
viewTC ((Map QName GeneralizedValue -> f (Map QName GeneralizedValue))
-> TCEnv -> f TCEnv
Lens' TCEnv (Map QName GeneralizedValue)
eGeneralizedVars ((Map QName GeneralizedValue -> f (Map QName GeneralizedValue))
 -> TCEnv -> f TCEnv)
-> ((Maybe GeneralizedValue -> f (Maybe GeneralizedValue))
    -> Map QName GeneralizedValue -> f (Map QName GeneralizedValue))
-> (Maybe GeneralizedValue -> f (Maybe GeneralizedValue))
-> TCEnv
-> f TCEnv
forall b c a. (b -> c) -> (a -> b) -> a -> c
. QName
-> Lens' (Map QName GeneralizedValue) (Maybe GeneralizedValue)
forall k v. Ord k => k -> Lens' (Map k v) (Maybe v)
key QName
x)
        sub <- checkpointSubstitution (genvalCheckpoint val)
        let (v, t) = applySubst sub (genvalTerm val, genvalType val)
        debug [] t v
        return (v, t)
      Defn
_ -> do
        [Char] -> Int -> TCMT IO Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.term.def" Int
30 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"  we are not a GeneralizableVar"
        -- since x is considered living in the top-level, we have to
        -- apply it to the current context
        vs <- QName -> TCMT IO [Arg Term]
forall (m :: * -> *).
(HasConstInfo m, ReadTCState m) =>
QName -> m [Arg Term]
freeVarsToApply QName
x
        reportSDoc "tc.term.def" 30 $ "  free vars:" <+> prettyList_ (map' prettyTCM vs)
        let t = Definition -> Type'' Term Term
defType Definition
d
            v = [Arg Term] -> Term
mkTerm [Arg Term]
vs -- applies x to vs, dropping parameters

        -- Andrea 2019-07-16, Check that the supplied arguments
        -- respect the pure modalities of the current context.
        -- Pure modalities are based on left-division, so it does not
        -- rely on "position" like positional modalities.
        checkModalityArgs d0 vs

        debug vs t v
        return (v, t)
  where
    debug :: Args -> Type -> Term -> TCM ()
    debug :: [Arg Term] -> Type'' Term Term -> Term -> TCMT IO ()
debug [Arg Term]
vs Type'' Term Term
t Term
v = do
      [Char] -> Int -> TCMT IO Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.term.def" Int
60 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$
        TCMT IO Doc
"freeVarsToApply to def " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
hsep ((Arg Term -> TCMT IO Doc) -> [Arg Term] -> [TCMT IO Doc]
forall a b. (a -> b) -> [a] -> [b]
map' ([Char] -> TCMT IO Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text ([Char] -> TCMT IO Doc)
-> (Arg Term -> [Char]) -> Arg Term -> TCMT IO Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Arg Term -> [Char]
forall a. Show a => a -> [Char]
show) [Arg Term]
vs)
      [Char] -> Int -> TCMT IO Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.term.def" Int
10 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
        [ TCMT IO Doc
"inferred def " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> QName -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM QName
x TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
hsep ((Arg Term -> TCMT IO Doc) -> [Arg Term] -> [TCMT IO Doc]
forall a b. (a -> b) -> [a] -> [b]
map' Arg Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Arg Term -> m Doc
prettyTCM [Arg Term]
vs)
        , Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
":" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Type'' Term Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type'' Term Term -> m Doc
prettyTCM Type'' Term Term
t
        , Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"-->" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
v ]

-- | @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'' Term Term
-> Expr
-> [Arg (Named_ Expr)]
-> TCM Term
checkHeadApplication Comparison
cmp Expr
e Type'' Term Term
t Expr
hd [Arg (Named_ Expr)]
args = do
  SortKit{ isNameOfUniv } <- TCMT IO SortKit
forall (m :: * -> *). (HasBuiltins m, MonadTCError m) => m SortKit
sortKit
  sharp <- fmap nameOfSharp <$> coinductionKit
  pOr    <- getNameOfConstrained builtinPOr
  pComp  <- getNameOfConstrained builtinComp
  pHComp <- getNameOfConstrained builtinHComp
  pTrans <- getNameOfConstrained builtinTrans
  mglue  <- getNameOfConstrained builtin_glue
  mglueU  <- getNameOfConstrained builtin_glueU
  case hd of
    A.Def' QName
c Suffix
s | Just (UnivSize
sz, Univ
u) <- QName -> Maybe (UnivSize, Univ)
isNameOfUniv QName
c -> UnivSize
-> Univ
-> Comparison
-> Expr
-> Type'' Term Term
-> QName
-> Suffix
-> [Arg (Named_ Expr)]
-> TCM Term
checkUniv UnivSize
sz Univ
u Comparison
cmp Expr
e Type'' Term Term
t QName
c Suffix
s [Arg (Named_ 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 | QName -> Maybe QName
forall a. a -> Maybe a
Just QName
c Maybe QName -> Maybe QName -> Bool
forall a. Eq a => a -> a -> Bool
== Maybe QName
sharp -> Expr
-> Type'' Term Term -> QName -> [Arg (Named_ Expr)] -> TCM Term
checkSharpApplication Expr
e Type'' Term Term
t QName
c [Arg (Named_ Expr)]
args

    -- Cubical primitives
    A.Def QName
c | QName -> Maybe QName
forall a. a -> Maybe a
Just QName
c Maybe QName -> Maybe QName -> Bool
forall a. Eq a => a -> a -> Bool
== Maybe QName
pComp -> Maybe
  (ArgRanges -> [Arg Term] -> Type'' Term Term -> TCMT IO [Arg Term])
-> TCM Term
defaultResult' (Maybe
   (ArgRanges -> [Arg Term] -> Type'' Term Term -> TCMT IO [Arg Term])
 -> TCM Term)
-> Maybe
     (ArgRanges -> [Arg Term] -> Type'' Term Term -> TCMT IO [Arg Term])
-> TCM Term
forall a b. (a -> b) -> a -> b
$ (ArgRanges -> [Arg Term] -> Type'' Term Term -> TCMT IO [Arg Term])
-> Maybe
     (ArgRanges -> [Arg Term] -> Type'' Term Term -> TCMT IO [Arg Term])
forall a. a -> Maybe a
Just ((ArgRanges
  -> [Arg Term] -> Type'' Term Term -> TCMT IO [Arg Term])
 -> Maybe
      (ArgRanges
       -> [Arg Term] -> Type'' Term Term -> TCMT IO [Arg Term]))
-> (ArgRanges
    -> [Arg Term] -> Type'' Term Term -> TCMT IO [Arg Term])
-> Maybe
     (ArgRanges -> [Arg Term] -> Type'' Term Term -> TCMT IO [Arg Term])
forall a b. (a -> b) -> a -> b
$ QName
-> ArgRanges
-> [Arg Term]
-> Type'' Term Term
-> TCMT IO [Arg Term]
checkPrimComp QName
c
    A.Def QName
c | QName -> Maybe QName
forall a. a -> Maybe a
Just QName
c Maybe QName -> Maybe QName -> Bool
forall a. Eq a => a -> a -> Bool
== Maybe QName
pHComp -> Maybe
  (ArgRanges -> [Arg Term] -> Type'' Term Term -> TCMT IO [Arg Term])
-> TCM Term
defaultResult' (Maybe
   (ArgRanges -> [Arg Term] -> Type'' Term Term -> TCMT IO [Arg Term])
 -> TCM Term)
-> Maybe
     (ArgRanges -> [Arg Term] -> Type'' Term Term -> TCMT IO [Arg Term])
-> TCM Term
forall a b. (a -> b) -> a -> b
$ (ArgRanges -> [Arg Term] -> Type'' Term Term -> TCMT IO [Arg Term])
-> Maybe
     (ArgRanges -> [Arg Term] -> Type'' Term Term -> TCMT IO [Arg Term])
forall a. a -> Maybe a
Just ((ArgRanges
  -> [Arg Term] -> Type'' Term Term -> TCMT IO [Arg Term])
 -> Maybe
      (ArgRanges
       -> [Arg Term] -> Type'' Term Term -> TCMT IO [Arg Term]))
-> (ArgRanges
    -> [Arg Term] -> Type'' Term Term -> TCMT IO [Arg Term])
-> Maybe
     (ArgRanges -> [Arg Term] -> Type'' Term Term -> TCMT IO [Arg Term])
forall a b. (a -> b) -> a -> b
$ QName
-> ArgRanges
-> [Arg Term]
-> Type'' Term Term
-> TCMT IO [Arg Term]
checkPrimHComp QName
c
    A.Def QName
c | QName -> Maybe QName
forall a. a -> Maybe a
Just QName
c Maybe QName -> Maybe QName -> Bool
forall a. Eq a => a -> a -> Bool
== Maybe QName
pTrans -> Maybe
  (ArgRanges -> [Arg Term] -> Type'' Term Term -> TCMT IO [Arg Term])
-> TCM Term
defaultResult' (Maybe
   (ArgRanges -> [Arg Term] -> Type'' Term Term -> TCMT IO [Arg Term])
 -> TCM Term)
-> Maybe
     (ArgRanges -> [Arg Term] -> Type'' Term Term -> TCMT IO [Arg Term])
-> TCM Term
forall a b. (a -> b) -> a -> b
$ (ArgRanges -> [Arg Term] -> Type'' Term Term -> TCMT IO [Arg Term])
-> Maybe
     (ArgRanges -> [Arg Term] -> Type'' Term Term -> TCMT IO [Arg Term])
forall a. a -> Maybe a
Just ((ArgRanges
  -> [Arg Term] -> Type'' Term Term -> TCMT IO [Arg Term])
 -> Maybe
      (ArgRanges
       -> [Arg Term] -> Type'' Term Term -> TCMT IO [Arg Term]))
-> (ArgRanges
    -> [Arg Term] -> Type'' Term Term -> TCMT IO [Arg Term])
-> Maybe
     (ArgRanges -> [Arg Term] -> Type'' Term Term -> TCMT IO [Arg Term])
forall a b. (a -> b) -> a -> b
$ QName
-> ArgRanges
-> [Arg Term]
-> Type'' Term Term
-> TCMT IO [Arg Term]
checkPrimTrans QName
c
    A.Def QName
c | QName -> Maybe QName
forall a. a -> Maybe a
Just QName
c Maybe QName -> Maybe QName -> Bool
forall a. Eq a => a -> a -> Bool
== Maybe QName
pOr   -> Maybe
  (ArgRanges -> [Arg Term] -> Type'' Term Term -> TCMT IO [Arg Term])
-> TCM Term
defaultResult' (Maybe
   (ArgRanges -> [Arg Term] -> Type'' Term Term -> TCMT IO [Arg Term])
 -> TCM Term)
-> Maybe
     (ArgRanges -> [Arg Term] -> Type'' Term Term -> TCMT IO [Arg Term])
-> TCM Term
forall a b. (a -> b) -> a -> b
$ (ArgRanges -> [Arg Term] -> Type'' Term Term -> TCMT IO [Arg Term])
-> Maybe
     (ArgRanges -> [Arg Term] -> Type'' Term Term -> TCMT IO [Arg Term])
forall a. a -> Maybe a
Just ((ArgRanges
  -> [Arg Term] -> Type'' Term Term -> TCMT IO [Arg Term])
 -> Maybe
      (ArgRanges
       -> [Arg Term] -> Type'' Term Term -> TCMT IO [Arg Term]))
-> (ArgRanges
    -> [Arg Term] -> Type'' Term Term -> TCMT IO [Arg Term])
-> Maybe
     (ArgRanges -> [Arg Term] -> Type'' Term Term -> TCMT IO [Arg Term])
forall a b. (a -> b) -> a -> b
$ QName
-> ArgRanges
-> [Arg Term]
-> Type'' Term Term
-> TCMT IO [Arg Term]
checkPOr QName
c
    A.Def QName
c | QName -> Maybe QName
forall a. a -> Maybe a
Just QName
c Maybe QName -> Maybe QName -> Bool
forall a. Eq a => a -> a -> Bool
== Maybe QName
mglue -> Maybe
  (ArgRanges -> [Arg Term] -> Type'' Term Term -> TCMT IO [Arg Term])
-> TCM Term
defaultResult' (Maybe
   (ArgRanges -> [Arg Term] -> Type'' Term Term -> TCMT IO [Arg Term])
 -> TCM Term)
-> Maybe
     (ArgRanges -> [Arg Term] -> Type'' Term Term -> TCMT IO [Arg Term])
-> TCM Term
forall a b. (a -> b) -> a -> b
$ (ArgRanges -> [Arg Term] -> Type'' Term Term -> TCMT IO [Arg Term])
-> Maybe
     (ArgRanges -> [Arg Term] -> Type'' Term Term -> TCMT IO [Arg Term])
forall a. a -> Maybe a
Just ((ArgRanges
  -> [Arg Term] -> Type'' Term Term -> TCMT IO [Arg Term])
 -> Maybe
      (ArgRanges
       -> [Arg Term] -> Type'' Term Term -> TCMT IO [Arg Term]))
-> (ArgRanges
    -> [Arg Term] -> Type'' Term Term -> TCMT IO [Arg Term])
-> Maybe
     (ArgRanges -> [Arg Term] -> Type'' Term Term -> TCMT IO [Arg Term])
forall a b. (a -> b) -> a -> b
$ QName
-> ArgRanges
-> [Arg Term]
-> Type'' Term Term
-> TCMT IO [Arg Term]
check_glue QName
c
    A.Def QName
c | QName -> Maybe QName
forall a. a -> Maybe a
Just QName
c Maybe QName -> Maybe QName -> Bool
forall a. Eq a => a -> a -> Bool
== Maybe QName
mglueU -> Maybe
  (ArgRanges -> [Arg Term] -> Type'' Term Term -> TCMT IO [Arg Term])
-> TCM Term
defaultResult' (Maybe
   (ArgRanges -> [Arg Term] -> Type'' Term Term -> TCMT IO [Arg Term])
 -> TCM Term)
-> Maybe
     (ArgRanges -> [Arg Term] -> Type'' Term Term -> TCMT IO [Arg Term])
-> TCM Term
forall a b. (a -> b) -> a -> b
$ (ArgRanges -> [Arg Term] -> Type'' Term Term -> TCMT IO [Arg Term])
-> Maybe
     (ArgRanges -> [Arg Term] -> Type'' Term Term -> TCMT IO [Arg Term])
forall a. a -> Maybe a
Just ((ArgRanges
  -> [Arg Term] -> Type'' Term Term -> TCMT IO [Arg Term])
 -> Maybe
      (ArgRanges
       -> [Arg Term] -> Type'' Term Term -> TCMT IO [Arg Term]))
-> (ArgRanges
    -> [Arg Term] -> Type'' Term Term -> TCMT IO [Arg Term])
-> Maybe
     (ArgRanges -> [Arg Term] -> Type'' Term Term -> TCMT IO [Arg Term])
forall a b. (a -> b) -> a -> b
$ QName
-> ArgRanges
-> [Arg Term]
-> Type'' Term Term
-> TCMT IO [Arg Term]
check_glueU QName
c

    Expr
_ -> TCM Term
defaultResult
  where
  defaultResult :: TCM Term
  defaultResult :: TCM Term
defaultResult = Maybe
  (ArgRanges -> [Arg Term] -> Type'' Term Term -> TCMT IO [Arg Term])
-> TCM Term
defaultResult' Maybe
  (ArgRanges -> [Arg Term] -> Type'' Term Term -> TCMT IO [Arg Term])
forall a. Maybe a
Nothing
  defaultResult' :: Maybe (ArgRanges -> Args -> Type -> TCM Args) -> TCM Term
  defaultResult' :: Maybe
  (ArgRanges -> [Arg Term] -> Type'' Term Term -> TCMT IO [Arg Term])
-> TCM Term
defaultResult' Maybe
  (ArgRanges -> [Arg Term] -> Type'' Term Term -> TCMT IO [Arg Term])
mk = do
    (f, t0) <- Expr -> TCM ([Elim' Term] -> Term, Type'' Term Term)
inferHead Expr
hd
    expandLast <- viewTC eExpandLast
    checkArguments cmp expandLast hd args t0 t $ \ st :: ArgsCheckState CheckedTarget
st@(ACState [CheckedArg]
cas Expr
_fun Type'' Term Term
t1 CheckedTarget
checkedTarget) -> do
      let check :: Maybe (TCM Args)
          check :: Maybe (TCMT IO [Arg Term])
check = do
            k <- Maybe
  (ArgRanges -> [Arg Term] -> Type'' Term Term -> TCMT IO [Arg Term])
mk
            vs <- allApplyElims $ map' caElim cas
            pure $ k (map' caRange cas) vs t1
      st' <- case Maybe (TCMT IO [Arg Term])
check of
               Just TCMT IO [Arg Term]
ck -> ([Elim' Term]
-> ArgsCheckState CheckedTarget -> ArgsCheckState CheckedTarget
forall a. [Elim' Term] -> ArgsCheckState a -> ArgsCheckState a
`setACElims` ArgsCheckState CheckedTarget
st) ([Elim' Term] -> ArgsCheckState CheckedTarget)
-> ([Arg Term] -> [Elim' Term])
-> [Arg Term]
-> ArgsCheckState CheckedTarget
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Arg Term -> Elim' Term) -> [Arg Term] -> [Elim' Term]
forall a b. (a -> b) -> [a] -> [b]
map' Arg Term -> Elim' Term
forall a. Arg a -> Elim' a
Apply ([Arg Term] -> ArgsCheckState CheckedTarget)
-> TCMT IO [Arg Term] -> TCMT IO (ArgsCheckState CheckedTarget)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCMT IO [Arg Term]
ck
               Maybe (TCMT IO [Arg Term])
Nothing -> ArgsCheckState CheckedTarget
-> TCMT IO (ArgsCheckState CheckedTarget)
forall a. a -> TCMT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ArgsCheckState CheckedTarget
st
      v <- unfoldInlined =<< checkHeadConstraints f st'
      coerce' cmp checkedTarget v t1 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 = TCM a -> TCM a
forall a. TCM a -> TCM a
reallyDontExpandLast
  | Bool
otherwise      = TCM a -> TCM a
forall a. a -> a
id
  where
    isExistingMeta :: Bool
isExistingMeta = Maybe MetaId -> Bool
forall a. Maybe a -> Bool
isJust (Maybe MetaId -> Bool) -> Maybe MetaId -> Bool
forall a b. (a -> b) -> a -> b
$ MetaInfo -> Maybe MetaId
A.metaNumber (MetaInfo -> Maybe MetaId) -> Maybe MetaInfo -> Maybe MetaId
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
_) = MetaInfo -> Maybe MetaInfo
forall a. a -> Maybe a
Just MetaInfo
i
    metaInfo (A.Underscore MetaInfo
i)     = MetaInfo -> Maybe MetaInfo
forall a. a -> Maybe a
Just MetaInfo
i
    metaInfo (A.ScopedExpr ScopeInfo
_ Expr
e)   = Expr -> Maybe MetaInfo
metaInfo Expr
e
    metaInfo Expr
_                    = Maybe MetaInfo
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
  z <- TCM (Either e r) -> ExceptT e (TCMT IO) (Either e r)
forall (m :: * -> *) a. Monad m => m a -> ExceptT e m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TCM (Either e r) -> ExceptT e (TCMT IO) (Either e r))
-> TCM (Either e r) -> ExceptT e (TCMT IO) (Either e r)
forall a b. (a -> b) -> a -> b
$ Call -> TCM (Either e r) -> TCM (Either e r)
forall a. Call -> TCMT IO a -> TCMT IO a
forall (m :: * -> *) a. MonadTrace m => Call -> m a -> m a
traceCall Call
call (TCM (Either e r) -> TCM (Either e r))
-> TCM (Either e r) -> TCM (Either e r)
forall a b. (a -> b) -> a -> b
$ ExceptT e (TCMT IO) r -> TCM (Either e r)
forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
runExceptT ExceptT e (TCMT IO) r
m
  case z of
    Right r
e  -> r -> ExceptT e (TCMT IO) r
forall a. a -> ExceptT e (TCMT IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return r
e
    Left e
err -> e -> ExceptT e (TCMT IO) r
forall a. e -> ExceptT e (TCMT IO) a
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'' Term Term
-> Type'' Term Term
-> TCM Term
coerce' Comparison
cmp CheckedTarget
NotCheckedTarget           Term
v Type'' Term Term
inferred Type'' Term Term
expected = Comparison
-> Term -> Type'' Term Term -> Type'' Term Term -> TCM Term
coerce Comparison
cmp Term
v Type'' Term Term
inferred Type'' Term Term
expected
coerce' Comparison
cmp (CheckedTarget Maybe ProblemId
Nothing)    Term
v Type'' Term Term
_        Type'' Term Term
_        = Term -> TCM Term
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Term
v
coerce' Comparison
cmp (CheckedTarget (Just ProblemId
pid)) Term
v Type'' Term Term
_        Type'' Term Term
expected = Type'' Term Term -> Term -> ProblemId -> TCM Term
blockTermOnProblem Type'' Term Term
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
       -- ^ How the inferred type should be compared to the expected result type.
  -> ExpandHidden
       -- ^ Insert trailing hidden arguments?
  -> A.Expr
       -- ^ The function.
  -> [NamedArg A.Expr]
       -- ^ The arguments.
  -> Type
       -- ^ Type of the function.
  -> Maybe Type
       -- ^ Optional: expected result type (type of the whole application).
  -> ExceptT (ArgsCheckState [NamedArg A.Expr]) TCM (ArgsCheckState CheckedTarget)
       -- ^ Upon failure, return the current state for creating a postponed type checking problem.
checkArgumentsE :: Comparison
-> ExpandHidden
-> Expr
-> [Arg (Named_ Expr)]
-> Type'' Term Term
-> Maybe (Type'' Term Term)
-> ExceptT
     (ArgsCheckState [Arg (Named_ Expr)])
     (TCMT IO)
     (ArgsCheckState CheckedTarget)
checkArgumentsE Comparison
cmp ExpandHidden
exph Expr
hd [Arg (Named_ Expr)]
args Type'' Term Term
t0 Maybe (Type'' Term Term)
t = do
  sPathView <- ExceptT
  (ArgsCheckState [Arg (Named_ Expr)])
  (TCMT IO)
  (Type'' Term Term -> PathView)
forall (m :: * -> *).
HasBuiltins m =>
m (Type'' Term Term -> PathView)
pathView'
  checkArgumentsE'
    S{ sChecked       = NotCheckedTarget
     , sComp          = cmp
     , sExpand        = exph
     , sFun           = hd
     , sArgs          = zip args $ List.suffixesSatisfying visible args
     , sArgsLen       = length args
     , sFunType       = t0
     , sResultType    = t
     , sSizeLtChecked = False
     , sSkipCheck     = DontSkip
     , sPathView      = sPathView
     }

-- | 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 -> Expr
sFun :: A.Expr
    -- ^ The function.
  , CheckArgumentsE'State -> [(Arg (Named_ Expr), Bool)]
sArgs :: [(NamedArg A.Expr, Bool)]
    -- ^ Arguments, along with information about whether a given
    -- argument and all remaining arguments are 'visible'.
  , CheckArgumentsE'State -> Int
sArgsLen :: !Nat
    -- ^ The length of 'sArgs'.
  , CheckArgumentsE'State -> Type'' Term Term
sFunType :: Type
    -- ^ The function's type.
  , CheckArgumentsE'State -> Maybe (Type'' Term Term)
sResultType :: Maybe Type
    -- ^ The type of the application.
  , CheckArgumentsE'State -> Bool
sSizeLtChecked :: !Bool
    -- ^ Have we checked if 'sResultType' is 'BoundedLt'?
  , CheckArgumentsE'State -> SkipCheck
sSkipCheck :: !SkipCheck
    -- ^ Should the target type check be skipped?
  , CheckArgumentsE'State -> Type'' Term Term -> 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

type CheckArgumentsE' = ExceptT (ArgsCheckState [NamedArg A.Expr]) TCM (ArgsCheckState CheckedTarget)

checkArgumentsE'
  :: CheckArgumentsE'State
  -> CheckArgumentsE'

-- Case: no arguments, do not insert trailing hidden arguments: We are done.
checkArgumentsE' :: CheckArgumentsE'State
-> ExceptT
     (ArgsCheckState [Arg (Named_ Expr)])
     (TCMT IO)
     (ArgsCheckState CheckedTarget)
checkArgumentsE' S{ sArgs :: CheckArgumentsE'State -> [(Arg (Named_ Expr), Bool)]
sArgs = [], Expr
sFun :: CheckArgumentsE'State -> Expr
sFun :: Expr
sFun, Type'' Term Term
sFunType :: CheckArgumentsE'State -> Type'' Term Term
sFunType :: Type'' Term Term
sFunType, CheckedTarget
sChecked :: CheckArgumentsE'State -> CheckedTarget
sChecked :: CheckedTarget
sChecked, ExpandHidden
sExpand :: CheckArgumentsE'State -> ExpandHidden
sExpand :: ExpandHidden
sExpand }
  | ExpandHidden -> Bool
isDontExpandLast ExpandHidden
sExpand =
    ArgsCheckState CheckedTarget
-> ExceptT
     (ArgsCheckState [Arg (Named_ Expr)])
     (TCMT IO)
     (ArgsCheckState CheckedTarget)
forall a.
a -> ExceptT (ArgsCheckState [Arg (Named_ Expr)]) (TCMT IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return (ArgsCheckState CheckedTarget
 -> ExceptT
      (ArgsCheckState [Arg (Named_ Expr)])
      (TCMT IO)
      (ArgsCheckState CheckedTarget))
-> ArgsCheckState CheckedTarget
-> ExceptT
     (ArgsCheckState [Arg (Named_ Expr)])
     (TCMT IO)
     (ArgsCheckState CheckedTarget)
forall a b. (a -> b) -> a -> b
$ ACState
      { acCheckedArgs :: [CheckedArg]
acCheckedArgs = []
      , acFun :: Expr
acFun         = Expr
sFun
      , acType :: Type'' Term Term
acType        = Type'' Term Term
sFunType
      , acData :: CheckedTarget
acData        = CheckedTarget
sChecked
      }

-- Case: no arguments, but need to insert trailing hiddens.
checkArgumentsE' S{ sArgs :: CheckArgumentsE'State -> [(Arg (Named_ Expr), Bool)]
sArgs = [], Expr
sFun :: CheckArgumentsE'State -> Expr
sFun :: Expr
sFun, Type'' Term Term
sFunType :: CheckArgumentsE'State -> Type'' Term Term
sFunType :: Type'' Term Term
sFunType, CheckedTarget
sChecked :: CheckArgumentsE'State -> CheckedTarget
sChecked :: CheckedTarget
sChecked, Maybe (Type'' Term Term)
sResultType :: CheckArgumentsE'State -> Maybe (Type'' Term Term)
sResultType :: Maybe (Type'' Term Term)
sResultType } =
  Call
-> ExceptT
     (ArgsCheckState [Arg (Named_ Expr)])
     (TCMT IO)
     (ArgsCheckState CheckedTarget)
-> ExceptT
     (ArgsCheckState [Arg (Named_ Expr)])
     (TCMT IO)
     (ArgsCheckState CheckedTarget)
forall e r. Call -> ExceptT e (TCMT IO) r -> ExceptT e (TCMT IO) r
traceCallE (Expr
-> [Arg (Named_ Expr)]
-> Type'' Term Term
-> Maybe (Type'' Term Term)
-> Call
CheckArguments Expr
sFun [] Type'' Term Term
sFunType Maybe (Type'' Term Term)
sResultType) (ExceptT
   (ArgsCheckState [Arg (Named_ Expr)])
   (TCMT IO)
   (ArgsCheckState CheckedTarget)
 -> ExceptT
      (ArgsCheckState [Arg (Named_ Expr)])
      (TCMT IO)
      (ArgsCheckState CheckedTarget))
-> ExceptT
     (ArgsCheckState [Arg (Named_ Expr)])
     (TCMT IO)
     (ArgsCheckState CheckedTarget)
-> ExceptT
     (ArgsCheckState [Arg (Named_ Expr)])
     (TCMT IO)
     (ArgsCheckState CheckedTarget)
forall a b. (a -> b) -> a -> b
$ TCMT IO (ArgsCheckState CheckedTarget)
-> ExceptT
     (ArgsCheckState [Arg (Named_ Expr)])
     (TCMT IO)
     (ArgsCheckState CheckedTarget)
forall (m :: * -> *) a.
Monad m =>
m a -> ExceptT (ArgsCheckState [Arg (Named_ Expr)]) m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TCMT IO (ArgsCheckState CheckedTarget)
 -> ExceptT
      (ArgsCheckState [Arg (Named_ Expr)])
      (TCMT IO)
      (ArgsCheckState CheckedTarget))
-> TCMT IO (ArgsCheckState CheckedTarget)
-> ExceptT
     (ArgsCheckState [Arg (Named_ Expr)])
     (TCMT IO)
     (ArgsCheckState CheckedTarget)
forall a b. (a -> b) -> a -> b
$ do
    sResultType <- (Type'' Term Term -> TCM Term)
-> Maybe (Type'' Term Term) -> TCMT IO (Maybe Term)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Maybe a -> f (Maybe b)
traverse (Type'' Term Term -> Term
forall t a. Type'' t a -> a
unEl (Type'' Term Term -> Term)
-> (Type'' Term Term -> TCMT IO (Type'' Term Term))
-> Type'' Term Term
-> TCM Term
forall (m :: * -> *) b c a.
Functor m =>
(b -> c) -> (a -> m b) -> a -> m c
<.> Type'' Term Term -> TCMT IO (Type'' Term Term)
forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce) Maybe (Type'' Term Term)
sResultType
    (ncargs, t) <- implicitCheckedArgs (-1) (\ Hiding
h [Char]
_x -> Maybe Term -> Hiding -> Bool
expand Maybe Term
sResultType Hiding
h) sFunType
    return $ ACState
      { acCheckedArgs = map' namedThing ncargs
      , acFun         = sFun
      , acType        = t
      , acData        = sChecked
      }
  where
  expand :: Maybe Term -> Hiding -> Bool
expand (Just (Pi Dom' Term (Type'' Term Term)
dom Abs (Type'' Term Term)
_)) Hiding
Hidden     = Bool -> Bool
not (Dom' Term (Type'' Term Term) -> Bool
forall a. LensHiding a => a -> Bool
hidden Dom' Term (Type'' Term Term)
dom)
  expand Maybe Term
_                 Hiding
Hidden     = Bool
True
  expand (Just (Pi Dom' Term (Type'' Term Term)
dom Abs (Type'' Term Term)
_)) Instance{} = Bool -> Bool
not (Dom' Term (Type'' Term Term) -> Bool
forall a. LensHiding a => a -> Bool
isInstance Dom' Term (Type'' Term Term)
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 -> [(Arg (Named_ Expr), Bool)]
sArgs = sArgs :: [(Arg (Named_ Expr), Bool)]
sArgs@((arg :: Arg (Named_ Expr)
arg@(Arg ArgInfo
info Named_ Expr
e), Bool
sArgsVisible) : [(Arg (Named_ Expr), Bool)]
args), Int
sArgsLen :: CheckArgumentsE'State -> Int
sArgsLen :: Int
sArgsLen, CheckedTarget
sChecked :: CheckArgumentsE'State -> CheckedTarget
sChecked :: CheckedTarget
sChecked, Comparison
sComp :: CheckArgumentsE'State -> Comparison
sComp :: Comparison
sComp, Expr
sFun :: CheckArgumentsE'State -> Expr
sFun :: Expr
sFun, Type'' Term Term
sFunType :: CheckArgumentsE'State -> Type'' Term Term
sFunType :: Type'' Term Term
sFunType, Type'' Term Term -> PathView
sPathView :: CheckArgumentsE'State -> Type'' Term Term -> PathView
sPathView :: Type'' Term Term -> PathView
sPathView, Maybe (Type'' Term Term)
sResultType :: CheckArgumentsE'State -> Maybe (Type'' Term Term)
sResultType :: Maybe (Type'' Term Term)
sResultType, SkipCheck
sSkipCheck :: CheckArgumentsE'State -> SkipCheck
sSkipCheck :: SkipCheck
sSkipCheck, Bool
sSizeLtChecked :: CheckArgumentsE'State -> Bool
sSizeLtChecked :: Bool
sSizeLtChecked } =

    Call
-> ExceptT
     (ArgsCheckState [Arg (Named_ Expr)])
     (TCMT IO)
     (ArgsCheckState CheckedTarget)
-> ExceptT
     (ArgsCheckState [Arg (Named_ Expr)])
     (TCMT IO)
     (ArgsCheckState CheckedTarget)
forall e r. Call -> ExceptT e (TCMT IO) r -> ExceptT e (TCMT IO) r
traceCallE (Expr
-> [Arg (Named_ Expr)]
-> Type'' Term Term
-> Maybe (Type'' Term Term)
-> Call
CheckArguments Expr
sFun (((Arg (Named_ Expr), Bool) -> Arg (Named_ Expr))
-> [(Arg (Named_ Expr), Bool)] -> [Arg (Named_ Expr)]
forall a b. (a -> b) -> [a] -> [b]
map' (Arg (Named_ Expr), Bool) -> Arg (Named_ Expr)
forall a b. (a, b) -> a
fst [(Arg (Named_ Expr), Bool)]
sArgs) Type'' Term Term
sFunType Maybe (Type'' Term Term)
sResultType) (ExceptT
   (ArgsCheckState [Arg (Named_ Expr)])
   (TCMT IO)
   (ArgsCheckState CheckedTarget)
 -> ExceptT
      (ArgsCheckState [Arg (Named_ Expr)])
      (TCMT IO)
      (ArgsCheckState CheckedTarget))
-> ExceptT
     (ArgsCheckState [Arg (Named_ Expr)])
     (TCMT IO)
     (ArgsCheckState CheckedTarget)
-> ExceptT
     (ArgsCheckState [Arg (Named_ Expr)])
     (TCMT IO)
     (ArgsCheckState CheckedTarget)
forall a b. (a -> b) -> a -> b
$ do
      TCMT IO ()
-> ExceptT (ArgsCheckState [Arg (Named_ Expr)]) (TCMT IO) ()
forall (m :: * -> *) a.
Monad m =>
m a -> ExceptT (ArgsCheckState [Arg (Named_ Expr)]) m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TCMT IO ()
 -> ExceptT (ArgsCheckState [Arg (Named_ Expr)]) (TCMT IO) ())
-> TCMT IO ()
-> ExceptT (ArgsCheckState [Arg (Named_ Expr)]) (TCMT IO) ()
forall a b. (a -> b) -> a -> b
$ [Char] -> Int -> TCMT IO Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.term.args" Int
30 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep
        [ TCMT IO Doc
"checkArgumentsE"
--        , "  sArgs =" <+> prettyA sArgs
        , Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
          [ TCMT IO Doc
"e (argument) =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Named_ Expr -> TCMT IO Doc
forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA Named_ Expr
e
          , TCMT IO Doc
"sFun         =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Expr -> TCMT IO Doc
forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA Expr
sFun
          , TCMT IO Doc
"sFunType     =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Type'' Term Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type'' Term Term -> m Doc
prettyTCM Type'' Term Term
sFunType
          , TCMT IO Doc
"sResultType  =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
-> (Type'' Term Term -> TCMT IO Doc)
-> Maybe (Type'' Term Term)
-> TCMT IO Doc
forall b a. b -> (a -> b) -> Maybe a -> b
maybe TCMT IO Doc
"Nothing" Type'' Term Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type'' Term Term -> m Doc
prettyTCM Maybe (Type'' Term Term)
sResultType
          ]
        ]
      -- First, insert implicit arguments, depending on current argument @arg@.
      let hx :: Hiding
hx = ArgInfo -> Hiding
forall a. LensHiding a => a -> Hiding
getHiding ArgInfo
info  -- hiding of current argument
          mx :: Maybe ArgName
          mx :: Maybe [Char]
mx = Named_ Expr -> Maybe [Char]
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 (Hiding -> Hiding -> Bool
forall a b. (LensHiding a, LensHiding b) => a -> b -> Bool
sameHiding Hiding
hy Hiding
hx) Bool -> Bool -> Bool
|| Bool -> ([Char] -> Bool) -> Maybe [Char] -> Bool
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
False ([Char]
y [Char] -> [Char] -> Bool
forall a. Eq a => a -> a -> Bool
/=) Maybe [Char]
mx
      [Char]
-> Int
-> TCMT IO Doc
-> ExceptT (ArgsCheckState [Arg (Named_ Expr)]) (TCMT IO) ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.term.args" Int
30 (TCMT IO Doc
 -> ExceptT (ArgsCheckState [Arg (Named_ Expr)]) (TCMT IO) ())
-> TCMT IO Doc
-> ExceptT (ArgsCheckState [Arg (Named_ Expr)]) (TCMT IO) ()
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
        [ TCMT IO Doc
"calling implicitCheckedArgs"
        , Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"hx       = " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [Char] -> TCMT IO Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text (Hiding -> [Char]
forall a. Show a => a -> [Char]
show Hiding
hx)
        , Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"mx       = " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
-> ([Char] -> TCMT IO Doc) -> Maybe [Char] -> TCMT IO Doc
forall b a. b -> (a -> b) -> Maybe a -> b
maybe TCMT IO Doc
"nothing" [Char] -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => [Char] -> m Doc
prettyTCM Maybe [Char]
mx
        ]
      (ncargs, sFunType) <- TCM ([Named_ CheckedArg], Type'' Term Term)
-> ExceptT
     (ArgsCheckState [Arg (Named_ Expr)])
     (TCMT IO)
     ([Named_ CheckedArg], Type'' Term Term)
forall (m :: * -> *) a.
Monad m =>
m a -> ExceptT (ArgsCheckState [Arg (Named_ Expr)]) m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TCM ([Named_ CheckedArg], Type'' Term Term)
 -> ExceptT
      (ArgsCheckState [Arg (Named_ Expr)])
      (TCMT IO)
      ([Named_ CheckedArg], Type'' Term Term))
-> TCM ([Named_ CheckedArg], Type'' Term Term)
-> ExceptT
     (ArgsCheckState [Arg (Named_ Expr)])
     (TCMT IO)
     ([Named_ CheckedArg], Type'' Term Term)
forall a b. (a -> b) -> a -> b
$ Int
-> (Hiding -> [Char] -> Bool)
-> Type'' Term Term
-> TCM ([Named_ CheckedArg], Type'' Term Term)
implicitCheckedArgs (-Int
1) Hiding -> [Char] -> Bool
expand Type'' Term Term
sFunType
      -- Separate names from args.
      let (mxs, cargs) = List.unzipWith (\ (Named Maybe NamedName
mx CheckedArg
ca) -> (Maybe NamedName
mx, CheckedArg
ca)) ncargs
          xs           = [Maybe NamedName] -> [NamedName]
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.
      sFunType <- lift $ forcePiUsingInjectivity sFunType

      -- We are done inserting implicit args.  Now, try to check @arg@.
      ifBlocked sFunType
        (\ Blocker
_ Type'' Term Term
sFunType -> ArgsCheckState [Arg (Named_ Expr)]
-> ExceptT
     (ArgsCheckState [Arg (Named_ Expr)])
     (TCMT IO)
     (ArgsCheckState CheckedTarget)
forall a.
ArgsCheckState [Arg (Named_ Expr)]
-> ExceptT (ArgsCheckState [Arg (Named_ Expr)]) (TCMT IO) a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (ArgsCheckState [Arg (Named_ Expr)]
 -> ExceptT
      (ArgsCheckState [Arg (Named_ Expr)])
      (TCMT IO)
      (ArgsCheckState CheckedTarget))
-> ArgsCheckState [Arg (Named_ Expr)]
-> ExceptT
     (ArgsCheckState [Arg (Named_ Expr)])
     (TCMT IO)
     (ArgsCheckState CheckedTarget)
forall a b. (a -> b) -> a -> b
$ ACState
            { acCheckedArgs :: [CheckedArg]
acCheckedArgs = [CheckedArg]
cargs
            , acFun :: Expr
acFun         = Expr
sFun
            , acType :: Type'' Term Term
acType        = Type'' Term Term
sFunType
            , acData :: [Arg (Named_ Expr)]
acData        = ((Arg (Named_ Expr), Bool) -> Arg (Named_ Expr))
-> [(Arg (Named_ Expr), Bool)] -> [Arg (Named_ Expr)]
forall a b. (a -> b) -> [a] -> [b]
map' (Arg (Named_ Expr), Bool) -> Arg (Named_ Expr)
forall a b. (a, b) -> a
fst [(Arg (Named_ Expr), Bool)]
sArgs
            }) {- else -} $ \ NotBlocked
_ Type'' Term Term
sFunType -> do

        -- What can go wrong?

        -- 1. We ran out of function types.
        let shouldBePi :: ExceptT
  (ArgsCheckState [Arg (Named_ Expr)])
  (TCMT IO)
  (ArgsCheckState CheckedTarget)
shouldBePi =
              -- a) It is an explicit argument, but we ran out of function types.
              if ArgInfo -> Bool
forall a. LensHiding a => a -> Bool
visible ArgInfo
info then TCMT IO (ArgsCheckState CheckedTarget)
-> ExceptT
     (ArgsCheckState [Arg (Named_ Expr)])
     (TCMT IO)
     (ArgsCheckState CheckedTarget)
forall a.
TCM a -> ExceptT (ArgsCheckState [Arg (Named_ Expr)]) (TCMT IO) a
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCMT IO (ArgsCheckState CheckedTarget)
 -> ExceptT
      (ArgsCheckState [Arg (Named_ Expr)])
      (TCMT IO)
      (ArgsCheckState CheckedTarget))
-> (TypeError -> TCMT IO (ArgsCheckState CheckedTarget))
-> TypeError
-> ExceptT
     (ArgsCheckState [Arg (Named_ Expr)])
     (TCMT IO)
     (ArgsCheckState CheckedTarget)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypeError -> TCMT IO (ArgsCheckState CheckedTarget)
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError
 -> ExceptT
      (ArgsCheckState [Arg (Named_ Expr)])
      (TCMT IO)
      (ArgsCheckState CheckedTarget))
-> TypeError
-> ExceptT
     (ArgsCheckState [Arg (Named_ Expr)])
     (TCMT IO)
     (ArgsCheckState CheckedTarget)
forall a b. (a -> b) -> a -> b
$ Expr -> Type'' Term Term -> TypeError
CannotApply Expr
sFun Type'' Term Term
sFunType
              -- b) It is an implicit argument, and we did not insert any implicits.
              --    Thus, the type was not a function type to start with.
              else [NamedName]
-> ExceptT
     (ArgsCheckState [Arg (Named_ Expr)])
     (TCMT IO)
     (ArgsCheckState CheckedTarget)
-> (List1 NamedName
    -> ExceptT
         (ArgsCheckState [Arg (Named_ Expr)])
         (TCMT IO)
         (ArgsCheckState CheckedTarget))
-> ExceptT
     (ArgsCheckState [Arg (Named_ Expr)])
     (TCMT IO)
     (ArgsCheckState CheckedTarget)
forall a b. [a] -> b -> (List1 a -> b) -> b
List1.ifNull [NamedName]
xs {-then-} (TCMT IO (ArgsCheckState CheckedTarget)
-> ExceptT
     (ArgsCheckState [Arg (Named_ Expr)])
     (TCMT IO)
     (ArgsCheckState CheckedTarget)
forall a.
TCM a -> ExceptT (ArgsCheckState [Arg (Named_ Expr)]) (TCMT IO) a
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCMT IO (ArgsCheckState CheckedTarget)
 -> ExceptT
      (ArgsCheckState [Arg (Named_ Expr)])
      (TCMT IO)
      (ArgsCheckState CheckedTarget))
-> (TypeError -> TCMT IO (ArgsCheckState CheckedTarget))
-> TypeError
-> ExceptT
     (ArgsCheckState [Arg (Named_ Expr)])
     (TCMT IO)
     (ArgsCheckState CheckedTarget)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypeError -> TCMT IO (ArgsCheckState CheckedTarget)
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError
 -> ExceptT
      (ArgsCheckState [Arg (Named_ Expr)])
      (TCMT IO)
      (ArgsCheckState CheckedTarget))
-> TypeError
-> ExceptT
     (ArgsCheckState [Arg (Named_ Expr)])
     (TCMT IO)
     (ArgsCheckState CheckedTarget)
forall a b. (a -> b) -> a -> b
$ Expr -> Type'' Term Term -> TypeError
CannotApply Expr
sFun Type'' Term Term
sFunType)
              -- 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.
              {-else-} (TCMT IO (ArgsCheckState CheckedTarget)
-> ExceptT
     (ArgsCheckState [Arg (Named_ Expr)])
     (TCMT IO)
     (ArgsCheckState CheckedTarget)
forall a.
TCM a -> ExceptT (ArgsCheckState [Arg (Named_ Expr)]) (TCMT IO) a
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCMT IO (ArgsCheckState CheckedTarget)
 -> ExceptT
      (ArgsCheckState [Arg (Named_ Expr)])
      (TCMT IO)
      (ArgsCheckState CheckedTarget))
-> (List1 NamedName -> TCMT IO (ArgsCheckState CheckedTarget))
-> List1 NamedName
-> ExceptT
     (ArgsCheckState [Arg (Named_ Expr)])
     (TCMT IO)
     (ArgsCheckState CheckedTarget)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypeError -> TCMT IO (ArgsCheckState CheckedTarget)
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> TCMT IO (ArgsCheckState CheckedTarget))
-> (List1 NamedName -> TypeError)
-> List1 NamedName
-> TCMT IO (ArgsCheckState CheckedTarget)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Arg (Named_ Expr) -> List1 NamedName -> TypeError
WrongNamedArgument Arg (Named_ Expr)
arg)

        -- 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 [Arg (Named_ Expr)])
  (TCMT IO)
  (ArgsCheckState CheckedTarget)
wrongPi = [NamedName]
-> ExceptT
     (ArgsCheckState [Arg (Named_ Expr)])
     (TCMT IO)
     (ArgsCheckState CheckedTarget)
-> (List1 NamedName
    -> ExceptT
         (ArgsCheckState [Arg (Named_ Expr)])
         (TCMT IO)
         (ArgsCheckState CheckedTarget))
-> ExceptT
     (ArgsCheckState [Arg (Named_ Expr)])
     (TCMT IO)
     (ArgsCheckState CheckedTarget)
forall a b. [a] -> b -> (List1 a -> b) -> b
List1.ifNull [NamedName]
xs
              -- b) We have not inserted any implicits.
                {-then-} (TCMT IO (ArgsCheckState CheckedTarget)
-> ExceptT
     (ArgsCheckState [Arg (Named_ Expr)])
     (TCMT IO)
     (ArgsCheckState CheckedTarget)
forall a.
TCM a -> ExceptT (ArgsCheckState [Arg (Named_ Expr)]) (TCMT IO) a
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCMT IO (ArgsCheckState CheckedTarget)
 -> ExceptT
      (ArgsCheckState [Arg (Named_ Expr)])
      (TCMT IO)
      (ArgsCheckState CheckedTarget))
-> (TypeError -> TCMT IO (ArgsCheckState CheckedTarget))
-> TypeError
-> ExceptT
     (ArgsCheckState [Arg (Named_ Expr)])
     (TCMT IO)
     (ArgsCheckState CheckedTarget)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypeError -> TCMT IO (ArgsCheckState CheckedTarget)
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError
 -> ExceptT
      (ArgsCheckState [Arg (Named_ Expr)])
      (TCMT IO)
      (ArgsCheckState CheckedTarget))
-> TypeError
-> ExceptT
     (ArgsCheckState [Arg (Named_ Expr)])
     (TCMT IO)
     (ArgsCheckState CheckedTarget)
forall a b. (a -> b) -> a -> b
$ Type'' Term Term -> TypeError
WrongHidingInApplication Type'' Term Term
sFunType)
              -- c) We inserted implicits, but did not find his one.
                {-else-} (TCMT IO (ArgsCheckState CheckedTarget)
-> ExceptT
     (ArgsCheckState [Arg (Named_ Expr)])
     (TCMT IO)
     (ArgsCheckState CheckedTarget)
forall a.
TCM a -> ExceptT (ArgsCheckState [Arg (Named_ Expr)]) (TCMT IO) a
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCMT IO (ArgsCheckState CheckedTarget)
 -> ExceptT
      (ArgsCheckState [Arg (Named_ Expr)])
      (TCMT IO)
      (ArgsCheckState CheckedTarget))
-> (List1 NamedName -> TCMT IO (ArgsCheckState CheckedTarget))
-> List1 NamedName
-> ExceptT
     (ArgsCheckState [Arg (Named_ Expr)])
     (TCMT IO)
     (ArgsCheckState CheckedTarget)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypeError -> TCMT IO (ArgsCheckState CheckedTarget)
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> TCMT IO (ArgsCheckState CheckedTarget))
-> (List1 NamedName -> TypeError)
-> List1 NamedName
-> TCMT IO (ArgsCheckState CheckedTarget)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Arg (Named_ Expr) -> List1 NamedName -> TypeError
WrongNamedArgument Arg (Named_ Expr)
arg)

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

        s <- CheckArgumentsE'State
-> ExceptT
     (ArgsCheckState [Arg (Named_ Expr)])
     (TCMT IO)
     CheckArgumentsE'State
forall a.
a -> ExceptT (ArgsCheckState [Arg (Named_ Expr)]) (TCMT IO) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure CheckArgumentsE'State
s
          { sFun       = A.App (A.defaultAppInfo $ getRange (sFun, arg)) sFun arg
          , sArgs      = args
          , sArgsLen   = sArgsLen - 1
          , sFunType   = sFunType
          , sSkipCheck = next
          }

        -- Check the target type if we can get away with it.
        s <- lift $
          case (sChecked, skip, sResultType) of
            (CheckedTarget
NotCheckedTarget, Bool
False, Just Type'' Term Term
sResultType) | Bool
sArgsVisible -> do
              -- How many visible Π's (up to at most sArgsLen) does
              -- sFunType start with?
              tel <- MaybeT (TCMT IO) (TelV (Type'' Term Term))
-> TCMT IO (Maybe (TelV (Type'' Term Term)))
forall (m :: * -> *) a. MaybeT m a -> m (Maybe a)
runMaybeT (MaybeT (TCMT IO) (TelV (Type'' Term Term))
 -> TCMT IO (Maybe (TelV (Type'' Term Term))))
-> MaybeT (TCMT IO) (TelV (Type'' Term Term))
-> TCMT IO (Maybe (TelV (Type'' Term Term)))
forall a b. (a -> b) -> a -> b
$ Int
-> (Dom' Term (Type'' Term Term) -> Bool)
-> Type'' Term Term
-> MaybeT (TCMT IO) (TelV (Type'' Term Term))
forall (m :: * -> *).
(MonadReduce m, MonadAddContext m) =>
Int
-> (Dom' Term (Type'' Term Term) -> Bool)
-> Type'' Term Term
-> MaybeT m (TelV (Type'' Term Term))
safeTelViewUpTo' Int
sArgsLen Dom' Term (Type'' Term Term) -> Bool
forall a. LensHiding a => a -> Bool
visible Type'' Term Term
sFunType
              case tel of
                Maybe (TelV (Type'' Term Term))
Nothing             -> do
                  -- Telescope has invalidated @rewrite arguments in it, so we
                  -- have to delay checking the target type
                  -- We could make this a bit more efficient by counting the
                  -- number of @rewrite arguments and skipping exactly that many
                  -- args
                  CheckArgumentsE'State -> TCM CheckArgumentsE'State
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return CheckArgumentsE'State
s { sSkipCheck = Skip }
                Just (TelV Tele (Dom' Term (Type'' Term Term))
tel Type'' Term Term
tgt) -> do
                  let visiblePis :: Int
visiblePis = Tele (Dom' Term (Type'' Term Term)) -> Int
forall a. Sized a => a -> Int
size Tele (Dom' Term (Type'' Term Term))
tel

                      -- The free variables less than visiblePis in tgt.
                      freeInTgt :: VarSet
freeInTgt =
                        (VarSet, VarSet) -> VarSet
forall a b. (a, b) -> a
fst ((VarSet, VarSet) -> VarSet) -> (VarSet, VarSet) -> VarSet
forall a b. (a -> b) -> a -> b
$ Int -> VarSet -> (VarSet, VarSet)
VarSet.split Int
visiblePis (VarSet -> (VarSet, VarSet)) -> VarSet -> (VarSet, VarSet)
forall a b. (a -> b) -> a -> b
$ Type'' Term Term -> VarSet
forall t. Free t => t -> VarSet
freeVarSet Type'' Term Term
tgt

                  rigid <- CheckArgumentsE'State -> Type'' Term Term -> TCM IsRigid
isRigid CheckArgumentsE'State
s Type'' Term Term
tgt
                  -- The target must be rigid.
                  case rigid of
                    IsNotRigid IsPermanent
reason ->
                          -- Skip the next visiblePis - 1 - k checks.
                      let skip :: Int -> CheckArgumentsE'State
skip Int
k   = CheckArgumentsE'State
s{ sSkipCheck =
                                        SkipNext $ visiblePis - 1 - k
                                      }
                          dontSkip :: CheckArgumentsE'State
dontSkip = CheckArgumentsE'State
s
                      in CheckArgumentsE'State -> TCM CheckArgumentsE'State
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (CheckArgumentsE'State -> TCM CheckArgumentsE'State)
-> CheckArgumentsE'State -> TCM CheckArgumentsE'State
forall a b. (a -> b) -> a -> b
$ case IsPermanent
reason of
                        IsPermanent
Permanent   -> Int -> CheckArgumentsE'State
skip Int
0
                        IsPermanent
Unspecified -> CheckArgumentsE'State
dontSkip
                        AVar Int
x      ->
                          if Int
x Int -> VarSet -> Bool
`VarSet.member` VarSet
freeInTgt
                          then Int -> CheckArgumentsE'State
skip Int
x
                          else Int -> CheckArgumentsE'State
skip Int
0
                    IsRigid
IsRigid -> do
                      -- Andreas, 2024-03-01, issue #7158 reported by Amy.
                      -- We need to check that the arity of the function type
                      -- is sufficient before checking the target,
                      -- otherwise the target is non-sensical.
                      if Int
visiblePis Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
sArgsLen then CheckArgumentsE'State -> TCM CheckArgumentsE'State
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return CheckArgumentsE'State
s else do

                          -- Is any free variable in tgt less than
                          -- visiblePis?
                      let dep :: Bool
dep = Bool -> Bool
not (VarSet -> Bool
forall a. Null a => a -> Bool
null VarSet
freeInTgt)
                      -- The target must be non-dependent.
                      if Bool
dep then CheckArgumentsE'State -> TCM CheckArgumentsE'State
forall a. a -> TCMT IO a
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).
                      (isSizeLt, sResultType, s) <-
                        if Bool
sSizeLtChecked
                        then (Bool, Type'' Term Term, CheckArgumentsE'State)
-> TCMT IO (Bool, Type'' Term Term, CheckArgumentsE'State)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool
False, Type'' Term Term
sResultType, CheckArgumentsE'State
s)
                        else do
                          sResultType <- Type'' Term Term -> TCMT IO (Type'' Term Term)
forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce Type'' Term Term
sResultType
                          isSizeLt    <- isSizeType sResultType <&> \case
                            Just (BoundedLt Term
_) -> Bool
True
                            Maybe BoundedSize
_                  -> Bool
False
                          return ( isSizeLt
                                , sResultType
                                , s{ sResultType    = Just sResultType
                                    , sSizeLtChecked = True
                                    , sSkipCheck     =
                                        if isSizeLt then Skip else DontSkip
                                    }
                                )
                      if isSizeLt then return s else do

                      let tgt1 = Substitution' (SubstArg (Type'' Term Term))
-> Type'' Term Term -> Type'' Term Term
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst
                                  (Impossible -> Int -> Substitution' Term
forall a. Impossible -> Int -> Substitution' a
strengthenS Impossible
HasCallStack => Impossible
impossible Int
visiblePis)
                                  Type'' Term Term
tgt
                      reportSDoc "tc.term.args.target" 30 $ vcat
                        [ "Checking target types first"
                        , nest 2 $ "inferred =" <+> prettyTCM tgt1
                        , nest 2 $ "expected =" <+> prettyTCM sResultType ]
                      chk <-
                        traceCall
                          (CheckTargetType
                            (fuseRange sFun sArgs) tgt1 sResultType) $
                          CheckedTarget <$>
                            ifNoConstraints_ (compareType sComp tgt1 sResultType)
                              (return Nothing) (return . Just)
                      return s{ sChecked = chk }

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

        -- sFunType <- lift $ forcePi (getHiding info)
        --                  (maybe "_" rangedThing $ nameOf e) sFunType
        case unEl sFunType of
          Pi dom :: Dom' Term (Type'' Term Term)
dom@(Dom' Term (Type'' Term Term) -> Type'' Term Term
forall t e. Dom' t e -> e
unDom -> Type'' Term Term
a) Abs (Type'' Term Term)
b
            | let info' :: ArgInfo
info' = Dom' Term (Type'' Term Term)
dom Dom' Term (Type'' Term Term)
-> Getting ArgInfo (Dom' Term (Type'' Term Term)) ArgInfo
-> ArgInfo
forall s a. s -> Getting a s a -> a
^. Getting ArgInfo (Dom' Term (Type'' Term Term)) ArgInfo
forall t e (f :: * -> *).
Functor f =>
(ArgInfo -> f ArgInfo) -> Dom' t e -> f (Dom' t e)
dInfo,
              let dname :: Maybe NamedName
dname = Dom' Term (Type'' Term Term)
dom Dom' Term (Type'' Term Term)
-> Getting
     (Maybe NamedName) (Dom' Term (Type'' Term Term)) (Maybe NamedName)
-> Maybe NamedName
forall s a. s -> Getting a s a -> a
^. Getting
  (Maybe NamedName) (Dom' Term (Type'' Term Term)) (Maybe NamedName)
forall t e (f :: * -> *).
Functor f =>
(Maybe NamedName -> f (Maybe NamedName))
-> Dom' t e -> f (Dom' t e)
dName,
              let name :: [Char]
name  = [Char] -> Maybe NamedName -> [Char]
forall a.
(LensNamed a, NameOf a ~ NamedName) =>
[Char] -> a -> [Char]
bareNameWithDefault [Char]
"_" Maybe NamedName
dname,
              ArgInfo -> ArgInfo -> Bool
forall a b. (LensHiding a, LensHiding b) => a -> b -> Bool
sameHiding ArgInfo
info ArgInfo
info'
              Bool -> Bool -> Bool
&& (ArgInfo -> Bool
forall a. LensHiding a => a -> Bool
visible ArgInfo
info Bool -> Bool -> Bool
|| Bool -> ([Char] -> Bool) -> Maybe [Char] -> Bool
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
True ([Char]
name [Char] -> [Char] -> Bool
forall a. Eq a => a -> a -> Bool
==) Maybe [Char]
mx) -> do
                Maybe (LocalEquation' Term)
-> (LocalEquation' Term
    -> ExceptT (ArgsCheckState [Arg (Named_ Expr)]) (TCMT IO) ())
-> ExceptT (ArgsCheckState [Arg (Named_ Expr)]) (TCMT IO) ()
forall (m :: * -> *) a. Monad m => Maybe a -> (a -> m ()) -> m ()
whenJust (Dom' Term (Type'' Term Term) -> Maybe (LocalEquation' Term)
forall t e. Dom' t e -> Maybe (LocalEquation' t)
domEq Dom' Term (Type'' Term Term)
dom) \LocalEquation' Term
eq ->
                  [Char]
-> Int
-> TCMT IO Doc
-> ExceptT (ArgsCheckState [Arg (Named_ Expr)]) (TCMT IO) ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"rewriting" Int
30 (TCMT IO Doc
 -> ExceptT (ArgsCheckState [Arg (Named_ Expr)]) (TCMT IO) ())
-> TCMT IO Doc
-> ExceptT (ArgsCheckState [Arg (Named_ Expr)]) (TCMT IO) ()
forall a b. (a -> b) -> a -> b
$
                    TCMT IO Doc
"Applying equational constraint to context: " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> LocalEquation' Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => LocalEquation' Term -> m Doc
prettyTCM LocalEquation' Term
eq
                u <- TCM Term
-> ExceptT (ArgsCheckState [Arg (Named_ Expr)]) (TCMT IO) Term
forall (m :: * -> *) a.
Monad m =>
m a -> ExceptT (ArgsCheckState [Arg (Named_ Expr)]) m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TCM Term
 -> ExceptT (ArgsCheckState [Arg (Named_ Expr)]) (TCMT IO) Term)
-> TCM Term
-> ExceptT (ArgsCheckState [Arg (Named_ Expr)]) (TCMT IO) Term
forall a b. (a -> b) -> a -> b
$ Dom' Term (Type'' Term Term) -> TCM Term -> TCM Term
forall e a. Dom e -> TCM a -> TCM a
applyDomToContext Dom' Term (Type'' Term Term)
dom (TCM Term -> TCM Term) -> TCM Term -> TCM Term
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 = (nameOf e) <|> dname }
                  Arg (Named_ Expr) -> Type'' Term Term -> TCM Term
checkNamedArg (ArgInfo -> Named_ Expr -> Arg (Named_ Expr)
forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
info' Named_ Expr
e') Type'' Term Term
a

                c <- lift $ makeLockConstraint sFunType u
                -- save relevance info' from domain in argument
                let ca = CheckedArg{ caElim :: Elim' Term
caElim = Arg Term -> Elim' Term
forall a. Arg a -> Elim' a
Apply (ArgInfo -> Term -> Arg Term
forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
info' Term
u), caRange :: Range
caRange = Named_ Expr -> Range
forall a. HasRange a => a -> Range
getRange Named_ Expr
e, caConstraint :: Maybe (Abs Constraint)
caConstraint = Maybe (Abs Constraint)
c }
                addCheckedArgs cargs ca $
                  checkArgumentsE' s{ sFunType = absApp b u }
            | Bool
otherwise -> do
                let info' :: ArgInfo
info' = Dom' Term (Type'' Term Term)
dom Dom' Term (Type'' Term Term)
-> Getting ArgInfo (Dom' Term (Type'' Term Term)) ArgInfo
-> ArgInfo
forall s a. s -> Getting a s a -> a
^. Getting ArgInfo (Dom' Term (Type'' Term Term)) ArgInfo
forall t e (f :: * -> *).
Functor f =>
(ArgInfo -> f ArgInfo) -> Dom' t e -> f (Dom' t e)
dInfo
                [Char]
-> Int
-> TCMT IO Doc
-> ExceptT (ArgsCheckState [Arg (Named_ Expr)]) (TCMT IO) ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"error" Int
10 (TCMT IO Doc
 -> ExceptT (ArgsCheckState [Arg (Named_ Expr)]) (TCMT IO) ())
-> TCMT IO Doc
-> ExceptT (ArgsCheckState [Arg (Named_ Expr)]) (TCMT IO) ()
forall a b. (a -> b) -> a -> b
$ Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
                  [ [Char] -> TCMT IO Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text ([Char] -> TCMT IO Doc) -> [Char] -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ [Char]
"info      = " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++! ArgInfo -> [Char]
forall a. Show a => a -> [Char]
show ArgInfo
info
                  , [Char] -> TCMT IO Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text ([Char] -> TCMT IO Doc) -> [Char] -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ [Char]
"info'     = " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++! ArgInfo -> [Char]
forall a. Show a => a -> [Char]
show ArgInfo
info'
                  , [Char] -> TCMT IO Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text ([Char] -> TCMT IO Doc) -> [Char] -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ [Char]
"absName b = " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++! Abs (Type'' Term Term) -> [Char]
forall a. Abs a -> [Char]
absName Abs (Type'' Term Term)
b
                  , [Char] -> TCMT IO Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text ([Char] -> TCMT IO Doc) -> [Char] -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ [Char]
"nameOf e  = " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++! Maybe NamedName -> [Char]
forall a. Show a => a -> [Char]
show (Named_ Expr -> Maybe NamedName
forall name a. Named name a -> Maybe name
nameOf Named_ Expr
e)
                  ]
                ExceptT
  (ArgsCheckState [Arg (Named_ Expr)])
  (TCMT IO)
  (ArgsCheckState CheckedTarget)
wrongPi
          Term
_
            | ArgInfo -> Bool
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'' Term Term -> PathView
sPathView Type'' Term Term
sFunType -> do
                TCMT IO ()
-> ExceptT (ArgsCheckState [Arg (Named_ Expr)]) (TCMT IO) ()
forall (m :: * -> *) a.
Monad m =>
m a -> ExceptT (ArgsCheckState [Arg (Named_ Expr)]) m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TCMT IO ()
 -> ExceptT (ArgsCheckState [Arg (Named_ Expr)]) (TCMT IO) ())
-> TCMT IO ()
-> ExceptT (ArgsCheckState [Arg (Named_ Expr)]) (TCMT IO) ()
forall a b. (a -> b) -> a -> b
$ [Char] -> Int -> TCMT IO Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.term.args" Int
30 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ [Char] -> TCMT IO Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text ([Char] -> TCMT IO Doc) -> [Char] -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ Arg Term -> [Char]
forall a. Show a => a -> [Char]
show Arg Term
bA
                u <- TCM Term
-> ExceptT (ArgsCheckState [Arg (Named_ Expr)]) (TCMT IO) Term
forall (m :: * -> *) a.
Monad m =>
m a -> ExceptT (ArgsCheckState [Arg (Named_ Expr)]) m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TCM Term
 -> ExceptT (ArgsCheckState [Arg (Named_ Expr)]) (TCMT IO) Term)
-> TCM Term
-> ExceptT (ArgsCheckState [Arg (Named_ Expr)]) (TCMT IO) Term
forall a b. (a -> b) -> a -> b
$ Expr -> Type'' Term Term -> TCM Term
checkExpr (Named_ Expr -> Expr
forall name a. Named name a -> a
namedThing Named_ Expr
e) (Type'' Term Term -> TCM Term)
-> TCMT IO (Type'' Term Term) -> TCM Term
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< TCMT IO (Type'' Term Term)
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m (Type'' Term Term)
primIntervalType
                let ca = CheckedArg
                     { caElim :: Elim' Term
caElim       = Term -> Term -> Term -> Elim' Term
forall a. a -> a -> a -> Elim' a
IApply (Arg Term -> Term
forall e. Arg e -> e
unArg Arg Term
x) (Arg Term -> Term
forall e. Arg e -> e
unArg Arg Term
y) Term
u
                     , caRange :: Range
caRange      = Named_ Expr -> Range
forall a. HasRange a => a -> Range
getRange Named_ Expr
e
                     , caConstraint :: Maybe (Abs Constraint)
caConstraint = Maybe (Abs Constraint)
forall a. Maybe a
Nothing
                     }
                addCheckedArgs cargs ca $
                  checkArgumentsE'
                    s{ sChecked = NotCheckedTarget
                     , sFunType = El sort $ unArg bA `apply` [argN u]
                     }
          Term
_ -> ExceptT
  (ArgsCheckState [Arg (Named_ Expr)])
  (TCMT IO)
  (ArgsCheckState CheckedTarget)
shouldBePi
  where
    addCheckedArgs ::
         [CheckedArg]
      -> CheckedArg
      -> CheckArgumentsE'
      -> CheckArgumentsE'
    addCheckedArgs :: [CheckedArg]
-> CheckedArg
-> ExceptT
     (ArgsCheckState [Arg (Named_ Expr)])
     (TCMT IO)
     (ArgsCheckState CheckedTarget)
-> ExceptT
     (ArgsCheckState [Arg (Named_ Expr)])
     (TCMT IO)
     (ArgsCheckState CheckedTarget)
addCheckedArgs [CheckedArg]
cas CheckedArg
ca ExceptT
  (ArgsCheckState [Arg (Named_ Expr)])
  (TCMT IO)
  (ArgsCheckState CheckedTarget)
cont = do
      let upd :: ArgsCheckState a -> ArgsCheckState a
          upd :: forall a. ArgsCheckState a -> ArgsCheckState a
upd ArgsCheckState a
st = ArgsCheckState a
st{ acCheckedArgs = cas ++! ca : acCheckedArgs st }
      -- Add checked arguments to both regular and exceptional result of @cont@.
      (ArgsCheckState [Arg (Named_ Expr)]
 -> ArgsCheckState [Arg (Named_ Expr)])
-> ExceptT
     (ArgsCheckState [Arg (Named_ Expr)])
     (TCMT IO)
     (ArgsCheckState CheckedTarget)
-> ExceptT
     (ArgsCheckState [Arg (Named_ Expr)])
     (TCMT IO)
     (ArgsCheckState CheckedTarget)
forall e (m :: * -> *) a. MonadError e m => (e -> e) -> m a -> m a
withError ArgsCheckState [Arg (Named_ Expr)]
-> ArgsCheckState [Arg (Named_ Expr)]
forall a. ArgsCheckState a -> ArgsCheckState a
upd (ExceptT
   (ArgsCheckState [Arg (Named_ Expr)])
   (TCMT IO)
   (ArgsCheckState CheckedTarget)
 -> ExceptT
      (ArgsCheckState [Arg (Named_ Expr)])
      (TCMT IO)
      (ArgsCheckState CheckedTarget))
-> ExceptT
     (ArgsCheckState [Arg (Named_ Expr)])
     (TCMT IO)
     (ArgsCheckState CheckedTarget)
-> ExceptT
     (ArgsCheckState [Arg (Named_ Expr)])
     (TCMT IO)
     (ArgsCheckState CheckedTarget)
forall a b. (a -> b) -> a -> b
$ ArgsCheckState CheckedTarget -> ArgsCheckState CheckedTarget
forall a. ArgsCheckState a -> ArgsCheckState a
upd (ArgsCheckState CheckedTarget -> ArgsCheckState CheckedTarget)
-> ExceptT
     (ArgsCheckState [Arg (Named_ Expr)])
     (TCMT IO)
     (ArgsCheckState CheckedTarget)
-> ExceptT
     (ArgsCheckState [Arg (Named_ Expr)])
     (TCMT IO)
     (ArgsCheckState CheckedTarget)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ExceptT
  (ArgsCheckState [Arg (Named_ Expr)])
  (TCMT IO)
  (ArgsCheckState CheckedTarget)
cont

-- | 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'' Term Term -> TCM IsRigid
isRigid CheckArgumentsE'State
s Type'' Term Term
t | PathType{} <- CheckArgumentsE'State -> Type'' Term Term -> PathView
sPathView CheckArgumentsE'State
s Type'' Term Term
t =
  -- Path is not rigid.
  IsRigid -> TCM IsRigid
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (IsRigid -> TCM IsRigid) -> IsRigid -> TCM IsRigid
forall a b. (a -> b) -> a -> b
$ IsPermanent -> IsRigid
IsNotRigid IsPermanent
Permanent
isRigid CheckArgumentsE'State
_ (El Sort
_ Term
t) = case Term
t of
  Var Int
x [Elim' Term]
_    -> IsRigid -> TCM IsRigid
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (IsRigid -> TCM IsRigid) -> IsRigid -> TCM IsRigid
forall a b. (a -> b) -> a -> b
$ IsPermanent -> IsRigid
IsNotRigid (Int -> IsPermanent
AVar Int
x)
  Lam{}      -> IsRigid -> TCM IsRigid
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (IsRigid -> TCM IsRigid) -> IsRigid -> TCM IsRigid
forall a b. (a -> b) -> a -> b
$ IsPermanent -> IsRigid
IsNotRigid IsPermanent
Permanent
  Lit{}      -> IsRigid -> TCM IsRigid
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (IsRigid -> TCM IsRigid) -> IsRigid -> TCM IsRigid
forall a b. (a -> b) -> a -> b
$ IsPermanent -> IsRigid
IsNotRigid IsPermanent
Permanent
  Con{}      -> IsRigid -> TCM IsRigid
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (IsRigid -> TCM IsRigid) -> IsRigid -> TCM IsRigid
forall a b. (a -> b) -> a -> b
$ IsPermanent -> IsRigid
IsNotRigid IsPermanent
Permanent
  Pi Dom' Term (Type'' Term Term)
dom Abs (Type'' Term Term)
_   -> IsRigid -> TCM IsRigid
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (IsRigid -> TCM IsRigid) -> IsRigid -> TCM IsRigid
forall a b. (a -> b) -> a -> b
$
                if Dom' Term (Type'' Term Term) -> Bool
forall a. LensHiding a => a -> Bool
visible Dom' Term (Type'' Term Term)
dom then IsRigid
IsRigid else IsPermanent -> IsRigid
IsNotRigid IsPermanent
Permanent
  Sort{}     -> IsRigid -> TCM IsRigid
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (IsRigid -> TCM IsRigid) -> IsRigid -> TCM IsRigid
forall a b. (a -> b) -> a -> b
$ IsPermanent -> IsRigid
IsNotRigid IsPermanent
Permanent
  Level{}    -> IsRigid -> TCM IsRigid
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (IsRigid -> TCM IsRigid) -> IsRigid -> TCM IsRigid
forall a b. (a -> b) -> a -> b
$ IsPermanent -> IsRigid
IsNotRigid IsPermanent
Permanent
  MetaV{}    -> IsRigid -> TCM IsRigid
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (IsRigid -> TCM IsRigid) -> IsRigid -> TCM IsRigid
forall a b. (a -> b) -> a -> b
$ IsPermanent -> IsRigid
IsNotRigid IsPermanent
Unspecified
  DontCare{} -> IsRigid -> TCM IsRigid
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (IsRigid -> TCM IsRigid) -> IsRigid -> TCM IsRigid
forall a b. (a -> b) -> a -> b
$ IsPermanent -> IsRigid
IsNotRigid IsPermanent
Permanent
  Dummy{}    -> IsRigid -> TCM IsRigid
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (IsRigid -> TCM IsRigid) -> IsRigid -> TCM IsRigid
forall a b. (a -> b) -> a -> b
$ IsPermanent -> IsRigid
IsNotRigid IsPermanent
Permanent
  Def QName
d [Elim' Term]
_    -> QName -> TCMT IO Definition
forall (m :: * -> *).
(HasConstInfo m, HasCallStack) =>
QName -> m Definition
getConstInfo QName
d TCMT IO Definition -> (Definition -> Defn) -> TCMT IO Defn
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> Definition -> Defn
theDef TCMT IO Defn -> (Defn -> IsRigid) -> TCM IsRigid
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \case
    Axiom{}                   -> IsRigid
IsRigid
    DataOrRecSig{}            -> IsRigid
IsRigid
    AbstractDefn{}            -> IsRigid
IsRigid
    Function{funClauses :: Defn -> [Clause]
funClauses = [Clause]
cs} -> if [Clause] -> Bool
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{}             -> IsRigid
forall a. HasCallStack => a
__IMPOSSIBLE__
    GeneralizableVar{}        -> IsRigid
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?
  -> A.Expr               -- ^ Function.
  -> [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
-> Expr
-> [Arg (Named_ Expr)]
-> Tele (Dom' Term (Type'' Term Term))
-> TCMT IO ([Elim' Term], Tele (Dom' Term (Type'' Term Term)))
checkArguments_ Comparison
cmp ExpandHidden
exh Expr
fun [Arg (Named_ Expr)]
args Tele (Dom' Term (Type'' Term Term))
tel = TCMT IO ([Elim' Term], Tele (Dom' Term (Type'' Term Term)))
-> TCMT IO ([Elim' Term], Tele (Dom' Term (Type'' Term Term)))
forall a. TCM a -> TCM a
postponeInstanceConstraints (TCMT IO ([Elim' Term], Tele (Dom' Term (Type'' Term Term)))
 -> TCMT IO ([Elim' Term], Tele (Dom' Term (Type'' Term Term))))
-> TCMT IO ([Elim' Term], Tele (Dom' Term (Type'' Term Term)))
-> TCMT IO ([Elim' Term], Tele (Dom' Term (Type'' Term Term)))
forall a b. (a -> b) -> a -> b
$ do
    z <- ExceptT
  (ArgsCheckState [Arg (Named_ Expr)])
  (TCMT IO)
  (ArgsCheckState CheckedTarget)
-> TCM
     (Either
        (ArgsCheckState [Arg (Named_ Expr)])
        (ArgsCheckState CheckedTarget))
forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
runExceptT (ExceptT
   (ArgsCheckState [Arg (Named_ Expr)])
   (TCMT IO)
   (ArgsCheckState CheckedTarget)
 -> TCM
      (Either
         (ArgsCheckState [Arg (Named_ Expr)])
         (ArgsCheckState CheckedTarget)))
-> ExceptT
     (ArgsCheckState [Arg (Named_ Expr)])
     (TCMT IO)
     (ArgsCheckState CheckedTarget)
-> TCM
     (Either
        (ArgsCheckState [Arg (Named_ Expr)])
        (ArgsCheckState CheckedTarget))
forall a b. (a -> b) -> a -> b
$
      Comparison
-> ExpandHidden
-> Expr
-> [Arg (Named_ Expr)]
-> Type'' Term Term
-> Maybe (Type'' Term Term)
-> ExceptT
     (ArgsCheckState [Arg (Named_ Expr)])
     (TCMT IO)
     (ArgsCheckState CheckedTarget)
checkArgumentsE Comparison
cmp ExpandHidden
exh Expr
fun [Arg (Named_ Expr)]
args (Tele (Dom' Term (Type'' Term Term))
-> Type'' Term Term -> Type'' Term Term
telePi Tele (Dom' Term (Type'' Term Term))
tel Type'' Term Term
HasCallStack => Type'' Term Term
__DUMMY_TYPE__) Maybe (Type'' Term Term)
forall a. Maybe a
Nothing
    case z of
      Right (ACState [CheckedArg]
cas Expr
_ Type'' Term Term
t CheckedTarget
_) -> do
        es <- [CheckedArg] -> TCM [Elim' Term]
noHeadConstraints [CheckedArg]
cas
        let TelV tel' _ = telView' t
        return (es, tel')
      Left ArgsCheckState [Arg (Named_ Expr)]
_ -> TCMT IO ([Elim' Term], Tele (Dom' Term (Type'' Term Term)))
forall a. HasCallStack => a
__IMPOSSIBLE__  -- type cannot be blocked as it is generated by telePi

-- | @checkArguments cmp exph hd args t0 t k@ tries @checkArgumentsE cmp exph hd 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 := ((hd : t0) args) : t@.
checkArguments ::
     Comparison
       -- ^ How the inferred type should be compared to the expected result type.
  -> ExpandHidden
       -- ^ Insert trailing hidden arguments?
  -> A.Expr
       -- ^ The function (a head).
  -> [NamedArg A.Expr]
       -- ^ The arguments to check.
  -> Type
       -- ^ Type of the function.
  -> Type
       -- ^ Expected result type (type of the whole application).
  -> (ArgsCheckState CheckedTarget -> TCM Term)
       -- ^ Continuation receiving the check arguments.
  -> TCM Term
checkArguments :: Comparison
-> ExpandHidden
-> Expr
-> [Arg (Named_ Expr)]
-> Type'' Term Term
-> Type'' Term Term
-> (ArgsCheckState CheckedTarget -> TCM Term)
-> TCM Term
checkArguments Comparison
cmp ExpandHidden
exph Expr
hd [Arg (Named_ Expr)]
args Type'' Term Term
t0 Type'' Term Term
t ArgsCheckState CheckedTarget -> TCM Term
k = TCM Term -> TCM Term
forall a. TCM a -> TCM a
postponeInstanceConstraints (TCM Term -> TCM Term) -> TCM Term -> TCM Term
forall a b. (a -> b) -> a -> b
$ do
  z <- ExceptT
  (ArgsCheckState [Arg (Named_ Expr)])
  (TCMT IO)
  (ArgsCheckState CheckedTarget)
-> TCM
     (Either
        (ArgsCheckState [Arg (Named_ Expr)])
        (ArgsCheckState CheckedTarget))
forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
runExceptT (ExceptT
   (ArgsCheckState [Arg (Named_ Expr)])
   (TCMT IO)
   (ArgsCheckState CheckedTarget)
 -> TCM
      (Either
         (ArgsCheckState [Arg (Named_ Expr)])
         (ArgsCheckState CheckedTarget)))
-> ExceptT
     (ArgsCheckState [Arg (Named_ Expr)])
     (TCMT IO)
     (ArgsCheckState CheckedTarget)
-> TCM
     (Either
        (ArgsCheckState [Arg (Named_ Expr)])
        (ArgsCheckState CheckedTarget))
forall a b. (a -> b) -> a -> b
$ Comparison
-> ExpandHidden
-> Expr
-> [Arg (Named_ Expr)]
-> Type'' Term Term
-> Maybe (Type'' Term Term)
-> ExceptT
     (ArgsCheckState [Arg (Named_ Expr)])
     (TCMT IO)
     (ArgsCheckState CheckedTarget)
checkArgumentsE Comparison
cmp ExpandHidden
exph Expr
hd [Arg (Named_ Expr)]
args Type'' Term Term
t0 (Type'' Term Term -> Maybe (Type'' Term Term)
forall a. a -> Maybe a
Just Type'' Term Term
t)
  case z of
    Right ArgsCheckState CheckedTarget
st -> ArgsCheckState CheckedTarget -> TCM Term
k ArgsCheckState CheckedTarget
st
    Left ArgsCheckState [Arg (Named_ Expr)]
problem -> ArgsCheckState [Arg (Named_ Expr)]
-> Comparison
-> ExpandHidden
-> Expr
-> [Arg (Named_ Expr)]
-> Type'' Term Term
-> Type'' Term Term
-> (ArgsCheckState CheckedTarget -> TCM Term)
-> TCM Term
postponeArgs ArgsCheckState [Arg (Named_ Expr)]
problem Comparison
cmp ExpandHidden
exph Expr
hd [Arg (Named_ Expr)]
args Type'' Term Term
t0 Type'' Term Term
t ArgsCheckState CheckedTarget -> TCM Term
k
      -- if unsuccessful, postpone checking until t0 unblocks

postponeArgs ::
     (ArgsCheckState [NamedArg A.Expr])
       -- ^ The last sound state of the arguments checker.
  -> Comparison
       -- ^ How the inferred type should be compared to the expected result type.
  -> ExpandHidden
       -- ^ Insert trailing hidden arguments?
  -> A.Expr
       -- ^ The original function (a head).
  -> [NamedArg A.Expr]
       -- ^ The original arguments to check.
  -> Type
       -- ^ Type of the original function.
  -> Type
       -- ^ Expected result type (type of the whole application).
  -> (ArgsCheckState CheckedTarget -> TCM Term)
       -- ^ Continuation receiving the check arguments.
  -> TCM Term
postponeArgs :: ArgsCheckState [Arg (Named_ Expr)]
-> Comparison
-> ExpandHidden
-> Expr
-> [Arg (Named_ Expr)]
-> Type'' Term Term
-> Type'' Term Term
-> (ArgsCheckState CheckedTarget -> TCM Term)
-> TCM Term
postponeArgs (ACState [CheckedArg]
cas Expr
fun Type'' Term Term
t1 [Arg (Named_ Expr)]
es) Comparison
cmp ExpandHidden
exph Expr
hd [Arg (Named_ Expr)]
args Type'' Term Term
t0 Type'' Term Term
t ArgsCheckState CheckedTarget -> TCM Term
k = do
  [Char] -> Int -> TCMT IO Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.term.expr.args" Int
80 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$
    [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep [ TCMT IO Doc
"postponed checking arguments"
        , Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
4 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
prettyList ((Arg (Named_ Expr) -> TCMT IO Doc)
-> [Arg (Named_ Expr)] -> [TCMT IO Doc]
forall a b. (a -> b) -> [a] -> [b]
map' (Expr -> TCMT IO Doc
forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA (Expr -> TCMT IO Doc)
-> (Arg (Named_ Expr) -> Expr) -> Arg (Named_ Expr) -> TCMT IO Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Named_ Expr -> Expr
forall name a. Named name a -> a
namedThing (Named_ Expr -> Expr)
-> (Arg (Named_ Expr) -> Named_ Expr) -> Arg (Named_ Expr) -> Expr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Arg (Named_ Expr) -> Named_ Expr
forall e. Arg e -> e
unArg) [Arg (Named_ Expr)]
args)
        , Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"against"
        , Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
4 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ Type'' Term Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type'' Term Term -> m Doc
prettyTCM Type'' Term Term
t0
        ] TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
$$
    [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep [ TCMT IO Doc
"progress:"
        , Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"checked" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
prettyList ((CheckedArg -> TCMT IO Doc) -> [CheckedArg] -> [TCMT IO Doc]
forall a b. (a -> b) -> [a] -> [b]
map' (Elim' Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Elim' Term -> m Doc
prettyTCM (Elim' Term -> TCMT IO Doc)
-> (CheckedArg -> Elim' Term) -> CheckedArg -> TCMT IO Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CheckedArg -> Elim' Term
caElim) [CheckedArg]
cas)
        , Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"remaining" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep
            [ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
prettyList ((Arg (Named_ Expr) -> TCMT IO Doc)
-> [Arg (Named_ Expr)] -> [TCMT IO Doc]
forall a b. (a -> b) -> [a] -> [b]
map' (Expr -> TCMT IO Doc
forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA (Expr -> TCMT IO Doc)
-> (Arg (Named_ Expr) -> Expr) -> Arg (Named_ Expr) -> TCMT IO Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Named_ Expr -> Expr
forall name a. Named name a -> a
namedThing (Named_ Expr -> Expr)
-> (Arg (Named_ Expr) -> Named_ Expr) -> Arg (Named_ Expr) -> Expr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Arg (Named_ Expr) -> Named_ Expr
forall e. Arg e -> e
unArg) [Arg (Named_ Expr)]
es)
            , Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
":" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Type'' Term Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type'' Term Term -> m Doc
prettyTCM Type'' Term Term
t1
            ]
        ]
  TypeCheckingProblem -> TCM Term
postponeTypeCheckingProblem_ (TypeCheckingProblem -> TCM Term)
-> TypeCheckingProblem -> TCM Term
forall a b. (a -> b) -> a -> b
$
    Comparison
-> ExpandHidden
-> Expr
-> [Arg (Named_ Expr)]
-> Type'' Term Term
-> Type'' Term Term
-> (ArgsCheckState CheckedTarget -> TCM Term)
-> TypeCheckingProblem
CheckArgs Comparison
cmp ExpandHidden
exph Expr
fun [Arg (Named_ Expr)]
es Type'' Term Term
t1 Type'' Term Term
t ((ArgsCheckState CheckedTarget -> TCM Term) -> TypeCheckingProblem)
-> (ArgsCheckState CheckedTarget -> TCM Term)
-> TypeCheckingProblem
forall a b. (a -> b) -> a -> b
$ \ (ACState [CheckedArg]
cas' Expr
func Type'' Term Term
t CheckedTarget
pid) ->
      ArgsCheckState CheckedTarget -> TCM Term
k (ArgsCheckState CheckedTarget -> TCM Term)
-> ArgsCheckState CheckedTarget -> TCM Term
forall a b. (a -> b) -> a -> b
$ [CheckedArg]
-> Expr
-> Type'' Term Term
-> CheckedTarget
-> ArgsCheckState CheckedTarget
forall a.
[CheckedArg] -> Expr -> Type'' Term Term -> a -> ArgsCheckState a
ACState ([CheckedArg]
cas [CheckedArg] -> [CheckedArg] -> [CheckedArg]
forall a. [a] -> [a] -> [a]
++! [CheckedArg]
cas') Expr
func Type'' Term Term
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
       -- ^ How the inferred type of the application should be compared to the expected type.
  -> A.Expr
       -- ^ The whole application expression.
  -> Type
       -- ^ The expected type of the whole application.
  -> ConHead
       -- ^ The head of the application.
  -> A.Expr
       -- ^ The original head of the application.
  -> [NamedArg A.Expr]
       -- ^ The arguments.
  -> TCM Term
checkConstructorApplication :: Comparison
-> Expr
-> Type'' Term Term
-> ConHead
-> Expr
-> [Arg (Named_ Expr)]
-> TCM Term
checkConstructorApplication Comparison
cmp Expr
org Type'' Term Term
t ConHead
c Expr
hd [Arg (Named_ Expr)]
args = do
  [Char] -> Int -> TCMT IO Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.term.con" Int
50 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
    [ TCMT IO Doc
"entering checkConstructorApplication"
    , Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
      [ TCMT IO Doc
"org  =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Expr -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Expr -> m Doc
prettyTCM Expr
org
      , TCMT IO Doc
"t    =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Type'' Term Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type'' Term Term -> m Doc
prettyTCM Type'' Term Term
t
      , TCMT IO Doc
"c    =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> ConHead -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => ConHead -> m Doc
prettyTCM ConHead
c
      , TCMT IO Doc
"args =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> do [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
prettyList ([TCMT IO Doc] -> TCMT IO Doc) -> [TCMT IO Doc] -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ (Arg (Named_ Expr) -> TCMT IO Doc)
-> [Arg (Named_ Expr)] -> [TCMT IO Doc]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Arg (Named_ Expr) -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Arg (Named_ Expr) -> m Doc
prettyTCM [Arg (Named_ Expr)]
args
    ] ]

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

  checkModality (conName c) cdef

  let paramsGiven = [Arg (Named_ Expr)] -> Bool
checkForParams [Arg (Named_ Expr)]
args
  if paramsGiven then fallback else do
    reportSDoc "tc.term.con" 50 $ "checkConstructorApplication: no parameters explicitly supplied, continuing..."

    let Constructor{conData = d, conPars = npars} = theDef cdef
    reportSDoc "tc.term.con" 50 $ nest 2 $ "d    =" <+> prettyTCM 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
    t0 <- reduce (Def d [])
    tReduced <- reduce t
    case (t0, unEl tReduced) of -- Only fully applied constructors get special treatment
      (Def QName
d0 [Elim' Term]
_, Def QName
d' [Elim' Term]
es) -> do
        let ~(Just [Arg Term]
vs) = [Elim' Term] -> Maybe [Arg Term]
forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims [Elim' Term]
es
        [Char] -> Int -> TCMT IO Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.term.con" Int
50 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"d0   =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> QName -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM QName
d0
        [Char] -> Int -> TCMT IO Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.term.con" Int
50 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"d'   =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> QName -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM QName
d'
        [Char] -> Int -> TCMT IO Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.term.con" Int
50 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"vs   =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [Arg Term] -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => [Arg Term] -> m Doc
prettyTCM [Arg Term]
vs
        if QName
d' QName -> QName -> Bool
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.
         npars' <- QName -> TCMT IO (Maybe Int)
forall (m :: * -> *).
(HasCallStack, HasConstInfo m) =>
QName -> m (Maybe Int)
getNumberOfParameters QName
d'
         caseMaybe (sequenceA $ Pair (Just npars) npars') fallback $ \ (Pair Int
n Int
n') -> do
           [Char] -> Int -> TCMT IO Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.term.con" Int
50 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ [Char] -> TCMT IO Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text ([Char] -> TCMT IO Doc) -> [Char] -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ [Char]
"n    = " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++! Int -> [Char]
forall a. Show a => a -> [Char]
show Int
n
           [Char] -> Int -> TCMT IO Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.term.con" Int
50 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ [Char] -> TCMT IO Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text ([Char] -> TCMT IO Doc) -> [Char] -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ [Char]
"n'   = " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++! Int -> [Char]
forall a. Show a => a -> [Char]
show Int
n'
           Bool -> TCMT IO () -> TCMT IO ()
forall b (m :: * -> *). (IsBool b, Monad m) => b -> m () -> m ()
when (Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
n')  -- preprocessor does not like ', so put on next line
             TCMT IO ()
forall a. HasCallStack => a
__IMPOSSIBLE__
           let ps :: [Arg Term]
ps    = Int -> [Arg Term] -> [Arg Term]
forall a. Int -> [a] -> [a]
take Int
n ([Arg Term] -> [Arg Term]) -> [Arg Term] -> [Arg Term]
forall a b. (a -> b) -> a -> b
$ Int -> [Arg Term] -> [Arg Term]
forall a. Int -> [a] -> [a]
drop (Int
n' Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
n) [Arg Term]
vs
               ctype :: Type'' Term Term
ctype = Definition -> Type'' Term Term
defType Definition
cdef
           [Char] -> Int -> TCMT IO Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.term.con" Int
20 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
             [ TCMT IO Doc
"special checking of constructor application of" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> ConHead -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => ConHead -> m Doc
prettyTCM ConHead
c
             , Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat [ TCMT IO Doc
"ps     =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [Arg Term] -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => [Arg Term] -> m Doc
prettyTCM [Arg Term]
ps
                             , TCMT IO Doc
"ctype  =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Type'' Term Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type'' Term Term -> m Doc
prettyTCM Type'' Term Term
ctype ] ]
           let ctype' :: Type'' Term Term
ctype' = Type'' Term Term
ctype Type'' Term Term -> [Arg Term] -> Type'' Term Term
`piApply` [Arg Term]
ps
           [Char] -> Int -> TCMT IO Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.term.con" Int
20 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"ctype' =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Type'' Term Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type'' Term Term -> m Doc
prettyTCM Type'' Term Term
ctype'
           -- get the parameter names
           let TelV Tele (Dom' Term (Type'' Term Term))
ptel Type'' Term Term
_ = Int -> Type'' Term Term -> TelV (Type'' Term Term)
telView'UpTo Int
n Type'' Term Term
ctype
           let pnames :: [Dom' Term [Char]]
pnames = (Dom' Term ([Char], Type'' Term Term) -> Dom' Term [Char])
-> [Dom' Term ([Char], Type'' Term Term)] -> [Dom' Term [Char]]
forall a b. (a -> b) -> [a] -> [b]
map' ((([Char], Type'' Term Term) -> [Char])
-> Dom' Term ([Char], Type'' Term Term) -> Dom' Term [Char]
forall a b. (a -> b) -> Dom' Term a -> Dom' Term b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ([Char], Type'' Term Term) -> [Char]
forall a b. (a, b) -> a
fst) ([Dom' Term ([Char], Type'' Term Term)] -> [Dom' Term [Char]])
-> [Dom' Term ([Char], Type'' Term Term)] -> [Dom' Term [Char]]
forall a b. (a -> b) -> a -> b
$ Tele (Dom' Term (Type'' Term Term))
-> [Dom' Term ([Char], Type'' Term Term)]
forall t. Tele (Dom t) -> [Dom ([Char], t)]
telToList Tele (Dom' Term (Type'' Term Term))
ptel
           -- drop the parameter arguments
               args' :: [Arg (Named_ Expr)]
args' = [Dom' Term [Char]] -> [Arg (Named_ Expr)] -> [Arg (Named_ Expr)]
dropArgs [Dom' Term [Char]]
pnames [Arg (Named_ Expr)]
args
           -- check the non-parameter arguments
           expandLast <- Lens' TCEnv ExpandHidden -> TCMT IO ExpandHidden
forall (m :: * -> *) a. MonadTCEnv m => Lens' TCEnv a -> m a
viewTC (ExpandHidden -> f ExpandHidden) -> TCEnv -> f TCEnv
Lens' TCEnv ExpandHidden
eExpandLast
           checkArguments cmp expandLast hd args' ctype' t \ st :: ArgsCheckState CheckedTarget
st@(ACState [CheckedArg]
_ Expr
_ Type'' Term Term
t' CheckedTarget
targetCheck) -> do
             [Char] -> Int -> TCMT IO Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.term.con" Int
20 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
               [ [Char] -> TCMT IO Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text [Char]
"es     =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [Elim' Term] -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => [Elim' Term] -> m Doc
prettyTCM [Elim' Term]
es
               , [Char] -> TCMT IO Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text [Char]
"t'     =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Type'' Term Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type'' Term Term -> m Doc
prettyTCM Type'' Term Term
t' ]
             v <- ([Elim' Term] -> Term) -> ArgsCheckState CheckedTarget -> TCM Term
forall a. ([Elim' Term] -> Term) -> ArgsCheckState a -> TCM Term
checkHeadConstraints (ConHead -> ConInfo -> [Elim' Term] -> Term
Con ConHead
c ConInfo
ConOCon) ArgsCheckState CheckedTarget
st
             coerce' cmp targetCheck v t' t
      (Term, Term)
_ -> do
        [Char] -> Int -> TCMT IO Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.term.con" Int
50 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
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'' Term Term
-> Expr
-> [Arg (Named_ Expr)]
-> TCM Term
checkHeadApplication Comparison
cmp Expr
org Type'' Term Term
t (AmbiguousQName -> Expr
A.Con (QName -> AmbiguousQName
unambiguous (QName -> AmbiguousQName) -> QName -> AmbiguousQName
forall a b. (a -> b) -> a -> b
$ ConHead -> QName
conName ConHead
c)) [Arg (Named_ 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 :: [Arg (Named_ Expr)] -> Bool
checkForParams [Arg (Named_ Expr)]
args =
      let ([Arg (Named_ Expr)]
hargs, [Arg (Named_ Expr)]
rest) = (Arg (Named_ Expr) -> Bool)
-> [Arg (Named_ Expr)]
-> ([Arg (Named_ Expr)], [Arg (Named_ Expr)])
forall a. (a -> Bool) -> [a] -> ([a], [a])
break Arg (Named_ Expr) -> Bool
forall a. LensHiding a => a -> Bool
visible [Arg (Named_ Expr)]
args
          notUnderscore :: Expr -> Bool
notUnderscore A.Underscore{} = Bool
False
          notUnderscore Expr
_              = Bool
True
      in  (Arg (Named_ Expr) -> Bool) -> [Arg (Named_ Expr)] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (Expr -> Bool
notUnderscore (Expr -> Bool)
-> (Arg (Named_ Expr) -> Expr) -> Arg (Named_ Expr) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expr -> Expr
unScope (Expr -> Expr)
-> (Arg (Named_ Expr) -> Expr) -> Arg (Named_ Expr) -> Expr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Arg (Named_ Expr) -> Expr
forall a. NamedArg a -> a
namedArg) [Arg (Named_ Expr)]
hargs

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

        namedPar :: b -> [Dom' t b] -> Maybe [Dom' t b]
namedPar   b
x = (Dom' t b -> Bool) -> [Dom' t b] -> Maybe [Dom' t b]
forall {t}. (t -> Bool) -> [t] -> Maybe [t]
dropPar ((b
x b -> b -> Bool
forall a. Eq a => a -> a -> Bool
==) (b -> Bool) -> (Dom' t b -> b) -> Dom' t b -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Dom' t b -> b
forall t e. Dom' t e -> e
unDom)
        unnamedPar :: a -> [b] -> Maybe [b]
unnamedPar a
h = (b -> Bool) -> [b] -> Maybe [b]
forall {t}. (t -> Bool) -> [t] -> Maybe [t]
dropPar (a -> b -> Bool
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    = [t] -> Maybe [t]
forall a. a -> Maybe a
Just [t]
ps
                              | Bool
otherwise = (t -> Bool) -> [t] -> Maybe [t]
dropPar t -> Bool
this [t]
ps
        dropPar t -> Bool
_ [] = Maybe [t]
forall a. Maybe a
Nothing

-- | Return an unblocking action in case of failure.
type DisambiguateConstructor = TCM (Either (Blocker, ConstructorDisambiguationData) ConHead)

-- | Successfully disambiguate constructor with given choice.
decideOn :: ConHead -> DisambiguateConstructor
decideOn :: ConHead -> DisambiguateConstructor
decideOn ConHead
c = do
  [Char] -> Int -> [Char] -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"tc.check.term.con" Int
40 ([Char] -> TCMT IO ()) -> [Char] -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ [Char]
"  decided on: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++! ConHead -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow ConHead
c
  Induction -> QName -> TCMT IO ()
storeDisambiguatedConstructor (ConHead -> Induction
conInductive ConHead
c) (ConHead -> QName
conName ConHead
c)
  Either (Blocker, ConstructorDisambiguationData) ConHead
-> DisambiguateConstructor
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Either (Blocker, ConstructorDisambiguationData) ConHead
 -> DisambiguateConstructor)
-> Either (Blocker, ConstructorDisambiguationData) ConHead
-> DisambiguateConstructor
forall a b. (a -> b) -> a -> b
$ ConHead -> Either (Blocker, ConstructorDisambiguationData) ConHead
forall a b. b -> Either a b
Right ConHead
c

-- | Returns an unblocking action in case of failure.
disambiguateConstructor :: AmbiguousQName -> A.Args -> Type -> DisambiguateConstructor
disambiguateConstructor :: AmbiguousQName
-> [Arg (Named_ Expr)]
-> Type'' Term Term
-> DisambiguateConstructor
disambiguateConstructor AmbiguousQName
ambC [Arg (Named_ Expr)]
args Type'' Term Term
t = do
  [Char] -> Int -> [Char] -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"tc.check.term.con" Int
40 ([Char] -> TCMT IO ()) -> [Char] -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ [Char]
"Ambiguous constructor: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++! AmbiguousQName -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow AmbiguousQName
ambC
  [Char] -> Int -> TCMT IO Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.check.term.con" Int
40 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat ([TCMT IO Doc] -> TCMT IO Doc) -> [TCMT IO Doc] -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"Arguments:" TCMT IO Doc -> [TCMT IO Doc] -> [TCMT IO Doc]
forall a. a -> [a] -> [a]
: (Arg (Named_ Expr) -> TCMT IO Doc)
-> [Arg (Named_ Expr)] -> [TCMT IO Doc]
forall a b. (a -> b) -> [a] -> [b]
map' (Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCMT IO Doc -> TCMT IO Doc)
-> (Arg (Named_ Expr) -> TCMT IO Doc)
-> Arg (Named_ Expr)
-> TCMT IO Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Arg (Named_ Expr) -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Arg (Named_ Expr) -> m Doc
prettyTCM) [Arg (Named_ Expr)]
args
  let cs0 :: NonEmpty QName
cs0 = AmbiguousQName -> NonEmpty QName
getAmbiguous AmbiguousQName
ambC

  -- Get the datatypes of the various constructors
  let getData :: Defn -> QName
getData Constructor{conData :: Defn -> QName
conData = QName
d} = QName
d
      getData Defn
_                        = QName
forall a. HasCallStack => a
__IMPOSSIBLE__
  [Char] -> Int -> [Char] -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"tc.check.term.con" Int
40 ([Char] -> TCMT IO ()) -> [Char] -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ [Char]
"  ranges before: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++! Range -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow (NonEmpty QName -> Range
forall a. HasRange a => a -> Range
getRange NonEmpty 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
  ccons  <- List1 (Either SigError (QName, ConHead)) -> [(QName, ConHead)]
forall a b. List1 (Either a b) -> [b]
List1.rights (List1 (Either SigError (QName, ConHead)) -> [(QName, ConHead)])
-> TCMT IO (List1 (Either SigError (QName, ConHead)))
-> TCMT IO [(QName, ConHead)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do
     NonEmpty QName
-> (QName -> TCMT IO (Either SigError (QName, ConHead)))
-> TCMT IO (List1 (Either SigError (QName, ConHead)))
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM NonEmpty QName
cs0 ((QName -> TCMT IO (Either SigError (QName, ConHead)))
 -> TCMT IO (List1 (Either SigError (QName, ConHead))))
-> (QName -> TCMT IO (Either SigError (QName, ConHead)))
-> TCMT IO (List1 (Either SigError (QName, ConHead)))
forall a b. (a -> b) -> a -> b
$ \ QName
c -> (ConHead -> (QName, ConHead))
-> Either SigError ConHead -> Either SigError (QName, ConHead)
forall b d a. (b -> d) -> Either a b -> Either a d
mapRight (QName
c,) (Either SigError ConHead -> Either SigError (QName, ConHead))
-> TCMT IO (Either SigError ConHead)
-> TCMT IO (Either SigError (QName, ConHead))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> HasCallStack => QName -> TCMT IO (Either SigError ConHead)
QName -> TCMT IO (Either SigError ConHead)
getConForm QName
c
  reportSLn "tc.check.term.con" 40 $ "  reduced: " ++! prettyShow (map' snd ccons)
  case ccons of
    []    -> TypeError -> DisambiguateConstructor
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> DisambiguateConstructor)
-> TypeError -> DisambiguateConstructor
forall a b. (a -> b) -> a -> b
$ QName -> TypeError
AbstractConstructorNotInScope (QName -> TypeError) -> QName -> TypeError
forall a b. (a -> b) -> a -> b
$ NonEmpty QName -> QName
forall a. NonEmpty a -> a
List1.head NonEmpty QName
cs0
    [(QName
c0,ConHead
con)] -> do
      let c :: ConHead
c = QName -> ConHead -> ConHead
forall a. LensConName a => QName -> a -> a
setConName QName
c0 ConHead
con
      [Char] -> Int -> [Char] -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"tc.check.term.con" Int
40 ([Char] -> TCMT IO ()) -> [Char] -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ [Char]
"  only one non-abstract constructor: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++! ConHead -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow ConHead
c
      ConHead -> DisambiguateConstructor
decideOn ConHead
c
    cons :: (QName, ConHead)
cons@(QName
c0,ConHead
_):[(QName, ConHead)]
conss   -> do
      dcs :: List1 (QName, Type, ConHead) <- NonEmpty (QName, ConHead)
-> ((QName, ConHead) -> TCMT IO (QName, Type'' Term Term, ConHead))
-> TCMT IO (NonEmpty (QName, Type'' Term Term, ConHead))
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM ((QName, ConHead)
cons (QName, ConHead) -> [(QName, ConHead)] -> NonEmpty (QName, ConHead)
forall a. a -> [a] -> NonEmpty a
:| [(QName, ConHead)]
conss) (((QName, ConHead) -> TCMT IO (QName, Type'' Term Term, ConHead))
 -> TCMT IO (NonEmpty (QName, Type'' Term Term, ConHead)))
-> ((QName, ConHead) -> TCMT IO (QName, Type'' Term Term, ConHead))
-> TCMT IO (NonEmpty (QName, Type'' Term Term, ConHead))
forall a b. (a -> b) -> a -> b
$ \ (QName
c, ConHead
con) -> do
        t   <- Definition -> Type'' Term Term
defType (Definition -> Type'' Term Term)
-> TCMT IO Definition -> TCMT IO (Type'' Term Term)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> TCMT IO Definition
forall (m :: * -> *).
(HasConstInfo m, HasCallStack) =>
QName -> m Definition
getConstInfo QName
c
        def <- getConInfo con
        pure (getData (theDef def), t, setConName c con)
      resolveAmbiguousConstructor $ ConstructorDisambiguationData c0 dcs args t

-- | Retry a constructor disambiguation.
disambiguateConstructor' :: ConstructorDisambiguationData -> (ConHead -> TCM Term) -> TCM Term
disambiguateConstructor' :: ConstructorDisambiguationData -> (ConHead -> TCM Term) -> TCM Term
disambiguateConstructor' ConstructorDisambiguationData
bcd ConHead -> TCM Term
cont = do
  (ConHead -> TCM Term) -> DisambiguateConstructor -> TCM Term
afterDisambiguation ConHead -> TCM Term
cont (DisambiguateConstructor -> TCM Term)
-> DisambiguateConstructor -> TCM Term
forall a b. (a -> b) -> a -> b
$ ConstructorDisambiguationData -> DisambiguateConstructor
resolveAmbiguousConstructor ConstructorDisambiguationData
bcd

-- | Postpone a failing disambiguation or call given continuation.
afterDisambiguation :: (ConHead -> TCM Term) -> DisambiguateConstructor -> TCM Term
afterDisambiguation :: (ConHead -> TCM Term) -> DisambiguateConstructor -> TCM Term
afterDisambiguation ConHead -> TCM Term
cont DisambiguateConstructor
run =
  DisambiguateConstructor
run DisambiguateConstructor
-> (Either (Blocker, ConstructorDisambiguationData) ConHead
    -> TCM Term)
-> TCM Term
forall a b. TCMT IO a -> (a -> TCMT IO b) -> TCMT IO b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
    Left (Blocker
unblock, ConstructorDisambiguationData
bcd) -> TypeCheckingProblem -> Blocker -> TCM Term
postponeTypeCheckingProblem (ConstructorDisambiguationData
-> (ConHead -> TCM Term) -> TypeCheckingProblem
DisambiguateConstructor ConstructorDisambiguationData
bcd ConHead -> TCM Term
cont) Blocker
unblock
    Right ConHead
c -> ConHead -> TCM Term
cont ConHead
c

-- | Resolve ambiguous constructor by looking at target type and argument skeleton.
resolveAmbiguousConstructor :: ConstructorDisambiguationData -> DisambiguateConstructor
resolveAmbiguousConstructor :: ConstructorDisambiguationData -> DisambiguateConstructor
resolveAmbiguousConstructor bcd :: ConstructorDisambiguationData
bcd@(ConstructorDisambiguationData QName
c0 NonEmpty (QName, Type'' Term Term, ConHead)
dcs1 [Arg (Named_ Expr)]
args Type'' Term Term
t) = do
      let dcs :: [Item (NonEmpty (QName, Type'' Term Term, ConHead))]
dcs = NonEmpty (QName, Type'' Term Term, ConHead)
-> [Item (NonEmpty (QName, Type'' Term Term, ConHead))]
forall l. IsList l => l -> [Item l]
List1.toList NonEmpty (QName, Type'' Term Term, ConHead)
dcs1

      -- Lets look at the target type at this point
      TelV tel t1 <- Type'' Term Term -> TCMT IO (TelV (Type'' Term Term))
forall (m :: * -> *).
PureTCM m =>
Type'' Term Term -> m (TelV (Type'' Term Term))
telViewPath Type'' Term Term
t
      addContext tel $ do
       reportSDoc "tc.check.term.con" 40 $ nest 2 $
         "target type: " <+> prettyTCM t1
       -- If we don't have a target type yet, try to look at the argument types.
       ifBlocked t1 (\ Blocker
b Type'' Term Term
_ -> [(QName, Type'' Term Term, ConHead)]
-> [Arg (Named_ Expr)]
-> DisambiguateConstructor
-> DisambiguateConstructor
disambiguateByArgs [(QName, Type'' Term Term, ConHead)]
[Item (NonEmpty (QName, Type'' Term Term, ConHead))]
dcs [Arg (Named_ Expr)]
args (DisambiguateConstructor -> DisambiguateConstructor)
-> DisambiguateConstructor -> DisambiguateConstructor
forall a b. (a -> b) -> a -> b
$ Blocker -> DisambiguateConstructor
postpone Blocker
b) $ \ NotBlocked
_ Type'' Term Term
t' ->
         TCMT IO (Maybe (QName, DataOrRecord))
-> DisambiguateConstructor
-> ((QName, DataOrRecord) -> DisambiguateConstructor)
-> DisambiguateConstructor
forall (m :: * -> *) a b.
Monad m =>
m (Maybe a) -> m b -> (a -> m b) -> m b
caseMaybeM (Term -> TCMT IO (Maybe (QName, DataOrRecord))
isDataOrRecord (Term -> TCMT IO (Maybe (QName, DataOrRecord)))
-> Term -> TCMT IO (Maybe (QName, DataOrRecord))
forall a b. (a -> b) -> a -> b
$ Type'' Term Term -> Term
forall t a. Type'' t a -> a
unEl Type'' Term Term
t') (Type'' Term Term -> DisambiguateConstructor
badCon Type'' Term Term
t') (((QName, DataOrRecord) -> DisambiguateConstructor)
 -> DisambiguateConstructor)
-> ((QName, DataOrRecord) -> DisambiguateConstructor)
-> DisambiguateConstructor
forall a b. (a -> b) -> a -> b
$ \ (QName
d, DataOrRecord
_) -> do
           let dcs' :: [(QName, Type'' Term Term, ConHead)]
dcs' = ((QName, Type'' Term Term, ConHead) -> Bool)
-> [(QName, Type'' Term Term, ConHead)]
-> [(QName, Type'' Term Term, ConHead)]
forall a. (a -> Bool) -> [a] -> [a]
filter ((QName
d QName -> QName -> Bool
forall a. Eq a => a -> a -> Bool
==) (QName -> Bool)
-> ((QName, Type'' Term Term, ConHead) -> QName)
-> (QName, Type'' Term Term, ConHead)
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (QName, Type'' Term Term, ConHead) -> QName
forall a b c. (a, b, c) -> a
fst3) [(QName, Type'' Term Term, ConHead)]
[Item (NonEmpty (QName, Type'' Term Term, ConHead))]
dcs
           case ((QName, Type'' Term Term, ConHead) -> ConHead)
-> [(QName, Type'' Term Term, ConHead)] -> [ConHead]
forall a b. (a -> b) -> [a] -> [b]
map' (QName, Type'' Term Term, ConHead) -> ConHead
forall a b c. (a, b, c) -> c
thd3 [(QName, Type'' Term Term, ConHead)]
dcs' of
             [ConHead
c] -> ConHead -> DisambiguateConstructor
decideOn ConHead
c
             []  -> Type'' Term Term -> DisambiguateConstructor
badCon (Type'' Term Term -> DisambiguateConstructor)
-> Type'' Term Term -> DisambiguateConstructor
forall a b. (a -> b) -> a -> b
$ Type'' Term Term
t' Type'' Term Term -> Term -> Type'' Term Term
forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> QName -> [Elim' Term] -> Term
Def QName
d []
             -- If the information from the target type did not eliminate ambiguity fully,
             -- try to further eliminate alternatives by looking at the arguments.
             ConHead
c:[ConHead]
cs-> [(QName, Type'' Term Term, ConHead)]
-> [Arg (Named_ Expr)]
-> DisambiguateConstructor
-> DisambiguateConstructor
disambiguateByArgs [(QName, Type'' Term Term, ConHead)]
dcs' [Arg (Named_ Expr)]
args (DisambiguateConstructor -> DisambiguateConstructor)
-> DisambiguateConstructor -> DisambiguateConstructor
forall a b. (a -> b) -> a -> b
$
                      TypeError -> DisambiguateConstructor
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> DisambiguateConstructor)
-> TypeError -> DisambiguateConstructor
forall a b. (a -> b) -> a -> b
$ QName -> NonEmpty QName -> TypeError
CantResolveOverloadedConstructorsTargetingSameDatatype QName
d (NonEmpty QName -> TypeError) -> NonEmpty QName -> TypeError
forall a b. (a -> b) -> a -> b
$
                        (ConHead -> QName) -> NonEmpty ConHead -> NonEmpty QName
forall a b. (a -> b) -> NonEmpty a -> NonEmpty b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ConHead -> QName
conName (NonEmpty ConHead -> NonEmpty QName)
-> NonEmpty ConHead -> NonEmpty QName
forall a b. (a -> b) -> a -> b
$ ConHead
c ConHead -> [ConHead] -> NonEmpty ConHead
forall a. a -> [a] -> NonEmpty a
:| [ConHead]
cs
  where
    postpone :: Blocker -> DisambiguateConstructor
postpone Blocker
b = Either (Blocker, ConstructorDisambiguationData) ConHead
-> DisambiguateConstructor
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Either (Blocker, ConstructorDisambiguationData) ConHead
 -> DisambiguateConstructor)
-> Either (Blocker, ConstructorDisambiguationData) ConHead
-> DisambiguateConstructor
forall a b. (a -> b) -> a -> b
$ (Blocker, ConstructorDisambiguationData)
-> Either (Blocker, ConstructorDisambiguationData) ConHead
forall a b. a -> Either a b
Left (Blocker
b, ConstructorDisambiguationData
bcd)
    badCon :: Type'' Term Term -> DisambiguateConstructor
badCon Type'' Term Term
t = TypeError -> DisambiguateConstructor
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> DisambiguateConstructor)
-> TypeError -> DisambiguateConstructor
forall a b. (a -> b) -> a -> b
$ QName -> Type'' Term Term -> TypeError
ConstructorDoesNotTargetGivenType QName
c0 Type'' Term Term
t

-- | Disambiguate constructor by looking at its arguments.
--
-- Look at simple visible arguments (variables (bound and generalizable ones) and defined names).
-- From these we can compute an approximate type effortlessly:
-- 1. Throw away hidden domains (needed for generalizable variables).
-- 2. If the remainder is a defined name that is not blocked on anything, we take this name as
--    approximate type of the argument.
-- This gives us a skeleton @[Maybe QName]@.  Compute the same from the constructor types
-- of the candidates and see if we find any mismatches that allow us to rule out the candidate.
disambiguateByArgs :: [(QName, Type, ConHead)] -> A.Args -> DisambiguateConstructor -> DisambiguateConstructor
disambiguateByArgs :: [(QName, Type'' Term Term, ConHead)]
-> [Arg (Named_ Expr)]
-> DisambiguateConstructor
-> DisambiguateConstructor
disambiguateByArgs [(QName, Type'' Term Term, ConHead)]
dcs [Arg (Named_ Expr)]
args DisambiguateConstructor
fallback = do

    -- Look for visible arguments that are just variables,
    -- so that we can get their type directly from the context
    -- without full-fledged type inference.
    askel <- TCM [Maybe QName]
visibleVarArgs
    reportSDoc "tc.check.term.con" 40 $ hsep $
      "trying disambiguation by arguments" : map' prettyTCM askel
    reportSDoc "tc.check.term.con" 80 $ hsep $
      "trying disambiguation by arguments" : map' pretty askel

    -- Filter out candidates with definitive mismatches.
    cands <- filterM (\ (QName
_d, Type'' Term Term
t, ConHead
_c) -> [Maybe QName] -> [Maybe QName] -> TCMT IO Bool
matchSkel [Maybe QName]
askel ([Maybe QName] -> TCMT IO Bool)
-> TCM [Maybe QName] -> TCMT IO Bool
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Type'' Term Term -> TCM [Maybe QName]
visibleConDoms Type'' Term Term
t) dcs
    case cands of
      [(QName
_d, Type'' Term Term
_t, ConHead
c)] -> ConHead -> DisambiguateConstructor
decideOn ConHead
c
      [(QName, Type'' Term Term, ConHead)]
_ -> DisambiguateConstructor
fallback
    where

    -- @match@ is successful if there no name conflict (q ≠ q')
    -- and the argument skeleton is not longer thatn the constructor skeleton.
    match ::
          [Maybe QName]   -- Specification (argument skeleton).
       -> [Maybe QName]   -- Candidate (constructor skeleton).
       -> Bool
    match :: [Maybe QName] -> [Maybe QName] -> Bool
match = (([Maybe QName], [Maybe QName]) -> Bool)
-> [Maybe QName] -> [Maybe QName] -> Bool
forall a b c. ((a, b) -> c) -> a -> b -> c
curry ((([Maybe QName], [Maybe QName]) -> Bool)
 -> [Maybe QName] -> [Maybe QName] -> Bool)
-> (([Maybe QName], [Maybe QName]) -> Bool)
-> [Maybe QName]
-> [Maybe QName]
-> Bool
forall a b. (a -> b) -> a -> b
$ \case
      ([], [Maybe QName]
_ ) -> Bool
True
      ([Maybe QName]
_ , []) -> Bool
False
      (Just QName
q : [Maybe QName]
ms, Just QName
q' : [Maybe QName]
ms') -> QName
q QName -> QName -> Bool
forall a. Eq a => a -> a -> Bool
== QName
q' Bool -> Bool -> Bool
&& [Maybe QName] -> [Maybe QName] -> Bool
match [Maybe QName]
ms [Maybe QName]
ms'
      (Maybe QName
_ : [Maybe QName]
ms, Maybe QName
_ : [Maybe QName]
ms') -> [Maybe QName] -> [Maybe QName] -> Bool
match [Maybe QName]
ms [Maybe QName]
ms'

    -- @match@ with debug printing.
    matchSkel :: [Maybe QName] -> [Maybe QName] -> TCM Bool
    matchSkel :: [Maybe QName] -> [Maybe QName] -> TCMT IO Bool
matchSkel [Maybe QName]
argsSkel [Maybe QName]
conSkel = do
      let res :: Bool
res = [Maybe QName] -> [Maybe QName] -> Bool
match [Maybe QName]
argsSkel [Maybe QName]
conSkel
      [Char] -> Int -> TCMT IO Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.check.term.con" Int
40 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
        [ TCMT IO Doc
"matchSkel returns" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Bool -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Bool
res TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
"on:"
        , Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ [Maybe QName] -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty [Maybe QName]
argsSkel
        , Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ [Maybe QName] -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty [Maybe QName]
conSkel
        ]
      Bool -> TCMT IO Bool
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
res

    -- Only look at visible arguments that are variables or similar identifiers.
    -- For variables/symbols @Just getTypeHead@ else @Nothing@.
    visibleVarArgs :: TCM [Maybe QName]
    visibleVarArgs :: TCM [Maybe QName]
visibleVarArgs = [Arg (Named_ Expr)]
-> (Arg (Named_ Expr) -> TCMT IO (Maybe QName))
-> TCM [Maybe QName]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM ((Arg (Named_ Expr) -> Bool)
-> [Arg (Named_ Expr)] -> [Arg (Named_ Expr)]
forall a. (a -> Bool) -> [a] -> [a]
filter Arg (Named_ Expr) -> Bool
forall a. LensHiding a => a -> Bool
visible [Arg (Named_ Expr)]
args) ((Arg (Named_ Expr) -> TCMT IO (Maybe QName)) -> TCM [Maybe QName])
-> (Arg (Named_ Expr) -> TCMT IO (Maybe QName))
-> TCM [Maybe QName]
forall a b. (a -> b) -> a -> b
$ \ (Arg (Named_ Expr)
arg :: NamedArg A.Expr) -> do
        let v :: Expr
v = Expr -> Expr
unScope (Expr -> Expr) -> Expr -> Expr
forall a b. (a -> b) -> a -> b
$ Arg (Named_ Expr) -> Expr
forall a. NamedArg a -> a
namedArg Arg (Named_ Expr)
arg
        [Char] -> Int -> TCMT IO Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.check.term.con" Int
40 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"is this a variable? :" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Expr -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Expr -> m Doc
prettyTCM Expr
v
        [Char] -> Int -> TCMT IO Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.check.term.con" Int
90 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"is this a variable? :" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> ([Char] -> TCMT IO Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text ([Char] -> TCMT IO Doc) -> (Expr -> [Char]) -> Expr -> TCMT IO Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expr -> [Char]
forall a. Show a => a -> [Char]
show) Expr
v
        case Expr
v of

          -- We can readly grab the type of a variable from the context.
          A.Var Name
x -> do
            t <- Dom' Term (Type'' Term Term) -> Type'' Term Term
forall t e. Dom' t e -> e
unDom (Dom' Term (Type'' Term Term) -> Type'' Term Term)
-> ((Term, Dom' Term (Type'' Term Term))
    -> Dom' Term (Type'' Term Term))
-> (Term, Dom' Term (Type'' Term Term))
-> Type'' Term Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Term, Dom' Term (Type'' Term Term))
-> Dom' Term (Type'' Term Term)
forall a b. (a, b) -> b
snd ((Term, Dom' Term (Type'' Term Term)) -> Type'' Term Term)
-> TCMT IO (Term, Dom' Term (Type'' Term Term))
-> TCMT IO (Type'' Term Term)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Name -> TCMT IO (Term, Dom' Term (Type'' Term Term))
forall (m :: * -> *).
(MonadDebug m, MonadFail m, MonadTCEnv m) =>
Name -> m (Term, Dom' Term (Type'' Term Term))
getVarInfo Name
x
            reportSDoc "tc.check.term.con" 40 $ "type of variable:" <+> prettyTCM t
            -- Just keep the name @D@ of type @D vs@
            getTypeHead t

          -- We can also grab the type of defined symbols if we find them in the signature.
          A.Def QName
x -> do
            QName -> TCMT IO (Either SigError Definition)
forall (m :: * -> *).
(HasConstInfo m, HasCallStack) =>
QName -> m (Either SigError Definition)
getConstInfo' QName
x TCMT IO (Either SigError Definition)
-> (Either SigError Definition -> TCMT IO (Maybe QName))
-> TCMT IO (Maybe QName)
forall a b. TCMT IO a -> (a -> TCMT IO b) -> TCMT IO b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
              Right Definition
def -> Type'' Term Term -> TCMT IO (Maybe QName)
getTypeHead (Type'' Term Term -> TCMT IO (Maybe QName))
-> Type'' Term Term -> TCMT IO (Maybe QName)
forall a b. (a -> b) -> a -> b
$ Definition -> Type'' Term Term
defType Definition
def
              Left{} -> Maybe QName -> TCMT IO (Maybe QName)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe QName
forall a. Maybe a
Nothing
          Expr
_ -> Maybe QName -> TCMT IO (Maybe QName)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe QName
forall a. Maybe a
Nothing

    -- List of visible arguments of the constructor candidate.
    -- E.g. vcons : {A : Set} {n : Nat} (x : A) (xs : Vec A n) → Vec A (suc n)
    -- becomes vcons : ? → Vec → .
    visibleConDoms :: Type -> TCM [Maybe QName]
    visibleConDoms :: Type'' Term Term -> TCM [Maybe QName]
visibleConDoms Type'' Term Term
t = do
      TelV tel _ <- Type'' Term Term -> TCMT IO (TelV (Type'' Term Term))
forall (m :: * -> *).
PureTCM m =>
Type'' Term Term -> m (TelV (Type'' Term Term))
telViewPath Type'' Term Term
t
      mapM (getTypeHead . snd . unDom) $ filter visible $ telToList tel

-- | If type is of the form @F vs@ and not blocked in any way, return @F@.
getTypeHead :: Type -> TCM (Maybe QName)
getTypeHead :: Type'' Term Term -> TCMT IO (Maybe QName)
getTypeHead Type'' Term Term
t = do
  res <- Type'' Term Term
-> (Blocker -> Type'' Term Term -> TCMT IO (Maybe QName))
-> (NotBlocked -> Type'' Term Term -> TCMT IO (Maybe QName))
-> TCMT IO (Maybe QName)
forall t (m :: * -> *) a.
(Reduce t, IsMeta t, MonadReduce m) =>
t -> (Blocker -> t -> m a) -> (NotBlocked -> t -> m a) -> m a
ifBlocked Type'' Term Term
t (\ Blocker
_ Type'' Term Term
_ -> Maybe QName -> TCMT IO (Maybe QName)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe QName
forall a. Maybe a
Nothing) ((NotBlocked -> Type'' Term Term -> TCMT IO (Maybe QName))
 -> TCMT IO (Maybe QName))
-> (NotBlocked -> Type'' Term Term -> TCMT IO (Maybe QName))
-> TCMT IO (Maybe QName)
forall a b. (a -> b) -> a -> b
$ \ NotBlocked
nb Type'' Term Term
t -> do
    case NotBlocked
nb of
      NotBlocked
ReallyNotBlocked -> do
        -- Drop initial hidden domains (only needed for generalizable variables).
        TelV _ core <- Int
-> (Dom' Term (Type'' Term Term) -> Bool)
-> Type'' Term Term
-> TCMT IO (TelV (Type'' Term Term))
forall (m :: * -> *).
(MonadReduce m, MonadAddContext m) =>
Int
-> (Dom' Term (Type'' Term Term) -> Bool)
-> Type'' Term Term
-> m (TelV (Type'' Term Term))
telViewUpTo' (Int -> Int
forall a. Num a => a -> a
negate Int
1) (Bool -> Bool
not (Bool -> Bool)
-> (Dom' Term (Type'' Term Term) -> Bool)
-> Dom' Term (Type'' Term Term)
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Dom' Term (Type'' Term Term) -> Bool
forall a. LensHiding a => a -> Bool
visible) Type'' Term Term
t
        case unEl core of
          Def QName
q [Elim' Term]
_ -> Maybe QName -> TCMT IO (Maybe QName)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe QName -> TCMT IO (Maybe QName))
-> Maybe QName -> TCMT IO (Maybe QName)
forall a b. (a -> b) -> a -> b
$ QName -> Maybe QName
forall a. a -> Maybe a
Just QName
q
          Term
_ -> Maybe QName -> TCMT IO (Maybe QName)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe QName
forall a. Maybe a
Nothing
      -- In the other cases, we do not get the data name.
      NotBlocked
_ -> Maybe QName -> TCMT IO (Maybe QName)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe QName
forall a. Maybe a
Nothing
  reportSDoc "tc.check.term.con" 80 $ hcat $ "getTypeHead(" : prettyTCM t : ") = " : pretty res : []
  return res


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

checkUnambiguousProjectionApplication :: Comparison -> A.Expr -> Type -> QName -> ProjOrigin -> A.Expr -> [NamedArg A.Expr] -> TCM Term
checkUnambiguousProjectionApplication :: Comparison
-> Expr
-> Type'' Term Term
-> QName
-> ProjOrigin
-> Expr
-> [Arg (Named_ Expr)]
-> TCM Term
checkUnambiguousProjectionApplication Comparison
cmp Expr
e Type'' Term Term
t QName
x ProjOrigin
o Expr
hd [Arg (Named_ Expr)]
args = do
  let fallback :: TCM Term
fallback = Comparison
-> Expr
-> Type'' Term Term
-> Expr
-> [Arg (Named_ Expr)]
-> TCM Term
checkHeadApplication Comparison
cmp Expr
e Type'' Term Term
t Expr
hd [Arg (Named_ 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, [Arg (Named_ Expr)]
args) of
    (ProjOrigin
ProjPostfix, Arg (Named_ Expr)
arg : [Arg (Named_ 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.
      TCMT IO (Maybe Projection)
-> TCM Term -> (Projection -> TCM Term) -> TCM Term
forall (m :: * -> *) a b.
Monad m =>
m (Maybe a) -> m b -> (a -> m b) -> m b
caseMaybeM (QName -> TCMT IO (Maybe Projection)
forall (m :: * -> *).
HasConstInfo m =>
QName -> m (Maybe Projection)
isProjection QName
x) TCM Term
fallback ((Projection -> TCM Term) -> TCM Term)
-> (Projection -> TCM Term) -> TCM Term
forall a b. (a -> b) -> a -> b
$ \ Projection
pr -> do
        Comparison
-> Expr
-> Type'' Term Term
-> Expr
-> [Arg (Named_ Expr)]
-> TCM Term
checkHeadApplication Comparison
cmp Expr
e Type'' Term Term
t Expr
hd (ArgInfo -> Arg (Named_ Expr) -> Arg (Named_ Expr)
forall a. LensArgInfo a => ArgInfo -> a -> a
setArgInfo (Projection -> ArgInfo
projArgInfo Projection
pr) Arg (Named_ Expr)
arg Arg (Named_ Expr) -> [Arg (Named_ Expr)] -> [Arg (Named_ Expr)]
forall a. a -> [a] -> [a]
: [Arg (Named_ Expr)]
rest)
    (ProjOrigin, [Arg (Named_ Expr)])
_ -> TCM Term
fallback

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

inferProjApp :: A.Expr -> ProjOrigin -> AmbiguousQName -> A.Expr -> A.Args -> TCM (Term, Type)
inferProjApp :: Expr
-> ProjOrigin
-> AmbiguousQName
-> Expr
-> [Arg (Named_ Expr)]
-> TCM (Term, Type'' Term Term)
inferProjApp Expr
e ProjOrigin
o AmbiguousQName
ds Expr
hd [Arg (Named_ Expr)]
args0 = do
  (v, t, _) <- Expr
-> ProjOrigin
-> AmbiguousQName
-> Expr
-> [Arg (Named_ Expr)]
-> Maybe (Comparison, Type'' Term Term)
-> TCM (Term, Type'' Term Term, CheckedTarget)
inferOrCheckProjApp Expr
e ProjOrigin
o AmbiguousQName
ds Expr
hd [Arg (Named_ Expr)]
args0 Maybe (Comparison, Type'' Term Term)
forall a. Maybe a
Nothing
  return (v, t)

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

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

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

checkProjAppToKnownPrincipalArg ::
  Comparison
  -> A.Expr
  -> ProjOrigin
  -> AmbiguousQName
  -> A.Expr
  -> A.Args
  -> Type
  -> Int
  -> Term
  -> Type
  -> PrincipalArgTypeMetas
  -> TCM Term
checkProjAppToKnownPrincipalArg :: Comparison
-> Expr
-> ProjOrigin
-> AmbiguousQName
-> Expr
-> [Arg (Named_ Expr)]
-> Type'' Term Term
-> Int
-> Term
-> Type'' Term Term
-> PrincipalArgTypeMetas
-> TCM Term
checkProjAppToKnownPrincipalArg Comparison
cmp Expr
e ProjOrigin
o AmbiguousQName
ds Expr
hd [Arg (Named_ Expr)]
args0 Type'' Term Term
t Int
k Term
v0 Type'' Term Term
pt PrincipalArgTypeMetas
patm = do
  (v, ti, targetCheck) <- Expr
-> ProjOrigin
-> AmbiguousQName
-> Expr
-> [Arg (Named_ Expr)]
-> Maybe (Comparison, Type'' Term Term)
-> Int
-> Term
-> Type'' Term Term
-> Maybe PrincipalArgTypeMetas
-> TCM (Term, Type'' Term Term, CheckedTarget)
inferOrCheckProjAppToKnownPrincipalArg Expr
e ProjOrigin
o AmbiguousQName
ds Expr
hd [Arg (Named_ Expr)]
args0 ((Comparison, Type'' Term Term)
-> Maybe (Comparison, Type'' Term Term)
forall a. a -> Maybe a
Just (Comparison
cmp, Type'' Term Term
t)) Int
k Term
v0 Type'' Term Term
pt (PrincipalArgTypeMetas -> Maybe PrincipalArgTypeMetas
forall a. a -> Maybe a
Just PrincipalArgTypeMetas
patm)
  coerce' cmp targetCheck v ti 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.
  -> AmbiguousQName
     -- ^ The projection name (potentially ambiguous).
  -> A.Expr
     -- ^ The projection as expression.
  -> 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
-> AmbiguousQName
-> Expr
-> [Arg (Named_ Expr)]
-> Maybe (Comparison, Type'' Term Term)
-> TCM (Term, Type'' Term Term, CheckedTarget)
inferOrCheckProjApp Expr
e ProjOrigin
o AmbiguousQName
ds Expr
hd [Arg (Named_ Expr)]
args Maybe (Comparison, Type'' Term Term)
mt = do
  [Char] -> Int -> TCMT IO Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.proj.amb" Int
20 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
    [ TCMT IO Doc
"checking ambiguous projection"
    , [Char] -> TCMT IO Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text ([Char] -> TCMT IO Doc) -> [Char] -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ [Char]
"  ds   = " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++! AmbiguousQName -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow AmbiguousQName
ds
    , [Char] -> TCMT IO Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text   [Char]
"  args = " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> do [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
prettyList ([TCMT IO Doc] -> TCMT IO Doc) -> [TCMT IO Doc] -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ (Arg (Named_ Expr) -> TCMT IO Doc)
-> [Arg (Named_ Expr)] -> [TCMT IO Doc]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Arg (Named_ Expr) -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Arg (Named_ Expr) -> m Doc
prettyTCM [Arg (Named_ Expr)]
args
    , [Char] -> TCMT IO Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text   [Char]
"  t    = " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Maybe (Comparison, Type'' Term Term)
-> TCMT IO Doc
-> ((Comparison, Type'' Term Term) -> TCMT IO Doc)
-> TCMT IO Doc
forall a b. Maybe a -> b -> (a -> b) -> b
caseMaybe Maybe (Comparison, Type'' Term Term)
mt TCMT IO Doc
"Nothing" (Comparison, Type'' Term Term) -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *).
MonadPretty m =>
(Comparison, Type'' Term Term) -> m Doc
prettyTCM
    ]

  let cmp :: Comparison
cmp = Maybe (Comparison, Type'' Term Term)
-> Comparison
-> ((Comparison, Type'' Term Term) -> Comparison)
-> Comparison
forall a b. Maybe a -> b -> (a -> b) -> b
caseMaybe Maybe (Comparison, Type'' Term Term)
mt Comparison
CmpEq (Comparison, Type'' Term Term) -> Comparison
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'' Term Term, CheckedTarget)
postpone Blocker
b = do
        tc <- Maybe (Comparison, Type'' Term Term)
-> TCMT IO (Type'' Term Term)
-> ((Comparison, Type'' Term Term) -> TCMT IO (Type'' Term Term))
-> TCMT IO (Type'' Term Term)
forall a b. Maybe a -> b -> (a -> b) -> b
caseMaybe Maybe (Comparison, Type'' Term Term)
mt TCMT IO (Type'' Term Term)
newTypeMeta_ (Type'' Term Term -> TCMT IO (Type'' Term Term)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Type'' Term Term -> TCMT IO (Type'' Term Term))
-> ((Comparison, Type'' Term Term) -> Type'' Term Term)
-> (Comparison, Type'' Term Term)
-> TCMT IO (Type'' Term Term)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Comparison, Type'' Term Term) -> Type'' Term Term
forall a b. (a, b) -> b
snd)
        v <- postponeTypeCheckingProblem (CheckExpr cmp e tc) b
        return (v, tc, 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 ((Int, Arg (Named_ Expr)) -> Bool)
-> [(Int, Arg (Named_ Expr))] -> [(Int, Arg (Named_ Expr))]
forall a. (a -> Bool) -> [a] -> [a]
filter (Arg (Named_ Expr) -> Bool
forall a. LensHiding a => a -> Bool
visible (Arg (Named_ Expr) -> Bool)
-> ((Int, Arg (Named_ Expr)) -> Arg (Named_ Expr))
-> (Int, Arg (Named_ Expr))
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Int, Arg (Named_ Expr)) -> Arg (Named_ Expr)
forall a b. (a, b) -> b
snd) ([(Int, Arg (Named_ Expr))] -> [(Int, Arg (Named_ Expr))])
-> [(Int, Arg (Named_ Expr))] -> [(Int, Arg (Named_ Expr))]
forall a b. (a -> b) -> a -> b
$ [Int] -> [Arg (Named_ Expr)] -> [(Int, Arg (Named_ Expr))]
forall a b. [a] -> [b] -> [(a, b)]
zip [Int
0..] [Arg (Named_ 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
    [] -> Maybe (Comparison, Type'' Term Term)
-> TCM (Term, Type'' Term Term, CheckedTarget)
-> ((Comparison, Type'' Term Term)
    -> TCM (Term, Type'' Term Term, CheckedTarget))
-> TCM (Term, Type'' Term Term, CheckedTarget)
forall a b. Maybe a -> b -> (a -> b) -> b
caseMaybe Maybe (Comparison, Type'' Term Term)
mt (AmbiguousQName -> TCM (Term, Type'' Term Term, CheckedTarget)
forall a. AmbiguousQName -> TCM a
refuseProjNotApplied AmbiguousQName
ds) (((Comparison, Type'' Term Term)
  -> TCM (Term, Type'' Term Term, CheckedTarget))
 -> TCM (Term, Type'' Term Term, CheckedTarget))
-> ((Comparison, Type'' Term Term)
    -> TCM (Term, Type'' Term Term, CheckedTarget))
-> TCM (Term, Type'' Term Term, CheckedTarget)
forall a b. (a -> b) -> a -> b
$ \ (Comparison
cmp , Type'' Term Term
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 _ptel core <- Int
-> (Dom' Term (Type'' Term Term) -> Bool)
-> Type'' Term Term
-> TCMT IO (TelV (Type'' Term Term))
forall (m :: * -> *).
(MonadReduce m, MonadAddContext m) =>
Int
-> (Dom' Term (Type'' Term Term) -> Bool)
-> Type'' Term Term
-> m (TelV (Type'' Term Term))
telViewUpTo' (-Int
1) (Bool -> Bool
not (Bool -> Bool)
-> (Dom' Term (Type'' Term Term) -> Bool)
-> Dom' Term (Type'' Term Term)
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Dom' Term (Type'' Term Term) -> Bool
forall a. LensHiding a => a -> Bool
visible) Type'' Term Term
t
      ifBlocked core (\ Blocker
m Type'' Term Term
_ -> Blocker -> TCM (Term, Type'' Term Term, CheckedTarget)
postpone Blocker
m) $ {-else-} \ NotBlocked
_ Type'' Term Term
core -> do
      Type'' Term Term
-> (Type'' Term Term
    -> TCM (Term, Type'' Term Term, CheckedTarget))
-> (Dom' Term (Type'' Term Term)
    -> Abs (Type'' Term Term)
    -> TCM (Term, Type'' Term Term, CheckedTarget))
-> TCM (Term, Type'' Term Term, CheckedTarget)
forall (m :: * -> *) a.
MonadReduce m =>
Type'' Term Term
-> (Type'' Term Term -> m a)
-> (Dom' Term (Type'' Term Term) -> Abs (Type'' Term Term) -> m a)
-> m a
ifNotPiType Type'' Term Term
core (\ Type'' Term Term
_ -> AmbiguousQName -> TCM (Term, Type'' Term Term, CheckedTarget)
forall a. AmbiguousQName -> TCM a
refuseProjNotApplied AmbiguousQName
ds) ((Dom' Term (Type'' Term Term)
  -> Abs (Type'' Term Term)
  -> TCM (Term, Type'' Term Term, CheckedTarget))
 -> TCM (Term, Type'' Term Term, CheckedTarget))
-> (Dom' Term (Type'' Term Term)
    -> Abs (Type'' Term Term)
    -> TCM (Term, Type'' Term Term, CheckedTarget))
-> TCM (Term, Type'' Term Term, CheckedTarget)
forall a b. (a -> b) -> a -> b
$ {-else-} \ Dom' Term (Type'' Term Term)
dom Abs (Type'' Term Term)
_b -> do
      Type'' Term Term
-> (Blocker
    -> Type'' Term Term -> TCM (Term, Type'' Term Term, CheckedTarget))
-> (NotBlocked
    -> Type'' Term Term -> TCM (Term, Type'' Term Term, CheckedTarget))
-> TCM (Term, Type'' Term Term, CheckedTarget)
forall t (m :: * -> *) a.
(Reduce t, IsMeta t, MonadReduce m) =>
t -> (Blocker -> t -> m a) -> (NotBlocked -> t -> m a) -> m a
ifBlocked (Dom' Term (Type'' Term Term) -> Type'' Term Term
forall t e. Dom' t e -> e
unDom Dom' Term (Type'' Term Term)
dom) (\ Blocker
m Type'' Term Term
_ -> Blocker -> TCM (Term, Type'' Term Term, CheckedTarget)
postpone Blocker
m) ((NotBlocked
  -> Type'' Term Term -> TCM (Term, Type'' Term Term, CheckedTarget))
 -> TCM (Term, Type'' Term Term, CheckedTarget))
-> (NotBlocked
    -> Type'' Term Term -> TCM (Term, Type'' Term Term, CheckedTarget))
-> TCM (Term, Type'' Term Term, CheckedTarget)
forall a b. (a -> b) -> a -> b
$ {-else-} \ NotBlocked
_ Type'' Term Term
ta -> do
      TCMT IO (Maybe (QName, [Arg Term], RecordData))
-> TCM (Term, Type'' Term Term, CheckedTarget)
-> ((QName, [Arg Term], RecordData)
    -> TCM (Term, Type'' Term Term, CheckedTarget))
-> TCM (Term, Type'' Term Term, CheckedTarget)
forall (m :: * -> *) a b.
Monad m =>
m (Maybe a) -> m b -> (a -> m b) -> m b
caseMaybeM (Type'' Term Term -> TCMT IO (Maybe (QName, [Arg Term], RecordData))
forall (m :: * -> *).
(HasCallStack, PureTCM m) =>
Type'' Term Term -> m (Maybe (QName, [Arg Term], RecordData))
isRecordType Type'' Term Term
ta) (AmbiguousQName
-> Maybe Term
-> Type'' Term Term
-> TCM (Term, Type'' Term Term, CheckedTarget)
forall a. AmbiguousQName -> Maybe Term -> Type'' Term Term -> TCM a
refuseProjNotRecordType AmbiguousQName
ds Maybe Term
forall a. Maybe a
Nothing Type'' Term Term
ta)
        \ (QName
_q, [Arg Term]
_pars, RecordData{ _recFields :: RecordData -> [Dom QName]
_recFields = [Dom QName]
fs }) -> do
          case [Dom QName] -> (Dom QName -> Maybe QName) -> [QName]
forall a b. [a] -> (a -> Maybe b) -> [b]
forMaybe [Dom QName]
fs ((Dom QName -> Maybe QName) -> [QName])
-> (Dom QName -> Maybe QName) -> [QName]
forall a b. (a -> b) -> a -> b
$ \ Dom QName
f -> (QName -> Bool) -> NonEmpty QName -> Maybe QName
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
Fold.find (Dom QName -> QName
forall t e. Dom' t e -> e
unDom Dom QName
f QName -> QName -> Bool
forall a. Eq a => a -> a -> Bool
==) (AmbiguousQName -> NonEmpty QName
getAmbiguous AmbiguousQName
ds) of
            [] -> AmbiguousQName -> TCM (Term, Type'' Term Term, CheckedTarget)
forall a. AmbiguousQName -> TCM a
refuseProjNoMatching AmbiguousQName
ds
            [QName
d] -> do
              QName -> TCMT IO ()
storeDisambiguatedProjection QName
d
              -- checkHeadApplication will check the target type
              (, Type'' Term Term
t, Maybe ProblemId -> CheckedTarget
CheckedTarget Maybe ProblemId
forall a. Maybe a
Nothing) (Term -> (Term, Type'' Term Term, CheckedTarget))
-> TCM Term -> TCM (Term, Type'' Term Term, CheckedTarget)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
                Comparison
-> Expr
-> Type'' Term Term
-> Expr
-> [Arg (Named_ Expr)]
-> TCM Term
checkHeadApplication Comparison
cmp Expr
e Type'' Term Term
t (ProjOrigin -> AmbiguousQName -> Expr
A.Proj ProjOrigin
o (AmbiguousQName -> Expr) -> AmbiguousQName -> Expr
forall a b. (a -> b) -> a -> b
$ QName -> AmbiguousQName
unambiguous QName
d) [Arg (Named_ Expr)]
args
            [QName]
_ -> TCM (Term, Type'' Term Term, CheckedTarget)
forall a. HasCallStack => a
__IMPOSSIBLE__

    -- Case: we have a visible argument
    ((Int
k, Arg (Named_ Expr)
arg) : [(Int, Arg (Named_ Expr))]
_) -> do
      (v0, ta) <- Expr -> TCM (Term, Type'' Term Term)
inferExpr (Expr -> TCM (Term, Type'' Term Term))
-> Expr -> TCM (Term, Type'' Term Term)
forall a b. (a -> b) -> a -> b
$ Arg (Named_ Expr) -> Expr
forall a. NamedArg a -> a
namedArg Arg (Named_ Expr)
arg
      reportSDoc "tc.proj.amb" 25 $ vcat
        [ "  principal arg " <+> prettyTCM arg
        , "  has type "      <+> prettyTCM ta
        ]
      inferOrCheckProjAppToKnownPrincipalArg e o ds hd args mt k v0 ta 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.
  -> AmbiguousQName
     -- ^ The projection name (potentially ambiguous).
  -> A.Expr
     -- ^ The projection (as application head).
  -> 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
-> AmbiguousQName
-> Expr
-> [Arg (Named_ Expr)]
-> Maybe (Comparison, Type'' Term Term)
-> Int
-> Term
-> Type'' Term Term
-> Maybe PrincipalArgTypeMetas
-> TCM (Term, Type'' Term Term, CheckedTarget)
inferOrCheckProjAppToKnownPrincipalArg Expr
e ProjOrigin
o AmbiguousQName
ds Expr
hd [Arg (Named_ Expr)]
args Maybe (Comparison, Type'' Term Term)
mt Int
k Term
v0 Type'' Term Term
ta Maybe PrincipalArgTypeMetas
mpatm = do
  let cmp :: Comparison
cmp = Maybe (Comparison, Type'' Term Term)
-> Comparison
-> ((Comparison, Type'' Term Term) -> Comparison)
-> Comparison
forall a b. Maybe a -> b -> (a -> b) -> b
caseMaybe Maybe (Comparison, Type'' Term Term)
mt Comparison
CmpEq (Comparison, Type'' Term Term) -> Comparison
forall a b. (a, b) -> a
fst
      postpone :: Blocker
-> PrincipalArgTypeMetas
-> TCM (Term, Type'' Term Term, CheckedTarget)
postpone Blocker
b PrincipalArgTypeMetas
patm = do
        tc <- Maybe (Comparison, Type'' Term Term)
-> TCMT IO (Type'' Term Term)
-> ((Comparison, Type'' Term Term) -> TCMT IO (Type'' Term Term))
-> TCMT IO (Type'' Term Term)
forall a b. Maybe a -> b -> (a -> b) -> b
caseMaybe Maybe (Comparison, Type'' Term Term)
mt TCMT IO (Type'' Term Term)
newTypeMeta_ (Type'' Term Term -> TCMT IO (Type'' Term Term)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Type'' Term Term -> TCMT IO (Type'' Term Term))
-> ((Comparison, Type'' Term Term) -> Type'' Term Term)
-> (Comparison, Type'' Term Term)
-> TCMT IO (Type'' Term Term)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Comparison, Type'' Term Term) -> Type'' Term Term
forall a b. (a, b) -> b
snd)
        v <- postponeTypeCheckingProblem (CheckProjAppToKnownPrincipalArg cmp e o ds hd args tc k v0 ta patm) b
        return (v, tc, NotCheckedTarget)
  -- ta should be a record type (after introducing the hidden args in v0)
  patm@(PrincipalArgTypeMetas vargs ta) <- case Maybe PrincipalArgTypeMetas
mpatm of
    -- keep using the previously created metas, when picking up a postponed
    -- problem - see #4924
    Just PrincipalArgTypeMetas
patm -> PrincipalArgTypeMetas -> TCMT IO PrincipalArgTypeMetas
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return PrincipalArgTypeMetas
patm
    -- create fresh metas
    Maybe PrincipalArgTypeMetas
Nothing -> ([Arg Term] -> Type'' Term Term -> PrincipalArgTypeMetas)
-> ([Arg Term], Type'' Term Term) -> PrincipalArgTypeMetas
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry [Arg Term] -> Type'' Term Term -> PrincipalArgTypeMetas
PrincipalArgTypeMetas (([Arg Term], Type'' Term Term) -> PrincipalArgTypeMetas)
-> TCMT IO ([Arg Term], Type'' Term Term)
-> TCMT IO PrincipalArgTypeMetas
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Int
-> (Hiding -> Bool)
-> Type'' Term Term
-> TCMT IO ([Arg Term], Type'' Term Term)
implicitArgs (-Int
1) (Bool -> Bool
not (Bool -> Bool) -> (Hiding -> Bool) -> Hiding -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Hiding -> Bool
forall a. LensHiding a => a -> Bool
visible) Type'' Term Term
ta
  let v = Term
v0 Term -> [Arg Term] -> Term
forall t. Apply t => t -> [Arg Term] -> t
`apply` [Arg Term]
vargs
  ifBlocked ta (\ Blocker
m Type'' Term Term
_ -> Blocker
-> PrincipalArgTypeMetas
-> TCM (Term, Type'' Term Term, CheckedTarget)
postpone Blocker
m PrincipalArgTypeMetas
patm) {-else-} $ \ NotBlocked
_ Type'' Term Term
ta -> do
  TCMT IO (Maybe (QName, [Arg Term], RecordData))
-> TCM (Term, Type'' Term Term, CheckedTarget)
-> ((QName, [Arg Term], RecordData)
    -> TCM (Term, Type'' Term Term, CheckedTarget))
-> TCM (Term, Type'' Term Term, CheckedTarget)
forall (m :: * -> *) a b.
Monad m =>
m (Maybe a) -> m b -> (a -> m b) -> m b
caseMaybeM (Type'' Term Term -> TCMT IO (Maybe (QName, [Arg Term], RecordData))
forall (m :: * -> *).
(HasCallStack, PureTCM m) =>
Type'' Term Term -> m (Maybe (QName, [Arg Term], RecordData))
isRecordType Type'' Term Term
ta) (AmbiguousQName
-> Maybe Term
-> Type'' Term Term
-> TCM (Term, Type'' Term Term, CheckedTarget)
forall a. AmbiguousQName -> Maybe Term -> Type'' Term Term -> TCM a
refuseProjNotRecordType AmbiguousQName
ds (Term -> Maybe Term
forall a. a -> Maybe a
Just Term
v0) Type'' Term Term
ta) (((QName, [Arg Term], RecordData)
  -> TCM (Term, Type'' Term Term, CheckedTarget))
 -> TCM (Term, Type'' Term Term, CheckedTarget))
-> ((QName, [Arg Term], RecordData)
    -> TCM (Term, Type'' Term Term, CheckedTarget))
-> TCM (Term, Type'' Term Term, CheckedTarget)
forall a b. (a -> b) -> a -> b
$ \ (QName
q, [Arg Term]
_pars0, RecordData
_) -> do

      -- try to project it with all of the possible projections
      let try :: QName
-> MaybeT
     (TCMT IO)
     (QName,
      (QName,
       ([Arg Term],
        (Dom' Term (Type'' Term Term), Term, Type'' Term Term))))
try QName
d = do
            [Char] -> Int -> TCMT IO Doc -> MaybeT (TCMT IO) ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.proj.amb" Int
30 (TCMT IO Doc -> MaybeT (TCMT IO) ())
-> TCMT IO Doc -> MaybeT (TCMT IO) ()
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
              [ [Char] -> TCMT IO Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text ([Char] -> TCMT IO Doc) -> [Char] -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ [Char]
"trying projection " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++! QName -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow QName
d
              , TCMT IO Doc
"  td  = " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO (Maybe (Type'' Term Term))
-> TCMT IO Doc -> (Type'' Term Term -> TCMT IO Doc) -> TCMT IO Doc
forall (m :: * -> *) a b.
Monad m =>
m (Maybe a) -> m b -> (a -> m b) -> m b
caseMaybeM (QName -> Type'' Term Term -> TCMT IO (Maybe (Type'' Term Term))
forall (m :: * -> *).
PureTCM m =>
QName -> Type'' Term Term -> m (Maybe (Type'' Term Term))
getDefType QName
d Type'' Term Term
ta) TCMT IO Doc
"Nothing" Type'' Term Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type'' Term Term -> m Doc
prettyTCM
              ]

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

            -- try to eliminate
            (dom, u, tb) <- MaybeT (projectTyped v ta o d `catchError` \ TCErr
_ -> Maybe (Dom' Term (Type'' Term Term), Term, Type'' Term Term)
-> TCMT
     IO (Maybe (Dom' Term (Type'' Term Term), Term, Type'' Term Term))
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (Dom' Term (Type'' Term Term), Term, Type'' Term Term)
forall a. Maybe a
Nothing)
            reportSDoc "tc.proj.amb" 30 $ vcat
              [ "  dom = " <+> prettyTCM dom
              , "  u   = " <+> prettyTCM u
              , "  tb  = " <+> prettyTCM tb
              ]
            (q', pars, _) <- MaybeT $ isRecordType $ unDom dom
            reportSDoc "tc.proj.amb" 30 $ vcat
              [ "  q   = " <+> prettyTCM q
              , "  q'  = " <+> prettyTCM q'
              ]
            guard (q == q')
            -- Get the type of the projection and check
            -- that the first visible argument is the record value.
            let tfull = Definition -> Type'' Term Term
defType Definition
def
            TelV tel _ <- lift $ telViewUpTo' (-1) (not . visible) tfull
            reportSDoc "tc.proj.amb" 30 $ vcat
              [ text $ "  size tel  = " ++! show (size tel)
              , text $ "  size pars = " ++! show (size pars)
              ]
            -- See issue 1960 for when the following assertion fails for
            -- the correct disambiguation.
            -- guard (natSize tel == natSize pars)

            guard =<< do isNothing <$> do lift $ checkModality' d def
            return (orig, (d, (pars, (dom, u, tb))))

      cands <- ((QName,
  (QName,
   ([Arg Term],
    (Dom' Term (Type'' Term Term), Term, Type'' Term Term))))
 -> QName)
-> [(QName,
     (QName,
      ([Arg Term],
       (Dom' Term (Type'' Term Term), Term, Type'' Term Term))))]
-> [List1
      (QName,
       (QName,
        ([Arg Term],
         (Dom' Term (Type'' Term Term), Term, Type'' Term Term))))]
forall b a. Ord b => (a -> b) -> [a] -> [List1 a]
List1.groupOn (QName,
 (QName,
  ([Arg Term],
   (Dom' Term (Type'' Term Term), Term, Type'' Term Term))))
-> QName
forall a b. (a, b) -> a
fst ([(QName,
   (QName,
    ([Arg Term],
     (Dom' Term (Type'' Term Term), Term, Type'' Term Term))))]
 -> [List1
       (QName,
        (QName,
         ([Arg Term],
          (Dom' Term (Type'' Term Term), Term, Type'' Term Term))))])
-> (NonEmpty
      (Maybe
         (QName,
          (QName,
           ([Arg Term],
            (Dom' Term (Type'' Term Term), Term, Type'' Term Term)))))
    -> [(QName,
         (QName,
          ([Arg Term],
           (Dom' Term (Type'' Term Term), Term, Type'' Term Term))))])
-> NonEmpty
     (Maybe
        (QName,
         (QName,
          ([Arg Term],
           (Dom' Term (Type'' Term Term), Term, Type'' Term Term)))))
-> [List1
      (QName,
       (QName,
        ([Arg Term],
         (Dom' Term (Type'' Term Term), Term, Type'' Term Term))))]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NonEmpty
  (Maybe
     (QName,
      (QName,
       ([Arg Term],
        (Dom' Term (Type'' Term Term), Term, Type'' Term Term)))))
-> [(QName,
     (QName,
      ([Arg Term],
       (Dom' Term (Type'' Term Term), Term, Type'' Term Term))))]
forall a. List1 (Maybe a) -> [a]
List1.catMaybes (NonEmpty
   (Maybe
      (QName,
       (QName,
        ([Arg Term],
         (Dom' Term (Type'' Term Term), Term, Type'' Term Term)))))
 -> [List1
       (QName,
        (QName,
         ([Arg Term],
          (Dom' Term (Type'' Term Term), Term, Type'' Term Term))))])
-> TCMT
     IO
     (NonEmpty
        (Maybe
           (QName,
            (QName,
             ([Arg Term],
              (Dom' Term (Type'' Term Term), Term, Type'' Term Term))))))
-> TCMT
     IO
     [List1
        (QName,
         (QName,
          ([Arg Term],
           (Dom' Term (Type'' Term Term), Term, Type'' Term Term))))]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (QName
 -> TCMT
      IO
      (Maybe
         (QName,
          (QName,
           ([Arg Term],
            (Dom' Term (Type'' Term Term), Term, Type'' Term Term))))))
-> NonEmpty QName
-> TCMT
     IO
     (NonEmpty
        (Maybe
           (QName,
            (QName,
             ([Arg Term],
              (Dom' Term (Type'' Term Term), Term, Type'' Term Term))))))
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> NonEmpty a -> m (NonEmpty b)
mapM (MaybeT
  (TCMT IO)
  (QName,
   (QName,
    ([Arg Term],
     (Dom' Term (Type'' Term Term), Term, Type'' Term Term))))
-> TCMT
     IO
     (Maybe
        (QName,
         (QName,
          ([Arg Term],
           (Dom' Term (Type'' Term Term), Term, Type'' Term Term)))))
forall (m :: * -> *) a. MaybeT m a -> m (Maybe a)
runMaybeT (MaybeT
   (TCMT IO)
   (QName,
    (QName,
     ([Arg Term],
      (Dom' Term (Type'' Term Term), Term, Type'' Term Term))))
 -> TCMT
      IO
      (Maybe
         (QName,
          (QName,
           ([Arg Term],
            (Dom' Term (Type'' Term Term), Term, Type'' Term Term))))))
-> (QName
    -> MaybeT
         (TCMT IO)
         (QName,
          (QName,
           ([Arg Term],
            (Dom' Term (Type'' Term Term), Term, Type'' Term Term)))))
-> QName
-> TCMT
     IO
     (Maybe
        (QName,
         (QName,
          ([Arg Term],
           (Dom' Term (Type'' Term Term), Term, Type'' Term Term)))))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. QName
-> MaybeT
     (TCMT IO)
     (QName,
      (QName,
       ([Arg Term],
        (Dom' Term (Type'' Term Term), Term, Type'' Term Term))))
try) (AmbiguousQName -> NonEmpty QName
getAmbiguous AmbiguousQName
ds)
      case cands of
        [] -> AmbiguousQName -> TCM (Term, Type'' Term Term, CheckedTarget)
forall a. AmbiguousQName -> TCM a
refuseProjNoMatching AmbiguousQName
ds
        (List1
  (QName,
   (QName,
    ([Arg Term],
     (Dom' Term (Type'' Term Term), Term, Type'' Term Term))))
_:List1
  (QName,
   (QName,
    ([Arg Term],
     (Dom' Term (Type'' Term Term), Term, Type'' Term Term))))
_:[List1
   (QName,
    (QName,
     ([Arg Term],
      (Dom' Term (Type'' Term Term), Term, Type'' Term Term))))]
_) -> AmbiguousQName
-> TCMT IO Doc -> TCM (Term, Type'' Term Term, CheckedTarget)
forall a. AmbiguousQName -> TCMT IO Doc -> TCM a
refuseProj AmbiguousQName
ds (TCMT IO Doc -> TCM (Term, Type'' Term Term, CheckedTarget))
-> TCMT IO Doc -> TCM (Term, Type'' Term Term, CheckedTarget)
forall a b. (a -> b) -> a -> b
$ [Char] -> TCMT IO Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
fwords [Char]
"several matching candidates can be applied."
        -- case: just one matching projection d
        -- the term u = d v
        -- the type tb is the type of this application
        [ (QName
_orig, (QName
d, ([Arg Term]
pars, (Dom' Term (Type'' Term Term)
_dom,Term
u,Type'' Term Term
tb)))) :| [(QName,
  (QName,
   ([Arg Term],
    (Dom' Term (Type'' Term Term), Term, Type'' Term Term))))]
_ ] -> do
          QName -> TCMT IO ()
storeDisambiguatedProjection QName
d

          -- Check parameters
          tfull <- QName -> TCMT IO (Type'' Term Term)
forall (m :: * -> *).
(HasConstInfo m, ReadTCState m) =>
QName -> m (Type'' Term Term)
typeOfConst QName
d
          (args0, princArg : args') <- pure $ splitAt' k args
          (_,_) <- checkKnownArguments args0 pars tfull

          -- Check remaining arguments
          let
            fun = AppInfo -> Expr -> Arg (Named_ Expr) -> Expr
A.App
              (Range -> AppInfo
A.defaultAppInfo (Range -> AppInfo) -> Range -> AppInfo
forall a b. (a -> b) -> a -> b
$ (Expr, [Arg (Named_ Expr)], Arg (Named_ Expr)) -> Range
forall a. HasRange a => a -> Range
getRange (Expr
hd, [Arg (Named_ Expr)]
args0, Arg (Named_ Expr)
princArg))
              (AppView -> Expr
A.unAppView (AppView -> Expr) -> AppView -> Expr
forall a b. (a -> b) -> a -> b
$ Expr -> [Arg (Named_ Expr)] -> AppView
forall arg. Expr -> [NamedArg arg] -> AppView' arg
A.Application Expr
hd [Arg (Named_ Expr)]
args0)
              Arg (Named_ Expr)
princArg
          z <- runExceptT $ checkArgumentsE cmp ExpandLast fun args' tb (snd <$> mt)
          case z of
            Right st :: ArgsCheckState CheckedTarget
st@(ACState [CheckedArg]
_ Expr
_ Type'' Term Term
trest CheckedTarget
targetCheck) -> do
              v <- ([Elim' Term] -> Term) -> ArgsCheckState CheckedTarget -> TCM Term
forall a. ([Elim' Term] -> Term) -> ArgsCheckState a -> TCM Term
checkHeadConstraints (Term
u Term -> [Elim' Term] -> Term
forall t. Apply t => t -> [Elim' Term] -> t
`applyE`) ArgsCheckState CheckedTarget
st
              return (v, trest, targetCheck)
            Left ArgsCheckState [Arg (Named_ Expr)]
problem -> do
              -- In the inference case:
              -- To create a postponed type checking problem,
              -- we do not use typeDontCare, but create a meta.
              tc <- Maybe (Comparison, Type'' Term Term)
-> TCMT IO (Type'' Term Term)
-> ((Comparison, Type'' Term Term) -> TCMT IO (Type'' Term Term))
-> TCMT IO (Type'' Term Term)
forall a b. Maybe a -> b -> (a -> b) -> b
caseMaybe Maybe (Comparison, Type'' Term Term)
mt TCMT IO (Type'' Term Term)
newTypeMeta_ (Type'' Term Term -> TCMT IO (Type'' Term Term)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Type'' Term Term -> TCMT IO (Type'' Term Term))
-> ((Comparison, Type'' Term Term) -> Type'' Term Term)
-> (Comparison, Type'' Term Term)
-> TCMT IO (Type'' Term Term)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Comparison, Type'' Term Term) -> Type'' Term Term
forall a b. (a, b) -> b
snd)
              v  <- postponeArgs problem cmp ExpandLast fun args' tb tc \ st :: ArgsCheckState CheckedTarget
st@(ACState [CheckedArg]
_ Expr
_ Type'' Term Term
trest CheckedTarget
targetCheck) -> do
                      v <- ([Elim' Term] -> Term) -> ArgsCheckState CheckedTarget -> TCM Term
forall a. ([Elim' Term] -> Term) -> ArgsCheckState a -> TCM Term
checkHeadConstraints (Term
u Term -> [Elim' Term] -> Term
forall t. Apply t => t -> [Elim' Term] -> t
`applyE`) ArgsCheckState CheckedTarget
st
                      coerce' cmp targetCheck v trest tc

              return (v, tc, NotCheckedTarget)

-- | Throw 'AmbiguousOverloadedProjection' with additional explanation.
refuseProj :: AmbiguousQName -> TCM Doc -> TCM a
refuseProj :: forall a. AmbiguousQName -> TCMT IO Doc -> TCM a
refuseProj AmbiguousQName
ds TCMT IO Doc
reason = TypeError -> TCMT IO a
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> TCMT IO a) -> (Doc -> TypeError) -> Doc -> TCMT IO a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. AmbiguousQName -> Doc -> TypeError
AmbiguousOverloadedProjection AmbiguousQName
ds (Doc -> TCMT IO a) -> TCMT IO Doc -> TCMT IO a
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< TCMT IO Doc
reason

refuseProjNotApplied, refuseProjNoMatching :: AmbiguousQName -> TCM a
refuseProjNotApplied :: forall a. AmbiguousQName -> TCM a
refuseProjNotApplied    AmbiguousQName
ds = AmbiguousQName -> TCMT IO Doc -> TCM a
forall a. AmbiguousQName -> TCMT IO Doc -> TCM a
refuseProj AmbiguousQName
ds (TCMT IO Doc -> TCM a) -> TCMT IO Doc -> TCM a
forall a b. (a -> b) -> a -> b
$ [Char] -> TCMT IO Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
fwords [Char]
"it is not applied to a visible argument"
refuseProjNoMatching :: forall a. AmbiguousQName -> TCM a
refuseProjNoMatching    AmbiguousQName
ds = AmbiguousQName -> TCMT IO Doc -> TCM a
forall a. AmbiguousQName -> TCMT IO Doc -> TCM a
refuseProj AmbiguousQName
ds (TCMT IO Doc -> TCM a) -> TCMT IO Doc -> TCM a
forall a b. (a -> b) -> a -> b
$ [Char] -> TCMT IO Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
fwords [Char]
"no matching candidate found"
refuseProjNotRecordType :: AmbiguousQName -> Maybe Term -> Type -> TCM a
refuseProjNotRecordType :: forall a. AmbiguousQName -> Maybe Term -> Type'' Term Term -> TCM a
refuseProjNotRecordType AmbiguousQName
ds Maybe Term
pValue Type'' Term Term
pType = do
  let dType :: TCMT IO Doc
dType = Type'' Term Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type'' Term Term -> m Doc
prettyTCM Type'' Term Term
pType
  let dValue :: TCMT IO Doc
dValue = Maybe Term -> TCMT IO Doc -> (Term -> TCMT IO Doc) -> TCMT IO Doc
forall a b. Maybe a -> b -> (a -> b) -> b
caseMaybe Maybe Term
pValue (Doc -> TCMT IO Doc
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Doc
forall a. Null a => a
empty) Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM
  AmbiguousQName -> TCMT IO Doc -> TCM a
forall a. AmbiguousQName -> TCMT IO Doc -> TCM a
refuseProj AmbiguousQName
ds (TCMT IO Doc -> TCM a) -> TCMT IO Doc -> TCM a
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([TCMT IO Doc] -> TCMT IO Doc) -> [TCMT IO Doc] -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$
    [TCMT IO Doc
"principal argument", TCMT IO Doc
dValue, TCMT IO Doc
"has type", TCMT IO Doc
dType, TCMT IO Doc
"while it should be of record type"]

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

checkUniv
  :: UnivSize -> Univ -> Comparison -> A.Expr -> Type
  -> QName -> Suffix -> [NamedArg A.Expr] -> TCM Term
checkUniv :: UnivSize
-> Univ
-> Comparison
-> Expr
-> Type'' Term Term
-> QName
-> Suffix
-> [Arg (Named_ Expr)]
-> TCM Term
checkUniv UnivSize
sz Univ
u Comparison
cmp Expr
e Type'' Term Term
t QName
q Suffix
suffix [Arg (Named_ Expr)]
args = do
  (v, t0) <- UnivSize
-> Univ
-> Expr
-> QName
-> Suffix
-> [Arg (Named_ Expr)]
-> TCM (Term, Type'' Term Term)
inferUniv UnivSize
sz Univ
u Expr
e QName
q Suffix
suffix [Arg (Named_ Expr)]
args
  coerce cmp v t0 t

inferUniv :: UnivSize -> Univ -> A.Expr -> QName -> Suffix -> [NamedArg A.Expr] -> TCM (Term, Type)
inferUniv :: UnivSize
-> Univ
-> Expr
-> QName
-> Suffix
-> [Arg (Named_ Expr)]
-> TCM (Term, Type'' Term Term)
inferUniv UnivSize
sz Univ
u Expr
e QName
q Suffix
s [Arg (Named_ Expr)]
args = do
  Univ -> TCMT IO ()
univChecks Univ
u
  case UnivSize
sz of
    UnivSize
USmall -> Univ
-> QName
-> Suffix
-> [Arg (Named_ Expr)]
-> TCM (Term, Type'' Term Term)
inferLeveledSort Univ
u QName
q Suffix
s [Arg (Named_ Expr)]
args
    UnivSize
ULarge -> Univ
-> QName
-> Suffix
-> [Arg (Named_ Expr)]
-> TCM (Term, Type'' Term Term)
inferUnivOmega Univ
u QName
q Suffix
s [Arg (Named_ Expr)]
args

univChecks :: Univ -> TCM ()
univChecks :: Univ -> TCMT IO ()
univChecks = \case
  Univ
UProp -> TCMT IO Bool -> TCMT IO () -> TCMT IO ()
forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
unlessM TCMT IO Bool
forall (m :: * -> *). HasOptions m => m Bool
isPropEnabled (TCMT IO () -> TCMT IO ()) -> TCMT IO () -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ TypeError -> TCMT IO ()
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError TypeError
NeedOptionProp
  Univ
UType -> () -> TCMT IO ()
forall a. a -> TCMT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
  Univ
USSet -> TCMT IO Bool -> TCMT IO () -> TCMT IO ()
forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
unlessM TCMT IO Bool
forall (m :: * -> *). HasOptions m => m Bool
isTwoLevelEnabled (TCMT IO () -> TCMT IO ()) -> TCMT IO () -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ TypeError -> TCMT IO ()
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError TypeError
NeedOptionTwoLevel

suffixToLevel :: Suffix -> Integer
suffixToLevel :: Suffix -> Integer
suffixToLevel = \case
  Suffix
NoSuffix -> Integer
0
  Suffix Integer
n -> Integer
n

inferLeveledSort ::
     Univ                -- ^ The universe type.
  -> QName               -- ^ Name of the universe, for error reporting.
  -> Suffix              -- ^ Level of the universe given via suffix (optional).
  -> [NamedArg A.Expr]   -- ^ Level of the universe given via argument (absent if suffix).
  -> TCM (Term, Type)    -- ^ Universe and its sort.
inferLeveledSort :: Univ
-> QName
-> Suffix
-> [Arg (Named_ Expr)]
-> TCM (Term, Type'' Term Term)
inferLeveledSort Univ
u QName
q Suffix
suffix = \case
  [] -> do
    let n :: Integer
n = Suffix -> Integer
suffixToLevel Suffix
suffix
    (Term, Type'' Term Term) -> TCM (Term, Type'' Term Term)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Sort -> Term
Sort (Univ -> Level' Term -> Sort
forall t. Univ -> Level' t -> Sort' t
Univ Univ
u (Level' Term -> Sort) -> Level' Term -> Sort
forall a b. (a -> b) -> a -> b
$ Integer -> Level' Term
ClosedLevel Integer
n) , Sort -> Type'' Term Term
sort (Univ -> Level' Term -> Sort
forall t. Univ -> Level' t -> Sort' t
Univ (Univ -> Univ
univUniv Univ
u) (Level' Term -> Sort) -> Level' Term -> Sort
forall a b. (a -> b) -> a -> b
$ Integer -> Level' Term
ClosedLevel (Integer -> Level' Term) -> Integer -> Level' Term
forall a b. (a -> b) -> a -> b
$ Integer
n Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
1))
  Arg (Named_ Expr)
arg : [Arg (Named_ Expr)]
args -> do
    Bool -> TCMT IO () -> TCMT IO ()
forall b (m :: * -> *). (IsBool b, Monad m) => b -> m () -> m ()
unless (Arg (Named_ Expr) -> Bool
forall a. LensHiding a => a -> Bool
visible Arg (Named_ Expr)
arg) (TCMT IO () -> TCMT IO ()) -> TCMT IO () -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ TypeError -> TCMT IO ()
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> TCMT IO ()) -> TypeError -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ Type'' Term Term -> TypeError
WrongHidingInApplication (Type'' Term Term -> TypeError) -> Type'' Term Term -> TypeError
forall a b. (a -> b) -> a -> b
$ Sort -> Type'' Term Term
sort (Sort -> Type'' Term Term) -> Sort -> Type'' Term Term
forall a b. (a -> b) -> a -> b
$ Univ -> Level' Term -> Sort
forall t. Univ -> Level' t -> Sort' t
Univ Univ
u (Level' Term -> Sort) -> Level' Term -> Sort
forall a b. (a -> b) -> a -> b
$ Integer -> Level' Term
ClosedLevel Integer
0
    TCMT IO Bool -> TCMT IO () -> TCMT IO ()
forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
unlessM TCMT IO Bool
forall (m :: * -> *). HasOptions m => m Bool
hasUniversePolymorphism (TCMT IO () -> TCMT IO ()) -> TCMT IO () -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ TypeError -> TCMT IO ()
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError TypeError
NeedOptionUniversePolymorphism
    [Arg (Named_ Expr)]
-> (List1 (Arg (Named_ Expr)) -> TCMT IO ()) -> TCMT IO ()
forall (m :: * -> *) a.
Applicative m =>
[a] -> (List1 a -> m ()) -> m ()
List1.unlessNull [Arg (Named_ Expr)]
args ((List1 (Arg (Named_ Expr)) -> TCMT IO ()) -> TCMT IO ())
-> (List1 (Arg (Named_ Expr)) -> TCMT IO ()) -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ Warning -> TCMT IO ()
forall (m :: * -> *).
(HasCallStack, MonadWarning m) =>
Warning -> m ()
warning (Warning -> TCMT IO ())
-> (List1 (Arg (Named_ Expr)) -> Warning)
-> List1 (Arg (Named_ Expr))
-> TCMT IO ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. QName -> List1 (Arg (Named_ Expr)) -> Warning
TooManyArgumentsToSort QName
q
    l <- Relevance -> TCMT IO (Level' Term) -> TCMT IO (Level' Term)
forall (tcm :: * -> *) r a.
(MonadTCEnv tcm, LensRelevance r) =>
r -> tcm a -> tcm a
applyRelevanceToContext Relevance
shapeIrrelevant (TCMT IO (Level' Term) -> TCMT IO (Level' Term))
-> TCMT IO (Level' Term) -> TCMT IO (Level' Term)
forall a b. (a -> b) -> a -> b
$ Arg (Named_ Expr) -> TCMT IO (Level' Term)
checkLevel Arg (Named_ Expr)
arg
    return (Sort $ Univ u l , sort (Univ (univUniv u) $ levelSuc l))

inferUnivOmega ::
     Univ                -- ^ The universe type.
  -> QName               -- ^ Name of the universe, for error reporting.
  -> Suffix              -- ^ Level of the universe given via suffix (optional).
  -> [NamedArg A.Expr]   -- ^ Level of the universe given via argument (should be absent).
  -> TCM (Term, Type)    -- ^ Universe and its sort.
inferUnivOmega :: Univ
-> QName
-> Suffix
-> [Arg (Named_ Expr)]
-> TCM (Term, Type'' Term Term)
inferUnivOmega Univ
u QName
q Suffix
suffix [Arg (Named_ Expr)]
args = do
    [Arg (Named_ Expr)]
-> (List1 (Arg (Named_ Expr)) -> TCMT IO ()) -> TCMT IO ()
forall (m :: * -> *) a.
Applicative m =>
[a] -> (List1 a -> m ()) -> m ()
List1.unlessNull [Arg (Named_ Expr)]
args ((List1 (Arg (Named_ Expr)) -> TCMT IO ()) -> TCMT IO ())
-> (List1 (Arg (Named_ Expr)) -> TCMT IO ()) -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ Warning -> TCMT IO ()
forall (m :: * -> *).
(HasCallStack, MonadWarning m) =>
Warning -> m ()
warning (Warning -> TCMT IO ())
-> (List1 (Arg (Named_ Expr)) -> Warning)
-> List1 (Arg (Named_ Expr))
-> TCMT IO ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. QName -> List1 (Arg (Named_ Expr)) -> Warning
TooManyArgumentsToSort QName
q
    let n :: Integer
n = Suffix -> Integer
suffixToLevel Suffix
suffix
    (Term, Type'' Term Term) -> TCM (Term, Type'' Term Term)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Sort -> Term
Sort (Univ -> Integer -> Sort
forall t. Univ -> Integer -> Sort' t
Inf Univ
u Integer
n) , Sort -> Type'' Term Term
sort (Univ -> Integer -> Sort
forall t. Univ -> Integer -> Sort' t
Inf (Univ -> Univ
univUniv Univ
u) (Integer -> Sort) -> Integer -> Sort
forall a b. (a -> b) -> a -> b
$ Integer
1 Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
n))

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

checkSharpApplication :: A.Expr -> Type -> QName -> [NamedArg A.Expr] -> TCM Term
checkSharpApplication :: Expr
-> Type'' Term Term -> QName -> [Arg (Named_ Expr)] -> TCM Term
checkSharpApplication Expr
e Type'' Term Term
t QName
c [Arg (Named_ Expr)]
args = do
  arg <- case [Arg (Named_ Expr)]
args of
           [Arg (Named_ Expr)
a] | Arg (Named_ Expr) -> Bool
forall a. LensHiding a => a -> Bool
visible Arg (Named_ Expr)
a -> Expr -> TCMT IO Expr
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr -> TCMT IO Expr) -> Expr -> TCMT IO Expr
forall a b. (a -> b) -> a -> b
$ Arg (Named_ Expr) -> Expr
forall a. NamedArg a -> a
namedArg Arg (Named_ Expr)
a
           [Arg (Named_ Expr)]
_ -> TypeError -> TCMT IO Expr
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> TCMT IO Expr) -> TypeError -> TCMT IO Expr
forall a b. (a -> b) -> a -> b
$ QName -> TypeError
WrongSharpArity QName
c

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

  kit <- coinductionKit'
  let flat = CoinductionKit -> QName
nameOfFlat CoinductionKit
kit
      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).
  forcedType <- do
    lvl <- levelType
    (_, l) <- newValueMeta RunMetaOccursCheck CmpLeq lvl
    lv  <- levelView l
    (_, a) <- newValueMeta RunMetaOccursCheck CmpEq (sort $ Type lv)
    return $ El (Type lv) $ Def inf [Apply $ setHiding Hidden $ defaultArg l, Apply $ defaultArg a]

  wrapper <- inFreshModuleIfFreeParams $
             setRunTimeModeUnlessInHardCompileTimeMode $ do
    -- Andreas, 2019-10-12: create helper functions in non-erased mode.
    -- Otherwise, they are not usable in meta-solutions in the term world.
    -- #4743: Except if hard compile-time mode is enabled.
    c' <- setRange (getRange c) <$>
            liftM2 qualify (killRange <$> currentModule)
                           (freshName_ name)

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

    i <- currentOrFreshMutualBlock

    -- If we are in irrelevant position, add definition irrelevantly.
    -- If we are in erased position, add definition as erased.
    -- TODO: is this sufficient?
    addConstant c' =<< do
      let ai = Modality -> ArgInfo -> ArgInfo
forall a. LensModality a => Modality -> a -> a
setModality Modality
mod ArgInfo
defaultArgInfo
      lang <- getLanguage
      fun  <- emptyFunction
      useTerPragma $
        (defaultDefn ai c' forcedType lang fun)
        { defMutual = i }

    checkFunDef info c' $ singleton clause

    reportSDoc "tc.term.expr.coind" 15 $ do
      def <- theDef <$> getConstInfo c'
      vcat $
        [ "The coinductive wrapper"
        , nest 2 $ prettyTCM mod <> (prettyTCM c' <+> ":")
        , nest 4 $ prettyTCM t
        , nest 2 $ prettyA clause
        ]
    return c'

  -- The application of the fresh function to the relevant
  -- arguments.
  e' <- Def wrapper . map' Apply <$> getContextArgs

  reportSDoc "tc.term.expr.coind" 15 $ vcat $
      [ "The coinductive constructor application"
      , nest 2 $ prettyTCM e
      , "was translated into the application"
      , nest 2 $ prettyTCM e'
      ]

  blockTerm t $ e' <$ workOnTypes (leqType forcedType 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'' Term Term
_) Abs Term
t = TCM Term
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
  Term -> TCM Term
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> TCM Term) -> Term -> TCM Term
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 -> ArgRanges -> Args -> Type -> TCM Args
checkPrimComp :: QName
-> ArgRanges
-> [Arg Term]
-> Type'' Term Term
-> TCMT IO [Arg Term]
checkPrimComp QName
c ArgRanges
rs [Arg Term]
vs Type'' Term Term
_ = do
  case [Arg Term]
vs of
    -- WAS: [l, a, phi, u, a0] -> do
    Arg Term
l : Arg Term
a : Arg Term
phi : Arg Term
u : Arg Term
a0 : [Arg Term]
rest -> do
      iz <- ArgInfo -> Term -> Arg Term
forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
defaultArgInfo (Term -> Arg Term) -> TCM Term -> TCMT IO (Arg Term)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> IntervalView -> TCM Term
forall (m :: * -> *). HasBuiltins m => IntervalView -> m Term
intervalUnview IntervalView
IZero
      let lz = Arg Term -> Term
forall e. Arg e -> e
unArg Arg Term
l Term -> [Arg Term] -> Term
forall t. Apply t => t -> [Arg Term] -> t
`apply` [Arg Term
iz]
          az = Arg Term -> Term
forall e. Arg e -> e
unArg Arg Term
a Term -> [Arg Term] -> Term
forall t. Apply t => t -> [Arg Term] -> t
`apply` [Arg Term
iz]
      ty <- el's (pure (unArg l `apply` [iz])) $ primPartial <#> pure (unArg l `apply` [iz]) <@> pure (unArg phi) <@> pure (unArg a `apply` [iz])
      bAz <- el' (pure $ lz) (pure $ az)
      a0 <- blockArg bAz (rs !!! 4) a0 $ do
        equalTerm ty -- (El (getSort t1) (apply (unArg a) [iz]))
          (Lam defaultArgInfo $ NoAbs "_" $ unArg a0)
          (apply (unArg u) [iz])
      return $ l : a : phi : u : a0 : rest
    [Arg Term]
_ -> TypeError -> TCMT IO [Arg Term]
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> TCMT IO [Arg Term])
-> TypeError -> TCMT IO [Arg Term]
forall a b. (a -> b) -> a -> b
$ QName -> TypeError
CubicalPrimitiveNotFullyApplied QName
c

-- | @primHComp : ∀ {ℓ} {A : Set ℓ} {φ : I} (u : ∀ i → Partial φ A) (a : A) → A@
--
--   Check:  @u i0 = (λ _ → a) : Partial φ A@.
--
checkPrimHComp :: QName -> ArgRanges -> Args -> Type -> TCM Args
checkPrimHComp :: QName
-> ArgRanges
-> [Arg Term]
-> Type'' Term Term
-> TCMT IO [Arg Term]
checkPrimHComp QName
c ArgRanges
rs [Arg Term]
vs Type'' Term Term
_ = do
  case [Arg Term]
vs of
    -- WAS: [l, a, phi, u, a0] -> do
    Arg Term
l : Arg Term
a : Arg Term
phi : Arg Term
u : Arg Term
a0 : [Arg Term]
rest -> do
      -- iz = i0
      iz <- ArgInfo -> Term -> Arg Term
forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
defaultArgInfo (Term -> Arg Term) -> TCM Term -> TCMT IO (Arg Term)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> IntervalView -> TCM Term
forall (m :: * -> *). HasBuiltins m => IntervalView -> m Term
intervalUnview IntervalView
IZero
      -- ty = Partial φ A
      ty <- el's (pure (unArg l)) $ primPartial <#> pure (unArg l) <@> pure (unArg phi) <@> pure (unArg a)
      -- (λ _ → a) = u i0 : ty
      bA <- el' (pure $ unArg l) (pure $ unArg a)
      a0 <- blockArg bA (rs !!! 4) a0 $ do
        equalTerm ty -- (El (getSort t1) (apply (unArg a) [iz]))
            (Lam defaultArgInfo $ NoAbs "_" $ unArg a0)
            (apply (unArg u) [iz])
      return $ l : a : phi : u : a0 : rest
    [Arg Term]
_ -> TypeError -> TCMT IO [Arg Term]
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> TCMT IO [Arg Term])
-> TypeError -> TCMT IO [Arg Term]
forall a b. (a -> b) -> a -> b
$ QName -> TypeError
CubicalPrimitiveNotFullyApplied QName
c

-- | @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 -> ArgRanges -> Args -> Type -> TCM Args
checkPrimTrans :: QName
-> ArgRanges
-> [Arg Term]
-> Type'' Term Term
-> TCMT IO [Arg Term]
checkPrimTrans QName
c ArgRanges
rs [Arg Term]
vs Type'' Term Term
_ = do
  case [Arg Term]
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 : [Arg Term]
rest -> do
      iz <- ArgInfo -> Term -> Arg Term
forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
defaultArgInfo (Term -> Arg Term) -> TCM Term -> TCMT IO (Arg Term)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> IntervalView -> TCM Term
forall (m :: * -> *). HasBuiltins m => IntervalView -> m Term
intervalUnview IntervalView
IZero
      -- ty = (i : I) -> Set (l i)
      ty <- runNamesT [] $ do
        l <- open $ unArg l
        nPi' "i" primIntervalType $ \ NamesT (TCMT IO) Term
i -> (Sort -> Type'' Term Term
sort (Sort -> Type'' Term Term)
-> (Term -> Sort) -> Term -> Type'' Term Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term -> Sort
tmSort (Term -> Type'' Term Term)
-> NamesT (TCMT IO) Term -> NamesT (TCMT IO) (Type'' Term Term)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (NamesT (TCMT IO) Term
l NamesT (TCMT IO) Term
-> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT (TCMT IO) Term
i))
      a <- blockArg ty (rs !!! 1) a $ do
        equalTermOnFace (unArg phi) ty
          (unArg a)
          (Lam defaultArgInfo $ NoAbs "_" $ apply (unArg a) [iz])
      return $ l : a : phi : rest
    [Arg Term]
_ -> TypeError -> TCMT IO [Arg Term]
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> TCMT IO [Arg Term])
-> TypeError -> TCMT IO [Arg Term]
forall a b. (a -> b) -> a -> b
$ QName -> TypeError
CubicalPrimitiveNotFullyApplied QName
c

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

-- 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 -> ArgRanges -> Args -> Type -> TCM Args
checkPOr :: QName
-> ArgRanges
-> [Arg Term]
-> Type'' Term Term
-> TCMT IO [Arg Term]
checkPOr QName
c ArgRanges
rs [Arg Term]
vs Type'' Term Term
_ = do
  case [Arg Term]
vs of
   Arg Term
l : Arg Term
phi1 : Arg Term
phi2 : Arg Term
a : Arg Term
u : Arg Term
v : [Arg Term]
rest -> do
      phi <- IntervalView -> TCM Term
forall (m :: * -> *). HasBuiltins m => IntervalView -> m Term
intervalUnview (Arg Term -> Arg Term -> IntervalView
IMin Arg Term
phi1 Arg Term
phi2)
      reportSDoc "tc.term.por" 10 $ text (show phi)
      t1 <- runNamesT [] $ do
             l <- open . unArg $ l
             a <- open . unArg $ a
             psi <- open =<< intervalUnview (IMax phi1 phi2)
             pPi' "o" psi $ \ NamesT (TCMT IO) Term
o -> NamesT (TCMT IO) Term
-> NamesT (TCMT IO) Term -> NamesT (TCMT IO) (Type'' Term Term)
forall (m :: * -> *).
Applicative m =>
m Term -> m Term -> m (Type'' Term Term)
el' NamesT (TCMT IO) Term
l (NamesT (TCMT IO) Term
a NamesT (TCMT IO) Term
-> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<..> NamesT (TCMT IO) Term
o)
      tv <- runNamesT [] $ do
             l    <- open . unArg $ l
             a    <- open . unArg $ a
             phi1 <- open . unArg $ phi1
             phi2 <- open . unArg $ phi2
             pPi' "o" phi2 $ \ NamesT (TCMT IO) Term
o -> NamesT (TCMT IO) Term
-> NamesT (TCMT IO) Term -> NamesT (TCMT IO) (Type'' Term Term)
forall (m :: * -> *).
Applicative m =>
m Term -> m Term -> m (Type'' Term Term)
el' NamesT (TCMT IO) Term
l (NamesT (TCMT IO) Term
a NamesT (TCMT IO) Term
-> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<..> (TCM Term -> NamesT (TCMT IO) Term
forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl TCM Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primIsOne2 NamesT (TCMT IO) Term
-> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT (TCMT IO) Term
phi1 NamesT (TCMT IO) Term
-> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT (TCMT IO) Term
phi2 NamesT (TCMT IO) Term
-> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT (TCMT IO) Term
o))
      v <- blockArg tv (rs !!! 5) v $ do
        -- ' φ₁ ∧ φ₂  ⊢ u , v : PartialP (φ₁ ∨ φ₂) \ o → a o
        equalTermOnFace phi t1 (unArg u) (unArg v)
      return $ l : phi1 : phi2 : a : u : v : rest
   [Arg Term]
_ -> TypeError -> TCMT IO [Arg Term]
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> TCMT IO [Arg Term])
-> TypeError -> TCMT IO [Arg Term]
forall a b. (a -> b) -> a -> b
$ QName -> TypeError
CubicalPrimitiveNotFullyApplied QName
c

-- | @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 -> ArgRanges -> Args -> Type -> TCM Args
check_glue :: QName
-> ArgRanges
-> [Arg Term]
-> Type'' Term Term
-> TCMT IO [Arg Term]
check_glue QName
c ArgRanges
rs [Arg Term]
vs Type'' Term Term
_ = do
  case [Arg Term]
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 : [Arg Term]
rest -> do
      v <- [[Char]] -> NamesT (TCMT IO) Term -> TCM Term
forall (m :: * -> *) a. [[Char]] -> NamesT m a -> m a
runNamesT [] (NamesT (TCMT IO) Term -> TCM Term)
-> NamesT (TCMT IO) Term -> TCM Term
forall a b. (a -> b) -> a -> b
$ do
            lb  <- Term -> NamesT (TCMT IO) (NamesT (TCMT IO) Term)
forall (m :: * -> *) a.
(Monad m, Subst a) =>
a -> NamesT m (NamesT m a)
open (Term -> NamesT (TCMT IO) (NamesT (TCMT IO) Term))
-> (Arg Term -> Term)
-> Arg Term
-> NamesT (TCMT IO) (NamesT (TCMT IO) Term)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Arg Term -> Term
forall e. Arg e -> e
unArg (Arg Term -> NamesT (TCMT IO) (NamesT (TCMT IO) Term))
-> Arg Term -> NamesT (TCMT IO) (NamesT (TCMT IO) Term)
forall a b. (a -> b) -> a -> b
$ Arg Term
lb
            la  <- open . unArg $ la
            bA  <- open . unArg $ bA
            phi <- open . unArg $ phi
            bT  <- open . unArg $ bT
            e   <- open . unArg $ e
            t   <- open . unArg $ t
            let f NamesT (TCMT IO) Term
o = TCM Term -> NamesT (TCMT IO) Term
forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl TCM Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primEquivFun NamesT (TCMT IO) Term
-> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> NamesT (TCMT IO) Term
lb NamesT (TCMT IO) Term
-> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> NamesT (TCMT IO) Term
la NamesT (TCMT IO) Term
-> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> (NamesT (TCMT IO) Term
bT NamesT (TCMT IO) Term
-> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<..> NamesT (TCMT IO) Term
o) NamesT (TCMT IO) Term
-> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> NamesT (TCMT IO) Term
bA NamesT (TCMT IO) Term
-> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> (NamesT (TCMT IO) Term
e NamesT (TCMT IO) Term
-> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<..> NamesT (TCMT IO) Term
o)
            glam defaultIrrelevantArgInfo "o" $ \ NamesT (TCMT IO) Term
o -> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
f NamesT (TCMT IO) Term
o NamesT (TCMT IO) Term
-> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> (NamesT (TCMT IO) Term
t NamesT (TCMT IO) Term
-> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<..> NamesT (TCMT IO) Term
o)
      ty <- runNamesT [] $ do
            lb  <- open . unArg $ lb
            phi <- open . unArg $ phi
            bA  <- open . unArg $ bA
            el's lb $ cl primPartialP <#> lb <@> phi <@> glam defaultIrrelevantArgInfo "o" (\ NamesT (TCMT IO) Term
_ -> NamesT (TCMT IO) Term
bA)
      let a' = ArgInfo -> Abs Term -> Term
Lam ArgInfo
defaultIrrelevantArgInfo ([Char] -> Term -> Abs Term
forall a. [Char] -> a -> Abs a
NoAbs [Char]
"o" (Term -> Abs Term) -> Term -> Abs Term
forall a b. (a -> b) -> a -> b
$ Arg Term -> Term
forall e. Arg e -> e
unArg Arg Term
a)
      ta <- el' (pure $ unArg la) (pure $ unArg bA)
      a <- blockArg ta (rs !!! 7) a $ equalTerm ty a' v
      return $ la : lb : bA : phi : bT : e : t : a : rest
   [Arg Term]
_ -> TypeError -> TCMT IO [Arg Term]
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> TCMT IO [Arg Term])
-> TypeError -> TCMT IO [Arg Term]
forall a b. (a -> b) -> a -> b
$ QName -> TypeError
CubicalPrimitiveNotFullyApplied QName
c


-- | @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 -> ArgRanges -> Args -> Type -> TCM Args
check_glueU :: QName
-> ArgRanges
-> [Arg Term]
-> Type'' Term Term
-> TCMT IO [Arg Term]
check_glueU QName
c ArgRanges
rs [Arg Term]
vs Type'' Term Term
_ = do
  case [Arg Term]
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 : [Arg Term]
rest -> do
      v <- [[Char]] -> NamesT (TCMT IO) Term -> TCM Term
forall (m :: * -> *) a. [[Char]] -> NamesT m a -> m a
runNamesT [] (NamesT (TCMT IO) Term -> TCM Term)
-> NamesT (TCMT IO) Term -> TCM Term
forall a b. (a -> b) -> a -> b
$ do
            la  <- Term -> NamesT (TCMT IO) (NamesT (TCMT IO) Term)
forall (m :: * -> *) a.
(Monad m, Subst a) =>
a -> NamesT m (NamesT m a)
open (Term -> NamesT (TCMT IO) (NamesT (TCMT IO) Term))
-> (Arg Term -> Term)
-> Arg Term
-> NamesT (TCMT IO) (NamesT (TCMT IO) Term)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Arg Term -> Term
forall e. Arg e -> e
unArg (Arg Term -> NamesT (TCMT IO) (NamesT (TCMT IO) Term))
-> Arg Term -> NamesT (TCMT IO) (NamesT (TCMT IO) Term)
forall a b. (a -> b) -> a -> b
$ Arg Term
la
            phi <- open . unArg $ phi
            bT  <- open . unArg $ bT
            bA  <- open . unArg $ bA
            t   <- open . unArg $ t
            let f NamesT (TCMT IO) Term
o = TCM Term -> NamesT (TCMT IO) Term
forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl TCM Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primTrans NamesT (TCMT IO) Term
-> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> [Char]
-> (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term)
-> NamesT (TCMT IO) Term
forall (m :: * -> *).
Monad m =>
[Char] -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
lam [Char]
"i" (NamesT (TCMT IO) Term
-> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
forall a b. a -> b -> a
const NamesT (TCMT IO) Term
la) NamesT (TCMT IO) Term
-> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> [Char]
-> (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term)
-> NamesT (TCMT IO) Term
forall (m :: * -> *).
Monad m =>
[Char] -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
lam [Char]
"i" (\ NamesT (TCMT IO) Term
i -> NamesT (TCMT IO) Term
bT NamesT (TCMT IO) Term
-> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> (TCM Term -> NamesT (TCMT IO) Term
forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl TCM Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primINeg NamesT (TCMT IO) Term
-> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT (TCMT IO) Term
i) NamesT (TCMT IO) Term
-> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<..> NamesT (TCMT IO) Term
o) NamesT (TCMT IO) Term
-> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> TCM Term -> NamesT (TCMT IO) Term
forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl TCM Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primIZero
            glam defaultIrrelevantArgInfo "o" $ \ NamesT (TCMT IO) Term
o -> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
f NamesT (TCMT IO) Term
o NamesT (TCMT IO) Term
-> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> (NamesT (TCMT IO) Term
t NamesT (TCMT IO) Term
-> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<..> NamesT (TCMT IO) Term
o)
      ty <- runNamesT [] $ do
            la  <- open . unArg $ la
            phi <- open . unArg $ phi
            bT  <- open . unArg $ bT
            pPi' "o" phi $ \ NamesT (TCMT IO) Term
o -> NamesT (TCMT IO) Term
-> NamesT (TCMT IO) Term -> NamesT (TCMT IO) (Type'' Term Term)
forall (m :: * -> *).
Applicative m =>
m Term -> m Term -> m (Type'' Term Term)
el' NamesT (TCMT IO) Term
la (NamesT (TCMT IO) Term
bT NamesT (TCMT IO) Term
-> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> TCM Term -> NamesT (TCMT IO) Term
forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl TCM Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primIZero NamesT (TCMT IO) Term
-> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<..> NamesT (TCMT IO) Term
o)
      let a' = ArgInfo -> Abs Term -> Term
Lam ArgInfo
defaultIrrelevantArgInfo ([Char] -> Term -> Abs Term
forall a. [Char] -> a -> Abs a
NoAbs [Char]
"o" (Term -> Abs Term) -> Term -> Abs Term
forall a b. (a -> b) -> a -> b
$ Arg Term -> Term
forall e. Arg e -> e
unArg Arg Term
a)
      ta <- runNamesT [] $ do
            la  <- open . unArg $ la
            phi <- open . unArg $ phi
            bT  <- open . unArg $ bT
            bA  <- open . unArg $ bA
            el' la (cl primSubOut <#> (cl primLevelSuc <@> la) <#> (Sort . tmSort <$> la) <#> phi <#> (bT <@> cl primIZero) <@> bA)
      a <- blockArg ta (rs !!! 5) a $ equalTerm ty a' v
      return $ la : phi : bT : bA : t : a : rest
   [Arg Term]
_ -> TypeError -> TCMT IO [Arg Term]
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> TCMT IO [Arg Term])
-> TypeError -> TCMT IO [Arg Term]
forall a b. (a -> b) -> a -> b
$ QName -> TypeError
CubicalPrimitiveNotFullyApplied QName
c