{-# LANGUAGE NondecreasingIndentation #-}

module Mikan.TypeChecking.Rules.Application
  ( AppHead(..), ArgsCheck, ArgRanges
  , checkArguments
  , checkArguments_
  , checkApplication
  , inferApplication
  , checkProjAppToKnownPrincipalArg
  , disambiguateConstructor'
  , univChecks
  , suffixToLevel
  , coerce'
  ) 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 Data.Foldable qualified as Fold
import Data.IntSet qualified as IntSet
import Data.Map.Strict qualified as Map
import Data.Text.Short (ShortText)
import Data.Text.Short qualified as TS

import Mikan.Interaction.Highlighting.Generate
  ( storeDisambiguatedConstructor, storeDisambiguatedProjection )

import Mikan.Syntax.Abstract qualified as A
import Mikan.Syntax.Abstract.Pattern (patternToExpr)
import Mikan.Syntax.Scope.Errors
import Mikan.Syntax.Abstract.Views as A
import Mikan.Syntax.Info qualified as A
import Mikan.Syntax.Concrete.Pretty () -- only Pretty instances
import Mikan.Syntax.Common
import Mikan.Syntax.Internal as I
import Mikan.Syntax.Position

import Mikan.TypeChecking.Conversion
import Mikan.TypeChecking.Constraints
import Mikan.TypeChecking.Datatypes
import Mikan.TypeChecking.Free
import Mikan.TypeChecking.Implicit
import Mikan.TypeChecking.Injectivity
import Mikan.TypeChecking.InstanceArguments (postponeInstanceConstraints)
import Mikan.TypeChecking.Level
import Mikan.TypeChecking.MetaVars
import Mikan.TypeChecking.Names
import Mikan.TypeChecking.Pretty
import Mikan.TypeChecking.Primitive hiding (Nat)
import Mikan.TypeChecking.Monad
import Mikan.TypeChecking.Records
import Mikan.TypeChecking.Reduce
import Mikan.TypeChecking.Rules.Def
import Mikan.TypeChecking.Rules.Term
import Mikan.TypeChecking.Rules.Cubical
import Mikan.TypeChecking.Substitute
import Mikan.TypeChecking.Telescope
import Mikan.TypeChecking.Warnings (warning)

import Mikan.Utils.Either
import Mikan.Utils.Function
import Mikan.Utils.Functor
import Mikan.Utils.Lens
import Mikan.Utils.List hiding (Suffix)
import Mikan.Utils.List qualified as List
import Mikan.Utils.List1 ( List1, pattern (:|) )
import Mikan.Utils.List1 qualified as List1
import Mikan.Utils.Maybe
import Mikan.Utils.Monad
import Mikan.Utils.Null
import Mikan.Syntax.Common.Pretty ( prettyShow )
import Mikan.Utils.Size
import Mikan.Utils.Tuple
import Mikan.Utils.VarSet qualified as VarSet

import Mikan.Utils.Impossible
import Mikan.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. Elims -> ArgsCheckState a -> ArgsCheckState a
setACElims Elims
es ArgsCheckState a
st = ArgsCheckState a
st{ acCheckedArgs = go es (acCheckedArgs st) }
  where
    go :: Elims -> [CheckedArg] -> [CheckedArg]
go [] [] = []
    go (Elim
e : Elims
es) (CheckedArg
ca : [CheckedArg]
cas) = CheckedArg
ca{ caElim = e } CheckedArg -> [CheckedArg] -> [CheckedArg]
forall a. a -> [a] -> [a]
: Elims -> [CheckedArg] -> [CheckedArg]
go Elims
es [CheckedArg]
cas
    go Elims
_ [CheckedArg]
_ = [CheckedArg]
forall a. HasCallStack => a
__IMPOSSIBLE__

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

-- | Something that can appear as the head of an elimination spine in
-- abstract syntax.
data AppHead
  = TermAppHd Term
    -- ^ A head term that has already been elaborated, and does not impose
    -- any constraints on the shape of its arguments.
    --
    -- Used for metavariables, which are already applied to their context,
    -- but may be of function type; and for the known-good argument that
    -- was used to disambiguate an overloaded projection, which may
    -- receive further arguments.
  | ConAppHd !ConHead !Int
    -- ^ A constructor with the given number of parameters.
  | PrimAppHd !QName !ArgsCheck
    -- ^ A bound primitive which imposes extra checks on its argument
    -- spine. In this case, the eliminations given must all be 'Apply',
    -- and the stored continuation indicates what extra checks should be
    -- performed.

type ArgsCheck = ArgRanges -> Elims -> Type -> TCM Elims

-- | Apply a head expression to its newly-checked arguments,
-- constructing an internal term.
--
-- This handles checking any side conditions on the eliminations that
-- are imposed by the head before building the term, like the
-- constraints on cubical primitives, or dropping the parameters of
-- constructors.
applyCheckedArgs :: AppHead -> ArgsCheckState a -> TCM Term
applyCheckedArgs :: forall a. AppHead -> ArgsCheckState a -> TCM Term
applyCheckedArgs AppHead
hd ACState{ acCheckedArgs :: forall a. ArgsCheckState a -> [CheckedArg]
acCheckedArgs = [CheckedArg]
cas, acType :: forall a. ArgsCheckState a -> Type
acType = Type
t1 } = case AppHead
hd of
  TermAppHd Term
tm   -> Term -> TCM Term
forall a. a -> TCMT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Term -> TCM Term) -> Term -> TCM Term
forall a b. (a -> b) -> a -> b
$! Term
tm Term -> Elims -> Term
forall t. Apply t => t -> Elims -> t
`applyE` (CheckedArg -> Elim) -> [CheckedArg] -> Elims
forall a b. (a -> b) -> [a] -> [b]
map' CheckedArg -> Elim
caElim [CheckedArg]
cas
  ConAppHd ConHead
cn Int
ps -> Term -> TCM Term
forall a. a -> TCMT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Term -> TCM Term) -> Term -> TCM Term
forall a b. (a -> b) -> a -> b
$! ConHead -> ConInfo -> Elims -> Term
Con ConHead
cn ConInfo
ConOCon (Elims -> Term) -> Elims -> Term
forall a b. (a -> b) -> a -> b
$! (CheckedArg -> Elim) -> [CheckedArg] -> Elims
forall a b. (a -> b) -> [a] -> [b]
map' CheckedArg -> Elim
caElim (Int -> [CheckedArg] -> [CheckedArg]
forall a. Int -> [a] -> [a]
drop Int
ps [CheckedArg]
cas)
  PrimAppHd QName
qn ArgsCheck
k -> do
    let !vs :: Elims
vs = (CheckedArg -> Elim) -> [CheckedArg] -> Elims
forall a b. (a -> b) -> [a] -> [b]
map' CheckedArg -> Elim
caElim [CheckedArg]
cas
    [Char] -> Int -> TCMT IO Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.term.args.prim" Int
30 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"checking primitive args" 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
qn TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
$$ Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (Elims -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Elims -> m Doc
prettyTCM Elims
vs)
    !as <- ArgsCheck
k ((CheckedArg -> Range) -> [CheckedArg] -> [Range]
forall a b. (a -> b) -> [a] -> [b]
map' CheckedArg -> Range
caRange [CheckedArg]
cas) Elims
vs Type
t1
    pure $! Def qn as


-- | @checkApplication hd args e t@ checks an application.
--   Precondition: @Application hs args = appView e@
--
--   @checkApplication@ disambiguates constructors
--   (and continues to 'checkConstructorApplication')
--   and resolves pattern synonyms.
checkApplication :: Comparison -> A.Expr -> A.Args -> A.Expr -> Type -> TCM Term
checkApplication :: Comparison -> Expr -> [NamedArg Expr] -> Expr -> Type -> TCM Term
checkApplication Comparison
cmp Expr
hd [NamedArg Expr]
args Expr
e Type
t =
  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
$ (NamedArg Expr -> TCMT IO Doc) -> [NamedArg Expr] -> [TCMT IO Doc]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap NamedArg Expr -> TCMT IO Doc
forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA [NamedArg 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 -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type -> m Doc
prettyTCM Type
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]
++! [NamedArg Expr] -> [Char]
forall a. Show a => a -> [Char]
show ([NamedArg Expr] -> [NamedArg Expr]
forall a. ExprLike a => a -> a
deepUnscope [NamedArg 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 -> [Char]
forall a. Show a => a -> [Char]
show Type
t
    ]
  case Expr -> Expr
unScope Expr
hd of
    -- Subcase: unambiguous projection
    A.Proj ProjOrigin
o AmbiguousQName
p | Just QName
x <- AmbiguousQName -> Maybe QName
getUnambiguous AmbiguousQName
p -> do
      Comparison
-> Expr
-> Type
-> QName
-> ProjOrigin
-> Expr
-> [NamedArg Expr]
-> TCM Term
checkUnambiguousProjectionApplication Comparison
cmp Expr
e Type
t QName
x ProjOrigin
o Expr
hd [NamedArg Expr]
args

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

    -- Subcase: unambiguous constructor
    A.Con AmbiguousQName
ambC | Just QName
c <- AmbiguousQName -> Maybe QName
getUnambiguous AmbiguousQName
ambC -> do
      -- augment c with record fields, but do not revert to original name
      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 -> ConHead -> Expr -> [NamedArg Expr] -> TCM Term
checkConstructorApplication Comparison
cmp Expr
e Type
t ConHead
c Expr
hd [NamedArg 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
-> [NamedArg Expr] -> Type -> DisambiguateConstructor
disambiguateConstructor AmbiguousQName
ambC [NamedArg Expr]
args Type
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      -> PatternSynonymError -> TCM Term
forall (m :: * -> *) e a.
(HasCallStack, MonadTCError m, Diagnostic e) =>
e -> m a
typeError (PatternSynonymError -> TCM Term)
-> PatternSynonymError -> TCM Term
forall a b. (a -> b) -> a -> b
$ AmbiguousQName -> PatternSynonymError
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 -> TCM Term
checkExpr' Comparison
cmp Expr
e' Type
t

    -- Subcase: macro
    A.Macro QName
x -> do
      -- First go: no parameters
      TelV tel _ <- Type -> TCMT IO (TelV Type)
forall (m :: * -> *).
(MonadReduce m, MonadAddContext m) =>
Type -> m (TelV Type)
telView (Type -> TCMT IO (TelV Type))
-> (Definition -> Type) -> Definition -> TCMT IO (TelV Type)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Definition -> Type
defType (Definition -> TCMT IO (TelV Type))
-> TCMT IO Definition -> TCMT IO (TelV Type)
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 (ArgName, Type)] -> [Dom' Term (ArgName, Type)]
forall a. HasCallStack => [a] -> [a]
init ([Dom' Term (ArgName, Type)] -> [Dom' Term (ArgName, Type)])
-> [Dom' Term (ArgName, Type)] -> [Dom' Term (ArgName, Type)]
forall a b. (a -> b) -> a -> b
$ Tele (Dom Type) -> [Dom' Term (ArgName, Type)]
forall t. Tele (Dom t) -> [Dom (ArgName, t)]
telToList Tele (Dom Type)
tel -- last argument is the hole term

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

          makeArgs :: [Dom (ShortText, Type)] -> [NamedArg A.Expr] -> ([NamedArg A.Expr], [NamedArg A.Expr])
          makeArgs [] [NamedArg Expr]
args = ([], [NamedArg Expr]
args)
          makeArgs [Dom' Term (ArgName, Type)]
_  []   = ([], [])
          makeArgs tel :: [Dom' Term (ArgName, Type)]
tel@(Dom' Term (ArgName, Type)
d : [Dom' Term (ArgName, Type)]
tel1) (NamedArg Expr
arg : [NamedArg Expr]
args) =
            case NamedArg Expr -> [Dom' Term (ArgName, Type)] -> ImplicitInsertion
forall e a. NamedArg e -> [Dom a] -> ImplicitInsertion
insertImplicit NamedArg Expr
arg [Dom' Term (ArgName, Type)]
tel of
              ImplicitInsertion
NoInsertNeeded -> ([NamedArg Expr] -> [NamedArg Expr])
-> ([NamedArg Expr], [NamedArg Expr])
-> ([NamedArg Expr], [NamedArg 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 -> NamedArg Expr -> NamedArg Expr
mkArg ((ArgName, Type) -> Type
forall a b. (a, b) -> b
snd ((ArgName, Type) -> Type) -> (ArgName, Type) -> Type
forall a b. (a -> b) -> a -> b
$ Dom' Term (ArgName, Type) -> (ArgName, Type)
forall t e. Dom' t e -> e
unDom Dom' Term (ArgName, Type)
d) NamedArg Expr
arg NamedArg Expr -> [NamedArg Expr] -> [NamedArg Expr]
forall a. a -> [a] -> [a]
:) (([NamedArg Expr], [NamedArg Expr])
 -> ([NamedArg Expr], [NamedArg Expr]))
-> ([NamedArg Expr], [NamedArg Expr])
-> ([NamedArg Expr], [NamedArg Expr])
forall a b. (a -> b) -> a -> b
$ [Dom' Term (ArgName, Type)]
-> [NamedArg Expr] -> ([NamedArg Expr], [NamedArg Expr])
makeArgs [Dom' Term (ArgName, Type)]
tel1 [NamedArg Expr]
args
              ImpInsert [Dom ()]
is   -> [Dom' Term (ArgName, Type)]
-> [NamedArg Expr] -> ([NamedArg Expr], [NamedArg Expr])
makeArgs (Int -> [Dom' Term (ArgName, Type)] -> [Dom' Term (ArgName, Type)]
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 (ArgName, Type)]
tel) (NamedArg Expr
arg NamedArg Expr -> [NamedArg Expr] -> [NamedArg Expr]
forall a. a -> [a] -> [a]
: [NamedArg Expr]
args)
              ImplicitInsertion
BadImplicits   -> (NamedArg Expr
arg NamedArg Expr -> [NamedArg Expr] -> [NamedArg Expr]
forall a. a -> [a] -> [a]
: [NamedArg Expr]
args, [])  -- fail later in checkHeadApplication
              NoSuchName{}   -> (NamedArg Expr
arg NamedArg Expr -> [NamedArg Expr] -> [NamedArg Expr]
forall a. a -> [a] -> [a]
: [NamedArg Expr]
args, [])  -- ditto

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

          desugared = Expr -> [NamedArg 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 -> [NamedArg Expr] -> AppView
forall arg. Expr -> [NamedArg arg] -> AppView' arg
Application (QName -> Expr
A.Def QName
x) ([NamedArg Expr] -> AppView) -> [NamedArg Expr] -> AppView
forall a b. (a -> b) -> a -> b
$ [NamedArg Expr]
macroArgs) [NamedArg Expr]
otherArgs

      checkExpr' cmp desugared t

    -- Subcase: unquote
    A.Unquote ExprInfo
_
      | [NamedArg Expr
arg] <- [NamedArg Expr]
args -> do
          (_, hole) <- RunMetaOccursCheck -> Comparison -> Type -> TCM (MetaId, Term)
newValueMeta RunMetaOccursCheck
RunMetaOccursCheck Comparison
CmpLeq Type
t
          unquoteM (namedArg arg) hole t
          return hole
      | NamedArg Expr
arg : [NamedArg Expr]
args <- [NamedArg Expr]
args -> do
          -- Example: unquote v a b : A
          --  Create meta H : (x : X) (y : Y x) → Z x y for the hole
          --  Check a : X, b : Y a
          --  Run the tactic on H
          --  Check H a b : A
          tel    <- [NamedArg Expr] -> TCM (Tele (Dom Type))
forall a. [Arg a] -> TCM (Tele (Dom Type))
metaTel [NamedArg Expr]
args                    -- (x : X) (y : Y x)
          target <- addContext tel newTypeMeta_     -- Z x y
          let holeType = Tele (Dom Type) -> Type -> Type
telePi_ Tele (Dom Type)
tel Type
target         -- (x : X) (y : Y x) → Z x y
          let hd       = NamedArg Expr -> Expr
forall a. NamedArg a -> a
namedArg NamedArg 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 Type))
metaTel []           = Tele (Dom Type) -> TCM (Tele (Dom Type))
forall a. a -> TCMT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Tele (Dom Type)
forall a. Tele a
EmptyTel
        metaTel (Arg a
arg : [Arg a]
args) = do
          a <- TCMT IO Type
newTypeMeta_
          let dom = Type
a Type -> Dom' Term a -> Dom Type
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 t. Arg a -> Dom' t a
domFromArg Arg a
arg
          ExtendTel dom . Abs "x" <$>
            addContext ("x" :: ShortText, dom) (metaTel args)

    -- Subcase: defined symbol or variable.
    Expr
_ -> do
      v <- Comparison -> Expr -> Type -> Expr -> [NamedArg Expr] -> TCM Term
checkHeadApplication Comparison
cmp Expr
e Type
t Expr
hd [NamedArg 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 -> [NamedArg Expr] -> Expr -> TCM (Term, Type)
inferApplication ExpandHidden
exh Expr
hd [NamedArg Expr]
args Expr
e | Bool -> Bool
not (Expr -> Bool
defOrVar Expr
hd) = do
  t <- TCMT IO Type -> TCMT IO Type
forall (m :: * -> *) a. (MonadTCEnv m, MonadDebug m) => m a -> m a
workOnTypes (TCMT IO Type -> TCMT IO Type) -> TCMT IO Type -> TCMT IO Type
forall a b. (a -> b) -> a -> b
$ TCMT IO Type
newTypeMeta_
  v <- checkExpr' CmpEq e t
  return (v, t)
inferApplication ExpandHidden
exh Expr
hd [NamedArg Expr]
args Expr
e = TCM (Term, Type) -> TCM (Term, Type)
forall a. TCM a -> TCM a
postponeInstanceConstraints (TCM (Term, Type) -> TCM (Term, Type))
-> TCM (Term, Type) -> TCM (Term, Type)
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
-> [NamedArg Expr]
-> TCM (Term, Type)
inferProjApp Expr
e ProjOrigin
o AmbiguousQName
p Expr
hd [NamedArg 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
-> [NamedArg Expr]
-> TCM (Term, Type)
inferUniv UnivSize
sz Univ
u Expr
e QName
x Suffix
s [NamedArg Expr]
args
    Expr
_ -> do
      (f, t0) <- Expr -> TCM (AppHead, Type)
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
acType = Type
t1}) -> (Term -> (Term, Type)) -> TCM Term -> TCM (Term, Type)
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
t1) (TCM Term -> TCM (Term, Type)) -> TCM Term -> TCM (Term, Type)
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
=<< AppHead -> ArgsCheckState CheckedTarget -> TCM Term
forall a. AppHead -> ArgsCheckState a -> TCM Term
applyCheckedArgs AppHead
f ArgsCheckState CheckedTarget
st
        Left ArgsCheckState [NamedArg Expr]
problem -> do
          t <- TCMT IO Type -> TCMT IO Type
forall (m :: * -> *) a. (MonadTCEnv m, MonadDebug m) => m a -> m a
workOnTypes (TCMT IO Type -> TCMT IO Type) -> TCMT IO Type -> TCMT IO Type
forall a b. (a -> b) -> a -> b
$ TCMT IO Type
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
=<< AppHead -> ArgsCheckState CheckedTarget -> TCM Term
forall a. AppHead -> ArgsCheckState a -> TCM Term
applyCheckedArgs AppHead
f ArgsCheckState CheckedTarget
st
          return (v, t)

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

inferHeadDef :: ProjOrigin -> QName -> TCM (AppHead, Type)
inferHeadDef :: ProjOrigin -> QName -> TCM (AppHead, Type)
inferHeadDef ProjOrigin
o QName
x = do
  qi <- QName -> TCMT IO Definition
forall (m :: * -> *).
(HasConstInfo m, HasCallStack) =>
QName -> m Definition
getConstInfo QName
x
  case theDef qi of
    -- the constrained primitives cannot be defined in a parametrised
    -- module, so there's no need to instantiate the telescope and the
    -- definition with the context parameters.
    Primitive{ primName :: Defn -> PrimitiveId
primName = PrimitiveId
name }
      | Just QName -> ArgsCheck
check <- PrimitiveId
name PrimitiveId
-> Map PrimitiveId (QName -> ArgsCheck)
-> Maybe (QName -> ArgsCheck)
forall k a. Ord k => k -> Map k a -> Maybe a
`Map.lookup` Map PrimitiveId (QName -> ArgsCheck)
cubicalPrimChecks -> (AppHead, Type) -> TCM (AppHead, Type)
forall a. a -> TCMT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (QName -> ArgsCheck -> AppHead
PrimAppHd QName
x (QName -> ArgsCheck
check QName
x), Definition -> Type
defType Definition
qi)

    -- otherwise, there might be some free vars to apply. if the
    -- definition is a projection, make sure the parameters get dropped
    -- when the definition is instantiated.
    -- (but no dropping happens afterwards.)
    Defn
def
      | Just Projection
p <- Defn -> Maybe Projection
isProjectionDefn Defn
def -> (Term -> AppHead) -> (Term, Type) -> (AppHead, Type)
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 Term -> AppHead
TermAppHd ((Term, Type) -> (AppHead, Type))
-> TCM (Term, Type) -> TCM (AppHead, Type)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ([Arg Term] -> Term) -> QName -> TCM (Term, Type)
inferDef (Projection -> ProjOrigin -> [Arg Term] -> Term
projDropParsApply Projection
p ProjOrigin
o) QName
x
      | Bool
otherwise                      -> (Term -> AppHead) -> (Term, Type) -> (AppHead, Type)
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 Term -> AppHead
TermAppHd ((Term, Type) -> (AppHead, Type))
-> TCM (Term, Type) -> TCM (AppHead, Type)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ([Arg Term] -> Term) -> QName -> TCM (Term, Type)
inferDef (QName -> Elims -> Term
Def QName
x (Elims -> Term) -> ([Arg Term] -> Elims) -> [Arg Term] -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Arg Term -> Elim) -> [Arg Term] -> Elims
forall a b. (a -> b) -> [a] -> [b]
map' Arg Term -> Elim
forall a. Arg a -> Elim' a
Apply)    QName
x

-- | Infer the type of a head thing (variable, function symbol, or constructor).
--   We return a function that applies the head to arguments.
--   This is because in case of a constructor we want to drop the parameters.
inferHead :: A.Expr -> TCM (AppHead, Type)
inferHead :: Expr -> TCM (AppHead, Type)
inferHead Expr
e = do
  case Expr
e of
    A.Var Name
x -> do -- traceCall (InferVar x) $ do
      (u, a) <- Name -> TCMT IO (Term, Dom Type)
forall (m :: * -> *).
(MonadDebug m, MonadFail m, MonadTCEnv m) =>
Name -> m (Term, Dom Type)
getVarInfo Name
x
      reportSDoc "tc.term.var" 20 $ hsep
        [ "variable" , prettyTCM x
        , "(" , text (show u) , ")"
        , "has type:" , prettyTCM a
        ]
      return (TermAppHd u, unDom a)

    A.Def QName
c  -> ProjOrigin -> QName -> TCM (AppHead, Type)
inferHeadDef ProjOrigin
ProjPrefix QName
c
    A.Def'{} -> TCM (AppHead, Type)
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 (AppHead, Type)
inferHeadDef ProjOrigin
o QName
d
    A.Proj{} -> TCM (AppHead, Type)
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 -> Elims -> 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 (ConAppHd con n, a)
    A.Con{} -> TCM (AppHead, Type)
forall a. HasCallStack => a
__IMPOSSIBLE__  -- inferHead will only be called on unambiguous constructors

    A.QuestionMark MetaInfo
i InteractionId
ii -> MetaInfo
-> (Comparison -> Type -> TCM (MetaId, Term))
-> TCM (AppHead, Type)
inferMeta MetaInfo
i (InteractionId -> Comparison -> Type -> TCM (MetaId, Term)
newQuestionMark InteractionId
ii)
    A.Underscore MetaInfo
i      -> MetaInfo
-> (Comparison -> Type -> TCM (MetaId, Term))
-> TCM (AppHead, Type)
inferMeta MetaInfo
i (MetaInfo
-> RunMetaOccursCheck -> Comparison -> Type -> TCM (MetaId, Term)
newValueMetaOfKind MetaInfo
i RunMetaOccursCheck
RunMetaOccursCheck)

    Expr
e -> do
      (term, t) <- Expr -> TCM (Term, Type)
inferExpr Expr
e
      return (TermAppHd term, t)

inferDef :: (Args -> Term) -> QName -> TCM (Term, Type)
inferDef :: ([Arg Term] -> Term) -> QName -> TCM (Term, Type)
inferDef [Arg Term] -> Term
mkTerm QName
x =
  Call -> TCM (Term, Type) -> TCM (Term, Type)
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) -> TCM (Term, Type))
-> TCM (Term, Type) -> TCM (Term, Type)
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)
    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
defType Definition
d
            v = [Arg Term] -> Term
mkTerm [Arg Term]
vs -- applies x to vs, dropping parameters

        debug vs t v
        return (v, t)
  where
    debug :: Args -> Type -> Term -> TCM ()
    debug :: [Arg Term] -> Type -> Term -> TCMT IO ()
debug [Arg Term]
vs Type
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 -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type -> m Doc
prettyTCM Type
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 -> Expr -> [NamedArg Expr] -> TCM Term
checkHeadApplication Comparison
cmp Expr
e Type
t Expr
hd [NamedArg Expr]
args = do
  SortKit{ isNameOfUniv } <- TCMT IO SortKit
forall (m :: * -> *). (HasBuiltins m, MonadTCError m) => m SortKit
sortKit
  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
-> QName
-> Suffix
-> [NamedArg Expr]
-> TCM Term
checkUniv UnivSize
sz Univ
u Comparison
cmp Expr
e Type
t QName
c Suffix
s [NamedArg Expr]
args

    -- Cubical primitives
    Expr
_ -> do
      (f, t0) <- Expr -> TCM (AppHead, Type)
inferHead Expr
hd
      expandLast <- viewTC eExpandLast
      checkArguments cmp expandLast hd args t0 t $ \ st :: ArgsCheckState CheckedTarget
st@(ACState [CheckedArg]
cas Expr
_fun Type
t1 CheckedTarget
checkedTarget) -> do
        v <- 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
=<< AppHead -> ArgsCheckState CheckedTarget -> TCM Term
forall a. AppHead -> ArgsCheckState a -> TCM Term
applyCheckedArgs AppHead
f ArgsCheckState CheckedTarget
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 -> Type -> TCM Term
coerce' Comparison
cmp CheckedTarget
NotCheckedTarget           Term
v Type
inferred Type
expected = Comparison -> Term -> Type -> Type -> TCM Term
coerce Comparison
cmp Term
v Type
inferred Type
expected
coerce' Comparison
cmp (CheckedTarget Maybe ProblemId
Nothing)    Term
v Type
_        Type
_        = 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
_        Type
expected = Type -> Term -> ProblemId -> TCM Term
blockTermOnProblem Type
expected Term
v ProblemId
pid

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

checkArgumentsE ::
     Comparison
       -- ^ 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
-> [NamedArg Expr]
-> Type
-> Maybe Type
-> ExceptT
     (ArgsCheckState [NamedArg Expr])
     (TCMT IO)
     (ArgsCheckState CheckedTarget)
checkArgumentsE Comparison
cmp ExpandHidden
exph Expr
hd [NamedArg Expr]
args Type
t0 Maybe Type
t = do
  sPathView <- ExceptT
  (ArgsCheckState [NamedArg Expr]) (TCMT IO) (Type -> PathView)
forall (m :: * -> *). HasBuiltins m => m (Type -> 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
     , 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 -> [(NamedArg Expr, Bool)]
sArgs :: [(NamedArg A.Expr, Bool)]
    -- ^ Arguments, along with information about whether a given
    -- argument and all remaining arguments are 'visible'.
  , CheckArgumentsE'State -> Int
sArgsLen :: !Nat
    -- ^ The length of 'sArgs'.
  , CheckArgumentsE'State -> Type
sFunType :: Type
    -- ^ The function's type.
  , CheckArgumentsE'State -> Maybe Type
sResultType :: Maybe Type
    -- ^ The type of the application.
  , CheckArgumentsE'State -> SkipCheck
sSkipCheck :: !SkipCheck
    -- ^ Should the target type check be skipped?
  , CheckArgumentsE'State -> Type -> PathView
sPathView :: Type -> PathView
    -- ^ The function returned by 'pathView''.
  }

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

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

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 [NamedArg Expr])
     (TCMT IO)
     (ArgsCheckState CheckedTarget)
checkArgumentsE' S{ sArgs :: CheckArgumentsE'State -> [(NamedArg Expr, Bool)]
sArgs = [], Expr
sFun :: CheckArgumentsE'State -> Expr
sFun :: Expr
sFun, Type
sFunType :: CheckArgumentsE'State -> Type
sFunType :: Type
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 [NamedArg Expr])
     (TCMT IO)
     (ArgsCheckState CheckedTarget)
forall a. a -> ExceptT (ArgsCheckState [NamedArg Expr]) (TCMT IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return (ArgsCheckState CheckedTarget
 -> ExceptT
      (ArgsCheckState [NamedArg Expr])
      (TCMT IO)
      (ArgsCheckState CheckedTarget))
-> ArgsCheckState CheckedTarget
-> ExceptT
     (ArgsCheckState [NamedArg Expr])
     (TCMT IO)
     (ArgsCheckState CheckedTarget)
forall a b. (a -> b) -> a -> b
$ ACState
      { acCheckedArgs :: [CheckedArg]
acCheckedArgs = []
      , acFun :: Expr
acFun         = Expr
sFun
      , acType :: Type
acType        = Type
sFunType
      , acData :: CheckedTarget
acData        = CheckedTarget
sChecked
      }

-- Case: no arguments, but need to insert trailing hiddens.
checkArgumentsE' S{ sArgs :: CheckArgumentsE'State -> [(NamedArg Expr, Bool)]
sArgs = [], Expr
sFun :: CheckArgumentsE'State -> Expr
sFun :: Expr
sFun, Type
sFunType :: CheckArgumentsE'State -> Type
sFunType :: Type
sFunType, CheckedTarget
sChecked :: CheckArgumentsE'State -> CheckedTarget
sChecked :: CheckedTarget
sChecked, Maybe Type
sResultType :: CheckArgumentsE'State -> Maybe Type
sResultType :: Maybe Type
sResultType } =
  Call
-> ExceptT
     (ArgsCheckState [NamedArg Expr])
     (TCMT IO)
     (ArgsCheckState CheckedTarget)
-> ExceptT
     (ArgsCheckState [NamedArg Expr])
     (TCMT IO)
     (ArgsCheckState CheckedTarget)
forall e r. Call -> ExceptT e (TCMT IO) r -> ExceptT e (TCMT IO) r
traceCallE (Expr -> [NamedArg Expr] -> Type -> Maybe Type -> Call
CheckArguments Expr
sFun [] Type
sFunType Maybe Type
sResultType) (ExceptT
   (ArgsCheckState [NamedArg Expr])
   (TCMT IO)
   (ArgsCheckState CheckedTarget)
 -> ExceptT
      (ArgsCheckState [NamedArg Expr])
      (TCMT IO)
      (ArgsCheckState CheckedTarget))
-> ExceptT
     (ArgsCheckState [NamedArg Expr])
     (TCMT IO)
     (ArgsCheckState CheckedTarget)
-> ExceptT
     (ArgsCheckState [NamedArg Expr])
     (TCMT IO)
     (ArgsCheckState CheckedTarget)
forall a b. (a -> b) -> a -> b
$ TCM (ArgsCheckState CheckedTarget)
-> ExceptT
     (ArgsCheckState [NamedArg Expr])
     (TCMT IO)
     (ArgsCheckState CheckedTarget)
forall (m :: * -> *) a.
Monad m =>
m a -> ExceptT (ArgsCheckState [NamedArg Expr]) m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TCM (ArgsCheckState CheckedTarget)
 -> ExceptT
      (ArgsCheckState [NamedArg Expr])
      (TCMT IO)
      (ArgsCheckState CheckedTarget))
-> TCM (ArgsCheckState CheckedTarget)
-> ExceptT
     (ArgsCheckState [NamedArg Expr])
     (TCMT IO)
     (ArgsCheckState CheckedTarget)
forall a b. (a -> b) -> a -> b
$ do
    sResultType <- (Type -> TCM Term) -> Maybe Type -> 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
forall t a. Type'' t a -> a
unEl (Type -> Term) -> (Type -> TCMT IO Type) -> Type -> TCM Term
forall (m :: * -> *) b c a.
Functor m =>
(b -> c) -> (a -> m b) -> a -> m c
<.> Type -> TCMT IO Type
forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce) Maybe Type
sResultType
    (ncargs, t) <- implicitCheckedArgs (-1) (\ Hiding
h ArgName
_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 Type
dom Abs Type
_)) Hiding
Hidden     = Bool -> Bool
not (Dom Type -> Bool
forall a. LensHiding a => a -> Bool
hidden Dom Type
dom)
  expand Maybe Term
_                 Hiding
Hidden     = Bool
True
  expand (Just (Pi Dom Type
dom Abs Type
_)) Instance{} = Bool -> Bool
not (Dom Type -> Bool
forall a. LensHiding a => a -> Bool
isInstance Dom Type
dom)
  expand Maybe Term
_                 Instance{} = Bool
True
  expand Maybe Term
_                 Hiding
NotHidden  = Bool
False

-- Case: argument given.
checkArgumentsE'
  s :: CheckArgumentsE'State
s@S{ sArgs :: CheckArgumentsE'State -> [(NamedArg Expr, Bool)]
sArgs = sArgs :: [(NamedArg Expr, Bool)]
sArgs@((arg :: NamedArg Expr
arg@(Arg ArgInfo
info Named_ Expr
e), Bool
sArgsVisible) : [(NamedArg Expr, Bool)]
args), 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
sFunType :: CheckArgumentsE'State -> Type
sFunType :: Type
sFunType, Type -> PathView
sPathView :: CheckArgumentsE'State -> Type -> PathView
sPathView :: Type -> PathView
sPathView, Maybe Type
sResultType :: CheckArgumentsE'State -> Maybe Type
sResultType :: Maybe Type
sResultType, SkipCheck
sSkipCheck :: CheckArgumentsE'State -> SkipCheck
sSkipCheck :: SkipCheck
sSkipCheck } =

    Call
-> ExceptT
     (ArgsCheckState [NamedArg Expr])
     (TCMT IO)
     (ArgsCheckState CheckedTarget)
-> ExceptT
     (ArgsCheckState [NamedArg Expr])
     (TCMT IO)
     (ArgsCheckState CheckedTarget)
forall e r. Call -> ExceptT e (TCMT IO) r -> ExceptT e (TCMT IO) r
traceCallE (Expr -> [NamedArg Expr] -> Type -> Maybe Type -> Call
CheckArguments Expr
sFun (((NamedArg Expr, Bool) -> NamedArg Expr)
-> [(NamedArg Expr, Bool)] -> [NamedArg Expr]
forall a b. (a -> b) -> [a] -> [b]
map' (NamedArg Expr, Bool) -> NamedArg Expr
forall a b. (a, b) -> a
fst [(NamedArg Expr, Bool)]
sArgs) Type
sFunType Maybe Type
sResultType) (ExceptT
   (ArgsCheckState [NamedArg Expr])
   (TCMT IO)
   (ArgsCheckState CheckedTarget)
 -> ExceptT
      (ArgsCheckState [NamedArg Expr])
      (TCMT IO)
      (ArgsCheckState CheckedTarget))
-> ExceptT
     (ArgsCheckState [NamedArg Expr])
     (TCMT IO)
     (ArgsCheckState CheckedTarget)
-> ExceptT
     (ArgsCheckState [NamedArg Expr])
     (TCMT IO)
     (ArgsCheckState CheckedTarget)
forall a b. (a -> b) -> a -> b
$ do
      TCMT IO () -> ExceptT (ArgsCheckState [NamedArg Expr]) (TCMT IO) ()
forall (m :: * -> *) a.
Monad m =>
m a -> ExceptT (ArgsCheckState [NamedArg Expr]) m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TCMT IO ()
 -> ExceptT (ArgsCheckState [NamedArg Expr]) (TCMT IO) ())
-> TCMT IO ()
-> ExceptT (ArgsCheckState [NamedArg 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 -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type -> m Doc
prettyTCM Type
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 -> TCMT IO Doc) -> Maybe Type -> TCMT IO Doc
forall b a. b -> (a -> b) -> Maybe a -> b
maybe TCMT IO Doc
"Nothing" Type -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type -> m Doc
prettyTCM Maybe Type
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 ArgName
mx = Named_ Expr -> Maybe ArgName
forall a. (LensNamed a, NameOf a ~ NamedName) => a -> Maybe ArgName
bareNameOf Named_ Expr
e    -- name of current argument
          -- do not insert visible arguments
          expand :: Hiding -> ArgName -> Bool
expand Hiding
NotHidden ArgName
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        ArgName
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 -> (ArgName -> Bool) -> Maybe ArgName -> Bool
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
False (ArgName
y ArgName -> ArgName -> Bool
forall a. Eq a => a -> a -> Bool
/=) Maybe ArgName
mx
      [Char]
-> Int
-> TCMT IO Doc
-> ExceptT (ArgsCheckState [NamedArg 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 [NamedArg Expr]) (TCMT IO) ())
-> TCMT IO Doc
-> ExceptT (ArgsCheckState [NamedArg 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
-> (ArgName -> TCMT IO Doc) -> Maybe ArgName -> TCMT IO Doc
forall b a. b -> (a -> b) -> Maybe a -> b
maybe TCMT IO Doc
"nothing" ArgName -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => ArgName -> m Doc
prettyTCM Maybe ArgName
mx
        ]
      (ncargs, sFunType) <- TCM ([Named_ CheckedArg], Type)
-> ExceptT
     (ArgsCheckState [NamedArg Expr])
     (TCMT IO)
     ([Named_ CheckedArg], Type)
forall (m :: * -> *) a.
Monad m =>
m a -> ExceptT (ArgsCheckState [NamedArg Expr]) m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TCM ([Named_ CheckedArg], Type)
 -> ExceptT
      (ArgsCheckState [NamedArg Expr])
      (TCMT IO)
      ([Named_ CheckedArg], Type))
-> TCM ([Named_ CheckedArg], Type)
-> ExceptT
     (ArgsCheckState [NamedArg Expr])
     (TCMT IO)
     ([Named_ CheckedArg], Type)
forall a b. (a -> b) -> a -> b
$ Int
-> (Hiding -> ArgName -> Bool)
-> Type
-> TCM ([Named_ CheckedArg], Type)
implicitCheckedArgs (-Int
1) Hiding -> ArgName -> Bool
expand Type
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 (typeError $ CannotApply sFun sFunType) sFunType

      -- We are done inserting implicit args.  Now, try to check @arg@.
      ifBlocked sFunType
        (\ Blocker
_ Type
sFunType -> ArgsCheckState [NamedArg Expr]
-> ExceptT
     (ArgsCheckState [NamedArg Expr])
     (TCMT IO)
     (ArgsCheckState CheckedTarget)
forall a.
ArgsCheckState [NamedArg Expr]
-> ExceptT (ArgsCheckState [NamedArg Expr]) (TCMT IO) a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (ArgsCheckState [NamedArg Expr]
 -> ExceptT
      (ArgsCheckState [NamedArg Expr])
      (TCMT IO)
      (ArgsCheckState CheckedTarget))
-> ArgsCheckState [NamedArg Expr]
-> ExceptT
     (ArgsCheckState [NamedArg 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
acType        = Type
sFunType
            , acData :: [NamedArg Expr]
acData        = ((NamedArg Expr, Bool) -> NamedArg Expr)
-> [(NamedArg Expr, Bool)] -> [NamedArg Expr]
forall a b. (a -> b) -> [a] -> [b]
map' (NamedArg Expr, Bool) -> NamedArg Expr
forall a b. (a, b) -> a
fst [(NamedArg Expr, Bool)]
sArgs
            }) {- else -} $ \ NotBlocked
_ Type
sFunType -> do

        -- What can go wrong?

        -- 1. We ran out of function types.
        let shouldBePi :: ExceptT
  (ArgsCheckState [NamedArg Expr])
  (TCMT IO)
  (ArgsCheckState CheckedTarget)
shouldBePi =
              -- a) It is an explicit argument, but we ran out of function types.
              if ArgInfo -> Bool
forall a. LensHiding a => a -> Bool
visible ArgInfo
info then TCM (ArgsCheckState CheckedTarget)
-> ExceptT
     (ArgsCheckState [NamedArg Expr])
     (TCMT IO)
     (ArgsCheckState CheckedTarget)
forall a.
TCM a -> ExceptT (ArgsCheckState [NamedArg Expr]) (TCMT IO) a
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCM (ArgsCheckState CheckedTarget)
 -> ExceptT
      (ArgsCheckState [NamedArg Expr])
      (TCMT IO)
      (ArgsCheckState CheckedTarget))
-> (TypeError -> TCM (ArgsCheckState CheckedTarget))
-> TypeError
-> ExceptT
     (ArgsCheckState [NamedArg Expr])
     (TCMT IO)
     (ArgsCheckState CheckedTarget)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypeError -> TCM (ArgsCheckState CheckedTarget)
forall (m :: * -> *) e a.
(HasCallStack, MonadTCError m, Diagnostic e) =>
e -> m a
typeError (TypeError
 -> ExceptT
      (ArgsCheckState [NamedArg Expr])
      (TCMT IO)
      (ArgsCheckState CheckedTarget))
-> TypeError
-> ExceptT
     (ArgsCheckState [NamedArg Expr])
     (TCMT IO)
     (ArgsCheckState CheckedTarget)
forall a b. (a -> b) -> a -> b
$ Expr -> Type -> TypeError
CannotApply Expr
sFun Type
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 [NamedArg Expr])
     (TCMT IO)
     (ArgsCheckState CheckedTarget)
-> (List1 NamedName
    -> ExceptT
         (ArgsCheckState [NamedArg Expr])
         (TCMT IO)
         (ArgsCheckState CheckedTarget))
-> ExceptT
     (ArgsCheckState [NamedArg Expr])
     (TCMT IO)
     (ArgsCheckState CheckedTarget)
forall a b. [a] -> b -> (List1 a -> b) -> b
List1.ifNull [NamedName]
xs {-then-} (TCM (ArgsCheckState CheckedTarget)
-> ExceptT
     (ArgsCheckState [NamedArg Expr])
     (TCMT IO)
     (ArgsCheckState CheckedTarget)
forall a.
TCM a -> ExceptT (ArgsCheckState [NamedArg Expr]) (TCMT IO) a
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCM (ArgsCheckState CheckedTarget)
 -> ExceptT
      (ArgsCheckState [NamedArg Expr])
      (TCMT IO)
      (ArgsCheckState CheckedTarget))
-> (TypeError -> TCM (ArgsCheckState CheckedTarget))
-> TypeError
-> ExceptT
     (ArgsCheckState [NamedArg Expr])
     (TCMT IO)
     (ArgsCheckState CheckedTarget)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypeError -> TCM (ArgsCheckState CheckedTarget)
forall (m :: * -> *) e a.
(HasCallStack, MonadTCError m, Diagnostic e) =>
e -> m a
typeError (TypeError
 -> ExceptT
      (ArgsCheckState [NamedArg Expr])
      (TCMT IO)
      (ArgsCheckState CheckedTarget))
-> TypeError
-> ExceptT
     (ArgsCheckState [NamedArg Expr])
     (TCMT IO)
     (ArgsCheckState CheckedTarget)
forall a b. (a -> b) -> a -> b
$ Expr -> Type -> TypeError
CannotApply Expr
sFun Type
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-} (TCM (ArgsCheckState CheckedTarget)
-> ExceptT
     (ArgsCheckState [NamedArg Expr])
     (TCMT IO)
     (ArgsCheckState CheckedTarget)
forall a.
TCM a -> ExceptT (ArgsCheckState [NamedArg Expr]) (TCMT IO) a
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCM (ArgsCheckState CheckedTarget)
 -> ExceptT
      (ArgsCheckState [NamedArg Expr])
      (TCMT IO)
      (ArgsCheckState CheckedTarget))
-> (List1 NamedName -> TCM (ArgsCheckState CheckedTarget))
-> List1 NamedName
-> ExceptT
     (ArgsCheckState [NamedArg Expr])
     (TCMT IO)
     (ArgsCheckState CheckedTarget)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypeError -> TCM (ArgsCheckState CheckedTarget)
forall (m :: * -> *) e a.
(HasCallStack, MonadTCError m, Diagnostic e) =>
e -> m a
typeError (TypeError -> TCM (ArgsCheckState CheckedTarget))
-> (List1 NamedName -> TypeError)
-> List1 NamedName
-> TCM (ArgsCheckState CheckedTarget)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NamedArg Expr -> List1 NamedName -> TypeError
WrongNamedArgument NamedArg 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 [NamedArg Expr])
  (TCMT IO)
  (ArgsCheckState CheckedTarget)
wrongPi = [NamedName]
-> ExceptT
     (ArgsCheckState [NamedArg Expr])
     (TCMT IO)
     (ArgsCheckState CheckedTarget)
-> (List1 NamedName
    -> ExceptT
         (ArgsCheckState [NamedArg Expr])
         (TCMT IO)
         (ArgsCheckState CheckedTarget))
-> ExceptT
     (ArgsCheckState [NamedArg 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-} (TCM (ArgsCheckState CheckedTarget)
-> ExceptT
     (ArgsCheckState [NamedArg Expr])
     (TCMT IO)
     (ArgsCheckState CheckedTarget)
forall a.
TCM a -> ExceptT (ArgsCheckState [NamedArg Expr]) (TCMT IO) a
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCM (ArgsCheckState CheckedTarget)
 -> ExceptT
      (ArgsCheckState [NamedArg Expr])
      (TCMT IO)
      (ArgsCheckState CheckedTarget))
-> (TypeError -> TCM (ArgsCheckState CheckedTarget))
-> TypeError
-> ExceptT
     (ArgsCheckState [NamedArg Expr])
     (TCMT IO)
     (ArgsCheckState CheckedTarget)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypeError -> TCM (ArgsCheckState CheckedTarget)
forall (m :: * -> *) e a.
(HasCallStack, MonadTCError m, Diagnostic e) =>
e -> m a
typeError (TypeError
 -> ExceptT
      (ArgsCheckState [NamedArg Expr])
      (TCMT IO)
      (ArgsCheckState CheckedTarget))
-> TypeError
-> ExceptT
     (ArgsCheckState [NamedArg Expr])
     (TCMT IO)
     (ArgsCheckState CheckedTarget)
forall a b. (a -> b) -> a -> b
$ Hiding -> Type -> TypeError
WrongHidingInApplication Hiding
hx Type
sFunType)
              -- c) We inserted implicits, but did not find his one.
                {-else-} (TCM (ArgsCheckState CheckedTarget)
-> ExceptT
     (ArgsCheckState [NamedArg Expr])
     (TCMT IO)
     (ArgsCheckState CheckedTarget)
forall a.
TCM a -> ExceptT (ArgsCheckState [NamedArg Expr]) (TCMT IO) a
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCM (ArgsCheckState CheckedTarget)
 -> ExceptT
      (ArgsCheckState [NamedArg Expr])
      (TCMT IO)
      (ArgsCheckState CheckedTarget))
-> (List1 NamedName -> TCM (ArgsCheckState CheckedTarget))
-> List1 NamedName
-> ExceptT
     (ArgsCheckState [NamedArg Expr])
     (TCMT IO)
     (ArgsCheckState CheckedTarget)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypeError -> TCM (ArgsCheckState CheckedTarget)
forall (m :: * -> *) e a.
(HasCallStack, MonadTCError m, Diagnostic e) =>
e -> m a
typeError (TypeError -> TCM (ArgsCheckState CheckedTarget))
-> (List1 NamedName -> TypeError)
-> List1 NamedName
-> TCM (ArgsCheckState CheckedTarget)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NamedArg Expr -> List1 NamedName -> TypeError
WrongNamedArgument NamedArg 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 [NamedArg Expr]) (TCMT IO) CheckArgumentsE'State
forall a. a -> ExceptT (ArgsCheckState [NamedArg 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
sResultType) | Bool
sArgsVisible -> do
              -- How many visible Π's (up to at most sArgsLen) does
              -- sFunType start with?
              TelV tel tgt <- Int -> (Dom Type -> Bool) -> Type -> TCMT IO (TelV Type)
forall (m :: * -> *).
(MonadReduce m, MonadAddContext m) =>
Int -> (Dom Type -> Bool) -> Type -> m (TelV Type)
telViewUpTo' Int
sArgsLen Dom Type -> Bool
forall a. LensHiding a => a -> Bool
visible Type
sFunType
              let visiblePis = Tele (Dom Type) -> Int
forall a. Sized a => a -> Int
size Tele (Dom Type)
tel

                  -- The free variables less than visiblePis in tgt.
                  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 -> VarSet
forall t. Free t => t -> VarSet
freeVarSet Type
tgt

              rigid <- isRigid s 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

                  let tgt1 :: Type
tgt1 = Substitution' (SubstArg Type) -> Type -> Type
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
tgt
                  [Char] -> Int -> TCMT IO Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.term.args.target" 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
vcat
                    [ TCMT IO Doc
"Checking target types first"
                    , 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
"inferred =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Type -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type -> m Doc
prettyTCM Type
tgt1
                    , 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
"expected =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Type -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type -> m Doc
prettyTCM Type
sResultType ]
                  chk <-
                    Call -> TCMT IO CheckedTarget -> TCMT IO CheckedTarget
forall a. Call -> TCMT IO a -> TCMT IO a
forall (m :: * -> *) a. MonadTrace m => Call -> m a -> m a
traceCall
                      (Range -> Type -> Type -> Call
CheckTargetType
                        (Expr -> [(NamedArg Expr, Bool)] -> Range
forall u t. (HasRange u, HasRange t) => u -> t -> Range
fuseRange Expr
sFun [(NamedArg Expr, Bool)]
sArgs) Type
tgt1 Type
sResultType) (TCMT IO CheckedTarget -> TCMT IO CheckedTarget)
-> TCMT IO CheckedTarget -> TCMT IO CheckedTarget
forall a b. (a -> b) -> a -> b
$
                      Maybe ProblemId -> CheckedTarget
CheckedTarget (Maybe ProblemId -> CheckedTarget)
-> TCMT IO (Maybe ProblemId) -> TCMT IO CheckedTarget
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
                        TCMT IO ()
-> TCMT IO (Maybe ProblemId)
-> (ProblemId -> TCMT IO (Maybe ProblemId))
-> TCMT IO (Maybe ProblemId)
forall a. TCMT IO () -> TCM a -> (ProblemId -> TCM a) -> TCM a
ifNoConstraints_ (Comparison -> Type -> Type -> TCMT IO ()
compareType Comparison
sComp Type
tgt1 Type
sResultType)
                          (Maybe ProblemId -> TCMT IO (Maybe ProblemId)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe ProblemId
forall a. Maybe a
Nothing) (Maybe ProblemId -> TCMT IO (Maybe ProblemId)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe ProblemId -> TCMT IO (Maybe ProblemId))
-> (ProblemId -> Maybe ProblemId)
-> ProblemId
-> TCMT IO (Maybe ProblemId)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ProblemId -> Maybe ProblemId
forall a. a -> Maybe a
Just)
                  return s{ sChecked = chk }

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

        case unEl sFunType of
          Pi dom :: Dom Type
dom@(Dom Type -> Type
forall t e. Dom' t e -> e
unDom -> Type
a) Abs Type
b
            | let info' :: ArgInfo
info' = Dom Type
dom Dom Type -> Getting ArgInfo (Dom Type) ArgInfo -> ArgInfo
forall s a. s -> Getting a s a -> a
^. Getting ArgInfo (Dom Type) ArgInfo
forall t e (f :: * -> *).
Functor f =>
(ArgInfo -> f ArgInfo) -> Dom' t e -> f (Dom' t e)
dInfo,
              let dname :: Maybe (NameOf (Dom Type))
dname = Dom Type -> Maybe (NameOf (Dom Type))
forall a. LensNamed a => a -> Maybe (NameOf a)
getNameOf Dom Type
dom,
              let name :: ArgName
name  = ArgName -> Maybe NamedName -> ArgName
forall a.
(LensNamed a, NameOf a ~ NamedName) =>
ArgName -> a -> ArgName
bareNameWithDefault ArgName
"_" Maybe (NameOf (Dom Type))
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 -> (ArgName -> Bool) -> Maybe ArgName -> Bool
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
True (ArgName
name ArgName -> ArgName -> Bool
forall a. Eq a => a -> a -> Bool
==) Maybe ArgName
mx) -> do
                u <- TCM Term -> ExceptT (ArgsCheckState [NamedArg Expr]) (TCMT IO) Term
forall (m :: * -> *) a.
Monad m =>
m a -> ExceptT (ArgsCheckState [NamedArg Expr]) m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TCM Term
 -> ExceptT (ArgsCheckState [NamedArg Expr]) (TCMT IO) Term)
-> TCM Term
-> ExceptT (ArgsCheckState [NamedArg Expr]) (TCMT IO) 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 }
                  NamedArg Expr -> Type -> TCM Term
checkNamedArg (ArgInfo -> Named_ Expr -> NamedArg Expr
forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
info' Named_ Expr
e') Type
a

                -- save info' from domain in argument
                let ca = CheckedArg{ caElim :: Elim
caElim = Arg Term -> Elim
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 }
                addCheckedArgs cargs ca $
                  checkArgumentsE' s{ sFunType = absApp b u }
            | Bool
otherwise -> do
                let info' :: ArgInfo
info' = Dom Type
dom Dom Type -> Getting ArgInfo (Dom Type) ArgInfo -> ArgInfo
forall s a. s -> Getting a s a -> a
^. Getting ArgInfo (Dom Type) 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 [NamedArg Expr]) (TCMT IO) ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"error" Int
10 (TCMT IO Doc
 -> ExceptT (ArgsCheckState [NamedArg Expr]) (TCMT IO) ())
-> TCMT IO Doc
-> ExceptT (ArgsCheckState [NamedArg 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]
++! ArgName -> [Char]
TS.unpack (Abs Type -> ArgName
forall a. Abs a -> ArgName
absName Abs Type
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 [NamedArg 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 -> PathView
sPathView Type
sFunType -> do
                TCMT IO () -> ExceptT (ArgsCheckState [NamedArg Expr]) (TCMT IO) ()
forall (m :: * -> *) a.
Monad m =>
m a -> ExceptT (ArgsCheckState [NamedArg Expr]) m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TCMT IO ()
 -> ExceptT (ArgsCheckState [NamedArg Expr]) (TCMT IO) ())
-> TCMT IO ()
-> ExceptT (ArgsCheckState [NamedArg 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 [NamedArg Expr]) (TCMT IO) Term
forall (m :: * -> *) a.
Monad m =>
m a -> ExceptT (ArgsCheckState [NamedArg Expr]) m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TCM Term
 -> ExceptT (ArgsCheckState [NamedArg Expr]) (TCMT IO) Term)
-> TCM Term
-> ExceptT (ArgsCheckState [NamedArg Expr]) (TCMT IO) Term
forall a b. (a -> b) -> a -> b
$ Expr -> Type -> TCM Term
checkExpr (Named_ Expr -> Expr
forall name a. Named name a -> a
namedThing Named_ Expr
e) (Type -> TCM Term) -> TCMT IO Type -> TCM Term
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< TCMT IO Type
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Type
primIntervalType
                let ca = CheckedArg
                     { caElim :: Elim
caElim       = Term -> Term -> Term -> Elim
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
                     }
                addCheckedArgs cargs ca $
                  checkArgumentsE'
                    s{ sChecked = NotCheckedTarget
                     , sFunType = El sort $ unArg bA `apply` [argN u]
                     }
          Term
_ -> ExceptT
  (ArgsCheckState [NamedArg Expr])
  (TCMT IO)
  (ArgsCheckState CheckedTarget)
shouldBePi
  where
    addCheckedArgs ::
         [CheckedArg]
      -> CheckedArg
      -> CheckArgumentsE'
      -> CheckArgumentsE'
    addCheckedArgs :: [CheckedArg]
-> CheckedArg
-> ExceptT
     (ArgsCheckState [NamedArg Expr])
     (TCMT IO)
     (ArgsCheckState CheckedTarget)
-> ExceptT
     (ArgsCheckState [NamedArg Expr])
     (TCMT IO)
     (ArgsCheckState CheckedTarget)
addCheckedArgs [CheckedArg]
cas CheckedArg
ca ExceptT
  (ArgsCheckState [NamedArg 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 [NamedArg Expr] -> ArgsCheckState [NamedArg Expr])
-> ExceptT
     (ArgsCheckState [NamedArg Expr])
     (TCMT IO)
     (ArgsCheckState CheckedTarget)
-> ExceptT
     (ArgsCheckState [NamedArg Expr])
     (TCMT IO)
     (ArgsCheckState CheckedTarget)
forall e (m :: * -> *) a. MonadError e m => (e -> e) -> m a -> m a
withError ArgsCheckState [NamedArg Expr] -> ArgsCheckState [NamedArg Expr]
forall a. ArgsCheckState a -> ArgsCheckState a
upd (ExceptT
   (ArgsCheckState [NamedArg Expr])
   (TCMT IO)
   (ArgsCheckState CheckedTarget)
 -> ExceptT
      (ArgsCheckState [NamedArg Expr])
      (TCMT IO)
      (ArgsCheckState CheckedTarget))
-> ExceptT
     (ArgsCheckState [NamedArg Expr])
     (TCMT IO)
     (ArgsCheckState CheckedTarget)
-> ExceptT
     (ArgsCheckState [NamedArg 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 [NamedArg Expr])
     (TCMT IO)
     (ArgsCheckState CheckedTarget)
-> ExceptT
     (ArgsCheckState [NamedArg Expr])
     (TCMT IO)
     (ArgsCheckState CheckedTarget)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ExceptT
  (ArgsCheckState [NamedArg 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 -> TCM IsRigid
isRigid CheckArgumentsE'State
s Type
t | PathType{} <- CheckArgumentsE'State -> Type -> PathView
sPathView CheckArgumentsE'State
s Type
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 Elims
_    -> 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 Type
dom Abs Type
_   -> 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 Type -> Bool
forall a. LensHiding a => a -> Bool
visible Dom Type
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 Elims
_    -> 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
-> [NamedArg Expr]
-> Tele (Dom Type)
-> TCMT IO (Elims, Tele (Dom Type))
checkArguments_ Comparison
cmp ExpandHidden
exh Expr
fun [NamedArg Expr]
args Tele (Dom Type)
tel = TCMT IO (Elims, Tele (Dom Type))
-> TCMT IO (Elims, Tele (Dom Type))
forall a. TCM a -> TCM a
postponeInstanceConstraints (TCMT IO (Elims, Tele (Dom Type))
 -> TCMT IO (Elims, Tele (Dom Type)))
-> TCMT IO (Elims, Tele (Dom Type))
-> TCMT IO (Elims, Tele (Dom Type))
forall a b. (a -> b) -> a -> b
$ do
    z <- ExceptT
  (ArgsCheckState [NamedArg Expr])
  (TCMT IO)
  (ArgsCheckState CheckedTarget)
-> TCM
     (Either
        (ArgsCheckState [NamedArg Expr]) (ArgsCheckState CheckedTarget))
forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
runExceptT (ExceptT
   (ArgsCheckState [NamedArg Expr])
   (TCMT IO)
   (ArgsCheckState CheckedTarget)
 -> TCM
      (Either
         (ArgsCheckState [NamedArg Expr]) (ArgsCheckState CheckedTarget)))
-> ExceptT
     (ArgsCheckState [NamedArg Expr])
     (TCMT IO)
     (ArgsCheckState CheckedTarget)
-> TCM
     (Either
        (ArgsCheckState [NamedArg Expr]) (ArgsCheckState CheckedTarget))
forall a b. (a -> b) -> a -> b
$
      Comparison
-> ExpandHidden
-> Expr
-> [NamedArg Expr]
-> Type
-> Maybe Type
-> ExceptT
     (ArgsCheckState [NamedArg Expr])
     (TCMT IO)
     (ArgsCheckState CheckedTarget)
checkArgumentsE Comparison
cmp ExpandHidden
exh Expr
fun [NamedArg Expr]
args (Tele (Dom Type) -> Type -> Type
telePi Tele (Dom Type)
tel Type
HasCallStack => Type
__DUMMY_TYPE__) Maybe Type
forall a. Maybe a
Nothing
    case z of
      Right (ACState [CheckedArg]
cas Expr
_ Type
t CheckedTarget
_) -> do
        let es :: Elims
es = (CheckedArg -> Elim) -> [CheckedArg] -> Elims
forall a b. (a -> b) -> [a] -> [b]
map' CheckedArg -> Elim
caElim [CheckedArg]
cas
        let TelV Tele (Dom Type)
tel' Type
_ = Type -> TelV Type
telView' Type
t
        (Elims, Tele (Dom Type)) -> TCMT IO (Elims, Tele (Dom Type))
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Elims
es, Tele (Dom Type)
tel')
      Left ArgsCheckState [NamedArg Expr]
_ -> TCMT IO (Elims, Tele (Dom Type))
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
-> [NamedArg Expr]
-> Type
-> Type
-> (ArgsCheckState CheckedTarget -> TCM Term)
-> TCM Term
checkArguments Comparison
cmp ExpandHidden
exph Expr
hd [NamedArg Expr]
args Type
t0 Type
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 [NamedArg Expr])
  (TCMT IO)
  (ArgsCheckState CheckedTarget)
-> TCM
     (Either
        (ArgsCheckState [NamedArg Expr]) (ArgsCheckState CheckedTarget))
forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
runExceptT (ExceptT
   (ArgsCheckState [NamedArg Expr])
   (TCMT IO)
   (ArgsCheckState CheckedTarget)
 -> TCM
      (Either
         (ArgsCheckState [NamedArg Expr]) (ArgsCheckState CheckedTarget)))
-> ExceptT
     (ArgsCheckState [NamedArg Expr])
     (TCMT IO)
     (ArgsCheckState CheckedTarget)
-> TCM
     (Either
        (ArgsCheckState [NamedArg Expr]) (ArgsCheckState CheckedTarget))
forall a b. (a -> b) -> a -> b
$ Comparison
-> ExpandHidden
-> Expr
-> [NamedArg Expr]
-> Type
-> Maybe Type
-> ExceptT
     (ArgsCheckState [NamedArg Expr])
     (TCMT IO)
     (ArgsCheckState CheckedTarget)
checkArgumentsE Comparison
cmp ExpandHidden
exph Expr
hd [NamedArg Expr]
args Type
t0 (Type -> Maybe Type
forall a. a -> Maybe a
Just Type
t)
  case z of
    Right ArgsCheckState CheckedTarget
st -> ArgsCheckState CheckedTarget -> TCM Term
k ArgsCheckState CheckedTarget
st
    Left ArgsCheckState [NamedArg Expr]
problem -> ArgsCheckState [NamedArg Expr]
-> Comparison
-> ExpandHidden
-> Expr
-> [NamedArg Expr]
-> Type
-> Type
-> (ArgsCheckState CheckedTarget -> TCM Term)
-> TCM Term
postponeArgs ArgsCheckState [NamedArg Expr]
problem Comparison
cmp ExpandHidden
exph Expr
hd [NamedArg Expr]
args Type
t0 Type
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 [NamedArg Expr]
-> Comparison
-> ExpandHidden
-> Expr
-> [NamedArg Expr]
-> Type
-> Type
-> (ArgsCheckState CheckedTarget -> TCM Term)
-> TCM Term
postponeArgs (ACState [CheckedArg]
cas Expr
fun Type
t1 [NamedArg Expr]
es) Comparison
cmp ExpandHidden
exph Expr
hd [NamedArg Expr]
args Type
t0 Type
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 ((NamedArg Expr -> TCMT IO Doc) -> [NamedArg 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)
-> (NamedArg Expr -> Expr) -> NamedArg 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)
-> (NamedArg Expr -> Named_ Expr) -> NamedArg Expr -> Expr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NamedArg Expr -> Named_ Expr
forall e. Arg e -> e
unArg) [NamedArg 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 -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type -> m Doc
prettyTCM Type
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 -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Elim -> m Doc
prettyTCM (Elim -> TCMT IO Doc)
-> (CheckedArg -> Elim) -> CheckedArg -> TCMT IO Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CheckedArg -> Elim
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 ((NamedArg Expr -> TCMT IO Doc) -> [NamedArg 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)
-> (NamedArg Expr -> Expr) -> NamedArg 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)
-> (NamedArg Expr -> Named_ Expr) -> NamedArg Expr -> Expr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NamedArg Expr -> Named_ Expr
forall e. Arg e -> e
unArg) [NamedArg 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 -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type -> m Doc
prettyTCM Type
t1
            ]
        ]
  TypeCheckingProblem -> TCM Term
postponeTypeCheckingProblem_ (TypeCheckingProblem -> TCM Term)
-> TypeCheckingProblem -> TCM Term
forall a b. (a -> b) -> a -> b
$
    Comparison
-> ExpandHidden
-> Expr
-> [NamedArg Expr]
-> Type
-> Type
-> (ArgsCheckState CheckedTarget -> TCM Term)
-> TypeCheckingProblem
CheckArgs Comparison
cmp ExpandHidden
exph Expr
fun [NamedArg Expr]
es Type
t1 Type
t ((ArgsCheckState CheckedTarget -> TCM Term) -> TypeCheckingProblem)
-> (ArgsCheckState CheckedTarget -> TCM Term)
-> TypeCheckingProblem
forall a b. (a -> b) -> a -> b
$ \ (ACState [CheckedArg]
cas' Expr
func Type
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 -> CheckedTarget -> ArgsCheckState CheckedTarget
forall a. [CheckedArg] -> Expr -> Type -> a -> ArgsCheckState a
ACState ([CheckedArg]
cas [CheckedArg] -> [CheckedArg] -> [CheckedArg]
forall a. [a] -> [a] -> [a]
++! [CheckedArg]
cas') Expr
func Type
t CheckedTarget
pid

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

-- | Check the type of a constructor application. This is easier than
--   a general application since the implicit arguments can be inserted
--   without looking at the arguments to the constructor.
checkConstructorApplication ::
  Comparison
       -- ^ 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 -> ConHead -> Expr -> [NamedArg Expr] -> TCM Term
checkConstructorApplication Comparison
cmp Expr
org Type
t ConHead
c Expr
hd [NamedArg 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 -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type -> m Doc
prettyTCM Type
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
$ (NamedArg Expr -> TCMT IO Doc) -> [NamedArg Expr] -> [TCMT IO Doc]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap NamedArg Expr -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => NamedArg Expr -> m Doc
prettyTCM [NamedArg Expr]
args
    ] ]

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

  let paramsGiven = [NamedArg Expr] -> Bool
checkForParams [NamedArg 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 Elims
_, Def QName
d' Elims
es) -> do
        let ~(Just [Arg Term]
vs) = Elims -> Maybe [Arg Term]
forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims Elims
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
ctype = Definition -> Type
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 -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type -> m Doc
prettyTCM Type
ctype ] ]
           let ctype' :: Type
ctype' = Type
ctype Type -> [Arg Term] -> Type
`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 -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type -> m Doc
prettyTCM Type
ctype'
           -- get the parameter names
           let TelV Tele (Dom Type)
ptel Type
_ = Int -> Type -> TelV Type
telView'UpTo Int
n Type
ctype
           let pnames :: [Dom' Term ArgName]
pnames = (Dom' Term (ArgName, Type) -> Dom' Term ArgName)
-> [Dom' Term (ArgName, Type)] -> [Dom' Term ArgName]
forall a b. (a -> b) -> [a] -> [b]
map' (((ArgName, Type) -> ArgName)
-> Dom' Term (ArgName, Type) -> Dom' Term ArgName
forall a b. (a -> b) -> Dom' Term a -> Dom' Term b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (ArgName, Type) -> ArgName
forall a b. (a, b) -> a
fst) ([Dom' Term (ArgName, Type)] -> [Dom' Term ArgName])
-> [Dom' Term (ArgName, Type)] -> [Dom' Term ArgName]
forall a b. (a -> b) -> a -> b
$ Tele (Dom Type) -> [Dom' Term (ArgName, Type)]
forall t. Tele (Dom t) -> [Dom (ArgName, t)]
telToList Tele (Dom Type)
ptel
           -- drop the parameter arguments
               args' :: [NamedArg Expr]
args' = [Dom' Term ArgName] -> [NamedArg Expr] -> [NamedArg Expr]
dropArgs [Dom' Term ArgName]
pnames [NamedArg 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
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
<+> Elims -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Elims -> m Doc
prettyTCM Elims
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 -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type -> m Doc
prettyTCM Type
t' ]
             v <- AppHead -> ArgsCheckState CheckedTarget -> TCM Term
forall a. AppHead -> ArgsCheckState a -> TCM Term
applyCheckedArgs (ConHead -> Int -> AppHead
ConAppHd ConHead
c Int
0) 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 -> Expr -> [NamedArg Expr] -> TCM Term
checkHeadApplication Comparison
cmp Expr
org Type
t (AmbiguousQName -> Expr
A.Con (QName -> AmbiguousQName
unambiguous (QName -> AmbiguousQName) -> QName -> AmbiguousQName
forall a b. (a -> b) -> a -> b
$ ConHead -> QName
conName ConHead
c)) [NamedArg Expr]
args

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

    -- Drop the constructor arguments that correspond to parameters.
    dropArgs :: [Dom' Term ArgName] -> [NamedArg Expr] -> [NamedArg Expr]
dropArgs [] [NamedArg Expr]
args                = [NamedArg Expr]
args
    dropArgs [Dom' Term ArgName]
ps []                  = [NamedArg Expr]
args
    dropArgs [Dom' Term ArgName]
ps args :: [NamedArg Expr]
args@(NamedArg Expr
arg : [NamedArg Expr]
args')
      | Just ArgName
p   <- Maybe ArgName
name,
        Just [Dom' Term ArgName]
ps' <- ArgName -> [Dom' Term ArgName] -> Maybe [Dom' Term ArgName]
forall {b} {t}. Eq b => b -> [Dom' t b] -> Maybe [Dom' t b]
namedPar ArgName
p [Dom' Term ArgName]
ps   = [Dom' Term ArgName] -> [NamedArg Expr] -> [NamedArg Expr]
dropArgs [Dom' Term ArgName]
ps' [NamedArg Expr]
args'
      | Maybe ArgName
Nothing  <- Maybe ArgName
name,
        Just [Dom' Term ArgName]
ps' <- Hiding -> [Dom' Term ArgName] -> Maybe [Dom' Term ArgName]
forall {a} {t}.
(LensHiding a, LensHiding t) =>
a -> [t] -> Maybe [t]
unnamedPar Hiding
h [Dom' Term ArgName]
ps = [Dom' Term ArgName] -> [NamedArg Expr] -> [NamedArg Expr]
dropArgs [Dom' Term ArgName]
ps' [NamedArg Expr]
args'
      | Bool
otherwise                   = [NamedArg Expr]
args
      where
        name :: Maybe ArgName
name = NamedArg Expr -> Maybe ArgName
forall a. (LensNamed a, NameOf a ~ NamedName) => a -> Maybe ArgName
bareNameOf NamedArg Expr
arg
        h :: Hiding
h    = NamedArg Expr -> Hiding
forall a. LensHiding a => a -> Hiding
getHiding NamedArg 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 -> [t] -> Maybe [t]
unnamedPar a
h = (t -> Bool) -> [t] -> Maybe [t]
forall {t}. (t -> Bool) -> [t] -> Maybe [t]
dropPar (a -> t -> 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
-> [NamedArg Expr] -> Type -> DisambiguateConstructor
disambiguateConstructor AmbiguousQName
ambC [NamedArg Expr]
args Type
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]
: (NamedArg Expr -> TCMT IO Doc) -> [NamedArg 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)
-> (NamedArg Expr -> TCMT IO Doc) -> NamedArg Expr -> TCMT IO Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NamedArg Expr -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => NamedArg Expr -> m Doc
prettyTCM) [NamedArg Expr]
args
  let cs0 :: List1 QName
cs0 = AmbiguousQName -> List1 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 (List1 QName -> Range
forall a. HasRange a => a -> Range
getRange List1 QName
cs0)
  -- We use the reduced constructor when disambiguating, but
  -- the original constructor for type checking. This is important
  -- since they may have different types (different parameters).
  -- See issue 279.
  -- Andreas, 2017-08-13, issue #2686: ignore abstract constructors
  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
     List1 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 List1 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 :: * -> *) e a.
(HasCallStack, MonadTCError m, Diagnostic e) =>
e -> 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
$ List1 QName -> QName
forall a. NonEmpty a -> a
List1.head List1 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, ConHead))
-> TCMT IO (List1 (QName, Type, 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, ConHead))
 -> TCMT IO (List1 (QName, Type, ConHead)))
-> ((QName, ConHead) -> TCMT IO (QName, Type, ConHead))
-> TCMT IO (List1 (QName, Type, ConHead))
forall a b. (a -> b) -> a -> b
$ \ (QName
c, ConHead
con) -> do
        t   <- Definition -> Type
defType (Definition -> Type) -> TCMT IO Definition -> TCMT IO Type
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 List1 (QName, Type, ConHead)
dcs1 [NamedArg Expr]
args Type
t) = do
      let dcs :: [Item (List1 (QName, Type, ConHead))]
dcs = List1 (QName, Type, ConHead)
-> [Item (List1 (QName, Type, ConHead))]
forall l. IsList l => l -> [Item l]
List1.toList List1 (QName, Type, ConHead)
dcs1

      -- Lets look at the target type at this point
      TelV tel t1 <- Type -> TCMT IO (TelV Type)
forall (m :: * -> *). PureTCM m => Type -> m (TelV Type)
telViewPath Type
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
_ -> [(QName, Type, ConHead)]
-> [NamedArg Expr]
-> DisambiguateConstructor
-> DisambiguateConstructor
disambiguateByArgs [(QName, Type, ConHead)]
[Item (List1 (QName, Type, ConHead))]
dcs [NamedArg Expr]
args (DisambiguateConstructor -> DisambiguateConstructor)
-> DisambiguateConstructor -> DisambiguateConstructor
forall a b. (a -> b) -> a -> b
$ Blocker -> DisambiguateConstructor
postpone Blocker
b) $ \ NotBlocked
_ Type
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
forall t a. Type'' t a -> a
unEl Type
t') (Type -> DisambiguateConstructor
badCon Type
t') (((QName, DataOrRecord) -> DisambiguateConstructor)
 -> DisambiguateConstructor)
-> ((QName, DataOrRecord) -> DisambiguateConstructor)
-> DisambiguateConstructor
forall a b. (a -> b) -> a -> b
$ \ (QName
d, DataOrRecord
_) -> do
           let dcs' :: [(QName, Type, ConHead)]
dcs' = ((QName, Type, ConHead) -> Bool)
-> [(QName, Type, ConHead)] -> [(QName, Type, ConHead)]
forall a. (a -> Bool) -> [a] -> [a]
filter ((QName
d QName -> QName -> Bool
forall a. Eq a => a -> a -> Bool
==) (QName -> Bool)
-> ((QName, Type, ConHead) -> QName)
-> (QName, Type, ConHead)
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Getting QName (QName, Type, ConHead) QName
-> (QName, Type, ConHead) -> QName
forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a
view Getting QName (QName, Type, ConHead) QName
forall s t a b. Field1 s t a b => Lens s t a b
Lens (QName, Type, ConHead) (QName, Type, ConHead) QName QName
_1) [(QName, Type, ConHead)]
[Item (List1 (QName, Type, ConHead))]
dcs
           case ((QName, Type, ConHead) -> ConHead)
-> [(QName, Type, ConHead)] -> [ConHead]
forall a b. (a -> b) -> [a] -> [b]
map' (Getting ConHead (QName, Type, ConHead) ConHead
-> (QName, Type, ConHead) -> ConHead
forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a
view Getting ConHead (QName, Type, ConHead) ConHead
forall s t a b. Field3 s t a b => Lens s t a b
Lens (QName, Type, ConHead) (QName, Type, ConHead) ConHead ConHead
_3) [(QName, Type, ConHead)]
dcs' of
             [ConHead
c] -> ConHead -> DisambiguateConstructor
decideOn ConHead
c
             []  -> Type -> DisambiguateConstructor
badCon (Type -> DisambiguateConstructor)
-> Type -> DisambiguateConstructor
forall a b. (a -> b) -> a -> b
$ Type
t' Type -> Term -> Type
forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> QName -> Elims -> 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, ConHead)]
-> [NamedArg Expr]
-> DisambiguateConstructor
-> DisambiguateConstructor
disambiguateByArgs [(QName, Type, ConHead)]
dcs' [NamedArg Expr]
args (DisambiguateConstructor -> DisambiguateConstructor)
-> DisambiguateConstructor -> DisambiguateConstructor
forall a b. (a -> b) -> a -> b
$
                      TypeError -> DisambiguateConstructor
forall (m :: * -> *) e a.
(HasCallStack, MonadTCError m, Diagnostic e) =>
e -> m a
typeError (TypeError -> DisambiguateConstructor)
-> TypeError -> DisambiguateConstructor
forall a b. (a -> b) -> a -> b
$ QName -> List1 QName -> TypeError
CantResolveOverloadedConstructorsTargetingSameDatatype QName
d (List1 QName -> TypeError) -> List1 QName -> TypeError
forall a b. (a -> b) -> a -> b
$
                        (ConHead -> QName) -> NonEmpty ConHead -> List1 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 -> List1 QName)
-> NonEmpty ConHead -> List1 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 -> DisambiguateConstructor
badCon Type
t = TypeError -> DisambiguateConstructor
forall (m :: * -> *) e a.
(HasCallStack, MonadTCError m, Diagnostic e) =>
e -> m a
typeError (TypeError -> DisambiguateConstructor)
-> TypeError -> DisambiguateConstructor
forall a b. (a -> b) -> a -> b
$ QName -> Type -> TypeError
ConstructorDoesNotTargetGivenType QName
c0 Type
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, ConHead)]
-> [NamedArg Expr]
-> DisambiguateConstructor
-> DisambiguateConstructor
disambiguateByArgs [(QName, Type, ConHead)]
dcs [NamedArg 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
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 -> TCM [Maybe QName]
visibleConDoms Type
t) dcs
    case cands of
      [(QName
_d, Type
_t, ConHead
c)] -> ConHead -> DisambiguateConstructor
decideOn ConHead
c
      [(QName, Type, 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 = [NamedArg Expr]
-> (NamedArg 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 ((NamedArg Expr -> Bool) -> [NamedArg Expr] -> [NamedArg Expr]
forall a. (a -> Bool) -> [a] -> [a]
filter NamedArg Expr -> Bool
forall a. LensHiding a => a -> Bool
visible [NamedArg Expr]
args) ((NamedArg Expr -> TCMT IO (Maybe QName)) -> TCM [Maybe QName])
-> (NamedArg Expr -> TCMT IO (Maybe QName)) -> TCM [Maybe QName]
forall a b. (a -> b) -> a -> b
$ \ (NamedArg Expr
arg :: NamedArg A.Expr) -> do
        let v :: Expr
v = Expr -> Expr
unScope (Expr -> Expr) -> Expr -> Expr
forall a b. (a -> b) -> a -> b
$ NamedArg Expr -> Expr
forall a. NamedArg a -> a
namedArg NamedArg 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 Type -> Type
forall t e. Dom' t e -> e
unDom (Dom Type -> Type)
-> ((Term, Dom Type) -> Dom Type) -> (Term, Dom Type) -> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Term, Dom Type) -> Dom Type
forall a b. (a, b) -> b
snd ((Term, Dom Type) -> Type)
-> TCMT IO (Term, Dom Type) -> TCMT IO Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Name -> TCMT IO (Term, Dom Type)
forall (m :: * -> *).
(MonadDebug m, MonadFail m, MonadTCEnv m) =>
Name -> m (Term, Dom Type)
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 -> TCMT IO (Maybe QName)
getTypeHead (Type -> TCMT IO (Maybe QName)) -> Type -> TCMT IO (Maybe QName)
forall a b. (a -> b) -> a -> b
$ Definition -> Type
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 : Type} {n : Nat} (x : A) (xs : Vec A n) → Vec A (suc n)
    -- becomes vcons : ? → Vec → .
    visibleConDoms :: Type -> TCM [Maybe QName]
    visibleConDoms :: Type -> TCM [Maybe QName]
visibleConDoms Type
t = do
      TelV tel _ <- Type -> TCMT IO (TelV Type)
forall (m :: * -> *). PureTCM m => Type -> m (TelV Type)
telViewPath Type
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 -> TCMT IO (Maybe QName)
getTypeHead Type
t = do
  res <- Type
-> (Blocker -> Type -> TCMT IO (Maybe QName))
-> (NotBlocked -> Type -> 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
t (\ Blocker
_ Type
_ -> 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 -> TCMT IO (Maybe QName))
 -> TCMT IO (Maybe QName))
-> (NotBlocked -> Type -> TCMT IO (Maybe QName))
-> TCMT IO (Maybe QName)
forall a b. (a -> b) -> a -> b
$ \ NotBlocked
nb Type
t -> do
    case NotBlocked
nb of
      NotBlocked
ReallyNotBlocked -> do
        -- Drop initial hidden domains (only needed for generalizable variables).
        TelV _ core <- Int -> (Dom Type -> Bool) -> Type -> TCMT IO (TelV Type)
forall (m :: * -> *).
(MonadReduce m, MonadAddContext m) =>
Int -> (Dom Type -> Bool) -> Type -> m (TelV Type)
telViewUpTo' (Int -> Int
forall a. Num a => a -> a
negate Int
1) (Bool -> Bool
not (Bool -> Bool) -> (Dom Type -> Bool) -> Dom Type -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Dom Type -> Bool
forall a. LensHiding a => a -> Bool
visible) Type
t
        case unEl core of
          Def QName
q Elims
_ -> 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
-> QName
-> ProjOrigin
-> Expr
-> [NamedArg Expr]
-> TCM Term
checkUnambiguousProjectionApplication Comparison
cmp Expr
e Type
t QName
x ProjOrigin
o Expr
hd [NamedArg Expr]
args = do
  let fallback :: TCM Term
fallback = Comparison -> Expr -> Type -> Expr -> [NamedArg Expr] -> TCM Term
checkHeadApplication Comparison
cmp Expr
e Type
t Expr
hd [NamedArg Expr]
args
  -- Andreas, 2021-02-19, issue #3289
  -- If a postfix projection was moved to the head by appView,
  -- we have to patch the first argument with the correct hiding info.
  case (ProjOrigin
o, [NamedArg Expr]
args) of
    (ProjOrigin
ProjPostfix, NamedArg Expr
arg : [NamedArg Expr]
rest) -> do
      -- Andreas, 2021-11-19, issue #5657:
      -- If @x@ has been brought into scope by e.g. @open R r@, it is no longer
      -- a projection even though the scope checker labels it so.
      -- Thus, @isProjection@ may fail.
      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 -> Expr -> [NamedArg Expr] -> TCM Term
checkHeadApplication Comparison
cmp Expr
e Type
t Expr
hd (ArgInfo -> NamedArg Expr -> NamedArg Expr
forall a. LensArgInfo a => ArgInfo -> a -> a
setArgInfo (Projection -> ArgInfo
projArgInfo Projection
pr) NamedArg Expr
arg NamedArg Expr -> [NamedArg Expr] -> [NamedArg Expr]
forall a. a -> [a] -> [a]
: [NamedArg Expr]
rest)
    (ProjOrigin, [NamedArg Expr])
_ -> TCM Term
fallback

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

inferProjApp :: A.Expr -> ProjOrigin -> AmbiguousQName -> A.Expr -> A.Args -> TCM (Term, Type)
inferProjApp :: Expr
-> ProjOrigin
-> AmbiguousQName
-> Expr
-> [NamedArg Expr]
-> TCM (Term, Type)
inferProjApp Expr
e ProjOrigin
o AmbiguousQName
ds Expr
hd [NamedArg Expr]
args0 = do
  (v, t, _) <- Expr
-> ProjOrigin
-> AmbiguousQName
-> Expr
-> [NamedArg Expr]
-> Maybe (Comparison, Type)
-> TCM (Term, Type, CheckedTarget)
inferOrCheckProjApp Expr
e ProjOrigin
o AmbiguousQName
ds Expr
hd [NamedArg Expr]
args0 Maybe (Comparison, Type)
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
-> [NamedArg Expr]
-> Type
-> TCM Term
checkProjApp Comparison
cmp Expr
e ProjOrigin
o AmbiguousQName
ds Expr
hd [NamedArg Expr]
args0 Type
t = do
  (v, ti, targetCheck) <- Expr
-> ProjOrigin
-> AmbiguousQName
-> Expr
-> [NamedArg Expr]
-> Maybe (Comparison, Type)
-> TCM (Term, Type, CheckedTarget)
inferOrCheckProjApp Expr
e ProjOrigin
o AmbiguousQName
ds Expr
hd [NamedArg Expr]
args0 ((Comparison, Type) -> Maybe (Comparison, Type)
forall a. a -> Maybe a
Just (Comparison
cmp, Type
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
-> [NamedArg Expr]
-> Type
-> Int
-> Term
-> Type
-> PrincipalArgTypeMetas
-> TCM Term
checkProjAppToKnownPrincipalArg Comparison
cmp Expr
e ProjOrigin
o AmbiguousQName
ds Expr
hd [NamedArg Expr]
args0 Type
t Int
k Term
v0 Type
pt PrincipalArgTypeMetas
patm = do
  (v, ti, targetCheck) <- Expr
-> ProjOrigin
-> AmbiguousQName
-> Expr
-> [NamedArg Expr]
-> Maybe (Comparison, Type)
-> Int
-> Term
-> Type
-> Maybe PrincipalArgTypeMetas
-> TCM (Term, Type, CheckedTarget)
inferOrCheckProjAppToKnownPrincipalArg Expr
e ProjOrigin
o AmbiguousQName
ds Expr
hd [NamedArg Expr]
args0 ((Comparison, Type) -> Maybe (Comparison, Type)
forall a. a -> Maybe a
Just (Comparison
cmp, Type
t)) Int
k Term
v0 Type
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
-> [NamedArg Expr]
-> Maybe (Comparison, Type)
-> TCM (Term, Type, CheckedTarget)
inferOrCheckProjApp Expr
e ProjOrigin
o AmbiguousQName
ds Expr
hd [NamedArg Expr]
args Maybe (Comparison, Type)
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
$ (NamedArg Expr -> TCMT IO Doc) -> [NamedArg Expr] -> [TCMT IO Doc]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap NamedArg Expr -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => NamedArg Expr -> m Doc
prettyTCM [NamedArg 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)
-> TCMT IO Doc
-> ((Comparison, Type) -> TCMT IO Doc)
-> TCMT IO Doc
forall a b. Maybe a -> b -> (a -> b) -> b
caseMaybe Maybe (Comparison, Type)
mt TCMT IO Doc
"Nothing" (Comparison, Type) -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => (Comparison, Type) -> m Doc
prettyTCM
    ]

  let cmp :: Comparison
cmp = Maybe (Comparison, Type)
-> Comparison -> ((Comparison, Type) -> Comparison) -> Comparison
forall a b. Maybe a -> b -> (a -> b) -> b
caseMaybe Maybe (Comparison, Type)
mt Comparison
CmpEq (Comparison, Type) -> 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, CheckedTarget)
postpone Blocker
b = do
        tc <- Maybe (Comparison, Type)
-> TCMT IO Type
-> ((Comparison, Type) -> TCMT IO Type)
-> TCMT IO Type
forall a b. Maybe a -> b -> (a -> b) -> b
caseMaybe Maybe (Comparison, Type)
mt TCMT IO Type
newTypeMeta_ (Type -> TCMT IO Type
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> TCMT IO Type)
-> ((Comparison, Type) -> Type)
-> (Comparison, Type)
-> TCMT IO Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Comparison, Type) -> Type
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, NamedArg Expr) -> Bool)
-> [(Int, NamedArg Expr)] -> [(Int, NamedArg Expr)]
forall a. (a -> Bool) -> [a] -> [a]
filter (NamedArg Expr -> Bool
forall a. LensHiding a => a -> Bool
visible (NamedArg Expr -> Bool)
-> ((Int, NamedArg Expr) -> NamedArg Expr)
-> (Int, NamedArg Expr)
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Int, NamedArg Expr) -> NamedArg Expr
forall a b. (a, b) -> b
snd) ([(Int, NamedArg Expr)] -> [(Int, NamedArg Expr)])
-> [(Int, NamedArg Expr)] -> [(Int, NamedArg Expr)]
forall a b. (a -> b) -> a -> b
$ [Int] -> [NamedArg Expr] -> [(Int, NamedArg Expr)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Int
0..] [NamedArg Expr]
args of

    -- Case: we have no visible argument to the projection.
    -- In inference mode, we really need the visible argument, postponing does not help
    [] -> Maybe (Comparison, Type)
-> TCM (Term, Type, CheckedTarget)
-> ((Comparison, Type) -> TCM (Term, Type, CheckedTarget))
-> TCM (Term, Type, CheckedTarget)
forall a b. Maybe a -> b -> (a -> b) -> b
caseMaybe Maybe (Comparison, Type)
mt (AmbiguousQName -> TCM (Term, Type, CheckedTarget)
forall a. AmbiguousQName -> TCM a
refuseProjNotApplied AmbiguousQName
ds) (((Comparison, Type) -> TCM (Term, Type, CheckedTarget))
 -> TCM (Term, Type, CheckedTarget))
-> ((Comparison, Type) -> TCM (Term, Type, CheckedTarget))
-> TCM (Term, Type, CheckedTarget)
forall a b. (a -> b) -> a -> b
$ \ (Comparison
cmp , Type
t) -> do
      -- If we have the type, we can try to get the type of the principal argument.
      -- It is the first visible argument.
      TelV _ptel core <- Int -> (Dom Type -> Bool) -> Type -> TCMT IO (TelV Type)
forall (m :: * -> *).
(MonadReduce m, MonadAddContext m) =>
Int -> (Dom Type -> Bool) -> Type -> m (TelV Type)
telViewUpTo' (-Int
1) (Bool -> Bool
not (Bool -> Bool) -> (Dom Type -> Bool) -> Dom Type -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Dom Type -> Bool
forall a. LensHiding a => a -> Bool
visible) Type
t
      ifBlocked core (\ Blocker
m Type
_ -> Blocker -> TCM (Term, Type, CheckedTarget)
postpone Blocker
m) $ {-else-} \ NotBlocked
_ Type
core -> do
      Type
-> (Type -> TCM (Term, Type, CheckedTarget))
-> (Dom Type -> Abs Type -> TCM (Term, Type, CheckedTarget))
-> TCM (Term, Type, CheckedTarget)
forall (m :: * -> *) a.
MonadReduce m =>
Type -> (Type -> m a) -> (Dom Type -> Abs Type -> m a) -> m a
ifNotPiType Type
core (\ Type
_ -> AmbiguousQName -> TCM (Term, Type, CheckedTarget)
forall a. AmbiguousQName -> TCM a
refuseProjNotApplied AmbiguousQName
ds) ((Dom Type -> Abs Type -> TCM (Term, Type, CheckedTarget))
 -> TCM (Term, Type, CheckedTarget))
-> (Dom Type -> Abs Type -> TCM (Term, Type, CheckedTarget))
-> TCM (Term, Type, CheckedTarget)
forall a b. (a -> b) -> a -> b
$ {-else-} \ Dom Type
dom Abs Type
_b -> do
      Type
-> (Blocker -> Type -> TCM (Term, Type, CheckedTarget))
-> (NotBlocked -> Type -> TCM (Term, Type, CheckedTarget))
-> TCM (Term, Type, CheckedTarget)
forall t (m :: * -> *) a.
(Reduce t, IsMeta t, MonadReduce m) =>
t -> (Blocker -> t -> m a) -> (NotBlocked -> t -> m a) -> m a
ifBlocked (Dom Type -> Type
forall t e. Dom' t e -> e
unDom Dom Type
dom) (\ Blocker
m Type
_ -> Blocker -> TCM (Term, Type, CheckedTarget)
postpone Blocker
m) ((NotBlocked -> Type -> TCM (Term, Type, CheckedTarget))
 -> TCM (Term, Type, CheckedTarget))
-> (NotBlocked -> Type -> TCM (Term, Type, CheckedTarget))
-> TCM (Term, Type, CheckedTarget)
forall a b. (a -> b) -> a -> b
$ {-else-} \ NotBlocked
_ Type
ta -> do
      TCMT IO (Maybe (QName, [Arg Term], RecordData))
-> TCM (Term, Type, CheckedTarget)
-> ((QName, [Arg Term], RecordData)
    -> TCM (Term, Type, CheckedTarget))
-> TCM (Term, Type, CheckedTarget)
forall (m :: * -> *) a b.
Monad m =>
m (Maybe a) -> m b -> (a -> m b) -> m b
caseMaybeM (Type -> TCMT IO (Maybe (QName, [Arg Term], RecordData))
forall (m :: * -> *).
(HasCallStack, PureTCM m) =>
Type -> m (Maybe (QName, [Arg Term], RecordData))
isRecordType Type
ta) (AmbiguousQName
-> Maybe Term -> Type -> TCM (Term, Type, CheckedTarget)
forall a. AmbiguousQName -> Maybe Term -> Type -> TCM a
refuseProjNotRecordType AmbiguousQName
ds Maybe Term
forall a. Maybe a
Nothing Type
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) -> List1 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 -> List1 QName
getAmbiguous AmbiguousQName
ds) of
            [] -> AmbiguousQName -> TCM (Term, Type, 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
t, Maybe ProblemId -> CheckedTarget
CheckedTarget Maybe ProblemId
forall a. Maybe a
Nothing) (Term -> (Term, Type, CheckedTarget))
-> TCM Term -> TCM (Term, Type, CheckedTarget)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
                Comparison -> Expr -> Type -> Expr -> [NamedArg Expr] -> TCM Term
checkHeadApplication Comparison
cmp Expr
e Type
t (ProjOrigin -> AmbiguousQName -> Expr
A.Proj ProjOrigin
o (AmbiguousQName -> Expr) -> AmbiguousQName -> Expr
forall a b. (a -> b) -> a -> b
$ QName -> AmbiguousQName
unambiguous QName
d) [NamedArg Expr]
args
            [QName]
_ -> TCM (Term, Type, CheckedTarget)
forall a. HasCallStack => a
__IMPOSSIBLE__

    -- Case: we have a visible argument
    ((Int
k, NamedArg Expr
arg) : [(Int, NamedArg Expr)]
_) -> do
      (v0, ta) <- Expr -> TCM (Term, Type)
inferExpr (Expr -> TCM (Term, Type)) -> Expr -> TCM (Term, Type)
forall a b. (a -> b) -> a -> b
$ NamedArg Expr -> Expr
forall a. NamedArg a -> a
namedArg NamedArg 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
-> [NamedArg Expr]
-> Maybe (Comparison, Type)
-> Int
-> Term
-> Type
-> Maybe PrincipalArgTypeMetas
-> TCM (Term, Type, CheckedTarget)
inferOrCheckProjAppToKnownPrincipalArg Expr
e ProjOrigin
o AmbiguousQName
ds Expr
hd [NamedArg Expr]
args Maybe (Comparison, Type)
mt Int
k Term
v0 Type
ta Maybe PrincipalArgTypeMetas
mpatm = do
  let cmp :: Comparison
cmp = Maybe (Comparison, Type)
-> Comparison -> ((Comparison, Type) -> Comparison) -> Comparison
forall a b. Maybe a -> b -> (a -> b) -> b
caseMaybe Maybe (Comparison, Type)
mt Comparison
CmpEq (Comparison, Type) -> Comparison
forall a b. (a, b) -> a
fst
      postpone :: Blocker -> PrincipalArgTypeMetas -> TCM (Term, Type, CheckedTarget)
postpone Blocker
b PrincipalArgTypeMetas
patm = do
        tc <- Maybe (Comparison, Type)
-> TCMT IO Type
-> ((Comparison, Type) -> TCMT IO Type)
-> TCMT IO Type
forall a b. Maybe a -> b -> (a -> b) -> b
caseMaybe Maybe (Comparison, Type)
mt TCMT IO Type
newTypeMeta_ (Type -> TCMT IO Type
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> TCMT IO Type)
-> ((Comparison, Type) -> Type)
-> (Comparison, Type)
-> TCMT IO Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Comparison, Type) -> Type
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 -> PrincipalArgTypeMetas)
-> ([Arg Term], Type) -> PrincipalArgTypeMetas
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry [Arg Term] -> Type -> PrincipalArgTypeMetas
PrincipalArgTypeMetas (([Arg Term], Type) -> PrincipalArgTypeMetas)
-> TCMT IO ([Arg Term], Type) -> TCMT IO PrincipalArgTypeMetas
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Int -> (Hiding -> Bool) -> Type -> TCMT IO ([Arg Term], Type)
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
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
_ -> Blocker -> PrincipalArgTypeMetas -> TCM (Term, Type, CheckedTarget)
postpone Blocker
m PrincipalArgTypeMetas
patm) {-else-} $ \ NotBlocked
_ Type
ta -> do
  TCMT IO (Maybe (QName, [Arg Term], RecordData))
-> TCM (Term, Type, CheckedTarget)
-> ((QName, [Arg Term], RecordData)
    -> TCM (Term, Type, CheckedTarget))
-> TCM (Term, Type, CheckedTarget)
forall (m :: * -> *) a b.
Monad m =>
m (Maybe a) -> m b -> (a -> m b) -> m b
caseMaybeM (Type -> TCMT IO (Maybe (QName, [Arg Term], RecordData))
forall (m :: * -> *).
(HasCallStack, PureTCM m) =>
Type -> m (Maybe (QName, [Arg Term], RecordData))
isRecordType Type
ta) (AmbiguousQName
-> Maybe Term -> Type -> TCM (Term, Type, CheckedTarget)
forall a. AmbiguousQName -> Maybe Term -> Type -> TCM a
refuseProjNotRecordType AmbiguousQName
ds (Term -> Maybe Term
forall a. a -> Maybe a
Just Term
v0) Type
ta) (((QName, [Arg Term], RecordData)
  -> TCM (Term, Type, CheckedTarget))
 -> TCM (Term, Type, CheckedTarget))
-> ((QName, [Arg Term], RecordData)
    -> TCM (Term, Type, CheckedTarget))
-> TCM (Term, Type, 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 Type, Term, Type)
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)
-> TCMT IO Doc -> (Type -> 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 -> TCMT IO (Maybe Type)
forall (m :: * -> *). PureTCM m => QName -> Type -> m (Maybe Type)
getDefType QName
d Type
ta) TCMT IO Doc
"Nothing" Type -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type -> 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 = Definition -> Maybe Projection
isProjectionDefinition 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 Type, Term, Type)
-> TCMT IO (Maybe (Dom Type, Term, Type))
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (Dom Type, Term, Type)
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
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)

            return (orig, d, pars, dom, u, tb)

      cands <- ((QName, QName, [Arg Term], Dom Type, Term, Type) -> QName)
-> [(QName, QName, [Arg Term], Dom Type, Term, Type)]
-> [List1 (QName, QName, [Arg Term], Dom Type, Term, Type)]
forall b a. Ord b => (a -> b) -> [a] -> [List1 a]
List1.groupOn (Getting
  QName (QName, QName, [Arg Term], Dom Type, Term, Type) QName
-> (QName, QName, [Arg Term], Dom Type, Term, Type) -> QName
forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a
view Getting
  QName (QName, QName, [Arg Term], Dom Type, Term, Type) QName
forall s t a b. Field1 s t a b => Lens s t a b
Lens
  (QName, QName, [Arg Term], Dom Type, Term, Type)
  (QName, QName, [Arg Term], Dom Type, Term, Type)
  QName
  QName
_1) ([(QName, QName, [Arg Term], Dom Type, Term, Type)]
 -> [List1 (QName, QName, [Arg Term], Dom Type, Term, Type)])
-> (List1 (Maybe (QName, QName, [Arg Term], Dom Type, Term, Type))
    -> [(QName, QName, [Arg Term], Dom Type, Term, Type)])
-> List1 (Maybe (QName, QName, [Arg Term], Dom Type, Term, Type))
-> [List1 (QName, QName, [Arg Term], Dom Type, Term, Type)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. List1 (Maybe (QName, QName, [Arg Term], Dom Type, Term, Type))
-> [(QName, QName, [Arg Term], Dom Type, Term, Type)]
forall a. List1 (Maybe a) -> [a]
List1.catMaybes (List1 (Maybe (QName, QName, [Arg Term], Dom Type, Term, Type))
 -> [List1 (QName, QName, [Arg Term], Dom Type, Term, Type)])
-> TCMT
     IO (List1 (Maybe (QName, QName, [Arg Term], Dom Type, Term, Type)))
-> TCMT IO [List1 (QName, QName, [Arg Term], Dom Type, Term, Type)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (QName
 -> TCMT
      IO (Maybe (QName, QName, [Arg Term], Dom Type, Term, Type)))
-> List1 QName
-> TCMT
     IO (List1 (Maybe (QName, QName, [Arg Term], Dom Type, Term, Type)))
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 Type, Term, Type)
-> TCMT IO (Maybe (QName, QName, [Arg Term], Dom Type, Term, Type))
forall (m :: * -> *) a. MaybeT m a -> m (Maybe a)
runMaybeT (MaybeT (TCMT IO) (QName, QName, [Arg Term], Dom Type, Term, Type)
 -> TCMT
      IO (Maybe (QName, QName, [Arg Term], Dom Type, Term, Type)))
-> (QName
    -> MaybeT
         (TCMT IO) (QName, QName, [Arg Term], Dom Type, Term, Type))
-> QName
-> TCMT IO (Maybe (QName, QName, [Arg Term], Dom Type, Term, Type))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. QName
-> MaybeT
     (TCMT IO) (QName, QName, [Arg Term], Dom Type, Term, Type)
try) (AmbiguousQName -> List1 QName
getAmbiguous AmbiguousQName
ds)
      case cands of
        [] -> AmbiguousQName -> TCM (Term, Type, CheckedTarget)
forall a. AmbiguousQName -> TCM a
refuseProjNoMatching AmbiguousQName
ds
        (List1 (QName, QName, [Arg Term], Dom Type, Term, Type)
_:List1 (QName, QName, [Arg Term], Dom Type, Term, Type)
_:[List1 (QName, QName, [Arg Term], Dom Type, Term, Type)]
_) -> AmbiguousQName -> TCMT IO Doc -> TCM (Term, Type, CheckedTarget)
forall a. AmbiguousQName -> TCMT IO Doc -> TCM a
refuseProj AmbiguousQName
ds (TCMT IO Doc -> TCM (Term, Type, CheckedTarget))
-> TCMT IO Doc -> TCM (Term, Type, 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 Type
_dom, Term
u, Type
tb) :| [(QName, QName, [Arg Term], Dom Type, Term, Type)]
_ ] -> do
          QName -> TCMT IO ()
storeDisambiguatedProjection QName
d

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

          -- Check remaining arguments
          let
            fun = AppInfo -> Expr -> NamedArg Expr -> Expr
A.App
              (Range -> AppInfo
A.defaultAppInfo (Range -> AppInfo) -> Range -> AppInfo
forall a b. (a -> b) -> a -> b
$ (Expr, [NamedArg Expr], NamedArg Expr) -> Range
forall a. HasRange a => a -> Range
getRange (Expr
hd, [NamedArg Expr]
args0, NamedArg Expr
princArg))
              (AppView -> Expr
A.unAppView (AppView -> Expr) -> AppView -> Expr
forall a b. (a -> b) -> a -> b
$ Expr -> [NamedArg Expr] -> AppView
forall arg. Expr -> [NamedArg arg] -> AppView' arg
A.Application Expr
hd [NamedArg Expr]
args0)
              NamedArg Expr
princArg
          z <- runExceptT $ checkArgumentsE cmp ExpandLast fun args' tb (snd <$> mt)
          case z of
            Right st :: ArgsCheckState CheckedTarget
st@(ACState [CheckedArg]
_ Expr
_ Type
trest CheckedTarget
targetCheck) -> do
              v <- AppHead -> ArgsCheckState CheckedTarget -> TCM Term
forall a. AppHead -> ArgsCheckState a -> TCM Term
applyCheckedArgs (Term -> AppHead
TermAppHd Term
u) ArgsCheckState CheckedTarget
st
              return (v, trest, targetCheck)
            Left ArgsCheckState [NamedArg Expr]
problem -> do
              -- In the inference case:
              -- To create a postponed type checking problem,
              -- we do not use typeDontCare, but create a meta.
              tc <- Maybe (Comparison, Type)
-> TCMT IO Type
-> ((Comparison, Type) -> TCMT IO Type)
-> TCMT IO Type
forall a b. Maybe a -> b -> (a -> b) -> b
caseMaybe Maybe (Comparison, Type)
mt TCMT IO Type
newTypeMeta_ (Type -> TCMT IO Type
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> TCMT IO Type)
-> ((Comparison, Type) -> Type)
-> (Comparison, Type)
-> TCMT IO Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Comparison, Type) -> Type
forall a b. (a, b) -> b
snd)
              v  <- postponeArgs problem cmp ExpandLast fun args' tb tc \ st :: ArgsCheckState CheckedTarget
st@(ACState [CheckedArg]
_ Expr
_ Type
trest CheckedTarget
targetCheck) -> do
                      v <- AppHead -> ArgsCheckState CheckedTarget -> TCM Term
forall a. AppHead -> ArgsCheckState a -> TCM Term
applyCheckedArgs (Term -> AppHead
TermAppHd Term
u) 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 :: * -> *) e a.
(HasCallStack, MonadTCError m, Diagnostic e) =>
e -> 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 -> TCM a
refuseProjNotRecordType AmbiguousQName
ds Maybe Term
pValue Type
pType = do
  let dType :: TCMT IO Doc
dType = Type -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type -> m Doc
prettyTCM Type
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
-> QName
-> Suffix
-> [NamedArg Expr]
-> TCM Term
checkUniv UnivSize
sz Univ
u Comparison
cmp Expr
e Type
t QName
q Suffix
suffix [NamedArg Expr]
args = do
  (v, t0) <- UnivSize
-> Univ
-> Expr
-> QName
-> Suffix
-> [NamedArg Expr]
-> TCM (Term, Type)
inferUniv UnivSize
sz Univ
u Expr
e QName
q Suffix
suffix [NamedArg 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
-> [NamedArg Expr]
-> TCM (Term, Type)
inferUniv UnivSize
sz Univ
u Expr
e QName
q Suffix
s [NamedArg Expr]
args = do
  Univ -> TCMT IO ()
univChecks Univ
u
  case UnivSize
sz of
    UnivSize
USmall -> Univ -> QName -> Suffix -> [NamedArg Expr] -> TCM (Term, Type)
inferLeveledSort Univ
u QName
q Suffix
s [NamedArg Expr]
args
    UnivSize
ULarge -> Univ -> QName -> Suffix -> [NamedArg Expr] -> TCM (Term, Type)
inferUnivOmega Univ
u QName
q Suffix
s [NamedArg 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 :: * -> *) e a.
(HasCallStack, MonadTCError m, Diagnostic e) =>
e -> 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 ()
forall a. a -> TCMT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()

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 -> [NamedArg Expr] -> TCM (Term, Type)
inferLeveledSort Univ
u QName
q Suffix
suffix = \case
  [] -> do
    let n :: Integer
n = Suffix -> Integer
suffixToLevel Suffix
suffix
    (Term, Type) -> TCM (Term, Type)
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
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))
  NamedArg Expr
arg : [NamedArg Expr]
args -> do
    Bool -> TCMT IO () -> TCMT IO ()
forall b (m :: * -> *). (IsBool b, Monad m) => b -> m () -> m ()
unless (NamedArg Expr -> Bool
forall a. LensHiding a => a -> Bool
visible NamedArg Expr
arg) (TCMT IO () -> TCMT IO ()) -> TCMT IO () -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ TypeError -> TCMT IO ()
forall (m :: * -> *) e a.
(HasCallStack, MonadTCError m, Diagnostic e) =>
e -> m a
typeError (TypeError -> TCMT IO ()) -> TypeError -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ Hiding -> Type -> TypeError
WrongHidingInApplication (NamedArg Expr -> Hiding
forall a. LensHiding a => a -> Hiding
getHiding NamedArg Expr
arg) (Type -> TypeError) -> Type -> TypeError
forall a b. (a -> b) -> a -> b
$ Sort -> Type
sort (Sort -> Type) -> Sort -> Type
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
    [NamedArg Expr]
-> (List1 (NamedArg Expr) -> TCMT IO ()) -> TCMT IO ()
forall (m :: * -> *) a.
Applicative m =>
[a] -> (List1 a -> m ()) -> m ()
List1.unlessNull [NamedArg Expr]
args ((List1 (NamedArg Expr) -> TCMT IO ()) -> TCMT IO ())
-> (List1 (NamedArg Expr) -> TCMT IO ()) -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ Warning -> TCMT IO ()
forall (m :: * -> *) e.
(HasCallStack, MonadWarning m, Diagnostic e) =>
e -> m ()
warning (Warning -> TCMT IO ())
-> (List1 (NamedArg Expr) -> Warning)
-> List1 (NamedArg Expr)
-> TCMT IO ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. QName -> List1 (NamedArg Expr) -> Warning
TooManyArgumentsToSort QName
q
    l <- NamedArg Expr -> TCM (Level' Term)
checkLevel NamedArg 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 -> [NamedArg Expr] -> TCM (Term, Type)
inferUnivOmega Univ
u QName
q Suffix
suffix [NamedArg Expr]
args = do
    [NamedArg Expr]
-> (List1 (NamedArg Expr) -> TCMT IO ()) -> TCMT IO ()
forall (m :: * -> *) a.
Applicative m =>
[a] -> (List1 a -> m ()) -> m ()
List1.unlessNull [NamedArg Expr]
args ((List1 (NamedArg Expr) -> TCMT IO ()) -> TCMT IO ())
-> (List1 (NamedArg Expr) -> TCMT IO ()) -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ Warning -> TCMT IO ()
forall (m :: * -> *) e.
(HasCallStack, MonadWarning m, Diagnostic e) =>
e -> m ()
warning (Warning -> TCMT IO ())
-> (List1 (NamedArg Expr) -> Warning)
-> List1 (NamedArg Expr)
-> TCMT IO ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. QName -> List1 (NamedArg Expr) -> Warning
TooManyArgumentsToSort QName
q
    let n :: Integer
n = Suffix -> Integer
suffixToLevel Suffix
suffix
    (Term, Type) -> TCM (Term, Type)
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
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))