{-# LANGUAGE NondecreasingIndentation #-}

module Agda.TypeChecking.Rules.Term where

import Prelude hiding ( null )

import Control.Monad.Except ( MonadError(..) )
import Control.Monad.Trans.Maybe ( runMaybeT )

import Data.Maybe
import qualified Data.DList as DL
import Data.Either (partitionEithers, lefts)
import qualified Data.List as List
import qualified Data.IntMap as IntMap
import qualified Data.Map as Map
import qualified Data.Set as Set

import Agda.Interaction.Options
import Agda.Interaction.Highlighting.Generate (disambiguateRecordFields)

import Agda.Syntax.Abstract (Binder, TypedBindingInfo (tbTacticAttr), unBind, binderName)
import qualified Agda.Syntax.Abstract as A
import Agda.Syntax.Abstract.Views as A
import qualified Agda.Syntax.Info as A
import Agda.Syntax.Concrete.Pretty () -- only Pretty instances
import Agda.Syntax.Concrete (FieldAssignment'(..), nameFieldA, TacticAttribute'(..))
import qualified Agda.Syntax.Concrete.Name as C
import Agda.Syntax.Common
import Agda.Syntax.Common.Pretty ( prettyShow )
import qualified Agda.Syntax.Common.Pretty as P
import Agda.Syntax.Internal as I
import Agda.Syntax.Internal.MetaVars
import Agda.Syntax.Position
import Agda.Syntax.Literal
import Agda.Syntax.Scope.Base ( ThingsInScope
                              , emptyScopeInfo
                              , exportedNamesInScope)
import Agda.Syntax.Scope.Monad (getNamedScope)

import Agda.TypeChecking.CompiledClause
import Agda.TypeChecking.Constraints
import Agda.TypeChecking.Conversion
import Agda.TypeChecking.Coverage.SplitTree
import Agda.TypeChecking.Datatypes
import Agda.TypeChecking.EtaContract
import Agda.TypeChecking.Generalize
import Agda.TypeChecking.Implicit
import Agda.TypeChecking.InstanceArguments
import Agda.TypeChecking.Irrelevance
import Agda.TypeChecking.IApplyConfluence
import Agda.TypeChecking.Level
import Agda.TypeChecking.MetaVars
import Agda.TypeChecking.Monad
import Agda.TypeChecking.Patterns.Abstract
import Agda.TypeChecking.Positivity.Occurrence
import Agda.TypeChecking.Pretty
import Agda.TypeChecking.Primitive
import Agda.TypeChecking.Quote
import Agda.TypeChecking.RecordPatterns
import Agda.TypeChecking.Records
import Agda.TypeChecking.Reduce
import Agda.TypeChecking.Rewriting (checkEquationValid, checkLocalRewriteRule)
import Agda.TypeChecking.Rules.LHS
import Agda.TypeChecking.SizedTypes
import Agda.TypeChecking.SizedTypes.Solve
import Agda.TypeChecking.Sort
import Agda.TypeChecking.Substitute
import Agda.TypeChecking.Telescope
import Agda.TypeChecking.Unquote
import Agda.TypeChecking.Warnings

import {-# SOURCE #-} Agda.TypeChecking.Empty ( ensureEmptyType )
import {-# SOURCE #-} Agda.TypeChecking.Rules.Def (checkFunDef', useTerPragma)
import {-# SOURCE #-} Agda.TypeChecking.Rules.Decl (checkSectionApplication)
import {-# SOURCE #-} Agda.TypeChecking.Rules.Application

import Agda.Utils.Function
import Agda.Utils.Functor
import Agda.Utils.Lens
import Agda.Utils.List
import Agda.Utils.List1  ( List1, pattern (:|) )
import Agda.Utils.List2  ( pattern List2 )
import qualified Agda.Utils.List1 as List1
import Agda.Utils.Maybe
import Agda.Utils.Monad
import Agda.Utils.Null
import qualified Agda.Utils.Set1 as Set1
import Agda.Utils.Singleton
import Agda.Utils.Size
import Agda.Utils.Tuple

import Agda.Utils.Impossible
import Agda.Utils.Boolean (implies)

---------------------------------------------------------------------------
-- * Types
---------------------------------------------------------------------------

-- | Check that an expression is a type.
isType :: A.Expr -> Sort -> TCM Type
isType :: Expr -> Sort' Term -> TCM (Type'' Term Term)
isType = Comparison -> Expr -> Sort' Term -> TCM (Type'' Term Term)
isType' Comparison
CmpLeq

-- | Check that an expression is a type.
--   * If @c == CmpEq@, the given sort must be the minimal sort.
--   * If @c == CmpLeq@, the given sort may be any bigger sort.
isType' :: Comparison -> A.Expr -> Sort -> TCM Type
isType' :: Comparison -> Expr -> Sort' Term -> TCM (Type'' Term Term)
isType' Comparison
c Expr
e Sort' Term
s =
    Call -> TCM (Type'' Term Term) -> TCM (Type'' Term Term)
forall a. Call -> TCMT IO a -> TCMT IO a
forall (m :: * -> *) a. MonadTrace m => Call -> m a -> m a
traceCall (Comparison -> Expr -> Sort' Term -> Call
IsTypeCall Comparison
c Expr
e Sort' Term
s) (TCM (Type'' Term Term) -> TCM (Type'' Term Term))
-> TCM (Type'' Term Term) -> TCM (Type'' Term Term)
forall a b. (a -> b) -> a -> b
$ do
    v <- Comparison -> Expr -> Type'' Term Term -> TCMT IO Term
checkExpr' Comparison
c Expr
e (Sort' Term -> Type'' Term Term
sort Sort' Term
s)
    return $ El s v

-- | Check that an expression is a type and infer its (minimal) sort.
isType_ :: A.Expr -> TCM Type
isType_ :: Expr -> TCM (Type'' Term Term)
isType_ Expr
e = Call -> TCM (Type'' Term Term) -> TCM (Type'' Term Term)
forall a. Call -> TCMT IO a -> TCMT IO a
forall (m :: * -> *) a. MonadTrace m => Call -> m a -> m a
traceCall (Expr -> Call
IsType_ Expr
e) (TCM (Type'' Term Term) -> TCM (Type'' Term Term))
-> TCM (Type'' Term Term) -> TCM (Type'' Term Term)
forall a b. (a -> b) -> a -> b
$ do
  ArgName
-> Int
-> (Type'' Term Term -> TCMT IO Doc)
-> TCM (Type'' Term Term)
-> TCM (Type'' Term Term)
forall (m :: * -> *) a.
MonadDebug m =>
ArgName -> Int -> (a -> TCMT IO Doc) -> m a -> m a
reportResult ArgName
"tc.term.istype" Int
15 (\Type'' Term Term
a -> [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
    [ TCMT IO Doc
"isType_" 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
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
"returns" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<?> Type'' Term Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type'' Term Term -> m Doc
prettyTCM Type'' Term Term
a
    ]) (TCM (Type'' Term Term) -> TCM (Type'' Term Term))
-> TCM (Type'' Term Term) -> TCM (Type'' Term Term)
forall a b. (a -> b) -> a -> b
$ do
  let fallback :: TCM (Type'' Term Term)
fallback = Comparison -> Expr -> Sort' Term -> TCM (Type'' Term Term)
isType' Comparison
CmpEq Expr
e (Sort' Term -> TCM (Type'' Term Term))
-> TCMT IO (Sort' Term) -> TCM (Type'' Term Term)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< do TCMT IO (Sort' Term) -> TCMT IO (Sort' Term)
forall (m :: * -> *) a.
(MonadTCEnv m, HasOptions m, MonadDebug m) =>
m a -> m a
workOnTypes (TCMT IO (Sort' Term) -> TCMT IO (Sort' Term))
-> TCMT IO (Sort' Term) -> TCMT IO (Sort' Term)
forall a b. (a -> b) -> a -> b
$ TCMT IO (Sort' Term)
newSortMeta
  SortKit{ isNameOfUniv } <- TCMT IO SortKit
forall (m :: * -> *). (HasBuiltins m, MonadTCError m) => m SortKit
sortKit
  case unScope e of
    A.Fun ExprInfo
i (Arg ArgInfo
info Expr
t) Expr
b -> do
      a <- (Maybe RewDom -> Type'' Term Term -> Dom' Term (Type'' Term Term))
-> (Maybe RewDom, Type'' Term Term) -> Dom' Term (Type'' Term Term)
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry (ArgInfo
-> Maybe RewDom -> Type'' Term Term -> Dom' Term (Type'' Term Term)
forall a. ArgInfo -> Maybe RewDom -> a -> Dom a
defaultArgDomRew ArgInfo
info) ((Maybe RewDom, Type'' Term Term) -> Dom' Term (Type'' Term Term))
-> TCMT IO (Maybe RewDom, Type'' Term Term)
-> TCMT IO (Dom' Term (Type'' Term Term))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
           Maybe Name
-> List1 ArgInfo
-> Expr
-> TCMT IO (Maybe RewDom, Type'' Term Term)
forall a.
(LensLock a, LensModality a, LensRewriteAnn a) =>
Maybe Name
-> List1 a -> Expr -> TCMT IO (Maybe RewDom, Type'' Term Term)
checkPiDomain Maybe Name
forall a. Maybe a
Nothing (ArgInfo
info ArgInfo -> [ArgInfo] -> List1 ArgInfo
forall a. a -> [a] -> NonEmpty a
:| []) Expr
t
      b <- isType_ b
      s <- inferFunSort a b
      let t' = Sort' Term -> Term -> Type'' Term Term
forall t a. Sort' t -> a -> Type'' t a
El Sort' Term
s (Term -> Type'' Term Term) -> Term -> Type'' Term Term
forall a b. (a -> b) -> a -> b
$ Dom' Term (Type'' Term Term) -> Abs (Type'' Term Term) -> Term
Pi Dom' Term (Type'' Term Term)
a (Abs (Type'' Term Term) -> Term) -> Abs (Type'' Term Term) -> Term
forall a b. (a -> b) -> a -> b
$ ArgName -> Type'' Term Term -> Abs (Type'' Term Term)
forall a. ArgName -> a -> Abs a
NoAbs ArgName
forall a. Underscore a => a
underscore Type'' Term Term
b
      hasPTSRule a (NoAbs underscore $ getSort b)
      --noFunctionsIntoSize t'
      return t'
    A.Pi ExprInfo
_ NonEmpty TypedBinding
tel Expr
e -> do
      (t0, t') <- Telescope
-> (Telescope -> TCM (Type'' Term Term, Type'' Term Term))
-> TCM (Type'' Term Term, Type'' Term Term)
forall a. Telescope -> (Telescope -> TCM a) -> TCM a
checkPiTelescope (NonEmpty TypedBinding -> [Item (NonEmpty TypedBinding)]
forall l. IsList l => l -> [Item l]
List1.toList NonEmpty TypedBinding
tel) ((Telescope -> TCM (Type'' Term Term, Type'' Term Term))
 -> TCM (Type'' Term Term, Type'' Term Term))
-> (Telescope -> TCM (Type'' Term Term, Type'' Term Term))
-> TCM (Type'' Term Term, Type'' Term Term)
forall a b. (a -> b) -> a -> b
$ \ Telescope
tel -> do
        t0  <- Type'' Term Term -> TCM (Type'' Term Term)
forall a (m :: * -> *).
(InstantiateFull a, MonadReduce m) =>
a -> m a
instantiateFull (Type'' Term Term -> TCM (Type'' Term Term))
-> TCM (Type'' Term Term) -> TCM (Type'' Term Term)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Expr -> TCM (Type'' Term Term)
isType_ Expr
e
        tel <- instantiateFull tel
        checkTelePiSort tel (getSort t0)
        return (t0, telePi tel t0)
      --noFunctionsIntoSize t'
      return t'

    A.Generalized Set1 QName
s Expr
e -> do
      (_, t') <- Set QName
-> TCM (Type'' Term Term) -> TCM ([Maybe QName], Type'' Term Term)
generalizeType (Set1 QName -> Set QName
forall a. NESet a -> Set a
Set1.toSet Set1 QName
s) (TCM (Type'' Term Term) -> TCM ([Maybe QName], Type'' Term Term))
-> TCM (Type'' Term Term) -> TCM ([Maybe QName], Type'' Term Term)
forall a b. (a -> b) -> a -> b
$ Expr -> TCM (Type'' Term Term)
isType_ Expr
e
      --noFunctionsIntoSize t'
      return t'

    -- Prop/(S)Set(ω)ᵢ
    A.Def' QName
x Suffix
suffix
      | Just (UnivSize
sz, Univ
u) <- QName -> Maybe (UnivSize, Univ)
isNameOfUniv QName
x
      , let n :: Integer
n = Suffix -> Integer
suffixToLevel Suffix
suffix
      -> do
        Univ -> TCM ()
univChecks Univ
u
        Type'' Term Term -> TCM (Type'' Term Term)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Type'' Term Term -> TCM (Type'' Term Term))
-> (Sort' Term -> Type'' Term Term)
-> Sort' Term
-> TCM (Type'' Term Term)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sort' Term -> Type'' Term Term
sort (Sort' Term -> TCM (Type'' Term Term))
-> Sort' Term -> TCM (Type'' Term Term)
forall a b. (a -> b) -> a -> b
$ case UnivSize
sz of
          UnivSize
USmall -> Univ -> Level' Term -> Sort' Term
forall t. Univ -> Level' t -> Sort' t
Univ Univ
u (Level' Term -> Sort' Term) -> Level' Term -> Sort' Term
forall a b. (a -> b) -> a -> b
$ Integer -> Level' Term
ClosedLevel Integer
n
          UnivSize
ULarge -> Univ -> Integer -> Sort' Term
forall t. Univ -> Integer -> Sort' t
Inf Univ
u Integer
n

    -- Prop/(S)et ℓ
    A.App AppInfo
i Expr
s Arg (Named_ Expr)
arg
      | Arg (Named_ Expr) -> Bool
forall a. LensHiding a => a -> Bool
visible Arg (Named_ Expr)
arg,
        A.Def QName
x <- Expr -> Expr
unScope Expr
s,
        Just (UnivSize
USmall, Univ
u) <- QName -> Maybe (UnivSize, Univ)
isNameOfUniv QName
x -> do
      Univ -> TCM ()
univChecks Univ
u
      TCMT IO Bool -> TCM () -> TCM ()
forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
unlessM TCMT IO Bool
forall (m :: * -> *). HasOptions m => m Bool
hasUniversePolymorphism (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ TypeError -> TCM ()
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError TypeError
NeedOptionUniversePolymorphism
      -- allow ShapeIrrelevant variables when checking level
      --   Set : (ShapeIrrelevant) Level -> Set\omega
      Relevance -> TCM (Type'' Term Term) -> TCM (Type'' Term Term)
forall (tcm :: * -> *) r a.
(MonadTCEnv tcm, LensRelevance r) =>
r -> tcm a -> tcm a
applyRelevanceToContext Relevance
shapeIrrelevant (TCM (Type'' Term Term) -> TCM (Type'' Term Term))
-> TCM (Type'' Term Term) -> TCM (Type'' Term Term)
forall a b. (a -> b) -> a -> b
$
        Sort' Term -> Type'' Term Term
sort (Sort' Term -> Type'' Term Term)
-> (Level' Term -> Sort' Term) -> Level' Term -> Type'' Term Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Univ -> Level' Term -> Sort' Term
forall t. Univ -> Level' t -> Sort' t
Univ Univ
u (Level' Term -> Type'' Term Term)
-> TCMT IO (Level' Term) -> TCM (Type'' Term Term)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Arg (Named_ Expr) -> TCMT IO (Level' Term)
checkLevel Arg (Named_ Expr)
arg

    -- Issue #707: Check an existing interaction point
    A.QuestionMark MetaInfo
minfo InteractionId
ii -> TCMT IO (Maybe MetaId)
-> TCM (Type'' Term Term)
-> (MetaId -> TCM (Type'' Term Term))
-> TCM (Type'' Term Term)
forall (m :: * -> *) a b.
Monad m =>
m (Maybe a) -> m b -> (a -> m b) -> m b
caseMaybeM (InteractionId -> TCMT IO (Maybe MetaId)
forall (m :: * -> *).
ReadTCState m =>
InteractionId -> m (Maybe MetaId)
lookupInteractionMeta InteractionId
ii) TCM (Type'' Term Term)
fallback ((MetaId -> TCM (Type'' Term Term)) -> TCM (Type'' Term Term))
-> (MetaId -> TCM (Type'' Term Term)) -> TCM (Type'' Term Term)
forall a b. (a -> b) -> a -> b
$ \ MetaId
x -> do
      -- -- | Just x <- A.metaNumber minfo -> do
      ArgName -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m ()
reportSDoc ArgName
"tc.ip" Int
20 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
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
"Rechecking meta "
        , MetaId -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => MetaId -> m Doc
prettyTCM MetaId
x
        , ArgName -> TCMT IO Doc
forall (m :: * -> *). Applicative m => ArgName -> m Doc
text (ArgName -> TCMT IO Doc) -> ArgName -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ ArgName
" for interaction point " ArgName -> ArgName -> ArgName
forall a. [a] -> [a] -> [a]
++! InteractionId -> ArgName
forall a. Show a => a -> ArgName
show InteractionId
ii
        ]
      mv <- MetaId -> TCMT IO MetaVariable
forall (m :: * -> *).
(HasCallStack, MonadDebug m, ReadTCState m) =>
MetaId -> m MetaVariable
lookupLocalMeta MetaId
x
      let s0 = Judgement MetaId -> Type'' Term Term
forall a. Judgement a -> Type'' Term Term
jMetaType (Judgement MetaId -> Type'' Term Term)
-> (MetaVariable -> Judgement MetaId)
-> MetaVariable
-> Type'' Term Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. MetaVariable -> Judgement MetaId
mvJudgement (MetaVariable -> Type'' Term Term)
-> MetaVariable -> Type'' Term Term
forall a b. (a -> b) -> a -> b
$ MetaVariable
mv
      -- Andreas, 2016-10-14, issue #2257
      -- The meta was created in a context of length @n@.
      let n  = Context' ContextEntry -> Int
forall a. Context' a -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (Context' ContextEntry -> Int)
-> (MetaVariable -> Context' ContextEntry) -> MetaVariable -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Getting (Context' ContextEntry) TCEnv (Context' ContextEntry)
-> TCEnv -> Context' ContextEntry
forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a
view Getting (Context' ContextEntry) TCEnv (Context' ContextEntry)
Lens' TCEnv (Context' ContextEntry)
eContext (TCEnv -> Context' ContextEntry)
-> (MetaVariable -> TCEnv) -> MetaVariable -> Context' ContextEntry
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Closure (Range' SrcFile) -> TCEnv
forall a. Closure a -> TCEnv
clEnv (Closure (Range' SrcFile) -> TCEnv)
-> (MetaVariable -> Closure (Range' SrcFile))
-> MetaVariable
-> TCEnv
forall b c a. (b -> c) -> (a -> b) -> a -> c
. MetaInfo -> Closure (Range' SrcFile)
miClosRange (MetaInfo -> Closure (Range' SrcFile))
-> (MetaVariable -> MetaInfo)
-> MetaVariable
-> Closure (Range' SrcFile)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. MetaVariable -> MetaInfo
mvInfo (MetaVariable -> Int) -> MetaVariable -> Int
forall a b. (a -> b) -> a -> b
$ MetaVariable
mv
      (vs, rest) <- splitAt' n <$> getContextArgs

      let oldCxtNames = (Name -> Name) -> [Name] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map' Name -> Name
nameCanonical ([Name] -> [Name]) -> [Name] -> [Name]
forall a b. (a -> b) -> a -> b
$ Context' ContextEntry -> [Name]
contextNames' (Context' ContextEntry -> [Name])
-> Context' ContextEntry -> [Name]
forall a b. (a -> b) -> a -> b
$ Getting (Context' ContextEntry) TCEnv (Context' ContextEntry)
-> TCEnv -> Context' ContextEntry
forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a
view Getting (Context' ContextEntry) TCEnv (Context' ContextEntry)
Lens' TCEnv (Context' ContextEntry)
eContext
                      (TCEnv -> Context' ContextEntry) -> TCEnv -> Context' ContextEntry
forall a b. (a -> b) -> a -> b
$ Closure (Range' SrcFile) -> TCEnv
forall a. Closure a -> TCEnv
clEnv (Closure (Range' SrcFile) -> TCEnv)
-> Closure (Range' SrcFile) -> TCEnv
forall a b. (a -> b) -> a -> b
$ MetaInfo -> Closure (Range' SrcFile)
miClosRange (MetaInfo -> Closure (Range' SrcFile))
-> MetaInfo -> Closure (Range' SrcFile)
forall a b. (a -> b) -> a -> b
$ MetaVariable -> MetaInfo
mvInfo (MetaVariable -> MetaInfo) -> MetaVariable -> MetaInfo
forall a b. (a -> b) -> a -> b
$ MetaVariable
mv

      newCxtNames <- map' nameCanonical <$> getContextNames'

      reportSDoc "tc.ip" 20 $ vcat
        [ "  s0   = " <+> prettyTCM s0
        , "  vs   = " <+> prettyTCM vs
        , "  rest = " <+> prettyTCM rest
        , "  oldCxtNames = " <+> prettyTCM oldCxtNames
        , "  newCxtNames = " <+> prettyTCM newCxtNames
        ]
      -- We assume the meta variable use here is in an extension of the original context.
      -- If not we revert to the old buggy behavior of #707 (see test/Succeed/Issue2257b).
      if (not $ List.isPrefixOf oldCxtNames newCxtNames) then fallback else do
      s1  <- reduce =<< piApplyM s0 vs
      reportSDoc "tc.ip" 20 $ vcat
        [ "  s1   = " <+> prettyTCM s1
        ]
      reportSDoc "tc.ip" 70 $ vcat
        [ "  s1   = " <+> text (show s1)
        ]
      case unEl s1 of
        Sort Sort' Term
s -> Type'' Term Term -> TCM (Type'' Term Term)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Type'' Term Term -> TCM (Type'' Term Term))
-> Type'' Term Term -> TCM (Type'' Term Term)
forall a b. (a -> b) -> a -> b
$! Sort' Term -> Term -> Type'' Term Term
forall t a. Sort' t -> a -> Type'' t a
El Sort' Term
s (Term -> Type'' Term Term) -> Term -> Type'' Term Term
forall a b. (a -> b) -> a -> b
$! MetaId -> Elims -> Term
MetaV MetaId
x (Elims -> Term) -> Elims -> Term
forall a b. (a -> b) -> a -> b
$! (Arg Term -> Elim) -> [Arg Term] -> Elims
forall a b. (a -> b) -> [a] -> [b]
map' Arg Term -> Elim
forall a. Arg a -> Elim' a
Apply [Arg Term]
vs
        Term
_ -> TCM (Type'' Term Term)
forall a. HasCallStack => a
__IMPOSSIBLE__

    Expr
_ -> TCM (Type'' Term Term)
fallback

checkLevel :: NamedArg A.Expr -> TCM Level
checkLevel :: Arg (Named_ Expr) -> TCMT IO (Level' Term)
checkLevel Arg (Named_ Expr)
arg = do
  lvl <- TCM (Type'' Term Term)
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
m (Type'' Term Term)
levelType
  levelView =<< checkNamedArg arg lvl

-- | Ensure that a (freshly created) function type does not inhabit 'SizeUniv'.
--   Precondition:  When @noFunctionsIntoSize t tBlame@ is called,
--   we are in the context of @tBlame@ in order to print it correctly.
--   Not being in context of @t@ should not matter, as we are only
--   checking whether its sort reduces to 'SizeUniv'.
--
--   Currently UNUSED since SizeUniv is turned off (as of 2016).
{-
noFunctionsIntoSize :: Type -> Type -> TCM ()
noFunctionsIntoSize t tBlame = do
  reportSDoc "tc.fun" 20 $ do
    let El s (Pi dom b) = tBlame
    sep [ "created function type " <+> prettyTCM tBlame
        , "with pts rule (" <+> prettyTCM (getSort dom) <+>
                        "," <+> underAbstraction_ b (prettyTCM . getSort) <+>
                        "," <+> prettyTCM s <+> ")"
        ]
  s <- reduce $ getSort t
  when (s == SizeUniv) $ do
    -- Andreas, 2015-02-14
    -- We have constructed a function type in SizeUniv
    -- which is illegal to prevent issue 1428.
    typeError $ FunctionTypeInSizeUniv $ unEl tBlame
-}

-- | Check that an expression is a type which is equal to a given type.
isTypeEqualTo :: A.Expr -> Type -> TCM Type
isTypeEqualTo :: Expr -> Type'' Term Term -> TCM (Type'' Term Term)
isTypeEqualTo Expr
e0 Type'' Term Term
t = Expr -> TCM Expr
scopedExpr Expr
e0 TCM Expr
-> (Expr -> TCM (Type'' Term Term)) -> TCM (Type'' Term 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
  A.ScopedExpr{} -> TCM (Type'' Term Term)
forall a. HasCallStack => a
__IMPOSSIBLE__
  A.Underscore MetaInfo
i | Maybe MetaId -> Bool
forall a. Maybe a -> Bool
isNothing (MetaInfo -> Maybe MetaId
A.metaNumber MetaInfo
i) -> Type'' Term Term -> TCM (Type'' Term Term)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Type'' Term Term
t
  Expr
e -> TCM (Type'' Term Term) -> TCM (Type'' Term Term)
forall (m :: * -> *) a.
(MonadTCEnv m, HasOptions m, MonadDebug m) =>
m a -> m a
workOnTypes (TCM (Type'' Term Term) -> TCM (Type'' Term Term))
-> TCM (Type'' Term Term) -> TCM (Type'' Term Term)
forall a b. (a -> b) -> a -> b
$ do
    t' <- Expr -> Sort' Term -> TCM (Type'' Term Term)
isType Expr
e (Type'' Term Term -> Sort' Term
forall a. LensSort a => a -> Sort' Term
getSort Type'' Term Term
t)
    t' <$ leqType t t'

leqType_ :: Type -> Type -> TCM ()
leqType_ :: Type'' Term Term -> Type'' Term Term -> TCM ()
leqType_ Type'' Term Term
t Type'' Term Term
t' = TCM () -> TCM ()
forall (m :: * -> *) a.
(MonadTCEnv m, HasOptions m, MonadDebug m) =>
m a -> m a
workOnTypes (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ Type'' Term Term -> Type'' Term Term -> TCM ()
leqType Type'' Term Term
t Type'' Term Term
t'

---------------------------------------------------------------------------
-- * Telescopes
---------------------------------------------------------------------------

-- | We track whether a module telescope came from a data declaration because
--   data telescopes cannot contain tactic arguments (because they result
--   in slightly weird behaviour w.r.t. checking parameters of constructors
--   are fully general)
data ModTelOrigin = ModTelData | ModTelNotData
  deriving (ModTelOrigin -> ModTelOrigin -> Bool
(ModTelOrigin -> ModTelOrigin -> Bool)
-> (ModTelOrigin -> ModTelOrigin -> Bool) -> Eq ModTelOrigin
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: ModTelOrigin -> ModTelOrigin -> Bool
== :: ModTelOrigin -> ModTelOrigin -> Bool
$c/= :: ModTelOrigin -> ModTelOrigin -> Bool
/= :: ModTelOrigin -> ModTelOrigin -> Bool
Eq, Int -> ModTelOrigin -> ArgName -> ArgName
[ModTelOrigin] -> ArgName -> ArgName
ModTelOrigin -> ArgName
(Int -> ModTelOrigin -> ArgName -> ArgName)
-> (ModTelOrigin -> ArgName)
-> ([ModTelOrigin] -> ArgName -> ArgName)
-> Show ModTelOrigin
forall a.
(Int -> a -> ArgName -> ArgName)
-> (a -> ArgName) -> ([a] -> ArgName -> ArgName) -> Show a
$cshowsPrec :: Int -> ModTelOrigin -> ArgName -> ArgName
showsPrec :: Int -> ModTelOrigin -> ArgName -> ArgName
$cshow :: ModTelOrigin -> ArgName
show :: ModTelOrigin -> ArgName
$cshowList :: [ModTelOrigin] -> ArgName -> ArgName
showList :: [ModTelOrigin] -> ArgName -> ArgName
Show)

checkGeneralizeTelescope ::
     ModTelOrigin
       -- ^ Origin of telescope (i.e. if it came from a data declaration)
  -> Maybe ModuleName
       -- ^ The module the telescope belongs to (if any).
  -> A.GeneralizeTelescope
       -- ^ Telescope to check and add to the context for the continuation.
  -> ([Maybe Name] -> Telescope -> TCM a)
       -- ^ Continuation living in the extended context.
  -> TCM a
checkGeneralizeTelescope :: forall a.
ModTelOrigin
-> Maybe ModuleName
-> GeneralizeTelescope
-> ([Maybe Name] -> Telescope -> TCM a)
-> TCM a
checkGeneralizeTelescope ModTelOrigin
o Maybe ModuleName
mm (A.GeneralizeTel Map QName Name
vars Telescope
tel) =
    ((([Maybe Name], Telescope) -> TCMT IO a) -> TCMT IO a)
-> (([Maybe Name], Telescope) -> TCMT IO a) -> TCMT IO a
tr (Map QName Name
-> (forall a1. (Telescope -> TCM a1) -> TCM a1)
-> ([Maybe Name] -> Telescope -> TCMT IO a)
-> TCMT IO a
forall a.
Map QName Name
-> (forall a1. (Telescope -> TCM a1) -> TCM a1)
-> ([Maybe Name] -> Telescope -> TCM a)
-> TCM a
generalizeTelescope Map QName Name
vars (ModTelOrigin -> Telescope -> (Telescope -> TCM a1) -> TCM a1
forall a.
ModTelOrigin -> Telescope -> (Telescope -> TCM a) -> TCM a
checkTelescope ModTelOrigin
o Telescope
tel) (([Maybe Name] -> Telescope -> TCMT IO a) -> TCMT IO a)
-> ((([Maybe Name], Telescope) -> TCMT IO a)
    -> [Maybe Name] -> Telescope -> TCMT IO a)
-> (([Maybe Name], Telescope) -> TCMT IO a)
-> TCMT IO a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (([Maybe Name], Telescope) -> TCMT IO a)
-> [Maybe Name] -> Telescope -> TCMT IO a
forall a b c. ((a, b) -> c) -> a -> b -> c
curry) ((([Maybe Name], Telescope) -> TCMT IO a) -> TCMT IO a)
-> (([Maybe Name] -> Telescope -> TCMT IO a)
    -> ([Maybe Name], Telescope) -> TCMT IO a)
-> ([Maybe Name] -> Telescope -> TCMT IO a)
-> TCMT IO a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([Maybe Name] -> Telescope -> TCMT IO a)
-> ([Maybe Name], Telescope) -> TCMT IO a
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry
  where
    tr :: ((([Maybe Name], Telescope) -> TCMT IO a) -> TCMT IO a)
-> (([Maybe Name], Telescope) -> TCMT IO a) -> TCMT IO a
tr = Bool
-> (((([Maybe Name], Telescope) -> TCMT IO a) -> TCMT IO a)
    -> (([Maybe Name], Telescope) -> TCMT IO a) -> TCMT IO a)
-> ((([Maybe Name], Telescope) -> TCMT IO a) -> TCMT IO a)
-> (([Maybe Name], Telescope) -> TCMT IO a)
-> TCMT IO a
forall b a. IsBool b => b -> (a -> a) -> a -> a
applyUnless (Telescope -> Bool
forall a. Null a => a -> Bool
null Telescope
tel) ((((([Maybe Name], Telescope) -> TCMT IO a) -> TCMT IO a)
  -> (([Maybe Name], Telescope) -> TCMT IO a) -> TCMT IO a)
 -> ((([Maybe Name], Telescope) -> TCMT IO a) -> TCMT IO a)
 -> (([Maybe Name], Telescope) -> TCMT IO a)
 -> TCMT IO a)
-> (((([Maybe Name], Telescope) -> TCMT IO a) -> TCMT IO a)
    -> (([Maybe Name], Telescope) -> TCMT IO a) -> TCMT IO a)
-> ((([Maybe Name], Telescope) -> TCMT IO a) -> TCMT IO a)
-> (([Maybe Name], Telescope) -> TCMT IO a)
-> TCMT IO a
forall a b. (a -> b) -> a -> b
$ Maybe ModuleName
-> (ModuleName
    -> ((([Maybe Name], Telescope) -> TCMT IO a) -> TCMT IO a)
    -> (([Maybe Name], Telescope) -> TCMT IO a)
    -> TCMT IO a)
-> ((([Maybe Name], Telescope) -> TCMT IO a) -> TCMT IO a)
-> (([Maybe Name], Telescope) -> TCMT IO a)
-> TCMT IO a
forall b a. Maybe b -> (b -> a -> a) -> a -> a
applyWhenJust Maybe ModuleName
mm ((ModuleName
  -> ((([Maybe Name], Telescope) -> TCMT IO a) -> TCMT IO a)
  -> (([Maybe Name], Telescope) -> TCMT IO a)
  -> TCMT IO a)
 -> ((([Maybe Name], Telescope) -> TCMT IO a) -> TCMT IO a)
 -> (([Maybe Name], Telescope) -> TCMT IO a)
 -> TCMT IO a)
-> (ModuleName
    -> ((([Maybe Name], Telescope) -> TCMT IO a) -> TCMT IO a)
    -> (([Maybe Name], Telescope) -> TCMT IO a)
    -> TCMT IO a)
-> ((([Maybe Name], Telescope) -> TCMT IO a) -> TCMT IO a)
-> (([Maybe Name], Telescope) -> TCMT IO a)
-> TCMT IO a
forall a b. (a -> b) -> a -> b
$ \ ModuleName
m ->
      Call
-> ((([Maybe Name], Telescope) -> TCMT IO a) -> TCMT IO a)
-> (([Maybe Name], Telescope) -> TCMT IO a)
-> TCMT IO a
forall a b.
Call
-> ((a -> TCMT IO b) -> TCMT IO b) -> (a -> TCMT IO b) -> TCMT IO b
forall (m :: * -> *) a b.
MonadTrace m =>
Call -> ((a -> m b) -> m b) -> (a -> m b) -> m b
traceCallCPS (Call
 -> ((([Maybe Name], Telescope) -> TCMT IO a) -> TCMT IO a)
 -> (([Maybe Name], Telescope) -> TCMT IO a)
 -> TCMT IO a)
-> Call
-> ((([Maybe Name], Telescope) -> TCMT IO a) -> TCMT IO a)
-> (([Maybe Name], Telescope) -> TCMT IO a)
-> TCMT IO a
forall a b. (a -> b) -> a -> b
$ ModuleName -> Telescope -> Call
CheckModuleParameters ModuleName
m Telescope
tel

-- | Type check a (module) telescope.
--   Binds the variables defined by the telescope.
checkTelescope :: ModTelOrigin -> A.Telescope -> (Telescope -> TCM a) -> TCM a
checkTelescope :: forall a.
ModTelOrigin -> Telescope -> (Telescope -> TCM a) -> TCM a
checkTelescope ModTelOrigin
o = LamOrPi -> Telescope -> (Telescope -> TCM a) -> TCM a
forall a. LamOrPi -> Telescope -> (Telescope -> TCM a) -> TCM a
checkTelescope' (ModTelOrigin -> LamOrPi
LamNotPi ModTelOrigin
o)

-- | Type check the telescope of a dependent function type.
--   Binds the resurrected variables defined by the telescope.
--   The returned telescope is unmodified (not resurrected).
checkPiTelescope :: A.Telescope -> (Telescope -> TCM a) -> TCM a
checkPiTelescope :: forall a. Telescope -> (Telescope -> TCM a) -> TCM a
checkPiTelescope = LamOrPi -> Telescope -> (Telescope -> TCM a) -> TCM a
forall a. LamOrPi -> Telescope -> (Telescope -> TCM a) -> TCM a
checkTelescope' LamOrPi
PiNotLam

-- | Flag to control resurrection on domains.
data LamOrPi
  = LamNotPi ModTelOrigin
      -- ^ We are checking a module telescope.
      --   We pass into the type world to check the domain type.
      --   This resurrects the whole context.
  | PiNotLam
      -- ^ We are checking a telescope in a Pi-type.
      --   We stay in the term world, but add resurrected
      --   domains to the context to check the remaining
      --   domains and codomain of the Pi-type.
  deriving (LamOrPi -> LamOrPi -> Bool
(LamOrPi -> LamOrPi -> Bool)
-> (LamOrPi -> LamOrPi -> Bool) -> Eq LamOrPi
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: LamOrPi -> LamOrPi -> Bool
== :: LamOrPi -> LamOrPi -> Bool
$c/= :: LamOrPi -> LamOrPi -> Bool
/= :: LamOrPi -> LamOrPi -> Bool
Eq, Int -> LamOrPi -> ArgName -> ArgName
[LamOrPi] -> ArgName -> ArgName
LamOrPi -> ArgName
(Int -> LamOrPi -> ArgName -> ArgName)
-> (LamOrPi -> ArgName)
-> ([LamOrPi] -> ArgName -> ArgName)
-> Show LamOrPi
forall a.
(Int -> a -> ArgName -> ArgName)
-> (a -> ArgName) -> ([a] -> ArgName -> ArgName) -> Show a
$cshowsPrec :: Int -> LamOrPi -> ArgName -> ArgName
showsPrec :: Int -> LamOrPi -> ArgName -> ArgName
$cshow :: LamOrPi -> ArgName
show :: LamOrPi -> ArgName
$cshowList :: [LamOrPi] -> ArgName -> ArgName
showList :: [LamOrPi] -> ArgName -> ArgName
Show)

-- | Type check a telescope. Binds the variables defined by the telescope.
checkTelescope' :: LamOrPi -> A.Telescope -> (Telescope -> TCM a) -> TCM a
checkTelescope' :: forall a. LamOrPi -> Telescope -> (Telescope -> TCM a) -> TCM a
checkTelescope' LamOrPi
lamOrPi []        Telescope -> TCM a
ret = Telescope -> TCM a
ret Telescope
forall a. Tele a
EmptyTel
checkTelescope' LamOrPi
lamOrPi (TypedBinding
b : Telescope
tel) Telescope -> TCM a
ret =
    LamOrPi -> TypedBinding -> (Telescope -> TCM a) -> TCM a
forall a. LamOrPi -> TypedBinding -> (Telescope -> TCM a) -> TCM a
checkTypedBindings LamOrPi
lamOrPi TypedBinding
b ((Telescope -> TCM a) -> TCM a) -> (Telescope -> TCM a) -> TCM a
forall a b. (a -> b) -> a -> b
$ \Telescope
tel1 ->
    LamOrPi -> Telescope -> (Telescope -> TCM a) -> TCM a
forall a. LamOrPi -> Telescope -> (Telescope -> TCM a) -> TCM a
checkTelescope' LamOrPi
lamOrPi Telescope
tel  ((Telescope -> TCM a) -> TCM a) -> (Telescope -> TCM a) -> TCM a
forall a b. (a -> b) -> a -> b
$ \Telescope
tel2 ->
        Telescope -> TCM a
ret (Telescope -> TCM a) -> Telescope -> TCM a
forall a b. (a -> b) -> a -> b
$ Telescope -> Telescope -> Telescope
forall t. Abstract t => Telescope -> t -> t
abstract Telescope
tel1 Telescope
tel2

-- | Check the domain of a function type.
--   Used in @checkTypedBindings@ and to typecheck @A.Fun@ cases.
checkDomain :: (LensLock a, LensModality a, LensRewriteAnn a)
  => LamOrPi -> Maybe Name -> List1 a -> A.Expr -> TCM (Maybe RewDom, Type)
checkDomain :: forall a.
(LensLock a, LensModality a, LensRewriteAnn a) =>
LamOrPi
-> Maybe Name
-> List1 a
-> Expr
-> TCMT IO (Maybe RewDom, Type'' Term Term)
checkDomain LamOrPi
lamOrPi Maybe Name
n List1 a
xs Expr
e = do
    -- Get cohesion and quantity of arguments, as well as if they are local
    -- rewrite rules. All of these properties should all be equal because
    -- they come from the same annotated Π-type.
    let (Cohesion
c :| [Cohesion]
cs) = (a -> Cohesion) -> List1 a -> NonEmpty Cohesion
forall a b. (a -> b) -> NonEmpty a -> NonEmpty b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Modality -> Cohesion
forall a. LensCohesion a => a -> Cohesion
getCohesion (Modality -> Cohesion) -> (a -> Modality) -> a -> Cohesion
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Modality
forall a. LensModality a => a -> Modality
getModality) List1 a
xs
    Bool -> TCM () -> TCM ()
forall b (m :: * -> *). (IsBool b, Monad m) => b -> m () -> m ()
unless ((Cohesion -> Bool) -> [Cohesion] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (Cohesion
c Cohesion -> Cohesion -> Bool
forall a. Eq a => a -> a -> Bool
==) [Cohesion]
cs) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ TCM ()
forall a. HasCallStack => a
__IMPOSSIBLE__

    let (Quantity
q :| [Quantity]
qs) = (a -> Quantity) -> List1 a -> NonEmpty Quantity
forall a b. (a -> b) -> NonEmpty a -> NonEmpty b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Modality -> Quantity
forall a. LensQuantity a => a -> Quantity
getQuantity (Modality -> Quantity) -> (a -> Modality) -> a -> Quantity
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Modality
forall a. LensModality a => a -> Modality
getModality) List1 a
xs
    Bool -> TCM () -> TCM ()
forall b (m :: * -> *). (IsBool b, Monad m) => b -> m () -> m ()
unless ((Quantity -> Bool) -> [Quantity] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (Quantity
q Quantity -> Quantity -> Bool
forall a. Eq a => a -> a -> Bool
==) [Quantity]
qs) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ TCM ()
forall a. HasCallStack => a
__IMPOSSIBLE__

    let (RewriteAnn
r :| [RewriteAnn]
rs) = (a -> RewriteAnn) -> List1 a -> NonEmpty RewriteAnn
forall a b. (a -> b) -> NonEmpty a -> NonEmpty b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (a -> RewriteAnn
forall a. LensRewriteAnn a => a -> RewriteAnn
getRewriteAnn) List1 a
xs
    Bool -> TCM () -> TCM ()
forall b (m :: * -> *). (IsBool b, Monad m) => b -> m () -> m ()
unless ((RewriteAnn -> Bool) -> [RewriteAnn] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (RewriteAnn
r RewriteAnn -> RewriteAnn -> Bool
forall a. Eq a => a -> a -> Bool
==) [RewriteAnn]
rs) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ TCM ()
forall a. HasCallStack => a
__IMPOSSIBLE__

    -- Also get whether the domain is a local rewrite rule. If it is, and there
    -- are multiple arguments, we warn that this is unnecessary

    t <- Quantity -> TCM (Type'' Term Term) -> TCM (Type'' Term Term)
forall (tcm :: * -> *) q a.
(MonadTCEnv tcm, LensQuantity q) =>
q -> tcm a -> tcm a
applyQuantityToJudgement Quantity
q (TCM (Type'' Term Term) -> TCM (Type'' Term Term))
-> TCM (Type'' Term Term) -> TCM (Type'' Term Term)
forall a b. (a -> b) -> a -> b
$
         Cohesion -> TCM (Type'' Term Term) -> TCM (Type'' Term Term)
forall (tcm :: * -> *) m a.
(MonadTCEnv tcm, LensCohesion m) =>
m -> tcm a -> tcm a
applyCohesionToContext Cohesion
c (TCM (Type'' Term Term) -> TCM (Type'' Term Term))
-> TCM (Type'' Term Term) -> TCM (Type'' Term Term)
forall a b. (a -> b) -> a -> b
$
         TCMT IO Bool
-> (TCM (Type'' Term Term) -> TCM (Type'' Term Term))
-> TCM (Type'' Term Term)
-> TCM (Type'' Term Term)
forall b (m :: * -> *) a.
(IsBool b, Monad m) =>
m b -> (m a -> m a) -> m a -> m a
applyWhenM (PragmaOptions -> Bool
optPolarity (PragmaOptions -> Bool) -> TCMT IO PragmaOptions -> TCMT IO Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCMT IO PragmaOptions
forall (m :: * -> *). HasOptions m => m PragmaOptions
pragmaOptions) (PolarityModality
-> TCM (Type'' Term Term) -> TCM (Type'' Term Term)
forall (tcm :: * -> *) p a.
(MonadTCEnv tcm, LensModalPolarity p) =>
p -> tcm a -> tcm a
applyPolarityToContext PolarityModality
negativePolarity) (TCM (Type'' Term Term) -> TCM (Type'' Term Term))
-> TCM (Type'' Term Term) -> TCM (Type'' Term Term)
forall a b. (a -> b) -> a -> b
$
         LamOrPi -> TCM (Type'' Term Term) -> TCM (Type'' Term Term)
forall {m :: * -> *} {a}.
(MonadTCEnv m, HasOptions m, MonadDebug m) =>
LamOrPi -> m a -> m a
modEnv LamOrPi
lamOrPi (TCM (Type'' Term Term) -> TCM (Type'' Term Term))
-> TCM (Type'' Term Term) -> TCM (Type'' Term Term)
forall a b. (a -> b) -> a -> b
$ Expr -> TCM (Type'' Term Term)
isType_ Expr
e
    -- Andrea TODO: also make sure that LockUniv implies IsLock
    when (any (\a
x -> case a -> Lock
forall a. LensLock a => a -> Lock
getLock a
x of { IsLock{} -> Bool
True ; Lock
_ -> Bool
False }) xs) $ do
         -- Solves issue #5033
        unlessM (isJust <$> getName' builtinLockUniv) $ do
          typeError $ NoBindingForPrimitive builtinLockUniv

        equalSort (getSort t) LockUniv

    cxt <- getContext
    let s = Context' ContextEntry
-> Maybe Name -> Type'' Term Term -> RewriteSource
LocalRewrite Context' ContextEntry
cxt Maybe Name
n Type'' Term Term
t

  -- For now, we disallow '@rewrite' domains on pi types
  -- In the future, this should be allowed only when the pi type is not in
  -- higher-order position (checked syntactically)
    r <- case lamOrPi of
      LamOrPi
PiNotLam | RewriteAnn -> Bool
forall a. LensRewriteAnn a => a -> Bool
isRewrite RewriteAnn
r -> RewriteAnn
IsNotRewrite RewriteAnn -> TCMT IO (Maybe (ZonkAny 0)) -> TCMT IO RewriteAnn
forall a b. a -> TCMT IO b -> TCMT IO a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$
        MaybeT (TCMT IO) (ZonkAny 0) -> TCMT IO (Maybe (ZonkAny 0))
forall (m :: * -> *) a. MaybeT m a -> m (Maybe a)
runMaybeT (RewriteSource
-> IllegalRewriteRuleReason -> MaybeT (TCMT IO) (ZonkAny 0)
forall (m :: * -> *) a.
MonadWarning m =>
RewriteSource -> IllegalRewriteRuleReason -> MaybeT m a
illegalRule RewriteSource
s IllegalRewriteRuleReason
LocalRewriteOutsideTelescope)
      LamOrPi
_                      -> RewriteAnn -> TCMT IO RewriteAnn
forall a. a -> TCMT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure RewriteAnn
r

    eq  <- checkEquationValid s r t
    rew <- traverse (checkLocalRewriteRule s) eq
    -- We do not (currently) distinguish failing to elaborate to a LocalEquation
    -- from failing to elaborate to a RewriteRule. In the case we have
    -- a valid LocalEquation, but failed to produce a RewriteRule, we could
    -- technically still store the LocalEquation and check the convertibility
    -- constraint at call sites. I don't think this is super important, but
    -- maybe worth trying in future.
    let rDom = LocalEquation' Term -> Maybe RewriteRule -> RewDom
forall t. LocalEquation' t -> Maybe RewriteRule -> RewDom' t
RewDom (LocalEquation' Term -> Maybe RewriteRule -> RewDom)
-> Maybe (LocalEquation' Term)
-> Maybe (Maybe RewriteRule -> RewDom)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe (LocalEquation' Term)
eq Maybe (Maybe RewriteRule -> RewDom)
-> Maybe (Maybe RewriteRule) -> Maybe RewDom
forall a b. Maybe (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (RewriteRule -> Maybe RewriteRule)
-> Maybe RewriteRule -> Maybe (Maybe RewriteRule)
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap RewriteRule -> Maybe RewriteRule
forall a. a -> Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Maybe (Maybe RewriteRule) -> Maybe RewriteRule
forall (m :: * -> *) a. Monad m => m (m a) -> m a
join Maybe (Maybe RewriteRule)
rew)
    whenJust rDom \RewDom
rDom' -> ArgName -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m ()
reportSDoc ArgName
"rewriting" Int
30 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$
      TCMT IO Doc
"Successfully elaborated: " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> LocalEquation' Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => LocalEquation' Term -> m Doc
prettyTCM (RewDom -> LocalEquation' Term
forall t. RewDom' t -> LocalEquation' t
rewDomEq RewDom
rDom') TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+>
        TCMT IO Doc
" into a rewrite rule"

    return (rDom, t)
  where
        -- if we are checking a typed lambda, we resurrect before we check the
        -- types, but do not modify the new context entries
        -- otherwise, if we are checking a pi, we do not resurrect, but
        -- modify the new context entries
        modEnv :: LamOrPi -> m a -> m a
modEnv (LamNotPi ModTelOrigin
_) = m a -> m a
forall (m :: * -> *) a.
(MonadTCEnv m, HasOptions m, MonadDebug m) =>
m a -> m a
workOnTypes
        modEnv LamOrPi
PiNotLam     = m a -> m a
forall a. a -> a
id

checkPiDomain :: (LensLock a, LensModality a,  LensRewriteAnn a)
              => Maybe Name -> List1 a -> A.Expr -> TCM (Maybe RewDom, Type)
checkPiDomain :: forall a.
(LensLock a, LensModality a, LensRewriteAnn a) =>
Maybe Name
-> List1 a -> Expr -> TCMT IO (Maybe RewDom, Type'' Term Term)
checkPiDomain = LamOrPi
-> Maybe Name
-> List1 a
-> Expr
-> TCMT IO (Maybe RewDom, Type'' Term Term)
forall a.
(LensLock a, LensModality a, LensRewriteAnn a) =>
LamOrPi
-> Maybe Name
-> List1 a
-> Expr
-> TCMT IO (Maybe RewDom, Type'' Term Term)
checkDomain LamOrPi
PiNotLam

-- | Check a typed binding and extends the context with the bound variables.
--   The telescope passed to the continuation is valid in the original context.
--
--   Parametrized by a flag whether we check a typed lambda or a Pi. This flag
--   is needed for irrelevance.

checkTypedBindings :: LamOrPi -> A.TypedBinding -> (Telescope -> TCM a) -> TCM a
checkTypedBindings :: forall a. LamOrPi -> TypedBinding -> (Telescope -> TCM a) -> TCM a
checkTypedBindings LamOrPi
lamOrPi (A.TBind Range' SrcFile
r TypedBindingInfo
tac List1 (Arg (Named_ (Binder' BindName)))
xps Expr
e) Telescope -> TCM a
ret = do
    let xs :: NonEmpty (NamedArg Name)
xs = (Arg (Named_ (Binder' BindName)) -> NamedArg Name)
-> List1 (Arg (Named_ (Binder' BindName)))
-> NonEmpty (NamedArg Name)
forall a b. (a -> b) -> NonEmpty a -> NonEmpty b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Binder' BindName -> Name)
-> Arg (Named_ (Binder' BindName)) -> NamedArg Name
forall a b. (a -> b) -> NamedArg a -> NamedArg b
updateNamedArg ((Binder' BindName -> Name)
 -> Arg (Named_ (Binder' BindName)) -> NamedArg Name)
-> (Binder' BindName -> Name)
-> Arg (Named_ (Binder' BindName))
-> NamedArg Name
forall a b. (a -> b) -> a -> b
$ BindName -> Name
A.unBind (BindName -> Name)
-> (Binder' BindName -> BindName) -> Binder' BindName -> Name
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Binder' BindName -> BindName
forall a. Binder' a -> a
A.binderName) List1 (Arg (Named_ (Binder' BindName)))
xps
    tac <- (Ranged Expr -> TCMT IO Term)
-> Maybe (Ranged Expr) -> 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 (LamOrPi -> Ranged Expr -> TCMT IO Term
checkTacticAttribute LamOrPi
lamOrPi) (Maybe (Ranged Expr) -> TCMT IO (Maybe Term))
-> Maybe (Ranged Expr) -> TCMT IO (Maybe Term)
forall a b. (a -> b) -> a -> b
$
      TacticAttribute' Expr -> Maybe (Ranged Expr)
forall a. TacticAttribute' a -> Maybe (Ranged a)
theTacticAttribute (TacticAttribute' Expr -> Maybe (Ranged Expr))
-> TacticAttribute' Expr -> Maybe (Ranged Expr)
forall a b. (a -> b) -> a -> b
$ TypedBindingInfo -> TacticAttribute' Expr
tbTacticAttr TypedBindingInfo
tac
    whenJust tac $ \ Term
t -> ArgName -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m ()
reportSDoc ArgName
"tc.term.tactic" Int
30 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"Checked tactic attribute:" 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
t
    -- Andreas, 2011-04-26 irrelevant function arguments may appear
    -- non-strictly in the codomain type
    -- 2011-10-04 if flag --experimental-irrelevance is set
    experimental <- optExperimentalIrrelevance <$> pragmaOptions

    -- We pick one of the names to report local rewrite errors on
    let x = BindName -> Name
unBind (BindName -> Name) -> BindName -> Name
forall a b. (a -> b) -> a -> b
$ Binder' BindName -> BindName
forall a. Binder' a -> a
binderName (Binder' BindName -> BindName) -> Binder' BindName -> BindName
forall a b. (a -> b) -> a -> b
$ Arg (Named_ (Binder' BindName)) -> Binder' BindName
forall a. NamedArg a -> a
namedArg (Arg (Named_ (Binder' BindName)) -> Binder' BindName)
-> Arg (Named_ (Binder' BindName)) -> Binder' BindName
forall a b. (a -> b) -> a -> b
$ List1 (Arg (Named_ (Binder' BindName)))
-> Arg (Named_ (Binder' BindName))
forall a. NonEmpty a -> a
List1.head List1 (Arg (Named_ (Binder' BindName)))
xps
    (rew, t) <- checkDomain lamOrPi (Just x) xps e
    whenJust rew $ \RewDom
r -> ArgName -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m ()
reportSDoc ArgName
"rewriting" Int
30 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"Checked local rewrite:" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> LocalEquation' Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => LocalEquation' Term -> m Doc
prettyTCM (RewDom -> LocalEquation' Term
forall t. RewDom' t -> LocalEquation' t
rewDomEq RewDom
r)

    -- Jesper, 2019-02-12, Issue #3534: warn if the type of an
    -- instance argument does not have the right shape
    List1.unlessNull (List1.filter isInstance xps) $ \ List1 (Arg (Named_ (Binder' BindName)))
ixs -> do
      (tel, _, target) <- Type'' Term Term -> TCM (Telescope, Term, OutputTypeName)
getOutputTypeName Type'' Term Term
t
      case target of
        OutputTypeName{} -> () -> TCM ()
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
        OutputTypeVar{}  -> () -> TCM ()
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
        OutputTypeNameNotYetKnown{} -> () -> TCM ()
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
        OutputTypeVisiblePi{} -> Expr -> TCM () -> TCM ()
forall (m :: * -> *) x a.
(MonadTrace m, HasRange x) =>
x -> m a -> m a
setCurrentRange Expr
e (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$
          Warning -> TCM ()
forall (m :: * -> *).
(HasCallStack, MonadWarning m) =>
Warning -> m ()
warning (Warning -> TCM ()) -> (Doc -> Warning) -> Doc -> TCM ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> Warning
InstanceArgWithExplicitArg (Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< TypedBinding -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => TypedBinding -> m Doc
prettyTCM (Range' SrcFile
-> List1 (Arg (Named_ (Binder' BindName))) -> Expr -> TypedBinding
A.mkTBind Range' SrcFile
r List1 (Arg (Named_ (Binder' BindName)))
ixs Expr
e)
        OutputTypeName
NoOutputTypeName -> Expr -> TCM () -> TCM ()
forall (m :: * -> *) x a.
(MonadTrace m, HasRange x) =>
x -> m a -> m a
setCurrentRange Expr
e (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$
          Warning -> TCM ()
forall (m :: * -> *).
(HasCallStack, MonadWarning m) =>
Warning -> m ()
warning (Warning -> TCM ()) -> (Doc -> Warning) -> Doc -> TCM ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> Warning
InstanceNoOutputTypeName (Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< TypedBinding -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => TypedBinding -> m Doc
prettyTCM (Range' SrcFile
-> List1 (Arg (Named_ (Binder' BindName))) -> Expr -> TypedBinding
A.mkTBind Range' SrcFile
r List1 (Arg (Named_ (Binder' BindName)))
ixs Expr
e)

    let setTacRew Maybe t
tac Maybe (RewDom' t)
rew Dom' t e
dom = Dom' t e
dom Dom' t e -> (Dom' t e -> Dom' t e) -> Dom' t e
forall a b. a -> (a -> b) -> b
& (Maybe t -> Identity (Maybe t)) -> Dom' t e -> Identity (Dom' t e)
forall t e (f :: * -> *).
Functor f =>
(Maybe t -> f (Maybe t)) -> Dom' t e -> f (Dom' t e)
dTactic ((Maybe t -> Identity (Maybe t))
 -> Dom' t e -> Identity (Dom' t e))
-> Maybe t -> Dom' t e -> Dom' t e
forall s t a b. ASetter s t a b -> b -> s -> t
.~ Maybe t
tac Dom' t e -> (Dom' t e -> Dom' t e) -> Dom' t e
forall a b. a -> (a -> b) -> b
& (Maybe (RewDom' t) -> Identity (Maybe (RewDom' t)))
-> Dom' t e -> Identity (Dom' t e)
forall t e (f :: * -> *).
Functor f =>
(Maybe (RewDom' t) -> f (Maybe (RewDom' t)))
-> Dom' t e -> f (Dom' t e)
dRew ((Maybe (RewDom' t) -> Identity (Maybe (RewDom' t)))
 -> Dom' t e -> Identity (Dom' t e))
-> Maybe (RewDom' t) -> Dom' t e -> Dom' t e
forall s t a b. ASetter s t a b -> b -> s -> t
.~ Maybe (RewDom' t)
rew
        setTacRewTel Maybe t
tac Maybe (RewDom' t)
rew Tele (Dom' t e)
EmptyTel            = Tele (Dom' t e)
forall a. Tele a
EmptyTel
        setTacRewTel Maybe t
tac Maybe (RewDom' t)
rew (ExtendTel Dom' t e
dom Abs (Tele (Dom' t e))
tel) =
          Dom' t e -> Abs (Tele (Dom' t e)) -> Tele (Dom' t e)
forall a. a -> Abs (Tele a) -> Tele a
ExtendTel (Maybe t -> Maybe (RewDom' t) -> Dom' t e -> Dom' t e
forall {t} {e}.
Maybe t -> Maybe (RewDom' t) -> Dom' t e -> Dom' t e
setTacRew Maybe t
tac Maybe (RewDom' t)
rew Dom' t e
dom) (Abs (Tele (Dom' t e)) -> Tele (Dom' t e))
-> Abs (Tele (Dom' t e)) -> Tele (Dom' t e)
forall a b. (a -> b) -> a -> b
$
            Maybe t -> Maybe (RewDom' t) -> Tele (Dom' t e) -> Tele (Dom' t e)
setTacRewTel (Int -> Maybe t -> Maybe t
forall a. Subst a => Int -> a -> a
raise Int
1 Maybe t
tac) (Int -> Maybe (RewDom' t) -> Maybe (RewDom' t)
forall a. Subst a => Int -> a -> a
raise Int
1 Maybe (RewDom' t)
rew) (Tele (Dom' t e) -> Tele (Dom' t e))
-> Abs (Tele (Dom' t e)) -> Abs (Tele (Dom' t e))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Abs (Tele (Dom' t e))
tel
        -- We need to convert to Dom and set the domTactic and domRew fields
        -- here in order to not drop @tactic and @rewrite annotations
        xs' = Maybe Term -> Maybe RewDom -> Dom' Term Name -> Dom' Term Name
forall {t} {e}.
Maybe t -> Maybe (RewDom' t) -> Dom' t e -> Dom' t e
setTacRew Maybe Term
tac Maybe RewDom
rew
                (Dom' Term Name -> Dom' Term Name)
-> (NamedArg Name -> Dom' Term Name)
-> NamedArg Name
-> Dom' Term Name
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NamedArg Name -> Dom' Term Name
domNameFromNamedArgName
                (NamedArg Name -> Dom' Term Name)
-> (NamedArg Name -> NamedArg Name)
-> NamedArg Name
-> Dom' Term Name
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LamOrPi -> Bool -> NamedArg Name -> NamedArg Name
forall {a} {b}.
(LensModalPolarity a, IsBool b, LensRelevance a) =>
LamOrPi -> b -> a -> a
modMod LamOrPi
lamOrPi Bool
experimental
              (NamedArg Name -> Dom' Term Name)
-> NonEmpty (NamedArg Name) -> NonEmpty (Dom' Term Name)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> NonEmpty (NamedArg Name)
xs
    let tel = Maybe Term -> Maybe RewDom -> Telescope -> Telescope
forall {t} {e}.
Subst t =>
Maybe t -> Maybe (RewDom' t) -> Tele (Dom' t e) -> Tele (Dom' t e)
setTacRewTel Maybe Term
tac Maybe RewDom
rew (Telescope -> Telescope) -> Telescope -> Telescope
forall a b. (a -> b) -> a -> b
$ NonEmpty (NamedArg Name) -> Type'' Term Term -> Telescope
namedBindsToTel1 NonEmpty (NamedArg Name)
xs Type'' Term Term
t

    addContext (xs', t) $ addTypedPatterns xps (ret tel)

    where
        -- if we are checking a typed lambda, we resurrect before we check the
        -- types, but do not modify the new context entries
        -- otherwise, if we are checking a pi, we do not resurrect, but
        -- modify the new context entries
        modMod :: LamOrPi -> b -> a -> a
modMod LamOrPi
PiNotLam b
xp =
          PolarityModality -> a -> a
forall a. LensModalPolarity a => PolarityModality -> a -> a
inverseApplyPolarity (ModalPolarity -> PolarityModality
withStandardLock ModalPolarity
UnusedPolarity) (a -> a) -> (a -> a) -> a -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
          b -> (a -> a) -> a -> a
forall b a. IsBool b => b -> (a -> a) -> a -> a
applyWhen b
xp ((Relevance -> Relevance) -> a -> a
forall a. LensRelevance a => (Relevance -> Relevance) -> a -> a
mapRelevance Relevance -> Relevance
irrelevantToShapeIrrelevant)
        modMod (LamNotPi ModTelOrigin
_) b
_ = a -> a
forall a. a -> a
id

checkTypedBindings LamOrPi
lamOrPi (A.TLet Range' SrcFile
_ List1 LetBinding
lbs) Telescope -> TCM a
ret = do
  List1 LetBinding -> TCM a -> TCM a
forall (t :: * -> *) a.
Foldable t =>
t LetBinding -> TCM a -> TCM a
checkLetBindings List1 LetBinding
lbs (Telescope -> TCM a
ret Telescope
forall a. Tele a
EmptyTel)

-- | After a typed binding has been checked, add the patterns it binds
addTypedPatterns :: List1 (NamedArg A.Binder) -> TCM a -> TCM a
addTypedPatterns :: forall a. List1 (Arg (Named_ (Binder' BindName))) -> TCM a -> TCM a
addTypedPatterns List1 (Arg (Named_ (Binder' BindName)))
xps TCM a
ret = do
  let
    ps :: [(Pattern' Expr, BindName)]
ps  = (Arg (Named_ (Binder' BindName))
 -> Maybe (Pattern' Expr, BindName))
-> List1 (Arg (Named_ (Binder' BindName)))
-> [(Pattern' Expr, BindName)]
forall a b. (a -> Maybe b) -> List1 a -> [b]
List1.mapMaybe (Binder' BindName -> Maybe (Pattern' Expr, BindName)
forall a. Binder' a -> Maybe (Pattern' Expr, a)
A.extractPattern (Binder' BindName -> Maybe (Pattern' Expr, BindName))
-> (Arg (Named_ (Binder' BindName)) -> Binder' BindName)
-> Arg (Named_ (Binder' BindName))
-> Maybe (Pattern' Expr, BindName)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Arg (Named_ (Binder' BindName)) -> Binder' BindName
forall a. NamedArg a -> a
namedArg) List1 (Arg (Named_ (Binder' BindName)))
xps
    lbs :: [LetBinding]
lbs = ((Pattern' Expr, BindName) -> LetBinding)
-> [(Pattern' Expr, BindName)] -> [LetBinding]
forall a b. (a -> b) -> [a] -> [b]
map' (Pattern' Expr, BindName) -> LetBinding
letBinding [(Pattern' Expr, BindName)]
ps

    letBinding :: (A.Pattern, A.BindName) -> A.LetBinding
    letBinding :: (Pattern' Expr, BindName) -> LetBinding
letBinding (Pattern' Expr
p, BindName
n) = LetInfo -> ArgInfo -> Pattern' Expr -> Expr -> LetBinding
A.LetPatBind (Range' SrcFile -> LetInfo
A.LetRange Range' SrcFile
r) ArgInfo
defaultArgInfo Pattern' Expr
p (Name -> Expr
A.Var (Name -> Expr) -> Name -> Expr
forall a b. (a -> b) -> a -> b
$ BindName -> Name
A.unBind BindName
n)
      where r :: Range' SrcFile
r = Pattern' Expr -> BindName -> Range' SrcFile
forall u t. (HasRange u, HasRange t) => u -> t -> Range' SrcFile
fuseRange Pattern' Expr
p BindName
n

  [LetBinding] -> TCM a -> TCM a
forall (t :: * -> *) a.
Foldable t =>
t LetBinding -> TCM a -> TCM a
checkLetBindings' [LetBinding]
lbs TCM a
ret

-- | Check a tactic attribute. Should have type Term → TC ⊤.
checkTacticAttribute :: LamOrPi -> Ranged A.Expr -> TCM Term
checkTacticAttribute :: LamOrPi -> Ranged Expr -> TCMT IO Term
checkTacticAttribute (LamNotPi ModTelOrigin
ModTelData) (Ranged Range' SrcFile
r Expr
e) = Range' SrcFile -> TCMT IO Term -> TCMT IO Term
forall (m :: * -> *) x a.
(MonadTrace m, HasRange x) =>
x -> m a -> m a
setCurrentRange Range' SrcFile
r (TCMT IO Term -> TCMT IO Term) -> TCMT IO Term -> TCMT IO Term
forall a b. (a -> b) -> a -> b
$
  TypeError -> TCMT IO Term
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> TCMT IO Term) -> TypeError -> TCMT IO Term
forall a b. (a -> b) -> a -> b
$ TypeError
TacticAttributeNotAllowed
checkTacticAttribute LamOrPi
_                     (Ranged Range' SrcFile
r Expr
e) = do
  expectedType <- TCMT IO Term -> TCM (Type'' Term Term)
forall (m :: * -> *). Functor m => m Term -> m (Type'' Term Term)
el TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTerm TCM (Type'' Term Term)
-> TCM (Type'' Term Term) -> TCM (Type'' Term Term)
forall (m :: * -> *).
HasOptions m =>
m (Type'' Term Term)
-> m (Type'' Term Term) -> m (Type'' Term Term)
--> TCMT IO Term -> TCM (Type'' Term Term)
forall (m :: * -> *). Functor m => m Term -> m (Type'' Term Term)
el (TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTCM TCMT IO Term -> TCMT IO Term -> TCMT IO Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primLevelZero TCMT IO Term -> TCMT IO Term -> TCMT IO Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primUnit)
  checkExpr e expectedType

checkPath :: NamedArg Binder -> A.Type -> A.Expr -> Type -> TCM Term
checkPath :: Arg (Named_ (Binder' BindName))
-> Expr -> Expr -> Type'' Term Term -> TCMT IO Term
checkPath Arg (Named_ (Binder' BindName))
xp Expr
typ Expr
body Type'' Term Term
ty = do
 ArgName -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m ()
reportSDoc ArgName
"tc.term.lambda" Int
30 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
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
hsep [ TCMT IO Doc
"checking path lambda", Arg (Named_ (Binder' BindName)) -> TCMT IO Doc
forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA Arg (Named_ (Binder' BindName))
xp ]
 case (Binder' BindName -> Maybe (Pattern' Expr, BindName)
forall a. Binder' a -> Maybe (Pattern' Expr, a)
A.extractPattern (Binder' BindName -> Maybe (Pattern' Expr, BindName))
-> Binder' BindName -> Maybe (Pattern' Expr, BindName)
forall a b. (a -> b) -> a -> b
$ Arg (Named_ (Binder' BindName)) -> Binder' BindName
forall a. NamedArg a -> a
namedArg Arg (Named_ (Binder' BindName))
xp) of
  Just{}  -> Arg (Named_ (Binder' BindName)) -> TCMT IO Term -> TCMT IO Term
forall (m :: * -> *) x a.
(MonadTrace m, HasRange x) =>
x -> m a -> m a
setCurrentRange Arg (Named_ (Binder' BindName))
xp (TCMT IO Term -> TCMT IO Term) -> TCMT IO Term -> TCMT IO Term
forall a b. (a -> b) -> a -> b
$ TypeError -> TCMT IO Term
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError TypeError
PatternInPathLambda
  Maybe (Pattern' Expr, BindName)
Nothing -> do
    let x :: NamedArg Name
x    = (Binder' BindName -> Name)
-> Arg (Named_ (Binder' BindName)) -> NamedArg Name
forall a b. (a -> b) -> NamedArg a -> NamedArg b
updateNamedArg (BindName -> Name
A.unBind (BindName -> Name)
-> (Binder' BindName -> BindName) -> Binder' BindName -> Name
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Binder' BindName -> BindName
forall a. Binder' a -> a
A.binderName) Arg (Named_ (Binder' BindName))
xp
        info :: ArgInfo
info = NamedArg Name -> ArgInfo
forall a. LensArgInfo a => a -> ArgInfo
getArgInfo NamedArg Name
x
    PathType s path level typ lhs rhs <- Type'' Term Term -> TCMT IO PathView
forall (m :: * -> *).
HasBuiltins m =>
Type'' Term Term -> m PathView
pathView Type'' Term Term
ty
    interval <- primIntervalType
    v <- addContext ([x], interval) $
           checkExpr body (El (raise 1 s) (raise 1 (unArg typ) `apply` [argN $ var 0]))
    iZero <- primIZero
    iOne  <- primIOne
    let lhs' = Int -> SubstArg Term -> Term -> Term
forall a. Subst a => Int -> SubstArg a -> a -> a
subst Int
0 Term
SubstArg Term
iZero Term
v
        rhs' = Int -> SubstArg Term -> Term -> Term
forall a. Subst a => Int -> SubstArg a -> a -> a
subst Int
0 Term
SubstArg Term
iOne  Term
v
    let t = ArgInfo -> Abs Term -> Term
Lam ArgInfo
info (Abs Term -> Term) -> Abs Term -> Term
forall a b. (a -> b) -> a -> b
$ ArgName -> Term -> Abs Term
forall a. ArgName -> a -> Abs a
Abs (NamedArg Name -> ArgName
namedArgName NamedArg Name
x) Term
v
    let btyp Term
i = Sort' Term -> Term -> Type'' Term Term
forall t a. Sort' t -> a -> Type'' t a
El Sort' Term
s (Arg Term -> Term
forall e. Arg e -> e
unArg Arg Term
typ Term -> [Arg Term] -> Term
forall t. Apply t => t -> [Arg Term] -> t
`apply` [Term -> Arg Term
forall e. e -> Arg e
argN Term
i])
    locallyTC eRange (const noRange) $ blockTerm ty $ setCurrentRange body $ do
      equalTerm (btyp iZero) lhs' (unArg lhs)
      equalTerm (btyp iOne) rhs' (unArg rhs)
      return t

---------------------------------------------------------------------------
-- * Lambda abstractions
---------------------------------------------------------------------------

-- | Type check a lambda expression.
--   "checkLambda bs e ty"  means  (\ bs -> e) : ty
checkLambda :: Comparison -> A.TypedBinding -> A.Expr -> Type -> TCM Term
checkLambda :: Comparison
-> TypedBinding -> Expr -> Type'' Term Term -> TCMT IO Term
checkLambda Comparison
cmp (A.TLet Range' SrcFile
_ List1 LetBinding
lbs) Expr
body Type'' Term Term
target =
  List1 LetBinding -> TCMT IO Term -> TCMT IO Term
forall (t :: * -> *) a.
Foldable t =>
t LetBinding -> TCM a -> TCM a
checkLetBindings List1 LetBinding
lbs (Expr -> Type'' Term Term -> TCMT IO Term
checkExpr Expr
body Type'' Term Term
target)
checkLambda Comparison
cmp b :: TypedBinding
b@(A.TBind Range' SrcFile
r TypedBindingInfo
tac List1 (Arg (Named_ (Binder' BindName)))
xps0 Expr
typ) Expr
body Type'' Term Term
target = do
  (tel, tgt0) <- Arg (Named_ (Binder' BindName))
-> Type'' Term Term -> TCM (Telescope, Type'' Term Term)
forall a.
HasRange a =>
NamedArg a -> Type'' Term Term -> TCM (Telescope, Type'' Term Term)
splitImplicitBinderT (List1 (Arg (Named_ (Binder' BindName)))
-> Arg (Named_ (Binder' BindName))
forall a. NonEmpty a -> a
List1.head List1 (Arg (Named_ (Binder' BindName)))
xps0) Type'' Term Term
target

  -- Andreas, 2020-03-25, issue #4481: since we have named lambdas now,
  -- we need to insert skipped hidden arguments.

  -- Amy, 2024-10-17: we can't simply insert the new binders into this
  -- same TBind, since those are all assumed to be of the same type.
  -- This matters when we're skipping binders to reach something of a
  -- different type, e.g. in
  --
  --    (λ {C = C} → C) : {A B : Set} {C : Nat} → Nat
  --
  -- The previous implementation would add two binders and check them
  -- with the same type as that of {C}, i.e. something like
  --
  --    (λ {A B C : _} → C)
  --
  -- which fails. The new strategy is to lob domains off the type until
  -- we reach the right argument, then just add them to the context, and
  -- bind them after returning.

  teleLam tel <$> addContext tel do
    checkLambda' cmp r tac xps0 typ body tgt0

checkLambda' ::
     Comparison                -- ^ @cmp@
  -> Range                     -- ^ Range @r@ of the typed binding
  -> A.TypedBindingInfo        -- ^ @tac@ tactic/finiteness attribute of the typed binding
  -> List1 (NamedArg Binder)   -- ^ @xps@ variables/patterns of the typed binding
  -> A.Type                    -- ^ @typ@ Type of the typed binding (underscore for untyped lambda).
  -> A.Expr                    -- ^ @body@
  -> Type                      -- ^ @target@
  -> TCM Term
checkLambda' :: Comparison
-> Range' SrcFile
-> TypedBindingInfo
-> List1 (Arg (Named_ (Binder' BindName)))
-> Expr
-> Expr
-> Type'' Term Term
-> TCMT IO Term
checkLambda' Comparison
cmp Range' SrcFile
r TypedBindingInfo
tac List1 (Arg (Named_ (Binder' BindName)))
xps Expr
typ Expr
body Type'' Term Term
target = do
  ArgName -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m ()
reportSDoc ArgName
"tc.term.lambda" Int
30 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
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
"checkLambda xs =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> List1 (Arg (Named_ (Binder' BindName))) -> TCMT IO Doc
forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA List1 (Arg (Named_ (Binder' BindName)))
xps
    , TCMT IO Doc
"possiblePath   =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Bool -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Bool -> m Doc
prettyTCM Bool
possiblePath
    , TCMT IO Doc
"numbinds       =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Int -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Int -> m Doc
prettyTCM Int
numbinds
    , TCMT IO Doc
"typ            =" 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 -> Expr
unScope Expr
typ)
    , TCMT IO Doc
"target         =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Type'' Term Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type'' Term Term -> m Doc
prettyTCM Type'' Term Term
target
    , TCMT IO Doc
"tactic         =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TacticAttribute' Expr -> TCMT IO Doc
forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA (TypedBindingInfo -> TacticAttribute' Expr
tbTacticAttr TypedBindingInfo
tac)
    ]
  ArgName -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m ()
reportSDoc ArgName
"tc.term.lambda" Int
60 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
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
"info           =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> (ArgName -> TCMT IO Doc
forall (m :: * -> *). Applicative m => ArgName -> m Doc
text (ArgName -> TCMT IO Doc)
-> (ArgInfo -> ArgName) -> ArgInfo -> TCMT IO Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ArgInfo -> ArgName
forall a. Show a => a -> ArgName
show) ArgInfo
info
    ]

  -- Consume @tac@:
  case TypedBindingInfo
tac of
    TypedBindingInfo
_ | TypedBindingInfo -> Bool
forall a. Null a => a -> Bool
null TypedBindingInfo
tac -> () -> TCM ()
forall a. a -> TCMT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
    A.TypedBindingInfo{ tbTacticAttr :: TypedBindingInfo -> TacticAttribute' Expr
tbTacticAttr = TacticAttribute (Just (Ranged Range' SrcFile
r Expr
e)) } -> do
      -- Andreas, 2024-02-22, issue #6783
      -- Error out if user supplied a tactic (rather than dropping it silently).
      Range' SrcFile -> TCM () -> TCM ()
forall (m :: * -> *) x a.
(MonadTrace m, HasRange x) =>
x -> m a -> m a
setCurrentRange Range' SrcFile
r (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ TypeError -> TCM ()
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> TCM ()) -> TypeError -> TCM ()
forall a b. (a -> b) -> a -> b
$ TypeError
TacticAttributeNotAllowed
    TypedBindingInfo
_ -> TCM ()
forall a. HasCallStack => a
__IMPOSSIBLE__

  TelV tel btyp <- Int -> Type'' Term Term -> TCMT IO (TelV (Type'' Term Term))
forall (m :: * -> *).
(MonadReduce m, MonadAddContext m) =>
Int -> Type'' Term Term -> m (TelV (Type'' Term Term))
telViewUpTo Int
numbinds Type'' Term Term
target
  reportSDoc "tc.term.lambda" 30 $ vcat
    [ "tel            =" <+> prettyTCM tel
    , "btyp           =" <+> prettyTCM btyp
    ]
  if numbinds == 1 && not (null tel) then useTargetType tel btyp
  else if possiblePath then trySeeingIfPath
  else dontUseTargetType =<< do pure (null tel) `and2M` (isJust <$> isBlocked btyp)
    -- If either @tel@ is not @null@ or @btyp@ is not blocked, then @target@ is not blocked,
    -- so we have nothing to block on, and cannot permit @dontUseTargetType@ to postpone.
    -- This happens e.g. in ill-typed cases like @(\ x -> x) : Nat@.
  where
    b :: TypedBinding
b = Range' SrcFile
-> TypedBindingInfo
-> List1 (Arg (Named_ (Binder' BindName)))
-> Expr
-> TypedBinding
A.TBind Range' SrcFile
r TypedBindingInfo
tac List1 (Arg (Named_ (Binder' BindName)))
xps Expr
typ
    xs :: List1 (NamedArg Name)
    xs :: NonEmpty (NamedArg Name)
xs = (Arg (Named_ (Binder' BindName)) -> NamedArg Name)
-> List1 (Arg (Named_ (Binder' BindName)))
-> NonEmpty (NamedArg Name)
forall a b. (a -> b) -> NonEmpty a -> NonEmpty b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Binder' BindName -> Name)
-> Arg (Named_ (Binder' BindName)) -> NamedArg Name
forall a b. (a -> b) -> NamedArg a -> NamedArg b
updateNamedArg (BindName -> Name
A.unBind (BindName -> Name)
-> (Binder' BindName -> BindName) -> Binder' BindName -> Name
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Binder' BindName -> BindName
forall a. Binder' a -> a
A.binderName)) List1 (Arg (Named_ (Binder' BindName)))
xps
    numbinds :: Int
numbinds = List1 (Arg (Named_ (Binder' BindName))) -> Int
forall a. NonEmpty a -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length List1 (Arg (Named_ (Binder' BindName)))
xps
    possiblePath :: Bool
possiblePath = Int
numbinds Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
1 Bool -> Bool -> Bool
&& Expr -> Bool
forall a. Underscore a => a -> Bool
isUnderscore (Expr -> Expr
unScope Expr
typ)
                   Bool -> Bool -> Bool
&& ArgInfo -> Bool
forall a. LensRelevance a => a -> Bool
isRelevant ArgInfo
info Bool -> Bool -> Bool
&& ArgInfo -> Bool
forall a. LensHiding a => a -> Bool
visible ArgInfo
info
    info :: ArgInfo
info = NamedArg Name -> ArgInfo
forall a. LensArgInfo a => a -> ArgInfo
getArgInfo (NamedArg Name -> ArgInfo) -> NamedArg Name -> ArgInfo
forall a b. (a -> b) -> a -> b
$ NonEmpty (NamedArg Name) -> NamedArg Name
forall a. NonEmpty a -> a
List1.head NonEmpty (NamedArg Name)
xs

    trySeeingIfPath :: TCMT IO Term
trySeeingIfPath = do
      ArgName -> Int -> ArgName -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> ArgName -> m ()
reportSLn ArgName
"tc.term.lambda" Int
60 (ArgName -> TCM ()) -> ArgName -> TCM ()
forall a b. (a -> b) -> a -> b
$ ArgName
"trySeeingIfPath for " ArgName -> ArgName -> ArgName
forall a. [a] -> [a] -> [a]
++! List1 (Arg (Named_ (Binder' BindName))) -> ArgName
forall a. Show a => a -> ArgName
show List1 (Arg (Named_ (Binder' BindName)))
xps
      let postpone' :: Blocker -> Type'' Term Term -> TCMT IO Term
postpone' Blocker
blocker Type'' Term Term
tgt =
            TCMT IO Bool -> TCMT IO Term -> TCMT IO Term -> TCMT IO Term
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM (Maybe Cubical -> Bool
forall a. Maybe a -> Bool
isNothing (Maybe Cubical -> Bool) -> TCMT IO (Maybe Cubical) -> TCMT IO Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCMT IO (Maybe Cubical)
forall (m :: * -> *). HasOptions m => m (Maybe Cubical)
cubicalOption) {-then-} (Bool -> TCMT IO Term
dontUseTargetType Bool
True) {-else-} (TCMT IO Term -> TCMT IO Term) -> TCMT IO Term -> TCMT IO Term
forall a b. (a -> b) -> a -> b
$ Blocker -> Type'' Term Term -> TCMT IO Term
postpone Blocker
blocker Type'' Term Term
tgt
      Type'' Term Term
-> (Blocker -> Type'' Term Term -> TCMT IO Term)
-> (NotBlocked -> Type'' Term Term -> TCMT IO Term)
-> TCMT IO Term
forall t (m :: * -> *) a.
(Reduce t, IsMeta t, MonadReduce m) =>
t -> (Blocker -> t -> m a) -> (NotBlocked -> t -> m a) -> m a
ifBlocked Type'' Term Term
target Blocker -> Type'' Term Term -> TCMT IO Term
postpone' ((NotBlocked -> Type'' Term Term -> TCMT IO Term) -> TCMT IO Term)
-> (NotBlocked -> Type'' Term Term -> TCMT IO Term) -> TCMT IO Term
forall a b. (a -> b) -> a -> b
$ \ NotBlocked
_ Type'' Term Term
t -> do
        TCMT IO Bool -> TCMT IO Term -> TCMT IO Term -> TCMT IO Term
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifNotM (PathView -> Bool
isPathType (PathView -> Bool) -> TCMT IO PathView -> TCMT IO Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type'' Term Term -> TCMT IO PathView
forall (m :: * -> *).
HasBuiltins m =>
Type'' Term Term -> m PathView
pathView Type'' Term Term
t) (Bool -> TCMT IO Term
dontUseTargetType Bool
False) {-else-} do
          -- Note that --cubical is on here since we returned from 'pathView'.
          Arg (Named_ (Binder' BindName))
-> Expr -> Expr -> Type'' Term Term -> TCMT IO Term
checkPath (List1 (Arg (Named_ (Binder' BindName)))
-> Arg (Named_ (Binder' BindName))
forall a. NonEmpty a -> a
List1.head List1 (Arg (Named_ (Binder' BindName)))
xps) Expr
typ Expr
body Type'' Term Term
t

    postpone_ :: TCMT IO Term
postpone_ = TypeCheckingProblem -> TCMT IO Term
postponeTypeCheckingProblem_ (TypeCheckingProblem -> TCMT IO Term)
-> TypeCheckingProblem -> TCMT IO Term
forall a b. (a -> b) -> a -> b
$
      Comparison -> Expr -> Type'' Term Term -> TypeCheckingProblem
CheckExpr Comparison
cmp (ExprInfo -> LamBinding -> Expr -> Expr
A.Lam ExprInfo
A.exprNoRange (TypedBinding -> LamBinding
A.DomainFull TypedBinding
b) Expr
body) Type'' Term Term
target

    postpone :: Blocker -> Type'' Term Term -> TCMT IO Term
postpone Blocker
blocker Type'' Term Term
tgt = (TypeCheckingProblem -> Blocker -> TCMT IO Term)
-> Blocker -> TypeCheckingProblem -> TCMT IO Term
forall a b c. (a -> b -> c) -> b -> a -> c
flip TypeCheckingProblem -> Blocker -> TCMT IO Term
postponeTypeCheckingProblem Blocker
blocker (TypeCheckingProblem -> TCMT IO Term)
-> TypeCheckingProblem -> TCMT IO Term
forall a b. (a -> b) -> a -> b
$
      Comparison -> Expr -> Type'' Term Term -> TypeCheckingProblem
CheckExpr Comparison
cmp (ExprInfo -> LamBinding -> Expr -> Expr
A.Lam ExprInfo
A.exprNoRange (TypedBinding -> LamBinding
A.DomainFull TypedBinding
b) Expr
body) Type'' Term Term
tgt

    -- Andreas, 2025-08-08.
    -- In case the target type does not resolve to a Pi,
    -- we construct a Pi-type from the yet unchecked type @typ@ of the domain(s)
    -- (which is underscore for an untyped lambda).
    -- This strategy is hazardous in various situations:
    --
    -- - We might be missing implicit lambdas that should precede the given lambda.
    --
    -- - If no modality is given at the lambda, we might commit to the default one
    --   which then might turn out to be the wrong one as more information surfaces.
    --   Unfortunately, we do not have modality metas otherwise we could postpone
    --   the decision.
    --
    -- To fix #7001, we could check whether the user has supplied the relevant modalities
    -- (depending on which language flags are on), and refuse to progress if they are missing.
    dontUseTargetType :: Bool -> TCMT IO Term
dontUseTargetType Bool
mayPostpone = TCMT IO Bool -> TCMT IO Term -> TCMT IO Term -> TCMT IO Term
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM (Bool -> TCMT IO Bool
forall a. a -> TCMT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
mayPostpone TCMT IO Bool -> TCMT IO Bool -> TCMT IO Bool
forall (m :: * -> *). Monad m => m Bool -> m Bool -> m Bool
`and2M` NonEmpty (NamedArg Name) -> TCMT IO Bool
userOmittedModalities NonEmpty (NamedArg Name)
xs) TCMT IO Term
postpone_ {-else-} do
      -- Checking λ (xs : argsT) → body : target
      ArgName -> Int -> TCM () -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> m () -> m ()
verboseS ArgName
"tc.term.lambda" Int
5 (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ ArgName -> TCM ()
forall (m :: * -> *). MonadStatistics m => ArgName -> m ()
tick ArgName
"lambda-no-target-type"

      -- First check that argsT is a valid type or create a meta for it.
      argsT <- TCM (Type'' Term Term) -> TCM (Type'' Term Term)
forall (m :: * -> *) a.
(MonadTCEnv m, HasOptions m, MonadDebug m) =>
m a -> m a
workOnTypes (TCM (Type'' Term Term) -> TCM (Type'' Term Term))
-> TCM (Type'' Term Term) -> TCM (Type'' Term Term)
forall a b. (a -> b) -> a -> b
$ Expr -> TCM (Type'' Term Term)
isType_ Expr
typ
      -- Andreas, 2025-08-08, issue #7001:
      -- If the user has not written explicitly a modality for the lambda-bound variable,
      -- the default modality is used which might not be correct.
      -- As a consequence, the speculated function type created by @telePi tel@ below
      -- may have the wrong modality.
      let tel = NonEmpty (NamedArg Name) -> Type'' Term Term -> Telescope
namedBindsToTel1 NonEmpty (NamedArg Name)
xs Type'' Term Term
argsT
      reportSDoc "tc.term.lambda" 30 $ "dontUseTargetType tel =" <+> pretty tel

      -- Andreas, 2015-05-28 Issue 1523
      -- If argsT is a SizeLt, it must be non-empty to avoid non-termination.
      -- TODO: do we need to block checkExpr?
      checkSizeLtSat $ unEl argsT

      -- Jesper 2019-12-17, #4261: we need to postpone here if
      -- checking of the record pattern fails; if we try to catch
      -- higher up the metas created during checking of @argsT@ are
      -- not available.
      let postponeOnBlockedPattern TCMT IO (Type'' Term Term, Term)
m = TCMT IO (Type'' Term Term, Term)
m TCMT IO (Type'' Term Term, Term)
-> ((TCErr, Blocker) -> TCMT IO (Type'' Term Term, Term))
-> TCMT IO (Type'' Term Term, Term)
forall a. TCM a -> ((TCErr, Blocker) -> TCM a) -> TCM a
`catchIlltypedPatternBlockedOnMeta` \(TCErr
err , Blocker
x) -> do
            ArgName -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m ()
reportSDoc ArgName
"tc.term" Int
50 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
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
"checking record pattern stuck on meta: " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> ArgName -> TCMT IO Doc
forall (m :: * -> *). Applicative m => ArgName -> m Doc
text (Blocker -> ArgName
forall a. Show a => a -> ArgName
show Blocker
x) ]
            t1 <- (NonEmpty (NamedArg Name), Type'' Term Term)
-> TCM (Type'' Term Term) -> TCM (Type'' Term Term)
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
(NonEmpty (NamedArg Name), Type'' Term Term) -> m a -> m a
addContext (NonEmpty (NamedArg Name)
xs, Type'' Term Term
argsT) (TCM (Type'' Term Term) -> TCM (Type'' Term Term))
-> TCM (Type'' Term Term) -> TCM (Type'' Term Term)
forall a b. (a -> b) -> a -> b
$ TCM (Type'' Term Term) -> TCM (Type'' Term Term)
forall (m :: * -> *) a.
(MonadTCEnv m, HasOptions m, MonadDebug m) =>
m a -> m a
workOnTypes TCM (Type'' Term Term)
newTypeMeta_
            let e    = ExprInfo -> LamBinding -> Expr -> Expr
A.Lam ExprInfo
A.exprNoRange (TypedBinding -> LamBinding
A.DomainFull TypedBinding
b) Expr
body
                tgt' = Telescope -> Type'' Term Term -> Type'' Term Term
telePi Telescope
tel Type'' Term Term
t1
            w <- postponeTypeCheckingProblem (CheckExpr cmp e tgt') x
            return (tgt' , w)

      -- Now check body : ?t₁
      -- DONT USE tel for addContext, as it loses NameIds.
      -- WRONG: v <- addContext tel $ checkExpr body t1
      (target0 , w) <- postponeOnBlockedPattern $
         addContext (xs, argsT) $ addTypedPatterns xps $ do
           t1 <- workOnTypes newTypeMeta_
           v  <- checkExpr' cmp body t1
           return (telePi tel t1 , teleLam tel v)

      -- Do not coerce hidden lambdas
      if notVisible info || any notVisible xs then do
        pid <- newProblem_ $ leqType target0 target
        blockTermOnProblem target w pid
      else do
        coerce cmp w target0 target


    useTargetType :: Telescope -> Type'' Term Term -> TCMT IO Term
useTargetType tel :: Telescope
tel@(ExtendTel Dom' Term (Type'' Term Term)
dom (Abs ArgName
y Telescope
EmptyTel)) Type'' Term Term
btyp = do
        ArgName -> Int -> TCM () -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> m () -> m ()
verboseS ArgName
"tc.term.lambda" Int
5 (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ ArgName -> TCM ()
forall (m :: * -> *). MonadStatistics m => ArgName -> m ()
tick ArgName
"lambda-with-target-type"
        ArgName -> Int -> ArgName -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> ArgName -> m ()
reportSLn ArgName
"tc.term.lambda" Int
30 (ArgName -> TCM ()) -> ArgName -> TCM ()
forall a b. (a -> b) -> a -> b
$ ArgName
"useTargetType y  = " ArgName -> ArgName -> ArgName
forall a. [a] -> [a] -> [a]
++! ArgName
y

        let (NamedArg Name
x :| []) = NonEmpty (NamedArg Name)
xs
        Bool -> TCM () -> TCM ()
forall b (m :: * -> *). (IsBool b, Monad m) => b -> m () -> m ()
unless (Dom' Term (Type'' Term Term) -> ArgInfo -> Bool
forall a b. (LensHiding a, LensHiding b) => a -> b -> Bool
sameHiding Dom' Term (Type'' Term Term)
dom ArgInfo
info) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ TypeError -> TCM ()
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> TCM ()) -> TypeError -> TCM ()
forall a b. (a -> b) -> a -> b
$ Type'' Term Term -> TypeError
WrongHidingInLambda Type'' Term Term
target
        Bool -> TCM () -> TCM ()
forall b (m :: * -> *). (IsBool b, Monad m) => b -> m () -> m ()
when (Maybe (WithOrigin (Ranged ArgName)) -> Bool
forall a. Maybe a -> Bool
isJust (Maybe (WithOrigin (Ranged ArgName)) -> Bool)
-> Maybe (WithOrigin (Ranged ArgName)) -> Bool
forall a b. (a -> b) -> a -> b
$ NamedArg Name -> Maybe (NameOf (NamedArg Name))
forall a. LensNamed a => a -> Maybe (NameOf a)
getNameOf NamedArg Name
x) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$
          -- Andreas, 2020-03-25, issue #4481: check for correct name
          Bool -> TCM () -> TCM ()
forall b (m :: * -> *). (IsBool b, Monad m) => b -> m () -> m ()
unless (Dom' Term (Type'' Term Term) -> NamedArg Name -> Bool
forall a b.
(LensNamed a, LensNamed b, NameOf a ~ WithOrigin (Ranged ArgName),
 NameOf b ~ WithOrigin (Ranged ArgName)) =>
a -> b -> Bool
namedSame Dom' Term (Type'' Term Term)
dom NamedArg Name
x) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$
            NamedArg Name -> TCM () -> TCM ()
forall (m :: * -> *) x a.
(MonadTrace m, HasRange x) =>
x -> m a -> m a
setCurrentRange NamedArg Name
x (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ TypeError -> TCM ()
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> TCM ()) -> TypeError -> TCM ()
forall a b. (a -> b) -> a -> b
$ TypeError
WrongHidingInLHS
        -- Andreas, 2011-10-01 ignore relevance in lambda if not explicitly given
        info <- Dom' Term (Type'' Term Term) -> ArgInfo -> TCM ArgInfo
forall dom.
(LensAnnotation dom, LensModality dom) =>
dom -> ArgInfo -> TCM ArgInfo
lambdaModalityCheck Dom' Term (Type'' Term Term)
dom ArgInfo
info
        -- Andreas, 2015-05-28 Issue 1523
        -- Ensure we are not stepping under a possibly non-existing size.
        -- TODO: do we need to block checkExpr?
        let a = Dom' Term (Type'' Term Term) -> Type'' Term Term
forall t e. Dom' t e -> e
unDom Dom' Term (Type'' Term Term)
dom
        checkSizeLtSat $ unEl a
        -- We only need to block the final term on the argument type
        -- comparison. The body will be blocked if necessary. We still want to
        -- compare the argument types first, so we spawn a new problem for that
        -- check.
        (pid, argT) <- newProblem $ isTypeEqualTo typ a
        -- Andreas, Issue 630: take name from function type if lambda name is "_"
        v <- lambdaAddContext (namedArg x) y (defaultArgDom info argT) $
               addTypedPatterns xps $ checkExpr' cmp body btyp
        blockTermOnProblem target (Lam info $ Abs (namedArgName x) v) pid

    useTargetType Telescope
_ Type'' Term Term
_ = TCMT IO Term
forall a. HasCallStack => a
__IMPOSSIBLE__

userOmittedModalities :: List1 (NamedArg Name) -> TCM Bool
userOmittedModalities :: NonEmpty (NamedArg Name) -> TCMT IO Bool
userOmittedModalities NonEmpty (NamedArg Name)
xs = do
  (PragmaOptions -> Bool
optErasure (PragmaOptions -> Bool) -> TCMT IO PragmaOptions -> TCMT IO Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCMT IO PragmaOptions
forall (m :: * -> *). HasOptions m => m PragmaOptions
pragmaOptions) TCMT IO Bool -> TCMT IO Bool -> TCMT IO Bool
forall (m :: * -> *). Monad m => m Bool -> m Bool -> m Bool
`and2M` Bool -> TCMT IO Bool
forall a. a -> TCMT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ((NamedArg Name -> Bool) -> NonEmpty (NamedArg Name) -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (Quantity -> Bool
forall a. Null a => a -> Bool
null (Quantity -> Bool)
-> (NamedArg Name -> Quantity) -> NamedArg Name -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NamedArg Name -> Quantity
forall a. LensQuantity a => a -> Quantity
getQuantity) NonEmpty (NamedArg Name)
xs)
-- TODO: extend to modalities beyond erasure.
-- userOmittedModalities :: List1 (NamedArg Name) -> TCM Bool
-- userOmittedModalities xs = do
--   erasure  <- optErasure <$> pragmaOptions
--   -- polarity <- optPolarity <$> pragmaOptions
--   return $ flip any xs \ x -> or
--     [ erasure  && null (getQuantity x)
--     -- TODO: ModalPolarity does not have a concept of default yet.
--     -- , polarity && null (getPolarityMod x)
--     -- TODO: a means for the user to tell they are serious about irrelevance,
--     -- e.g. flag --irrelevance.
--     -- Otherwise too many regressions.
--     -- , null $ getRelevance x
--     -- TODO: Cohesion and Annotation do not have a concept of default yet.
--     ]

-- | Check that modality info in lambda is compatible with modality
--   coming from the function type.
--   If lambda has no user-given modality, copy that of function type.
lambdaModalityCheck ::
     (LensAnnotation dom, LensModality dom)
  => dom -> ArgInfo -> TCM ArgInfo
lambdaModalityCheck :: forall dom.
(LensAnnotation dom, LensModality dom) =>
dom -> ArgInfo -> TCM ArgInfo
lambdaModalityCheck dom
dom =
  Annotation -> ArgInfo -> TCM ArgInfo
forall dom. LensAnnotation dom => dom -> ArgInfo -> TCM ArgInfo
lambdaAnnotationCheck (dom -> Annotation
forall a. LensAnnotation a => a -> Annotation
getAnnotation dom
dom) (ArgInfo -> TCM ArgInfo)
-> (ArgInfo -> TCM ArgInfo) -> ArgInfo -> TCM ArgInfo
forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=<
  Modality -> ArgInfo -> TCM ArgInfo
forall dom. LensModalPolarity dom => dom -> ArgInfo -> TCM ArgInfo
lambdaPolarityCheck Modality
m (ArgInfo -> TCM ArgInfo)
-> (ArgInfo -> TCM ArgInfo) -> ArgInfo -> TCM ArgInfo
forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=<
  Modality -> ArgInfo -> TCM ArgInfo
forall dom. LensCohesion dom => dom -> ArgInfo -> TCM ArgInfo
lambdaCohesionCheck Modality
m (ArgInfo -> TCM ArgInfo)
-> (ArgInfo -> TCM ArgInfo) -> ArgInfo -> TCM ArgInfo
forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=<
  Modality -> ArgInfo -> TCM ArgInfo
forall dom. LensQuantity dom => dom -> ArgInfo -> TCM ArgInfo
lambdaQuantityCheck Modality
m (ArgInfo -> TCM ArgInfo)
-> (ArgInfo -> TCM ArgInfo) -> ArgInfo -> TCM ArgInfo
forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=<
  Modality -> ArgInfo -> TCM ArgInfo
forall dom. LensRelevance dom => dom -> ArgInfo -> TCM ArgInfo
lambdaIrrelevanceCheck Modality
m
  where m :: Modality
m = dom -> Modality
forall a. LensModality a => a -> Modality
getModality dom
dom

-- | Check that irrelevance info in lambda is compatible with irrelevance
--   coming from the function type.
--   If lambda has no user-given relevance, copy that of function type.
lambdaIrrelevanceCheck :: LensRelevance dom => dom -> ArgInfo -> TCM ArgInfo
lambdaIrrelevanceCheck :: forall dom. LensRelevance dom => dom -> ArgInfo -> TCM ArgInfo
lambdaIrrelevanceCheck dom
dom ArgInfo
info
    -- Case: no specific user annotation: use relevance of function type
  | ArgInfo -> Relevance
forall a. LensRelevance a => a -> Relevance
getRelevance ArgInfo
info Relevance -> Relevance -> Bool
forall a. Eq a => a -> a -> Bool
== Relevance
defaultRelevance = ArgInfo -> TCM ArgInfo
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (ArgInfo -> TCM ArgInfo) -> ArgInfo -> TCM ArgInfo
forall a b. (a -> b) -> a -> b
$! Relevance -> ArgInfo -> ArgInfo
forall a. LensRelevance a => Relevance -> a -> a
setRelevance (dom -> Relevance
forall a. LensRelevance a => a -> Relevance
getRelevance dom
dom) ArgInfo
info
    -- Case: explicit user annotation is taken seriously
  | Bool
otherwise = do
      let rPi :: Relevance
rPi  = dom -> Relevance
forall a. LensRelevance a => a -> Relevance
getRelevance dom
dom  -- relevance of function type
      let rLam :: Relevance
rLam = ArgInfo -> Relevance
forall a. LensRelevance a => a -> Relevance
getRelevance ArgInfo
info -- relevance of lambda
      Bool -> TCM () -> TCM ()
forall b (m :: * -> *). (IsBool b, Monad m) => b -> m () -> m ()
unless (Relevance -> Relevance -> Bool
sameRelevance Relevance
rPi Relevance
rLam) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$
        TypeError -> TCM ()
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError TypeError
WrongIrrelevanceInLambda
      ArgInfo -> TCM ArgInfo
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ArgInfo
info

-- | Check that quantity info in lambda is compatible with quantity
--   coming from the function type.
--   If lambda has no user-given quantity, copy that of function type.
lambdaQuantityCheck :: LensQuantity dom => dom -> ArgInfo -> TCM ArgInfo
lambdaQuantityCheck :: forall dom. LensQuantity dom => dom -> ArgInfo -> TCM ArgInfo
lambdaQuantityCheck dom
dom ArgInfo
info
    -- Case: no specific user annotation: use quantity of function type
  | ArgInfo -> Bool
forall a. LensQuantity a => a -> Bool
noUserQuantity ArgInfo
info = ArgInfo -> TCM ArgInfo
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (ArgInfo -> TCM ArgInfo) -> ArgInfo -> TCM ArgInfo
forall a b. (a -> b) -> a -> b
$! Quantity -> ArgInfo -> ArgInfo
forall a. LensQuantity a => Quantity -> a -> a
setQuantity (dom -> Quantity
forall a. LensQuantity a => a -> Quantity
getQuantity dom
dom) ArgInfo
info
    -- Case: explicit user annotation is taken seriously
  | Bool
otherwise = do
      let qPi :: Quantity
qPi  = dom -> Quantity
forall a. LensQuantity a => a -> Quantity
getQuantity dom
dom  -- quantity of function type
      let qLam :: Quantity
qLam = ArgInfo -> Quantity
forall a. LensQuantity a => a -> Quantity
getQuantity ArgInfo
info -- quantity of lambda
      Bool -> TCM () -> TCM ()
forall b (m :: * -> *). (IsBool b, Monad m) => b -> m () -> m ()
unless (Quantity
qPi Quantity -> Quantity -> Bool
`sameQuantity` Quantity
qLam) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ do
        TypeError -> TCM ()
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError TypeError
WrongQuantityInLambda
      ArgInfo -> TCM ArgInfo
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ArgInfo
info

lambdaAnnotationCheck :: LensAnnotation dom => dom -> ArgInfo -> TCM ArgInfo
lambdaAnnotationCheck :: forall dom. LensAnnotation dom => dom -> ArgInfo -> TCM ArgInfo
lambdaAnnotationCheck dom
dom ArgInfo
info
    -- Case: no specific user annotation: use annotation of function type
  | ArgInfo -> Annotation
forall a. LensAnnotation a => a -> Annotation
getAnnotation ArgInfo
info Annotation -> Annotation -> Bool
forall a. Eq a => a -> a -> Bool
== Annotation
defaultAnnotation = ArgInfo -> TCM ArgInfo
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (ArgInfo -> TCM ArgInfo) -> ArgInfo -> TCM ArgInfo
forall a b. (a -> b) -> a -> b
$! Annotation -> ArgInfo -> ArgInfo
forall a. LensAnnotation a => Annotation -> a -> a
setAnnotation (dom -> Annotation
forall a. LensAnnotation a => a -> Annotation
getAnnotation dom
dom) ArgInfo
info
    -- Case: explicit user annotation is taken seriously
  | Bool
otherwise = do
      let aPi :: Annotation
aPi  = dom -> Annotation
forall a. LensAnnotation a => a -> Annotation
getAnnotation dom
dom  -- annotation of function type
      let aLam :: Annotation
aLam = ArgInfo -> Annotation
forall a. LensAnnotation a => a -> Annotation
getAnnotation ArgInfo
info -- annotation of lambda
      Bool -> TCM () -> TCM ()
forall b (m :: * -> *). (IsBool b, Monad m) => b -> m () -> m ()
unless (Annotation
aPi Annotation -> Annotation -> Bool
forall a. Eq a => a -> a -> Bool
== Annotation
aLam) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ do
        TypeError -> TCM ()
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError TypeError
WrongAnnotationInLambda
      ArgInfo -> TCM ArgInfo
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ArgInfo
info

-- | Check that cohesion info in lambda is compatible with cohesion
--   coming from the function type.
--   If lambda has no user-given cohesion, copy that of function type.
lambdaCohesionCheck :: LensCohesion dom => dom -> ArgInfo -> TCM ArgInfo
lambdaCohesionCheck :: forall dom. LensCohesion dom => dom -> ArgInfo -> TCM ArgInfo
lambdaCohesionCheck dom
dom ArgInfo
info
    -- Case: no specific user annotation: use cohesion of function type
  | ArgInfo -> Cohesion
forall a. LensCohesion a => a -> Cohesion
getCohesion ArgInfo
info Cohesion -> Cohesion -> Bool
forall a. Eq a => a -> a -> Bool
== Cohesion
defaultCohesion = ArgInfo -> TCM ArgInfo
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (ArgInfo -> TCM ArgInfo) -> ArgInfo -> TCM ArgInfo
forall a b. (a -> b) -> a -> b
$! Cohesion -> ArgInfo -> ArgInfo
forall a. LensCohesion a => Cohesion -> a -> a
setCohesion (dom -> Cohesion
forall a. LensCohesion a => a -> Cohesion
getCohesion dom
dom) ArgInfo
info
    -- Case: explicit user annotation is taken seriously
  | Bool
otherwise = do
      let cPi :: Cohesion
cPi  = dom -> Cohesion
forall a. LensCohesion a => a -> Cohesion
getCohesion dom
dom  -- cohesion of function type
      let cLam :: Cohesion
cLam = ArgInfo -> Cohesion
forall a. LensCohesion a => a -> Cohesion
getCohesion ArgInfo
info -- cohesion of lambda
      Bool -> TCM () -> TCM ()
forall b (m :: * -> *). (IsBool b, Monad m) => b -> m () -> m ()
unless (Cohesion
cPi Cohesion -> Cohesion -> Bool
`sameCohesion` Cohesion
cLam) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ do
        -- if there is a cohesion annotation then
        -- it better match the domain.
        TypeError -> TCM ()
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError TypeError
WrongCohesionInLambda
      ArgInfo -> TCM ArgInfo
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ArgInfo
info

-- | Check that polarity info in lambda is compatible with polarity
--   coming from the function type.
--   If lambda has no user-given polarity, copy that of function type.
lambdaPolarityCheck :: LensModalPolarity dom => dom -> ArgInfo -> TCM ArgInfo
lambdaPolarityCheck :: forall dom. LensModalPolarity dom => dom -> ArgInfo -> TCM ArgInfo
lambdaPolarityCheck dom
dom ArgInfo
info
    -- Case: no specific user annotation: use polarity of function type
  | ArgInfo -> PolarityModality
forall a. LensModalPolarity a => a -> PolarityModality
getModalPolarity ArgInfo
info PolarityModality -> PolarityModality -> Bool
forall a. Eq a => a -> a -> Bool
== PolarityModality
defaultPolarity = ArgInfo -> TCM ArgInfo
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (ArgInfo -> TCM ArgInfo) -> ArgInfo -> TCM ArgInfo
forall a b. (a -> b) -> a -> b
$! PolarityModality -> ArgInfo -> ArgInfo
forall a. LensModalPolarity a => PolarityModality -> a -> a
setModalPolarity (dom -> PolarityModality
forall a. LensModalPolarity a => a -> PolarityModality
getModalPolarity dom
dom) ArgInfo
info
    -- Case: explicit user annotation is taken seriously
  | Bool
otherwise = do
      let cPi :: PolarityModality
cPi  = dom -> PolarityModality
forall a. LensModalPolarity a => a -> PolarityModality
getModalPolarity dom
dom  -- polarity of function type
      let cLam :: PolarityModality
cLam = ArgInfo -> PolarityModality
forall a. LensModalPolarity a => a -> PolarityModality
getModalPolarity ArgInfo
info -- polarity of lambda
      Bool -> TCM () -> TCM ()
forall b (m :: * -> *). (IsBool b, Monad m) => b -> m () -> m ()
unless (PolarityModality
cPi PolarityModality -> PolarityModality -> Bool
`samePolarity` PolarityModality
cLam) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ do
        -- if there is a polarity annotation then
        -- it better match the domain.
        TypeError -> TCM ()
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError TypeError
WrongPolarityInLambda
      ArgInfo -> TCM ArgInfo
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ArgInfo
info

-- Andreas, issue #630: take name from function type if lambda name is "_".
lambdaAddContext :: MonadAddContext m => Name -> ArgName -> Dom Type -> m a -> m a
lambdaAddContext :: forall (m :: * -> *) a.
MonadAddContext m =>
Name -> ArgName -> Dom' Term (Type'' Term Term) -> m a -> m a
lambdaAddContext Name
x ArgName
y Dom' Term (Type'' Term Term)
dom
  | Name -> Bool
forall a. IsNoName a => a -> Bool
isNoName Name
x = (ArgName, Dom' Term (Type'' Term Term)) -> m a -> m a
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
(ArgName, Dom' Term (Type'' Term Term)) -> m a -> m a
addContext (ArgName
y, Dom' Term (Type'' Term Term)
dom)                 -- Note: String instance
  | Bool
otherwise  = (Name, Dom' Term (Type'' Term Term)) -> m a -> m a
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
(Name, Dom' Term (Type'' Term Term)) -> m a -> m a
addContext (Name
x, Dom' Term (Type'' Term Term)
dom)                 -- Name instance of addContext

-- | Checking a lambda whose domain type has already been checked.
checkPostponedLambda :: Comparison -> Arg (List1 (WithHiding Name), Maybe Type) -> A.Expr -> Type -> TCM Term
-- checkPostponedLambda cmp args@(Arg _    ([]    , _ )) body target = do
--   checkExpr' cmp body target
checkPostponedLambda :: Comparison
-> Arg (List1 (WithHiding Name), Maybe (Type'' Term Term))
-> Expr
-> Type'' Term Term
-> TCMT IO Term
checkPostponedLambda Comparison
cmp args :: Arg (List1 (WithHiding Name), Maybe (Type'' Term Term))
args@(Arg ArgInfo
info (WithHiding Hiding
h Name
x :| [WithHiding Name]
xs, Maybe (Type'' Term Term)
mt)) Expr
body Type'' Term Term
target = do
  let postpone :: Blocker -> Type'' Term Term -> TCMT IO Term
postpone Blocker
_ Type'' Term Term
t = TypeCheckingProblem -> TCMT IO Term
postponeTypeCheckingProblem_ (TypeCheckingProblem -> TCMT IO Term)
-> TypeCheckingProblem -> TCMT IO Term
forall a b. (a -> b) -> a -> b
$ Comparison
-> Arg (List1 (WithHiding Name), Maybe (Type'' Term Term))
-> Expr
-> Type'' Term Term
-> TypeCheckingProblem
CheckLambda Comparison
cmp Arg (List1 (WithHiding Name), Maybe (Type'' Term Term))
args Expr
body Type'' Term Term
t
      lamHiding :: Hiding
lamHiding = Hiding -> Hiding -> Hiding
forall a. Monoid a => a -> a -> a
mappend Hiding
h (Hiding -> Hiding) -> Hiding -> Hiding
forall a b. (a -> b) -> a -> b
$ ArgInfo -> Hiding
forall a. LensHiding a => a -> Hiding
getHiding ArgInfo
info
  Hiding
-> Type'' Term Term
-> (Blocker -> Type'' Term Term -> TCMT IO Term)
-> (Type'' Term Term -> TCMT IO Term)
-> TCMT IO Term
insertHiddenLambdas Hiding
lamHiding Type'' Term Term
target Blocker -> Type'' Term Term -> TCMT IO Term
postpone ((Type'' Term Term -> TCMT IO Term) -> TCMT IO Term)
-> (Type'' Term Term -> TCMT IO Term) -> TCMT IO Term
forall a b. (a -> b) -> a -> b
$ \ t :: Type'' Term Term
t@(El Sort' Term
_ (Pi Dom' Term (Type'' Term Term)
dom Abs (Type'' Term Term)
b)) -> do
    -- Andreas, 2011-10-01 ignore relevance in lambda if not explicitly given
    info' <- Hiding -> ArgInfo -> ArgInfo
forall a. LensHiding a => Hiding -> a -> a
setHiding Hiding
lamHiding (ArgInfo -> ArgInfo) -> TCM ArgInfo -> TCM ArgInfo
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Dom' Term (Type'' Term Term) -> ArgInfo -> TCM ArgInfo
forall dom.
(LensAnnotation dom, LensModality dom) =>
dom -> ArgInfo -> TCM ArgInfo
lambdaModalityCheck Dom' Term (Type'' Term Term)
dom ArgInfo
info
    -- We only need to block the final term on the argument type
    -- comparison. The body will be blocked if necessary. We still want to
    -- compare the argument types first, so we spawn a new problem for that
    -- check.
    mpid <- caseMaybe mt (return Nothing) $ \ Type'' Term Term
ascribedType -> ProblemId -> Maybe ProblemId
forall a. a -> Maybe a
Just (ProblemId -> Maybe ProblemId)
-> TCMT IO ProblemId -> TCMT IO (Maybe ProblemId)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do
      TCM () -> TCMT IO ProblemId
forall (m :: * -> *) a.
(MonadFresh ProblemId m, MonadConstraint m) =>
m a -> m ProblemId
newProblem_ (TCM () -> TCMT IO ProblemId) -> TCM () -> TCMT IO ProblemId
forall a b. (a -> b) -> a -> b
$ Type'' Term Term -> Type'' Term Term -> TCM ()
leqType (Dom' Term (Type'' Term Term) -> Type'' Term Term
forall t e. Dom' t e -> e
unDom Dom' Term (Type'' Term Term)
dom) Type'' Term Term
ascribedType
    -- We type-check the body with the ascribedType given by the user
    -- to get better error messages.
    -- Using the type dom from the usage context would be more precise,
    -- though.
    -- TODO: quantity
    let dom' = Relevance
-> Dom' Term (Type'' Term Term) -> Dom' Term (Type'' Term Term)
forall a. LensRelevance a => Relevance -> a -> a
setRelevance (ArgInfo -> Relevance
forall a. LensRelevance a => a -> Relevance
getRelevance ArgInfo
info') (Dom' Term (Type'' Term Term) -> Dom' Term (Type'' Term Term))
-> (Dom' Term (Type'' Term Term) -> Dom' Term (Type'' Term Term))
-> Dom' Term (Type'' Term Term)
-> Dom' Term (Type'' Term Term)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Hiding
-> Dom' Term (Type'' Term Term) -> Dom' Term (Type'' Term Term)
forall a. LensHiding a => Hiding -> a -> a
setHiding Hiding
lamHiding (Dom' Term (Type'' Term Term) -> Dom' Term (Type'' Term Term))
-> Dom' Term (Type'' Term Term) -> Dom' Term (Type'' Term Term)
forall a b. (a -> b) -> a -> b
$
          Dom' Term (Type'' Term Term)
-> (Type'' Term Term -> Dom' Term (Type'' Term Term))
-> Maybe (Type'' Term Term)
-> Dom' Term (Type'' Term Term)
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Dom' Term (Type'' Term Term)
dom (Dom' Term (Type'' Term Term)
dom Dom' Term (Type'' Term Term)
-> Type'' Term Term -> Dom' Term (Type'' Term Term)
forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$>) Maybe (Type'' Term Term)
mt
    v <- lambdaAddContext x (absName b) dom'  $
      checkPostponedLambda0 cmp (Arg info (xs, mt)) body $ absBody b
    let v' = ArgInfo -> Abs Term -> Term
Lam ArgInfo
info' (Abs Term -> Term) -> Abs Term -> Term
forall a b. (a -> b) -> a -> b
$ ArgName -> Term -> Abs Term
forall a. ArgName -> a -> Abs a
Abs (Name -> ArgName
nameToArgName Name
x) Term
v
    maybe (return v') (blockTermOnProblem t v') mpid

checkPostponedLambda0 :: Comparison -> Arg ([WithHiding Name], Maybe Type) -> A.Expr -> Type -> TCM Term
checkPostponedLambda0 :: Comparison
-> Arg ([WithHiding Name], Maybe (Type'' Term Term))
-> Expr
-> Type'' Term Term
-> TCMT IO Term
checkPostponedLambda0 Comparison
cmp (Arg ArgInfo
_    ([]    , Maybe (Type'' Term Term)
_ )) Expr
body Type'' Term Term
target =
  Comparison -> Expr -> Type'' Term Term -> TCMT IO Term
checkExpr' Comparison
cmp Expr
body Type'' Term Term
target
checkPostponedLambda0 Comparison
cmp (Arg ArgInfo
info (WithHiding Name
x : [WithHiding Name]
xs, Maybe (Type'' Term Term)
mt)) Expr
body Type'' Term Term
target =
  Comparison
-> Arg (List1 (WithHiding Name), Maybe (Type'' Term Term))
-> Expr
-> Type'' Term Term
-> TCMT IO Term
checkPostponedLambda Comparison
cmp (ArgInfo
-> (List1 (WithHiding Name), Maybe (Type'' Term Term))
-> Arg (List1 (WithHiding Name), Maybe (Type'' Term Term))
forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
info (WithHiding Name
x WithHiding Name -> [WithHiding Name] -> List1 (WithHiding Name)
forall a. a -> [a] -> NonEmpty a
:| [WithHiding Name]
xs, Maybe (Type'' Term Term)
mt)) Expr
body Type'' Term Term
target


-- | Insert hidden lambda until the hiding info of the domain type
--   matches the expected hiding info.
--   Throws 'WrongHidingInLambda'
insertHiddenLambdas
  :: Hiding                       -- ^ Expected hiding.
  -> Type                         -- ^ Expected to be a function type.
  -> (Blocker -> Type -> TCM Term) -- ^ Continuation on blocked type.
  -> (Type -> TCM Term)           -- ^ Continuation when expected hiding found.
                                  --   The continuation may assume that the @Type@
                                  --   is of the form @(El _ (Pi _ _))@.
  -> TCM Term                     -- ^ Term with hidden lambda inserted.
insertHiddenLambdas :: Hiding
-> Type'' Term Term
-> (Blocker -> Type'' Term Term -> TCMT IO Term)
-> (Type'' Term Term -> TCMT IO Term)
-> TCMT IO Term
insertHiddenLambdas Hiding
h Type'' Term Term
target Blocker -> Type'' Term Term -> TCMT IO Term
postpone Type'' Term Term -> TCMT IO Term
ret = do
  -- If the target type is blocked, we postpone,
  -- because we do not know if a hidden lambda needs to be inserted.
  Type'' Term Term
-> (Blocker -> Type'' Term Term -> TCMT IO Term)
-> (NotBlocked -> Type'' Term Term -> TCMT IO Term)
-> TCMT IO Term
forall t (m :: * -> *) a.
(Reduce t, IsMeta t, MonadReduce m) =>
t -> (Blocker -> t -> m a) -> (NotBlocked -> t -> m a) -> m a
ifBlocked Type'' Term Term
target Blocker -> Type'' Term Term -> TCMT IO Term
postpone ((NotBlocked -> Type'' Term Term -> TCMT IO Term) -> TCMT IO Term)
-> (NotBlocked -> Type'' Term Term -> TCMT IO Term) -> TCMT IO Term
forall a b. (a -> b) -> a -> b
$ \ NotBlocked
_ Type'' Term Term
t -> do
    case Type'' Term Term -> Term
forall t a. Type'' t a -> a
unEl Type'' Term Term
t of

      Pi Dom' Term (Type'' Term Term)
dom Abs (Type'' Term Term)
b -> do
        let h' :: Hiding
h' = Dom' Term (Type'' Term Term) -> Hiding
forall a. LensHiding a => a -> Hiding
getHiding Dom' Term (Type'' Term Term)
dom
        -- Found expected hiding: return function type.
        if Hiding -> Hiding -> Bool
forall a b. (LensHiding a, LensHiding b) => a -> b -> Bool
sameHiding Hiding
h Hiding
h' then Type'' Term Term -> TCMT IO Term
ret Type'' Term Term
t else do
          -- Found a visible argument but expected a hidden one:
          -- That's an error, as we cannot insert a visible lambda.
          if Hiding -> Bool
forall a. LensHiding a => a -> Bool
visible Hiding
h' then TypeError -> TCMT IO Term
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> TCMT IO Term) -> TypeError -> TCMT IO Term
forall a b. (a -> b) -> a -> b
$ Type'' Term Term -> TypeError
WrongHidingInLambda Type'' Term Term
target else do
            -- Otherwise, we found a hidden argument that we can insert.
            let x :: ArgName
x    = Abs (Type'' Term Term) -> ArgName
forall a. Abs a -> ArgName
absName Abs (Type'' Term Term)
b
            ArgInfo -> Abs Term -> Term
Lam (Origin -> ArgInfo -> ArgInfo
forall a. LensOrigin a => Origin -> a -> a
setOrigin Origin
Inserted (ArgInfo -> ArgInfo) -> ArgInfo -> ArgInfo
forall a b. (a -> b) -> a -> b
$ Dom' Term (Type'' Term Term) -> ArgInfo
forall t e. Dom' t e -> ArgInfo
domInfo Dom' Term (Type'' Term Term)
dom) (Abs Term -> Term) -> (Term -> Abs Term) -> Term -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ArgName -> Term -> Abs Term
forall a. ArgName -> a -> Abs a
Abs ArgName
x (Term -> Term) -> TCMT IO Term -> TCMT IO Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do
              (ArgName, Dom' Term (Type'' Term Term))
-> TCMT IO Term -> TCMT IO Term
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
(ArgName, Dom' Term (Type'' Term Term)) -> m a -> m a
addContext (ArgName
x, Dom' Term (Type'' Term Term)
dom) (TCMT IO Term -> TCMT IO Term) -> TCMT IO Term -> TCMT IO Term
forall a b. (a -> b) -> a -> b
$ Hiding
-> Type'' Term Term
-> (Blocker -> Type'' Term Term -> TCMT IO Term)
-> (Type'' Term Term -> TCMT IO Term)
-> TCMT IO Term
insertHiddenLambdas Hiding
h (Abs (Type'' Term Term) -> Type'' Term Term
forall a. Subst a => Abs a -> a
absBody Abs (Type'' Term Term)
b) Blocker -> Type'' Term Term -> TCMT IO Term
postpone Type'' Term Term -> TCMT IO Term
ret

      Term
_ -> TypeError -> TCMT IO Term
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> TCMT IO Term) -> TypeError -> TCMT IO Term
forall a b. (a -> b) -> a -> b
$ Type'' Term Term -> TypeError
ShouldBePi Type'' Term Term
target

-- | @checkAbsurdLambda i h e t@ checks absurd lambda against type @t@.
--   Precondition: @e = AbsurdLam i h@
checkAbsurdLambda :: Comparison -> A.ExprInfo -> Hiding -> A.Expr -> Type -> TCM Term
checkAbsurdLambda :: Comparison
-> ExprInfo -> Hiding -> Expr -> Type'' Term Term -> TCMT IO Term
checkAbsurdLambda Comparison
cmp ExprInfo
i Hiding
h Expr
e Type'' Term Term
t =
  TCMT IO Term -> TCMT IO Term
forall a. TCM a -> TCM a
setRunTimeModeUnlessInHardCompileTimeMode (TCMT IO Term -> TCMT IO Term) -> TCMT IO Term -> TCMT IO Term
forall a b. (a -> b) -> a -> b
$ do
      -- Andreas, 2019-10-01: check absurd lambdas in non-erased mode.
      -- Otherwise, they are not usable in meta-solutions in the term world.
      -- See test/Succeed/Issue3176.agda for an absurd lambda
      -- created in types.
      -- #4743: Except if hard compile-time mode is enabled.
  t <- Type'' Term Term -> TCM (Type'' Term Term)
forall a (m :: * -> *).
(InstantiateFull a, MonadReduce m) =>
a -> m a
instantiateFull Type'' Term Term
t
  ifBlocked t (\ Blocker
blocker Type'' Term Term
t' -> TypeCheckingProblem -> Blocker -> TCMT IO Term
postponeTypeCheckingProblem (Comparison -> Expr -> Type'' Term Term -> TypeCheckingProblem
CheckExpr Comparison
cmp Expr
e Type'' Term Term
t') Blocker
blocker) $ \ NotBlocked
_ Type'' Term Term
t' -> do
    case Type'' Term Term -> Term
forall t a. Type'' t a -> a
unEl Type'' Term Term
t' of
      Pi dom :: Dom' Term (Type'' Term Term)
dom@(Dom' Term (Type'' Term Term) -> Type'' Term Term
forall t e. Dom' t e -> e
unDom -> Type'' Term Term
a) Abs (Type'' Term Term)
b -> do
        let info' :: ArgInfo
info' = Dom' Term (Type'' Term Term)
dom Dom' Term (Type'' Term Term)
-> Getting ArgInfo (Dom' Term (Type'' Term Term)) ArgInfo
-> ArgInfo
forall s a. s -> Getting a s a -> a
^. Getting ArgInfo (Dom' Term (Type'' Term Term)) ArgInfo
forall t e (f :: * -> *).
Functor f =>
(ArgInfo -> f ArgInfo) -> Dom' t e -> f (Dom' t e)
dInfo
        if Bool -> Bool
not (Hiding -> ArgInfo -> Bool
forall a b. (LensHiding a, LensHiding b) => a -> b -> Bool
sameHiding Hiding
h ArgInfo
info') then
          TypeError -> TCMT IO Term
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> TCMT IO Term) -> TypeError -> TCMT IO Term
forall a b. (a -> b) -> a -> b
$ Type'' Term Term -> TypeError
WrongHidingInLambda Type'' Term Term
t'
        else Type'' Term Term -> TCMT IO Term -> TCMT IO Term
blockTerm Type'' Term Term
t' (TCMT IO Term -> TCMT IO Term) -> TCMT IO Term -> TCMT IO Term
forall a b. (a -> b) -> a -> b
$ do
          Range' SrcFile -> Type'' Term Term -> TCM ()
ensureEmptyType (ExprInfo -> Range' SrcFile
forall a. HasRange a => a -> Range' SrcFile
getRange ExprInfo
i) Type'' Term Term
a
          -- Add helper function
          aux <- Range' SrcFile
-> Dom' Term (Type'' Term Term)
-> Abs (Type'' Term Term)
-> TCM QName
makeAbsurdLambda (ExprInfo -> Range' SrcFile
forall a. HasRange a => a -> Range' SrcFile
getRange ExprInfo
i) Dom' Term (Type'' Term Term)
dom Abs (Type'' Term Term)
b
          -- Andreas 2012-01-30: since aux is lifted to toplevel
          -- it needs to be applied to the current telescope (issue 557)
          Def aux . map' Apply . teleArgs <$> getContextTelescope
      Term
_ -> TypeError -> TCMT IO Term
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> TCMT IO Term) -> TypeError -> TCMT IO Term
forall a b. (a -> b) -> a -> b
$ Type'' Term Term -> TypeError
ShouldBePi Type'' Term Term
t'

-- Create an absurd lambda with the given type.
-- Precondition: the given type is a pi type with an empty domain.
makeAbsurdLambda :: Range -> Dom Type -> Abs Type -> TCM QName
makeAbsurdLambda :: Range' SrcFile
-> Dom' Term (Type'' Term Term)
-> Abs (Type'' Term Term)
-> TCM QName
makeAbsurdLambda Range' SrcFile
r Dom' Term (Type'' Term Term)
a Abs (Type'' Term Term)
b = do
  let t :: Term
t = Dom' Term (Type'' Term Term) -> Abs (Type'' Term Term) -> Term
Pi Dom' Term (Type'' Term Term)
a Abs (Type'' Term Term)
b
      s :: Sort' Term
s = Dom' Term (Type'' Term Term)
-> Abs (Type'' Term Term) -> Sort' Term
mkPiSort Dom' Term (Type'' Term Term)
a Abs (Type'' Term Term)
b
      info :: ArgInfo
info = Dom' Term (Type'' Term Term) -> ArgInfo
forall t e. Dom' t e -> ArgInfo
domInfo Dom' Term (Type'' Term Term)
a
  top <- TCMT IO ModuleName
forall (m :: * -> *). MonadTCEnv m => m ModuleName
currentModule
  aux <- qualify top <$> freshName_ (r, absurdLambdaName)
  -- if we are in irrelevant / erased position, the helper function
  -- is added as irrelevant / erased
  mod <- currentModality
  reportSDoc "tc.term.absurd" 10 $ vcat
    [ ("Adding absurd function" <+> prettyTCM mod) <> prettyTCM aux
    , nest 2 $ "of type" <+> prettyTCM t
    ]
  lang <- getLanguage
  fun  <- emptyFunctionData
  addConstant aux $
    (\ Defn
d -> (ArgInfo
-> QName -> Type'' Term Term -> Language -> Defn -> Definition
defaultDefn (Modality -> ArgInfo -> ArgInfo
forall a. LensModality a => Modality -> a -> a
setModality Modality
mod ArgInfo
info) QName
aux (Sort' Term -> Term -> Type'' Term Term
forall t a. Sort' t -> a -> Type'' t a
El Sort' Term
s Term
t) Language
lang Defn
d)
            { defPolarity       = [Nonvariant]
            , defArgOccurrences = [Unused] })
    $ FunctionDefn fun
      { _funClauses        =
          [ Clause
            { clauseLHSRange  = r
            , clauseFullRange = r
            , clauseTel       = telFromList [fmap (absurdPatternName,) a]
            , namedClausePats = [Arg info $ Named (Just $ WithOrigin Inserted $ unranged $ absName b) $ absurdP 0]
            , clauseBody      = Nothing
            , clauseType      = Just $ setModality mod $ defaultArg $ absBody b
            , clauseCatchall    = YesCatchall empty      -- absurd clauses are safe as catch-alls
            , clauseRecursive   = NotRecursive
            , clauseUnreachable = Just True -- absurd clauses are unreachable
            , clauseEllipsis    = NoEllipsis
            , clauseWhereModule = Nothing
            }
          ]
      , _funCompiled       = Just $ Fail [Arg info "()"]
      , _funSplitTree      = Just $ SplittingDone 0
      , _funMutual         = Just []
      , _funTerminates     = Just True
      , _funExtLam         = Just $ ExtLamInfo top True empty
      }
  return aux

-- | @checkExtendedLambda i di erased qname cs e t@ check pattern matching lambda.
-- Precondition: @e = ExtendedLam i di erased qname cs@
checkExtendedLambda ::
  Comparison -> A.ExprInfo -> A.DefInfo -> Erased -> QName ->
  List1 A.Clause -> A.Expr -> Type -> TCM Term
checkExtendedLambda :: Comparison
-> ExprInfo
-> DefInfo
-> Erased
-> QName
-> NonEmpty Clause
-> Expr
-> Type'' Term Term
-> TCMT IO Term
checkExtendedLambda Comparison
cmp ExprInfo
i DefInfo
di Erased
erased QName
qname NonEmpty Clause
cs Expr
e Type'' Term Term
t = do
  mod <- TCMT IO Modality
forall (m :: * -> *). MonadTCEnv m => m Modality
currentModality
  when (isErased erased && not (hasQuantity0 mod)) $ typeError LambdaIsErased
  setModeUnlessInHardCompileTimeMode erased do
         -- Erased pattern-matching lambdas are checked in hard
         -- compile-time mode. For non-erased pattern-matching lambdas
         -- run-time mode is used, unless the current mode is hard
         -- compile-time mode.
    -- Andreas, 2016-06-16 issue #2045
    -- Try to get rid of unsolved size metas before we
    -- fix the type of the extended lambda auxiliary function
    solveSizeConstraints DontDefaultToInfty
    lamMod <- inFreshModuleIfFreeParams currentModule  -- #2883: need a fresh module if refined params
    t <- instantiateFull t
    ifBlocked t (\ Blocker
m Type'' Term Term
t' -> TypeCheckingProblem -> TCMT IO Term
postponeTypeCheckingProblem_ (TypeCheckingProblem -> TCMT IO Term)
-> TypeCheckingProblem -> TCMT IO Term
forall a b. (a -> b) -> a -> b
$ Comparison -> Expr -> Type'' Term Term -> TypeCheckingProblem
CheckExpr Comparison
cmp Expr
e Type'' Term Term
t') \ NotBlocked
_ Type'' Term Term
t -> do
      j   <- TCM MutualId
currentOrFreshMutualBlock
      mod <- currentModality
      let info = Modality -> ArgInfo -> ArgInfo
forall a. LensModality a => Modality -> a -> a
setModality Modality
mod ArgInfo
defaultArgInfo

      reportSDoc "tc.term.exlam" 20 $ vcat
        [ hsep
          [ text $ show $ A.defAbstract di
          , "extended lambda's implementation"
          , doubleQuotes $ prettyTCM qname
          , "has type:"
          ]
        , prettyTCM t -- <+> " where clauses: " <+> text (show cs)
        ]
      args     <- getContextArgs

      -- Andreas, Ulf, 2016-02-02: We want to postpone type checking an extended lambda
      -- in case the lhs checker failed due to insufficient type info for the patterns.
      -- Issues 480, 1159, 1811.
      abstract (A.defAbstract di) do
        -- Andreas, 2013-12-28: add extendedlambda as @Function@, not as @Axiom@;
        -- otherwise, @addClause@ in @checkFunDef'@ fails (see issue 1009).
        addConstant qname =<< do
          lang <- getLanguage
          fun  <- emptyFunction
          useTerPragma $
            (defaultDefn info qname t lang fun)
              { defMutual = j }
        checkFunDef' t info (Just $ ExtLamInfo lamMod False empty) di qname $
          List1.toList cs
        whenNothingM (viewTC eMutualBlock) $
          -- Andrea 10-03-2018: Should other checks be performed here too? e.g. termination/positivity/..
          checkIApplyConfluence_ qname
        return $! Def qname $! map' Apply args
  where
    -- Concrete definitions cannot use information about abstract things.
    abstract :: IsAbstract -> m a -> m a
abstract IsAbstract
ConcreteDef = m a -> m a
forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
inConcreteMode
    abstract IsAbstract
AbstractDef = m a -> m a
forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
inAbstractMode

-- | Run a computation.
--
--   * If successful, that's it, we are done.
--
--   * If @NotADatatype a@ or @CannotEliminateWithPattern p a@
--     is thrown and type @a@ is blocked on some meta @x@,
--     reset any changes to the state and pass (the error and) @x@ to the handler.
--
--   * If @SplitError (UnificationStuck c tel us vs _)@ is thrown and the unification
--     problem @us =?= vs : tel@ is blocked on some meta @x@ pass @x@ to the handler.
--
--   * If another error was thrown or the type @a@ is not blocked, reraise the error.
--
--   Note that the returned meta might only exists in the state where the error was
--   thrown, thus, be an invalid 'MetaId' in the current state.
--
catchIlltypedPatternBlockedOnMeta :: TCM a -> ((TCErr, Blocker) -> TCM a) -> TCM a
catchIlltypedPatternBlockedOnMeta :: forall a. TCM a -> ((TCErr, Blocker) -> TCM a) -> TCM a
catchIlltypedPatternBlockedOnMeta TCM a
m (TCErr, Blocker) -> TCM a
handle = do

  -- Andreas, 2016-07-13, issue 2028.
  -- Save the state to rollback the changes to the signature.
  st <- TCMT IO TCState
forall (m :: * -> *). MonadTCState m => m TCState
getTC

  m `catchError` \ TCErr
err -> do

    let reraise :: MonadError TCErr m => m a
        reraise :: forall (m :: * -> *) a. MonadError TCErr m => m a
reraise = TCErr -> m a
forall a. TCErr -> m a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError TCErr
err

    -- Get the blocker responsible for the type error.
    -- If we do not find a blocker or the error should not be handled,
    -- we reraise the error.
    blocker <- TCMT IO Blocker
-> (Blocker -> TCMT IO Blocker) -> Maybe Blocker -> TCMT IO Blocker
forall b a. b -> (a -> b) -> Maybe a -> b
maybe TCMT IO Blocker
forall (m :: * -> *) a. MonadError TCErr m => m a
reraise Blocker -> TCMT IO Blocker
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe Blocker -> TCMT IO Blocker)
-> Maybe Blocker -> TCMT IO Blocker
forall a b. (a -> b) -> a -> b
$! case TCErr
err of
      TypeError CallStack
_ TCState
s Closure TypeError
cl -> case Closure TypeError -> TypeError
forall a. Closure a -> a
clValue Closure TypeError
cl of
        SortOfSplitVarError Maybe Blocker
b Doc
_                       -> Maybe Blocker
b
        SplitError (UnificationStuck Maybe Blocker
b QName
c Telescope
tel [Arg Term]
us [Arg Term]
vs [UnificationFailure]
_) -> Maybe Blocker
b
        SplitError (BlockedType Blocker
b Closure (Type'' Term Term)
aClosure)           -> Blocker -> Maybe Blocker
forall a. a -> Maybe a
Just Blocker
b
        CannotEliminateWithPattern Maybe Blocker
b NamedArg (Pattern' Expr)
p Type'' Term Term
a              -> Maybe Blocker
b
        CannotEliminateWithProjection Maybe Blocker
b Arg (Type'' Term Term)
_ Bool
_ QName
_         -> Maybe Blocker
b
        -- Andrea: TODO look for blocking meta in tClosure and its Sort.
        -- SplitError (CannotCreateMissingClause _ _ _ tClosure) ->
        TypeError
_                                             -> Maybe Blocker
forall a. Maybe a
Nothing
      TCErr
_ -> Maybe Blocker
forall a. Maybe a
Nothing

    reportSDoc "tc.postpone" 20 $ vcat $
      [ "checking definition blocked on: " <+> prettyTCM blocker ]

    -- Note that we messed up the state a bit.  We might want to unroll these state changes.
    -- However, they are mostly harmless:
    -- 1. We created a new mutual block id.
    -- 2. We added a constant without definition.
    -- In fact, they are not so harmless, see issue 2028!
    -- Thus, reset the state!
    putTC st

    -- There might be metas in the blocker not known in the reset state, as they could have been
    -- created somewhere on the way to the type error.
    blocker <- (`onBlockingMetasM` blocker) $ \ MetaId
x ->
                MetaId -> TCMT IO (Maybe (Either RemoteMetaVariable MetaVariable))
forall (m :: * -> *).
ReadTCState m =>
MetaId -> m (Maybe (Either RemoteMetaVariable MetaVariable))
lookupMeta MetaId
x TCMT IO (Maybe (Either RemoteMetaVariable MetaVariable))
-> (Maybe (Either RemoteMetaVariable MetaVariable)
    -> TCMT IO Blocker)
-> TCMT IO Blocker
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
      -- Case: we do not know the meta, so cannot unblock.
      Maybe (Either RemoteMetaVariable MetaVariable)
Nothing -> Blocker -> TCMT IO Blocker
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Blocker
neverUnblock
      -- Case: we know the meta here.
      -- Just m | InstV{} <- mvInstantiation m -> __IMPOSSIBLE__  -- It cannot be instantiated yet.
      -- Andreas, 2018-11-23: I do not understand why @InstV@ is necessarily impossible.
      -- The reasoning is probably that the state @st@ is more advanced that @s@
      -- in which @x@ was blocking, thus metas in @st@ should be more instantiated than
      -- in @s@.  But issue #3403 presents a counterexample, so let's play save and reraise.
      -- Ulf, 2020-08-13: But treat this case as not blocked and reraise on both always and never.
      -- Ulf, 2020-08-13: Previously we returned neverUnblock for frozen metas here, but this is in
      -- fact not very helpful. Yes there is no hope of solving the problem, but throwing a hard
      -- error means we rob the user of the tools needed to figure out why the meta has not been
      -- solved. Better to leave the constraint.
      Just Left{} -> Blocker -> TCMT IO Blocker
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Blocker
alwaysUnblock
      Just (Right MetaVariable
m)
        | InstV{} <- MetaVariable -> MetaInstantiation
mvInstantiation MetaVariable
m -> Blocker -> TCMT IO Blocker
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Blocker
alwaysUnblock
        | Bool
otherwise                    -> Blocker -> TCMT IO Blocker
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Blocker -> TCMT IO Blocker) -> Blocker -> TCMT IO Blocker
forall a b. (a -> b) -> a -> b
$! MetaId -> Blocker
unblockOnMeta MetaId
x

    -- If it's not blocked or we can't ever unblock reraise the error.
    if blocker `elem` [neverUnblock, alwaysUnblock] then reraise else handle (err, blocker)

---------------------------------------------------------------------------
-- * Records
---------------------------------------------------------------------------

-- | Picks up record field assignments from modules that export a definition
--   that has the same name as the missing field.

expandModuleAssigns
  :: [Either A.Assign A.ModuleName]  -- ^ Modules and field assignments.
  -> [C.Name]                        -- ^ Names of fields of the record type.
  -> TCM A.Assigns                   -- ^ Completed field assignments from modules.
expandModuleAssigns :: [Either (FieldAssignment' Expr) ModuleName]
-> [Name] -> TCM Assigns
expandModuleAssigns [Either (FieldAssignment' Expr) ModuleName]
mfs [Name]
xs = do
  let (Assigns
fs , [ModuleName]
ms) = [Either (FieldAssignment' Expr) ModuleName]
-> (Assigns, [ModuleName])
forall a b. [Either a b] -> ([a], [b])
partitionEithers [Either (FieldAssignment' Expr) ModuleName]
mfs

  -- The fields of the record that have not been given by field assignments @fs@
  -- are looked up in the given modules @ms@.
  fs' <- [Name]
-> (Name -> TCMT IO (Maybe (FieldAssignment' Expr)))
-> TCMT IO [Maybe (FieldAssignment' Expr)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM ([Name]
xs [Name] -> [Name] -> [Name]
forall a. Eq a => [a] -> [a] -> [a]
List.\\ (FieldAssignment' Expr -> Name) -> Assigns -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map' (Getting Name (FieldAssignment' Expr) Name
-> FieldAssignment' Expr -> Name
forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a
view Getting Name (FieldAssignment' Expr) Name
forall a (f :: * -> *).
Functor f =>
(Name -> f Name) -> FieldAssignment' a -> f (FieldAssignment' a)
nameFieldA) Assigns
fs) ((Name -> TCMT IO (Maybe (FieldAssignment' Expr)))
 -> TCMT IO [Maybe (FieldAssignment' Expr)])
-> (Name -> TCMT IO (Maybe (FieldAssignment' Expr)))
-> TCMT IO [Maybe (FieldAssignment' Expr)]
forall a b. (a -> b) -> a -> b
$ \ Name
f -> do

    -- Get the possible assignments for field f from the modules.
    pms <- [ModuleName]
-> (ModuleName
    -> TCMT IO (Maybe (ModuleName, FieldAssignment' Expr)))
-> TCMT IO [Maybe (ModuleName, FieldAssignment' Expr)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [ModuleName]
ms ((ModuleName
  -> TCMT IO (Maybe (ModuleName, FieldAssignment' Expr)))
 -> TCMT IO [Maybe (ModuleName, FieldAssignment' Expr)])
-> (ModuleName
    -> TCMT IO (Maybe (ModuleName, FieldAssignment' Expr)))
-> TCMT IO [Maybe (ModuleName, FieldAssignment' Expr)]
forall a b. (a -> b) -> a -> b
$ \ ModuleName
m -> do
      modScope <- ModuleName -> ScopeM Scope
getNamedScope ModuleName
m
      let names :: ThingsInScope AbstractName
          names = Scope -> ThingsInScope AbstractName
forall a. InScope a => Scope -> ThingsInScope a
exportedNamesInScope Scope
modScope
      return $
        case Map.lookup f names of
          Just (AbstractName
n :| []) -> (ModuleName, FieldAssignment' Expr)
-> Maybe (ModuleName, FieldAssignment' Expr)
forall a. a -> Maybe a
Just (ModuleName
m, Name -> Expr -> FieldAssignment' Expr
forall a. Name -> a -> FieldAssignment' a
FieldAssignment Name
f (Expr -> FieldAssignment' Expr) -> Expr -> FieldAssignment' Expr
forall a b. (a -> b) -> a -> b
$ Expr -> Expr
forall a. KillRange a => KillRangeT a
killRange (Expr -> Expr) -> Expr -> Expr
forall a b. (a -> b) -> a -> b
$ AbstractName -> Expr
forall a. NameToExpr a => a -> Expr
A.nameToExpr AbstractName
n)
          Maybe (List1 AbstractName)
_ -> Maybe (ModuleName, FieldAssignment' Expr)
forall a. Maybe a
Nothing

    -- If we have several matching assignments, that's an error.
    case catMaybes pms of
      []        -> Maybe (FieldAssignment' Expr)
-> TCMT IO (Maybe (FieldAssignment' Expr))
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (FieldAssignment' Expr)
forall a. Maybe a
Nothing
      [(ModuleName
_, FieldAssignment' Expr
fa)] -> Maybe (FieldAssignment' Expr)
-> TCMT IO (Maybe (FieldAssignment' Expr))
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (FieldAssignment' Expr -> Maybe (FieldAssignment' Expr)
forall a. a -> Maybe a
Just FieldAssignment' Expr
fa)
      (ModuleName, FieldAssignment' Expr)
x:(ModuleName, FieldAssignment' Expr)
y:[(ModuleName, FieldAssignment' Expr)]
zs    -> TypeError -> TCMT IO (Maybe (FieldAssignment' Expr))
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> TCMT IO (Maybe (FieldAssignment' Expr)))
-> TypeError -> TCMT IO (Maybe (FieldAssignment' Expr))
forall a b. (a -> b) -> a -> b
$ Name -> List2 ModuleName -> TypeError
AmbiguousField Name
f (List2 ModuleName -> TypeError) -> List2 ModuleName -> TypeError
forall a b. (a -> b) -> a -> b
$ ((ModuleName, FieldAssignment' Expr) -> ModuleName)
-> List2 (ModuleName, FieldAssignment' Expr) -> List2 ModuleName
forall a b. (a -> b) -> List2 a -> List2 b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (ModuleName, FieldAssignment' Expr) -> ModuleName
forall a b. (a, b) -> a
fst (List2 (ModuleName, FieldAssignment' Expr) -> List2 ModuleName)
-> List2 (ModuleName, FieldAssignment' Expr) -> List2 ModuleName
forall a b. (a -> b) -> a -> b
$ (ModuleName, FieldAssignment' Expr)
-> (ModuleName, FieldAssignment' Expr)
-> [(ModuleName, FieldAssignment' Expr)]
-> List2 (ModuleName, FieldAssignment' Expr)
forall a. a -> a -> [a] -> List2 a
List2 (ModuleName, FieldAssignment' Expr)
x (ModuleName, FieldAssignment' Expr)
y [(ModuleName, FieldAssignment' Expr)]
zs
  return (fs ++! catMaybes fs')

-- | @checkRecordExpression fs e t@ checks record construction against type @t@.
-- Precondition @e = Rec _ fs@.
checkRecordExpression
  :: Comparison       -- ^ How do we related the inferred type of the record expression
                      --   to the expected type?  Subtype or equal type?
  -> A.RecordAssigns  -- ^ @mfs@: modules and field assignments.
  -> A.Expr           -- ^ Must be @A.Rec _ mfs@.
  -> Type             -- ^ Expected type of record expression.
  -> ConOrigin        -- ^ Is this a record expression or a @record where@ expression?
  -> TCM Term         -- ^ Record value in internal syntax.
checkRecordExpression :: Comparison
-> [Either (FieldAssignment' Expr) ModuleName]
-> Expr
-> Type'' Term Term
-> ConOrigin
-> TCMT IO Term
checkRecordExpression Comparison
cmp [Either (FieldAssignment' Expr) ModuleName]
mfs e :: Expr
e@(A.Rec KwRange
kwr ExprInfo
_r [Either (FieldAssignment' Expr) ModuleName]
_) Type'' Term Term
t ConOrigin
origin = do
  ArgName -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m ()
reportSDoc ArgName
"tc.term.rec" Int
10 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
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
"checking record expression"
    , Expr -> TCMT IO Doc
forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA Expr
e
    ]
  let
    resume :: TCMT IO Term
resume = TypeCheckingProblem -> TCMT IO Term
postponeTypeCheckingProblem_ (TypeCheckingProblem -> TCMT IO Term)
-> TypeCheckingProblem -> TCMT IO Term
forall a b. (a -> b) -> a -> b
$ Comparison -> Expr -> Type'' Term Term -> TypeCheckingProblem
CheckExpr Comparison
cmp Expr
e Type'' Term Term
t
    fields :: [Name]
fields = [ Name
x | Left (FieldAssignment Name
x Expr
_) <- [Either (FieldAssignment' Expr) ModuleName]
mfs ]
  Type'' Term Term
-> (Blocker -> Type'' Term Term -> TCMT IO Term)
-> (NotBlocked -> Type'' Term Term -> TCMT IO Term)
-> TCMT IO Term
forall t (m :: * -> *) a.
(Reduce t, IsMeta t, MonadReduce m) =>
t -> (Blocker -> t -> m a) -> (NotBlocked -> t -> m a) -> m a
ifBlocked Type'' Term Term
t (\ Blocker
_ Type'' Term Term
t -> TCMT IO Term
-> Comparison -> Expr -> [Name] -> Type'' Term Term -> TCMT IO Term
guessRecordType TCMT IO Term
resume Comparison
cmp Expr
e [Name]
fields Type'' Term Term
t) {-else-} ((NotBlocked -> Type'' Term Term -> TCMT IO Term) -> TCMT IO Term)
-> (NotBlocked -> Type'' Term Term -> TCMT IO Term) -> TCMT IO Term
forall a b. (a -> b) -> a -> b
$ \ NotBlocked
_ Type'' Term Term
t -> do
  case Type'' Term Term -> Term
forall t a. Type'' t a -> a
unEl Type'' Term Term
t of
    -- Case: We know the type of the record already.
    Def QName
r Elims
es  -> do
      let vs :: [Arg Term]
vs = Elims -> [Arg Term]
forall a. [Elim' a] -> [Arg a]
mustAllApplyElims Elims
es
      ArgName -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m ()
reportSDoc ArgName
"tc.term.rec" Int
20 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"  r   = " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall a. Semigroup a => a -> a -> a
<> Doc -> TCMT IO Doc
forall a. a -> TCMT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (QName -> Doc
forall a. Pretty a => a -> Doc
P.pretty QName
r)

      def <- QName -> TCMT IO RecordData
forall (m :: * -> *).
(HasCallStack, HasConstInfo m, ReadTCState m,
 MonadError TCErr m) =>
QName -> m RecordData
getRecordDef QName
r
      let -- Field names (C.Name) with ArgInfo from record type definition.
          cxs  = (Dom Name -> Arg Name) -> [Dom Name] -> [Arg Name]
forall a b. (a -> b) -> [a] -> [b]
map' Dom Name -> Arg Name
forall t a. Dom' t a -> Arg a
argFromDom ([Dom Name] -> [Arg Name]) -> [Dom Name] -> [Arg Name]
forall a b. (a -> b) -> a -> b
$ RecordData -> [Dom Name]
recordFieldNames RecordData
def
          -- Just field names.
          xs   = (Arg Name -> Name) -> [Arg Name] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map' Arg Name -> Name
forall e. Arg e -> e
unArg [Arg Name]
cxs
          -- Record constructor.
          con  = KillRangeT ConHead
forall a. KillRange a => KillRangeT a
killRange KillRangeT ConHead -> KillRangeT ConHead
forall a b. (a -> b) -> a -> b
$ RecordData -> ConHead
_recConHead RecordData
def
      reportSDoc "tc.term.rec" 20 $ vcat
        [ "  xs  = " <> pure (P.pretty xs)
        , "  ftel= " <> prettyTCM (_recTel def)
        , "  con = " <> pure (P.pretty con)
        ]

      -- Record expressions corresponding to erased record
      -- constructors can only be used in compile-time mode.
      constructorQ <- getQuantity <$> getConstInfo (conName con)
      currentQ     <- viewTC eQuantityZeroHardCompile
      unless (constructorQ `moreQuantity` currentQ) $ typeError RecordIsErased

      -- Andreas, 2018-09-06, issue #3122.
      -- Associate the concrete record field names used in the record expression
      -- to their counterpart in the record type definition.
      disambiguateRecordFields (map' _nameFieldA $ lefts mfs) (map' unDom $ _recFields def)

      -- Compute the list of given fields, decorated with the ArgInfo from the record def.
      -- Andreas, 2019-03-18, issue #3122, also pick up non-visible fields from the modules.
      fs <- expandModuleAssigns mfs xs

      -- Compute a list of metas for the missing visible fields.
      scope <- getScope
      let meta Name
x = MetaInfo -> Expr
A.Underscore (MetaInfo -> Expr) -> MetaInfo -> Expr
forall a b. (a -> b) -> a -> b
$ Range' SrcFile
-> ScopeInfo -> Maybe MetaId -> ArgName -> MetaKind -> MetaInfo
A.MetaInfo (KwRange -> Range' SrcFile
forall a. HasRange a => a -> Range' SrcFile
getRange KwRange
kwr) ScopeInfo
scope Maybe MetaId
forall a. Maybe a
Nothing (Name -> ArgName
forall a. Pretty a => a -> ArgName
prettyShow Name
x) MetaKind
A.UnificationMeta
      -- In @es@ omitted explicit fields are replaced by underscores.
      -- Omitted implicit or instance fields
      -- are still left out and inserted later by checkArguments_.
      es <- insertMissingFieldsWarn origin r meta fs cxs

      args <- checkArguments_ cmp ExpandLast e es (_recTel def `apply` vs) >>= \case
        (Elims
elims, Telescope
remainingTel) | Telescope -> Bool
forall a. Null a => a -> Bool
null Telescope
remainingTel
                              , Just [Arg Term]
args <- Elims -> Maybe [Arg Term]
forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims Elims
elims -> [Arg Term] -> TCMT IO [Arg Term]
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return [Arg Term]
args
        (Elims, Telescope)
_ -> TCMT IO [Arg Term]
forall a. HasCallStack => a
__IMPOSSIBLE__
      -- Don't need to block here!
      reportSDoc "tc.term.rec" 20 $ text $ "finished record expression"
      return $! Con con origin $! map' Apply args
    Term
_ -> TypeError -> TCMT IO Term
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> TCMT IO Term) -> TypeError -> TCMT IO Term
forall a b. (a -> b) -> a -> b
$ Type'' Term Term -> TypeError
ShouldBeRecordType Type'' Term Term
t
checkRecordExpression Comparison
_ [Either (FieldAssignment' Expr) ModuleName]
_ Expr
_ Type'' Term Term
_ ConOrigin
_ = TCMT IO Term
forall a. HasCallStack => a
__IMPOSSIBLE__

guessRecordType :: TCM Term -> Comparison -> A.Expr -> [C.Name] -> Type -> TCM Term
guessRecordType :: TCMT IO Term
-> Comparison -> Expr -> [Name] -> Type'' Term Term -> TCMT IO Term
guessRecordType TCMT IO Term
resume Comparison
cmp Expr
e [Name]
fields Type'' Term Term
t = do
  rs <- [Name] -> TCM [QName]
findPossibleRecords [Name]
fields
  reportSDoc "tc.term.rec" 30 $ "Possible records for" <+> prettyTCM t <+> "are" <?> pretty rs
  case rs of
      -- If there are no records with the right fields we might as well fail right away.
    [] -> TypeError -> TCMT IO Term
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> TCMT IO Term) -> TypeError -> TCMT IO Term
forall a b. (a -> b) -> a -> b
$ [Name] -> TypeError
NoKnownRecordWithSuchFields [Name]
fields
      -- If there's only one record with the appropriate fields, go with that.
    [QName
r] -> do
      -- #5198: Don't generate metas for parameters of the current module. In most cases they
      -- get solved, but not always.
      def <- 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
r
      ps  <- freeVarsToApply r
      let rt = Definition -> Type'' Term Term
defType Definition
def
      reportSDoc "tc.term.rec" 30 $ "Type of unique record" <+> prettyTCM rt
      vs  <- newArgsMeta rt
      target <- reduce $ piApply rt vs
      s  <- case unEl target of
        Sort Sort' Term
s  -> Sort' Term -> TCMT IO (Sort' Term)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Sort' Term
s
        Term
v       -> do
          ArgName -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m ()
reportSDoc ArgName
"impossible" Int
10 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
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
"The impossible happened when checking record expression against meta"
            , TCMT IO Doc
"Candidate record type r = " 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
r
            , TCMT IO Doc
"Type of r               = " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Type'' Term Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type'' Term Term -> m Doc
prettyTCM Type'' Term Term
rt
            , TCMT IO Doc
"Ends in (should be sort)= " 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
            , ArgName -> TCMT IO Doc
forall (m :: * -> *). Applicative m => ArgName -> m Doc
text (ArgName -> TCMT IO Doc) -> ArgName -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ ArgName
"  Raw                   =  " ArgName -> ArgName -> ArgName
forall a. [a] -> [a] -> [a]
++! Term -> ArgName
forall a. Show a => a -> ArgName
show Term
v
            ]
          TCMT IO (Sort' Term)
forall a. HasCallStack => a
__IMPOSSIBLE__
      let inferred = Sort' Term -> Term -> Type'' Term Term
forall t a. Sort' t -> a -> Type'' t a
El Sort' Term
s (Term -> Type'' Term Term) -> Term -> Type'' Term Term
forall a b. (a -> b) -> a -> b
$! QName -> Elims -> Term
Def QName
r (Elims -> Term) -> Elims -> Term
forall a b. (a -> b) -> a -> b
$! (Arg Term -> Elim) -> [Arg Term] -> Elims
forall a b. (a -> b) -> [a] -> [b]
map' Arg Term -> Elim
forall a. Arg a -> Elim' a
Apply ([Arg Term]
ps [Arg Term] -> [Arg Term] -> [Arg Term]
forall a. [a] -> [a] -> [a]
++! [Arg Term]
vs)
      v <- checkExpr e inferred
      coerce cmp v inferred t

      -- If there are more than one possible record we postpone
    QName
_:QName
_:[QName]
_ -> do
      ArgName -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m ()
reportSDoc ArgName
"tc.term.expr.rec" Int
10 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
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
"Postponing type checking of"
        , 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
$ Expr -> TCMT IO Doc
forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA Expr
e 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 -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Type'' Term Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type'' Term Term -> m Doc
prettyTCM Type'' Term Term
t
        ]
      TCMT IO Term
resume

-- | @checkRecordUpdate cmp ei recexpr fs e t@
--
-- Preconditions: @e = RecUpdate ei recexpr fs@ and @t@ is reduced.
--
checkRecordUpdate
  :: Comparison   -- ^ @cmp@
  -> KwRange      -- ^ Range of the @record@ keyword.
  -> A.ExprInfo   -- ^ @ei@
  -> A.Expr       -- ^ @recexpr@
  -> A.Assigns    -- ^ @fs@
  -> A.Expr       -- ^ @e = RecUpdate ei recexpr fs@
  -> Type         -- ^ Need not be reduced.
  -> TCM Term
checkRecordUpdate :: Comparison
-> KwRange
-> ExprInfo
-> Expr
-> Assigns
-> Expr
-> Type'' Term Term
-> TCMT IO Term
checkRecordUpdate Comparison
cmp KwRange
kwr ExprInfo
ei Expr
recexpr Assigns
fs Expr
eupd Type'' Term Term
t = do
  Type'' Term Term
-> (Blocker -> Type'' Term Term -> TCMT IO Term)
-> (NotBlocked -> Type'' Term Term -> TCMT IO Term)
-> TCMT IO Term
forall t (m :: * -> *) a.
(Reduce t, IsMeta t, MonadReduce m) =>
t -> (Blocker -> t -> m a) -> (NotBlocked -> t -> m a) -> m a
ifBlocked Type'' Term Term
t (\ Blocker
_ Type'' Term Term
_ -> TCMT IO Term
tryInfer) ((NotBlocked -> Type'' Term Term -> TCMT IO Term) -> TCMT IO Term)
-> (NotBlocked -> Type'' Term Term -> TCMT IO Term) -> TCMT IO Term
forall a b. (a -> b) -> a -> b
$ {-else-} \ NotBlocked
_ Type'' Term Term
t' -> do
    TCMT IO (Maybe (QName, [Arg Term], RecordData))
-> TCMT IO Term
-> ((QName, [Arg Term], RecordData) -> TCMT IO Term)
-> TCMT IO Term
forall (m :: * -> *) a b.
Monad m =>
m (Maybe a) -> m b -> (a -> m b) -> m b
caseMaybeM (Type'' Term Term -> TCMT IO (Maybe (QName, [Arg Term], RecordData))
forall (m :: * -> *).
(HasCallStack, PureTCM m) =>
Type'' Term Term -> m (Maybe (QName, [Arg Term], RecordData))
isRecordType Type'' Term Term
t') TCMT IO Term
should (((QName, [Arg Term], RecordData) -> TCMT IO Term) -> TCMT IO Term)
-> ((QName, [Arg Term], RecordData) -> TCMT IO Term)
-> TCMT IO Term
forall a b. (a -> b) -> a -> b
$ \ (QName
r, [Arg Term]
_pars, RecordData
defn) -> do
      -- Bind the record value (before update) to a fresh @name@.
      v <- Comparison -> Expr -> Type'' Term Term -> TCMT IO Term
checkExpr' Comparison
cmp Expr
recexpr Type'' Term Term
t'
      name <- freshNoName $ getRange recexpr
      addLetBinding defaultArgInfo Inserted name v t' $ do

        let projs = (Dom QName -> Arg QName) -> [Dom QName] -> [Arg QName]
forall a b. (a -> b) -> [a] -> [b]
map' Dom QName -> Arg QName
forall t a. Dom' t a -> Arg a
argFromDom ([Dom QName] -> [Arg QName]) -> [Dom QName] -> [Arg QName]
forall a b. (a -> b) -> a -> b
$ RecordData -> [Dom QName]
_recFields RecordData
defn

        -- Andreas, 2018-09-06, issue #3122.
        -- Associate the concrete record field names used in the record expression
        -- to their counterpart in the record type definition.
        disambiguateRecordFields (map' _nameFieldA fs) (map' unArg projs)

        -- Desugar record update expression into record expression.
        let fs' = (FieldAssignment' Expr -> (Name, Maybe Expr))
-> Assigns -> [(Name, Maybe Expr)]
forall a b. (a -> b) -> [a] -> [b]
map' (\ (FieldAssignment Name
x Expr
e) -> (Name
x, Expr -> Maybe Expr
forall a. a -> Maybe a
Just Expr
e)) Assigns
fs
        let axs = (Dom Name -> Arg Name) -> [Dom Name] -> [Arg Name]
forall a b. (a -> b) -> [a] -> [b]
map' Dom Name -> Arg Name
forall t a. Dom' t a -> Arg a
argFromDom ([Dom Name] -> [Arg Name]) -> [Dom Name] -> [Arg Name]
forall a b. (a -> b) -> a -> b
$ RecordData -> [Dom Name]
recordFieldNames RecordData
defn
        es  <- orderFieldsWarn ConORec r (const Nothing) axs fs'
        let es'  = (Arg QName -> Maybe Expr -> Maybe Expr)
-> [Arg QName] -> [Maybe Expr] -> [Maybe Expr]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (Name -> ExprInfo -> Arg QName -> Maybe Expr -> Maybe Expr
replaceFields Name
name ExprInfo
ei) [Arg QName]
projs [Maybe Expr]
es
        let erec = KwRange
-> ExprInfo -> [Either (FieldAssignment' Expr) ModuleName] -> Expr
A.Rec KwRange
kwr ExprInfo
ei [ FieldAssignment' Expr -> Either (FieldAssignment' Expr) ModuleName
forall a b. a -> Either a b
Left (Name -> Expr -> FieldAssignment' Expr
forall a. Name -> a -> FieldAssignment' a
FieldAssignment Name
x Expr
e) | (Arg ArgInfo
_ Name
x, Just Expr
e) <- [Arg Name] -> [Maybe Expr] -> [(Arg Name, Maybe Expr)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Arg Name]
axs [Maybe Expr]
es' ]
        -- Call the type checker on the desugared syntax.
        checkExpr' cmp erec t
  where
    replaceFields :: Name -> A.ExprInfo -> Arg A.QName -> Maybe A.Expr -> Maybe A.Expr
    replaceFields :: Name -> ExprInfo -> Arg QName -> Maybe Expr -> Maybe Expr
replaceFields Name
name ExprInfo
ei (Arg ArgInfo
ai QName
p) Maybe Expr
Nothing | ArgInfo -> Bool
forall a. LensHiding a => a -> Bool
visible ArgInfo
ai = Expr -> Maybe Expr
forall a. a -> Maybe a
Just (Expr -> Maybe Expr) -> Expr -> Maybe Expr
forall a b. (a -> b) -> a -> b
$
      -- omitted visible fields remain unchanged: @{ ...; p = p name; ...}@
      -- (hidden fields are supposed to be inferred)
      AppInfo -> Expr -> Arg (Named_ Expr) -> Expr
A.App
        (Range' SrcFile -> AppInfo
A.defaultAppInfo (Range' SrcFile -> AppInfo) -> Range' SrcFile -> AppInfo
forall a b. (a -> b) -> a -> b
$ ExprInfo -> Range' SrcFile
forall a. HasRange a => a -> Range' SrcFile
getRange ExprInfo
ei)
        (ProjOrigin -> AmbiguousQName -> Expr
A.Proj ProjOrigin
ProjSystem (AmbiguousQName -> Expr) -> AmbiguousQName -> Expr
forall a b. (a -> b) -> a -> b
$ QName -> AmbiguousQName
unambiguous QName
p)
        (Expr -> Arg (Named_ Expr)
forall a. a -> NamedArg a
defaultNamedArg (Expr -> Arg (Named_ Expr)) -> Expr -> Arg (Named_ Expr)
forall a b. (a -> b) -> a -> b
$ Name -> Expr
A.Var Name
name)
    replaceFields Name
_ ExprInfo
_ Arg QName
_ Maybe Expr
me = Maybe Expr
me  -- other fields get the user-written updates

    tryInfer :: TCMT IO Term
tryInfer = do
      (_, trec) <- Expr -> TCM (Term, Type'' Term Term)
inferExpr Expr
recexpr
      ifBlocked trec (\ Blocker
_ Type'' Term Term
_ -> TCMT IO Term
postpone) $ {-else-} \ NotBlocked
_ Type'' Term Term
_ -> do
        v <- Comparison -> Expr -> Type'' Term Term -> TCMT IO Term
checkExpr' Comparison
cmp Expr
eupd Type'' Term Term
trec
        coerce cmp v trec t

    postpone :: TCMT IO Term
postpone = TypeCheckingProblem -> TCMT IO Term
postponeTypeCheckingProblem_ (TypeCheckingProblem -> TCMT IO Term)
-> TypeCheckingProblem -> TCMT IO Term
forall a b. (a -> b) -> a -> b
$ Comparison -> Expr -> Type'' Term Term -> TypeCheckingProblem
CheckExpr Comparison
cmp Expr
eupd Type'' Term Term
t
    should :: TCMT IO Term
should   = TypeError -> TCMT IO Term
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> TCMT IO Term) -> TypeError -> TCMT IO Term
forall a b. (a -> b) -> a -> b
$ Type'' Term Term -> TypeError
ShouldBeRecordType Type'' Term Term
t

-- | Check a @record where@ expression, pushing information about the
-- type of the fields obtained from the context into the @let@-bindings.
checkRecordWhere
  :: Comparison
  -> KwRange
  -> A.ExprInfo     -- ^ @ei@
  -> Maybe A.Expr   -- ^ are we updating?
  -> [A.LetBinding] -- ^ @ds@
  -> A.Assigns      -- ^ @as@
  -> A.Expr         -- ^ the overall expression (for resumption)
  -> Type
  -> TCM Term

{-
The key problem with simply checking the let bindings and then
checking a made-up record literal is implicit insertion. Consider:

  record X : Set₁ where
    field
      it : {A : Set} → A → A
  _ = record where it x = x

Here we would first check `(λ x → x) : _0`, inventing a fresh meta
for the type of `it`-qua-let-binding, solving `_0 := _1 → _1`
because of the lambda, and then falling over when trying to unify
`_1 → _1 =? ∀ {A} → A → A`. Indeed we also can not simply

  _ = record where it : _0 ; it = ?

since checking the record expression would produce something like
record { it = λ {x} → ?0 }, where 'checkArgumentsE' has "helpfully"
inserted implicit binders for the argument, and `x` is obviously not
in scope in `_0`. But if we tell 'tryInsertHiddenLambda' to take a
hike, we *can* learn the actual type of the record field by putting
a meta there!

So the strategy for pushing type information into the bindings is
the following:

  * For every field-defining LetBind, replace its body with a meta;
    and set aside the actual expression to check later.

  * Check the synthesised record{} expression, but under
    reallyDontExpandLast.
    If the *types* of field bindings were previously bare metas,
    they will now be solved to the types of corresponding fields,
    even if these have implicit arguments.

  * Go back and actually check all the expressions we set aside at the
    start, solving the metas that we invented.
-}
checkRecordWhere :: Comparison
-> KwRange
-> ExprInfo
-> Maybe Expr
-> [LetBinding]
-> Assigns
-> Expr
-> Type'' Term Term
-> TCMT IO Term
checkRecordWhere Comparison
cmp KwRange
kwr ExprInfo
ei Maybe Expr
update [LetBinding]
decls Assigns
fs Expr
e Type'' Term Term
t = do
  let
    fnames :: [Name]
fnames  = [ Name
x | FieldAssignment Name
x Expr
_ <- Assigns
fs ]

    postpone :: TCMT IO Term
postpone = TypeCheckingProblem -> TCMT IO Term
postponeTypeCheckingProblem_ (TypeCheckingProblem -> TCMT IO Term)
-> TypeCheckingProblem -> TCMT IO Term
forall a b. (a -> b) -> a -> b
$ Comparison -> Expr -> Type'' Term Term -> TypeCheckingProblem
CheckExpr Comparison
cmp Expr
e Type'' Term Term
t
    tryinfer :: TCMT IO Term
tryinfer
      | Just Expr
e0 <- Maybe Expr
update = do
        (_, trec) <- Expr -> TCM (Term, Type'' Term Term)
inferExpr Expr
e0
        ifBlocked trec (\ Blocker
_ Type'' Term Term
_ -> TCMT IO Term
postpone) \NotBlocked
_ Type'' Term Term
_ -> do
          v <- Comparison -> Expr -> Type'' Term Term -> TCMT IO Term
checkExpr' Comparison
cmp Expr
e Type'' Term Term
trec
          coerce cmp v trec t
      | Bool
otherwise = TCMT IO Term
postpone

    findtype :: ((QName, [Arg Term], RecordData) -> TCMT IO Term) -> TCMT IO Term
findtype (QName, [Arg Term], RecordData) -> TCMT IO Term
cont = Type'' Term Term
-> (Blocker -> Type'' Term Term -> TCMT IO Term)
-> (NotBlocked -> Type'' Term Term -> TCMT IO Term)
-> TCMT IO Term
forall t (m :: * -> *) a.
(Reduce t, IsMeta t, MonadReduce m) =>
t -> (Blocker -> t -> m a) -> (NotBlocked -> t -> m a) -> m a
ifBlocked Type'' Term Term
t (\Blocker
_ Type'' Term Term
t -> TCMT IO Term
-> Comparison -> Expr -> [Name] -> Type'' Term Term -> TCMT IO Term
guessRecordType TCMT IO Term
tryinfer Comparison
cmp Expr
e [Name]
fnames Type'' Term Term
t) \NotBlocked
_ Type'' Term Term
t -> do
      TCMT IO (Maybe (QName, [Arg Term], RecordData))
-> TCMT IO Term
-> ((QName, [Arg Term], RecordData) -> TCMT IO Term)
-> TCMT IO Term
forall (m :: * -> *) a b.
Monad m =>
m (Maybe a) -> m b -> (a -> m b) -> m b
caseMaybeM (Type'' Term Term -> TCMT IO (Maybe (QName, [Arg Term], RecordData))
forall (m :: * -> *).
(HasCallStack, PureTCM m) =>
Type'' Term Term -> m (Maybe (QName, [Arg Term], RecordData))
isRecordType Type'' Term Term
t) (TypeError -> TCMT IO Term
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> TCMT IO Term) -> TypeError -> TCMT IO Term
forall a b. (a -> b) -> a -> b
$ Type'' Term Term -> TypeError
ShouldBeRecordType Type'' Term Term
t) (QName, [Arg Term], RecordData) -> TCMT IO Term
cont

  ((QName, [Arg Term], RecordData) -> TCMT IO Term) -> TCMT IO Term
findtype \ (QName
r, [Arg Term]
_pars, RecordData
defn) -> do
    let
      ei :: ExprInfo
ei    = Range' SrcFile -> ExprInfo
A.ExprRange (Expr -> Range' SrcFile
forall a. HasRange a => a -> Range' SrcFile
getRange Expr
e)
      cxs :: [Name]
cxs   = (Dom Name -> Name) -> [Dom Name] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map' Dom Name -> Name
forall t e. Dom' t e -> e
unDom ([Dom Name] -> [Name]) -> [Dom Name] -> [Name]
forall a b. (a -> b) -> a -> b
$ RecordData -> [Dom Name]
recordFieldNames RecordData
defn
      recfs :: Map Name Int
recfs = [(Name, Int)] -> Map Name Int
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList ([(Name, Int)] -> Map Name Int) -> [(Name, Int)] -> Map Name Int
forall a b. (a -> b) -> a -> b
$ [Name] -> [Int] -> [(Name, Int)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Name]
cxs [Int
0..]
      names :: Map Name (Int, Name)
names = [(Name, (Int, Name))] -> Map Name (Int, Name)
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList
        [ (Name
aname, (Int
idx, Name
fname))
        | FieldAssignment Name
fname (A.Var Name
aname) <- Assigns
fs
        , Just Int
idx <- Maybe Int -> [Maybe Int]
forall a. a -> [a]
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Name -> Map Name Int -> Maybe Int
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Name
fname Map Name Int
recfs)
        ]

    ArgName -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m ()
reportSDoc ArgName
"tc.record.where" Int
30 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
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 `record where` at type" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Type'' Term Term -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Type'' Term Term
t
      , TCMT IO Doc
"bound fields:" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Map Name (Int, Name) -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Map Name (Int, Name)
names
      ]

    let
      check :: [A.LetBinding] -> (IntMap.IntMap (A.BindName, MetaId, Term, A.Expr, Type -> TCM Term) -> TCM a) -> TCM a
      check :: forall a.
[LetBinding]
-> (IntMap
      (BindName, MetaId, Term, Expr, Type'' Term Term -> TCMT IO Term)
    -> TCM a)
-> TCM a
check (b :: LetBinding
b@(A.LetBind LetInfo
i ArgInfo
info BindName
x Expr
t Expr
e):[LetBinding]
bs) IntMap
  (BindName, MetaId, Term, Expr, Type'' Term Term -> TCMT IO Term)
-> TCM a
cont | Just (Int
idx, Name
fname) <- Name -> Map Name (Int, Name) -> Maybe (Int, Name)
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup (BindName -> Name
A.unBind BindName
x) Map Name (Int, Name)
names = do

        -- We create the meta with the actual type of the binding, to
        -- make sure that e.g. the user can choose to write a more
        -- general signature than the record type demands.
        t <- TCM (Type'' Term Term) -> TCM (Type'' Term Term)
forall (m :: * -> *) a.
(MonadTCEnv m, HasOptions m, MonadDebug m) =>
m a -> m a
workOnTypes (TCM (Type'' Term Term) -> TCM (Type'' Term Term))
-> TCM (Type'' Term Term) -> TCM (Type'' Term Term)
forall a b. (a -> b) -> a -> b
$ Expr -> TCM (Type'' Term Term)
isType_ Expr
t

        -- One minor quibble is that we should remember what let
        -- bindings are actually in the context when the binding is
        -- processed, and use *those*, rather than the full set of
        -- `let`-bindings that would otherwise be available.
        lets <- Map.keysSet <$> viewTC eLetBindings
        let
          restore = Lens' TCEnv (Map Name (Open LetBinding))
-> (Map Name (Open LetBinding) -> Map Name (Open LetBinding))
-> TCMT IO Term
-> TCMT IO Term
forall (m :: * -> *) a b.
MonadTCEnv m =>
Lens' TCEnv a -> (a -> a) -> m b -> m b
locallyTC (Map Name (Open LetBinding) -> f (Map Name (Open LetBinding)))
-> TCEnv -> f TCEnv
Lens' TCEnv (Map Name (Open LetBinding))
eLetBindings (Map Name (Open LetBinding)
-> Set Name -> Map Name (Open LetBinding)
forall k a. Ord k => Map k a -> Set k -> Map k a
`Map.restrictKeys` Set Name
lets)
          -- Unlike 'checkLetBinding' which sometimes needs to
          -- checkDontExpandLast, here we should always.
          checkit Type'' Term Term
t = TCMT IO Term -> TCMT IO Term
restore (TCMT IO Term -> TCMT IO Term) -> TCMT IO Term -> TCMT IO Term
forall a b. (a -> b) -> a -> b
$ ArgInfo -> TCMT IO Term -> TCMT IO Term
forall (tcm :: * -> *) a m.
(MonadTCEnv tcm, ExpandCase (tcm a), LensModality m) =>
m -> tcm a -> tcm a
applyModalityToContext ArgInfo
info (TCMT IO Term -> TCMT IO Term) -> TCMT IO Term -> TCMT IO Term
forall a b. (a -> b) -> a -> b
$ Comparison -> Expr -> Type'' Term Term -> TCMT IO Term
checkExpr' Comparison
CmpLeq Expr
e Type'' Term Term
t

        (mv, v) <- applyModalityToContext info $ newValueMeta RunMetaOccursCheck CmpEq t

        reportSDoc "tc.record.where" 30 $ "deferring field" <+> prettyA x <+> ":" <+> pretty t

        -- Then just add the let binding with the value set to a meta.
        lets `seq` addLetBinding info UserWritten (A.unBind x) v t $ check bs \IntMap
  (BindName, MetaId, Term, Expr, Type'' Term Term -> TCMT IO Term)
as ->
          IntMap
  (BindName, MetaId, Term, Expr, Type'' Term Term -> TCMT IO Term)
-> TCM a
cont (Int
-> (BindName, MetaId, Term, Expr, Type'' Term Term -> TCMT IO Term)
-> IntMap
     (BindName, MetaId, Term, Expr, Type'' Term Term -> TCMT IO Term)
-> IntMap
     (BindName, MetaId, Term, Expr, Type'' Term Term -> TCMT IO Term)
forall a. Int -> a -> IntMap a -> IntMap a
IntMap.insert Int
idx (BindName
x, MetaId
mv, Term
v, Expr
e, Type'' Term Term -> TCMT IO Term
checkit) IntMap
  (BindName, MetaId, Term, Expr, Type'' Term Term -> TCMT IO Term)
as)

      -- For any other bindings we can check them on the spot (so the
      -- hardest parts of 'checkLetBinding' don't need to be
      -- duplicated.)
      check (LetBinding
b:[LetBinding]
bs) IntMap
  (BindName, MetaId, Term, Expr, Type'' Term Term -> TCMT IO Term)
-> TCM a
cont = LetBinding -> TCM a -> TCM a
forall a. LetBinding -> TCM a -> TCM a
checkLetBinding LetBinding
b (TCM a -> TCM a) -> TCM a -> TCM a
forall a b. (a -> b) -> a -> b
$ [LetBinding]
-> (IntMap
      (BindName, MetaId, Term, Expr, Type'' Term Term -> TCMT IO Term)
    -> TCM a)
-> TCM a
forall a.
[LetBinding]
-> (IntMap
      (BindName, MetaId, Term, Expr, Type'' Term Term -> TCMT IO Term)
    -> TCM a)
-> TCM a
check [LetBinding]
bs IntMap
  (BindName, MetaId, Term, Expr, Type'' Term Term -> TCMT IO Term)
-> TCM a
cont
      check [] IntMap
  (BindName, MetaId, Term, Expr, Type'' Term Term -> TCMT IO Term)
-> TCM a
cont = IntMap
  (BindName, MetaId, Term, Expr, Type'' Term Term -> TCMT IO Term)
-> TCM a
cont IntMap
  (BindName, MetaId, Term, Expr, Type'' Term Term -> TCMT IO Term)
forall a. Monoid a => a
mempty

      -- Compute the actual synthesised field assignments we'll be
      -- using, handling record updates along the way. If there's no
      -- update, then the fields are just the ones that the user wrote;
      checkUpdate :: ([Either (FieldAssignment' Expr) ModuleName] -> TCMT IO Term)
-> TCMT IO Term
checkUpdate [Either (FieldAssignment' Expr) ModuleName] -> TCMT IO Term
cont = case Maybe Expr
update of
        Maybe Expr
Nothing -> [Either (FieldAssignment' Expr) ModuleName] -> TCMT IO Term
cont ((FieldAssignment' Expr
 -> Either (FieldAssignment' Expr) ModuleName)
-> Assigns -> [Either (FieldAssignment' Expr) ModuleName]
forall a b. (a -> b) -> [a] -> [b]
map' FieldAssignment' Expr -> Either (FieldAssignment' Expr) ModuleName
forall a b. a -> Either a b
Left Assigns
fs)
        Just Expr
exp0 -> do
          -- Otherwise, we check the original record value against the
          -- expected type, and use it to fill in any field assignments
          -- that were not given by the user.
          v    <- Comparison -> Expr -> Type'' Term Term -> TCMT IO Term
checkExpr' Comparison
cmp Expr
exp0 Type'' Term Term
t
          name <- freshNoName $ getRange exp0

          let
            here_keys = [Name] -> Set Name
forall a. Ord a => [a] -> Set a
Set.fromList [Name]
fnames
            proj QName
n = AppInfo -> Expr -> Arg (Named_ Expr) -> Expr
A.App (Range' SrcFile -> AppInfo
A.defaultAppInfo (Range' SrcFile -> AppInfo) -> Range' SrcFile -> AppInfo
forall a b. (a -> b) -> a -> b
$ ExprInfo -> Range' SrcFile
forall a. HasRange a => a -> Range' SrcFile
getRange ExprInfo
ei) (ProjOrigin -> AmbiguousQName -> Expr
A.Proj ProjOrigin
ProjSystem (AmbiguousQName -> Expr) -> AmbiguousQName -> Expr
forall a b. (a -> b) -> a -> b
$ QName -> AmbiguousQName
unambiguous QName
n) (Expr -> Arg (Named_ Expr)
forall a. a -> NamedArg a
defaultNamedArg (Name -> Expr
A.Var Name
name))
            fs' =
              [ FieldAssignment' Expr -> Either (FieldAssignment' Expr) ModuleName
forall a b. a -> Either a b
Left (Name -> Expr -> FieldAssignment' Expr
forall a. Name -> a -> FieldAssignment' a
FieldAssignment Name
fname (QName -> Expr
proj QName
pname))
              | (Name
fname, Dom QName -> QName
forall t e. Dom' t e -> e
unDom -> QName
pname) <- [Name] -> [Dom QName] -> [(Name, Dom QName)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Name]
cxs (RecordData -> [Dom QName]
_recFields RecordData
defn)
              , Name
fname Name -> Set Name -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.notMember` Set Name
here_keys
              ]

          addLetBinding defaultArgInfo Inserted name v t $ cont (fs' ++! map' Left fs)

    [LetBinding]
-> (IntMap
      (BindName, MetaId, Term, Expr, Type'' Term Term -> TCMT IO Term)
    -> TCMT IO Term)
-> TCMT IO Term
forall a.
[LetBinding]
-> (IntMap
      (BindName, MetaId, Term, Expr, Type'' Term Term -> TCMT IO Term)
    -> TCM a)
-> TCM a
check [LetBinding]
decls \IntMap
  (BindName, MetaId, Term, Expr, Type'' Term Term -> TCMT IO Term)
later -> ([Either (FieldAssignment' Expr) ModuleName] -> TCMT IO Term)
-> TCMT IO Term
checkUpdate \[Either (FieldAssignment' Expr) ModuleName]
fs' -> do
      -- Check the synthesised record expression, but make sure that
      -- checkArguments won't try to do implicit insertion on us.
      out <- TCMT IO Term -> TCMT IO Term
forall a. TCM a -> TCM a
reallyDontExpandLast (TCMT IO Term -> TCMT IO Term) -> TCMT IO Term -> TCMT IO Term
forall a b. (a -> b) -> a -> b
$
        Comparison
-> [Either (FieldAssignment' Expr) ModuleName]
-> Expr
-> Type'' Term Term
-> ConOrigin
-> TCMT IO Term
checkRecordExpression Comparison
cmp [Either (FieldAssignment' Expr) ModuleName]
fs' (KwRange
-> ExprInfo -> [Either (FieldAssignment' Expr) ModuleName] -> Expr
A.Rec KwRange
kwr ExprInfo
ei [Either (FieldAssignment' Expr) ModuleName]
fs') Type'' Term Term
t ConOrigin
ConORecWhere

      -- Then we can go back and check the bindings. (The name and
      -- expression are just for debug printing.)
      forM_ (IntMap.toAscList later) \(Int
_, (BindName
fname, MetaId
mid, Term
meta, Expr
e, Type'' Term Term -> TCMT IO Term
check)) -> do
        ty <- MetaId -> TCM (Type'' Term Term)
forall (m :: * -> *).
(HasBuiltins m, HasCallStack, MonadDebug m, MonadReduce m) =>
MetaId -> m (Type'' Term Term)
getMetaTypeInContext MetaId
mid

        reportSDoc "tc.record.where" 30 $ vcat
          [ "checking deferred `record where` binding for " <> prettyA fname <> ":"
          , nest 2 $ vcat
            [ prettyTCM meta <+> ":" <+> prettyTCM ty
            , prettyTCM meta <+> "=" <+> prettyA e ] ]

        v <- check ty
        equalTerm ty meta v

      pure out

---------------------------------------------------------------------------
-- * Literal
---------------------------------------------------------------------------

checkLiteral :: Literal -> Type -> TCM Term
checkLiteral :: Literal -> Type'' Term Term -> TCMT IO Term
checkLiteral Literal
lit Type'' Term Term
t = do
  t' <- Literal -> TCM (Type'' Term Term)
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
Literal -> m (Type'' Term Term)
litType Literal
lit
  coerce CmpEq (Lit lit) t' t

---------------------------------------------------------------------------
-- * Terms
---------------------------------------------------------------------------

-- | Same as 'Agda.Syntax.Abstract.Views.appView',
--   but produces correct 'Hiding' when constructing the 'AppView'
--   from a postfix projection.
appViewM :: A.Expr -> TCM AppView
appViewM :: Expr -> TCM AppView
appViewM Expr
e = do
  (f, es) <- Expr
-> TCM ([Arg (Named_ Expr)] -> AppView, DList (Arg (Named_ Expr)))
go Expr
e
  return $! f $! DL.toList es
  where
  go :: A.Expr -> TCM (A.Args -> AppView, DL.DList (NamedArg A.Expr))
  go :: Expr
-> TCM ([Arg (Named_ Expr)] -> AppView, DList (Arg (Named_ Expr)))
go = \case
    A.ScopedExpr ScopeInfo
_ Expr
e -> Expr
-> TCM ([Arg (Named_ Expr)] -> AppView, DList (Arg (Named_ Expr)))
go Expr
e
    A.App AppInfo
_ Expr
e1 Arg (Named_ Expr)
e2
      | A.Dot ExprInfo
_ Expr
e2' <- Expr -> Expr
unScope (Expr -> Expr) -> Expr -> Expr
forall a b. (a -> b) -> a -> b
$ Arg (Named_ Expr) -> Expr
forall a. NamedArg a -> a
namedArg Arg (Named_ Expr)
e2
      , Just (AmbiguousQName
f0, Expr
hd) <- Expr -> Maybe (AmbiguousQName, Expr)
maybeProjTurnPostfix Expr
e2'
      -> do
       ai <- case AmbiguousQName -> Maybe QName
getUnambiguous AmbiguousQName
f0 of
         Just QName
f -> QName -> TCMT IO (Maybe Projection)
forall (m :: * -> *).
HasConstInfo m =>
QName -> m (Maybe Projection)
isProjection QName
f TCMT IO (Maybe Projection)
-> (Maybe Projection -> TCM ArgInfo) -> TCM ArgInfo
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
           Just Projection
p | Projection -> Bool
isProperProjection_ Projection
p -> ArgInfo -> TCM ArgInfo
forall a. a -> TCMT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (ArgInfo -> TCM ArgInfo) -> ArgInfo -> TCM ArgInfo
forall a b. (a -> b) -> a -> b
$ Projection -> ArgInfo
projArgInfo Projection
p
           Maybe Projection
_ -> ArgInfo -> TCM ArgInfo
forall a. a -> TCMT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ArgInfo
defaultArgInfo
         Maybe QName
Nothing -> ArgInfo -> TCM ArgInfo
forall a. a -> TCMT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ArgInfo
defaultArgInfo
       return (Application hd, singleton (unnamedArg ai e1))
    A.App AppInfo
_ Expr
e1 Arg (Named_ Expr)
arg -> (DList (Arg (Named_ Expr)) -> DList (Arg (Named_ Expr)))
-> ([Arg (Named_ Expr)] -> AppView, DList (Arg (Named_ Expr)))
-> ([Arg (Named_ Expr)] -> AppView, DList (Arg (Named_ Expr)))
forall b c a. (b -> c) -> (a, b) -> (a, c)
forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second (DList (Arg (Named_ Expr))
-> Arg (Named_ Expr) -> DList (Arg (Named_ Expr))
forall a. DList a -> a -> DList a
`DL.snoc` Arg (Named_ Expr)
arg) (([Arg (Named_ Expr)] -> AppView, DList (Arg (Named_ Expr)))
 -> ([Arg (Named_ Expr)] -> AppView, DList (Arg (Named_ Expr))))
-> TCM ([Arg (Named_ Expr)] -> AppView, DList (Arg (Named_ Expr)))
-> TCM ([Arg (Named_ Expr)] -> AppView, DList (Arg (Named_ Expr)))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr
-> TCM ([Arg (Named_ Expr)] -> AppView, DList (Arg (Named_ Expr)))
go Expr
e1
    Expr
e -> ([Arg (Named_ Expr)] -> AppView, DList (Arg (Named_ Expr)))
-> TCM ([Arg (Named_ Expr)] -> AppView, DList (Arg (Named_ Expr)))
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr -> [Arg (Named_ Expr)] -> AppView
forall arg. Expr -> [NamedArg arg] -> AppView' arg
Application Expr
e, DList (Arg (Named_ Expr))
forall a. Monoid a => a
mempty)

-- | Remove top layers of scope info of expression and set the scope accordingly
--   in the 'TCState'.

scopedExpr :: A.Expr -> TCM A.Expr
scopedExpr :: Expr -> TCM Expr
scopedExpr (A.ScopedExpr ScopeInfo
scope Expr
e) = ScopeInfo -> TCM ()
setScope ScopeInfo
scope TCM () -> TCM Expr -> TCM Expr
forall a b. TCMT IO a -> TCMT IO b -> TCMT IO b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Expr -> TCM Expr
scopedExpr Expr
e
scopedExpr (A.Qualified ModuleName
mod Expr
e)    = Expr -> TCM Expr
scopedExpr Expr
e
scopedExpr Expr
e                      = Expr -> TCM Expr
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Expr
e

-- | Type check an expression.
checkExpr :: A.Expr -> Type -> TCM Term
checkExpr :: Expr -> Type'' Term Term -> TCMT IO Term
checkExpr = Comparison -> Expr -> Type'' Term Term -> TCMT IO Term
checkExpr' Comparison
CmpLeq

-- Andreas, 2019-10-13, issue #4125:
-- For the sake of readable types in interactive program construction,
-- avoid unnecessary unfoldings via 'reduce' in the type checker!
checkExpr'
  :: Comparison
  -> A.Expr
  -> Type        -- ^ Unreduced!
  -> TCM Term
checkExpr' :: Comparison -> Expr -> Type'' Term Term -> TCMT IO Term
checkExpr' Comparison
cmp Expr
e Type'' Term Term
t =
  ArgName -> Int -> ArgName -> TCMT IO Term -> TCMT IO Term
forall a. ArgName -> Int -> ArgName -> TCMT IO a -> TCMT IO a
forall (m :: * -> *) a.
MonadDebug m =>
ArgName -> Int -> ArgName -> m a -> m a
verboseBracket ArgName
"tc.term.expr.top" Int
5 ArgName
"checkExpr" (TCMT IO Term -> TCMT IO Term) -> TCMT IO Term -> TCMT IO Term
forall a b. (a -> b) -> a -> b
$
  ArgName
-> Int -> (Term -> TCMT IO Doc) -> TCMT IO Term -> TCMT IO Term
forall (m :: * -> *) a.
MonadDebug m =>
ArgName -> Int -> (a -> TCMT IO Doc) -> m a -> m a
reportResult ArgName
"tc.term.expr.top" Int
15 (\ Term
v -> [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
                                              [ TCMT IO Doc
"checkExpr" 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
fsep [ Expr -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Expr -> m Doc
prettyTCM Expr
e, TCMT IO Doc
":", Type'' Term Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type'' Term Term -> m Doc
prettyTCM Type'' Term Term
t ]
                                              , TCMT IO Doc
"  returns" 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 ]) (TCMT IO Term -> TCMT IO Term) -> TCMT IO Term -> TCMT IO Term
forall a b. (a -> b) -> a -> b
$
  Call -> TCMT IO Term -> TCMT IO Term
forall a. Call -> TCMT IO a -> TCMT IO a
forall (m :: * -> *) a. MonadTrace m => Call -> m a -> m a
traceCall (Comparison -> Expr -> Type'' Term Term -> Call
CheckExprCall Comparison
cmp Expr
e Type'' Term Term
t) (TCMT IO Term -> TCMT IO Term) -> TCMT IO Term -> TCMT IO Term
forall a b. (a -> b) -> a -> b
$ TCMT IO Term -> TCMT IO Term
forall a. TCM a -> TCM a
localScope (TCMT IO Term -> TCMT IO Term) -> TCMT IO Term -> TCMT IO Term
forall a b. (a -> b) -> a -> b
$ TCMT IO Term -> TCMT IO Term
forall a. TCM a -> TCM a
doExpandLast (TCMT IO Term -> TCMT IO Term) -> TCMT IO Term -> TCMT IO Term
forall a b. (a -> b) -> a -> b
$ Term -> TCMT IO Term
forall (m :: * -> *). PureTCM m => Term -> m Term
unfoldInlined (Term -> TCMT IO Term) -> TCMT IO Term -> TCMT IO Term
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< do
    ArgName -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m ()
reportSDoc ArgName
"tc.term.expr.top" Int
15 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$
        TCMT IO Doc
"Checking" 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
fsep [ Expr -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Expr -> m Doc
prettyTCM Expr
e, TCMT IO Doc
":", Type'' Term Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type'' Term Term -> m Doc
prettyTCM Type'' Term Term
t ]
          , Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"at " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> (ArgName -> TCMT IO Doc
forall (m :: * -> *). Applicative m => ArgName -> m Doc
text (ArgName -> TCMT IO Doc)
-> (Range' SrcFile -> ArgName) -> Range' SrcFile -> TCMT IO Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Range' SrcFile -> ArgName
forall a. Pretty a => a -> ArgName
prettyShow (Range' SrcFile -> TCMT IO Doc)
-> TCMT IO (Range' SrcFile) -> TCMT IO Doc
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< TCMT IO (Range' SrcFile)
forall (m :: * -> *). MonadTCEnv m => m (Range' SrcFile)
getCurrentRange)
          ]
    ArgName -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m ()
reportSDoc ArgName
"tc.term.expr.top.detailed" Int
80 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$
      TCMT IO Doc
"Checking" 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
fsep [ Expr -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Expr -> m Doc
prettyTCM Expr
e, TCMT IO Doc
":", ArgName -> TCMT IO Doc
forall (m :: * -> *). Applicative m => ArgName -> m Doc
text (Type'' Term Term -> ArgName
forall a. Show a => a -> ArgName
show Type'' Term Term
t) ]
    tReduced <- Type'' Term Term -> TCM (Type'' Term Term)
forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce Type'' Term Term
t
    reportSDoc "tc.term.expr.top" 15 $
        "    --> " <+> prettyTCM tReduced

    e <- scopedExpr e

    irrelevantIfProp <- runBlocked (isPropM t) >>= \case
      Right Bool
True  -> do
        let mod :: Modality
mod = Modality
unitModality { modRelevance = irrelevant }
        (TCMT IO Term -> TCMT IO Term)
-> TCMT IO (TCMT IO Term -> TCMT IO Term)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ((TCMT IO Term -> TCMT IO Term)
 -> TCMT IO (TCMT IO Term -> TCMT IO Term))
-> (TCMT IO Term -> TCMT IO Term)
-> TCMT IO (TCMT IO Term -> TCMT IO Term)
forall a b. (a -> b) -> a -> b
$! (Term -> Term) -> TCMT IO Term -> TCMT IO Term
forall a b. (a -> b) -> TCMT IO a -> TCMT IO b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Term -> Term
dontCare (TCMT IO Term -> TCMT IO Term)
-> (TCMT IO Term -> TCMT IO Term) -> TCMT IO Term -> TCMT IO Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Modality -> TCMT IO Term -> TCMT IO Term
forall (tcm :: * -> *) a m.
(MonadTCEnv tcm, ExpandCase (tcm a), LensModality m) =>
m -> tcm a -> tcm a
applyModalityToContext Modality
mod
      Either Blocker Bool
_ -> (TCMT IO Term -> TCMT IO Term)
-> TCMT IO (TCMT IO Term -> TCMT IO Term)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return TCMT IO Term -> TCMT IO Term
forall a. a -> a
id

    irrelevantIfProp $ tryInsertHiddenLambda e tReduced $ case e of

        A.ScopedExpr ScopeInfo
scope Expr
e -> TCMT IO Term
forall a. HasCallStack => a
__IMPOSSIBLE__ -- setScope scope >> checkExpr e t

        -- a meta variable without arguments: type check directly for efficiency
        A.QuestionMark MetaInfo
i InteractionId
ii -> (Comparison -> Type'' Term Term -> TCMT IO (MetaId, Term))
-> Comparison
-> Type'' Term Term
-> MetaInfo
-> InteractionId
-> TCMT IO Term
checkQuestionMark (RunMetaOccursCheck
-> Comparison -> Type'' Term Term -> TCMT IO (MetaId, Term)
newValueMeta' RunMetaOccursCheck
RunMetaOccursCheck) Comparison
cmp Type'' Term Term
t MetaInfo
i InteractionId
ii
        A.Underscore MetaInfo
i -> MetaInfo -> Comparison -> Type'' Term Term -> TCMT IO Term
checkUnderscore MetaInfo
i Comparison
cmp Type'' Term Term
t

        A.WithApp ExprInfo
_ Expr
e List1 Expr
es -> TypeError -> TCMT IO Term
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> TCMT IO Term) -> TypeError -> TCMT IO Term
forall a b. (a -> b) -> a -> b
$ ArgName -> TypeError
NotImplemented ArgName
"type checking of with application"

        e0 :: Expr
e0@(A.App AppInfo
i Expr
q (Arg ArgInfo
ai Named_ Expr
e))
          | A.Quote ExprInfo
_ <- Expr -> Expr
unScope Expr
q -> do
             if ArgInfo -> Bool
forall a. LensHiding a => a -> Bool
visible ArgInfo
ai then do
               x  <- Expr -> TCM QName
forall (m :: * -> *).
(MonadTCError m, MonadAbsToCon m) =>
Expr -> m QName
quotedName (Expr -> TCM QName) -> Expr -> TCM QName
forall a b. (a -> b) -> a -> b
$ Named_ Expr -> Expr
forall name a. Named name a -> a
namedThing Named_ Expr
e
               ty <- qNameType
               coerce cmp (quoteName x) ty t
             else TypeError -> TCMT IO Term
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> TCMT IO Term) -> TypeError -> TCMT IO Term
forall a b. (a -> b) -> a -> b
$ CannotQuote -> TypeError
CannotQuote CannotQuote
CannotQuoteHidden

          | A.QuoteTerm ExprInfo
_ <- Expr -> Expr
unScope Expr
q -> do
             if ArgInfo -> Bool
forall a. LensHiding a => a -> Bool
visible ArgInfo
ai then do
               (et, _) <- Expr -> TCM (Term, Type'' Term Term)
inferExpr (Named_ Expr -> Expr
forall name a. Named name a -> a
namedThing Named_ Expr
e)
               doQuoteTerm cmp et t
             else TypeError -> TCMT IO Term
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> TCMT IO Term) -> TypeError -> TCMT IO Term
forall a b. (a -> b) -> a -> b
$ CannotQuoteTerm -> TypeError
CannotQuoteTerm CannotQuoteTerm
CannotQuoteTermHidden

        A.Quote{}     -> TypeError -> TCMT IO Term
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> TCMT IO Term) -> TypeError -> TCMT IO Term
forall a b. (a -> b) -> a -> b
$ CannotQuote -> TypeError
CannotQuote CannotQuote
CannotQuoteNothing
        A.QuoteTerm{} -> TypeError -> TCMT IO Term
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> TCMT IO Term) -> TypeError -> TCMT IO Term
forall a b. (a -> b) -> a -> b
$ CannotQuoteTerm -> TypeError
CannotQuoteTerm CannotQuoteTerm
CannotQuoteTermNothing
        A.Unquote{}   -> UnquoteError -> TCMT IO Term
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
UnquoteError -> m a
unquoteError UnquoteError
NakedUnquote

        A.AbsurdLam ExprInfo
i Hiding
h -> Comparison
-> ExprInfo -> Hiding -> Expr -> Type'' Term Term -> TCMT IO Term
checkAbsurdLambda Comparison
cmp ExprInfo
i Hiding
h Expr
e Type'' Term Term
t

        A.ExtendedLam ExprInfo
i DefInfo
di Erased
erased QName
qname NonEmpty Clause
cs ->
          Comparison
-> ExprInfo
-> DefInfo
-> Erased
-> QName
-> NonEmpty Clause
-> Expr
-> Type'' Term Term
-> TCMT IO Term
checkExtendedLambda Comparison
cmp ExprInfo
i DefInfo
di Erased
erased QName
qname NonEmpty Clause
cs Expr
e Type'' Term Term
t

        A.Lam ExprInfo
i (A.DomainFull TypedBinding
b) Expr
e -> Comparison
-> TypedBinding -> Expr -> Type'' Term Term -> TCMT IO Term
checkLambda Comparison
cmp TypedBinding
b Expr
e Type'' Term Term
t

        A.Lam ExprInfo
i (A.DomainFree TacticAttribute' Expr
_ Arg (Named_ (Binder' BindName))
x) Expr
e0
          | Maybe (WithOrigin (Ranged ArgName)) -> Bool
forall a. Maybe a -> Bool
isNothing (Named_ (Binder' BindName) -> Maybe (WithOrigin (Ranged ArgName))
forall name a. Named name a -> Maybe name
nameOf (Named_ (Binder' BindName) -> Maybe (WithOrigin (Ranged ArgName)))
-> Named_ (Binder' BindName) -> Maybe (WithOrigin (Ranged ArgName))
forall a b. (a -> b) -> a -> b
$ Arg (Named_ (Binder' BindName)) -> Named_ (Binder' BindName)
forall e. Arg e -> e
unArg Arg (Named_ (Binder' BindName))
x) Bool -> Bool -> Bool
&& Maybe (Pattern' Expr) -> Bool
forall a. Maybe a -> Bool
isNothing (Binder' BindName -> Maybe (Pattern' Expr)
forall a. Binder' a -> Maybe (Pattern' Expr)
A.binderPattern (Binder' BindName -> Maybe (Pattern' Expr))
-> Binder' BindName -> Maybe (Pattern' Expr)
forall a b. (a -> b) -> a -> b
$ Arg (Named_ (Binder' BindName)) -> Binder' BindName
forall a. NamedArg a -> a
namedArg Arg (Named_ (Binder' BindName))
x) ->
              Comparison -> Expr -> Type'' Term Term -> TCMT IO Term
checkExpr' Comparison
cmp (ExprInfo -> LamBinding -> Expr -> Expr
A.Lam ExprInfo
i (ArgInfo -> Binder' Name -> LamBinding
domainFree (Arg (Named_ (Binder' BindName)) -> ArgInfo
forall a. LensArgInfo a => a -> ArgInfo
getArgInfo Arg (Named_ (Binder' BindName))
x) (Binder' Name -> LamBinding) -> Binder' Name -> LamBinding
forall a b. (a -> b) -> a -> b
$ BindName -> Name
A.unBind (BindName -> Name) -> Binder' BindName -> Binder' Name
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Arg (Named_ (Binder' BindName)) -> Binder' BindName
forall a. NamedArg a -> a
namedArg Arg (Named_ (Binder' BindName))
x) Expr
e0) Type'' Term Term
t
          | Bool
otherwise -> TCMT IO Term
forall a. HasCallStack => a
__IMPOSSIBLE__

        A.Lit ExprInfo
_ Literal
lit  -> Literal -> Type'' Term Term -> TCMT IO Term
checkLiteral Literal
lit Type'' Term Term
t
        A.Let ExprInfo
i List1 LetBinding
ds Expr
e -> List1 LetBinding -> TCMT IO Term -> TCMT IO Term
forall (t :: * -> *) a.
Foldable t =>
t LetBinding -> TCM a -> TCM a
checkLetBindings List1 LetBinding
ds (TCMT IO Term -> TCMT IO Term) -> TCMT IO Term -> TCMT IO Term
forall a b. (a -> b) -> a -> b
$ Comparison -> Expr -> Type'' Term Term -> TCMT IO Term
checkExpr' Comparison
cmp Expr
e Type'' Term Term
t
        e :: Expr
e@A.Pi{} -> do
            t' <- Expr -> TCM (Type'' Term Term)
isType_ Expr
e
            let s = Type'' Term Term -> Sort' Term
forall a. LensSort a => a -> Sort' Term
getSort Type'' Term Term
t'
                v = Type'' Term Term -> Term
forall t a. Type'' t a -> a
unEl Type'' Term Term
t'
            coerce cmp v (sort s) t

        A.Generalized Set1 QName
s Expr
e -> do
            (_, t') <- Set QName
-> TCM (Type'' Term Term) -> TCM ([Maybe QName], Type'' Term Term)
generalizeType (Set1 QName -> Set QName
forall a. NESet a -> Set a
Set1.toSet Set1 QName
s) (TCM (Type'' Term Term) -> TCM ([Maybe QName], Type'' Term Term))
-> TCM (Type'' Term Term) -> TCM ([Maybe QName], Type'' Term Term)
forall a b. (a -> b) -> a -> b
$ Expr -> TCM (Type'' Term Term)
isType_ Expr
e
            --noFunctionsIntoSize t' t'
            let s = Type'' Term Term -> Sort' Term
forall a. LensSort a => a -> Sort' Term
getSort Type'' Term Term
t'
                v = Type'' Term Term -> Term
forall t a. Type'' t a -> a
unEl Type'' Term Term
t'
            coerce cmp v (sort s) t

        e :: Expr
e@A.Fun{} -> do
            t' <- Expr -> TCM (Type'' Term Term)
isType_ Expr
e
            let s = Type'' Term Term -> Sort' Term
forall a. LensSort a => a -> Sort' Term
getSort Type'' Term Term
t'
                v = Type'' Term Term -> Term
forall t a. Type'' t a -> a
unEl Type'' Term Term
t'
            coerce cmp v (sort s) t

        A.Rec KwRange
_ ExprInfo
_ [Either (FieldAssignment' Expr) ModuleName]
fs  -> Comparison
-> [Either (FieldAssignment' Expr) ModuleName]
-> Expr
-> Type'' Term Term
-> ConOrigin
-> TCMT IO Term
checkRecordExpression Comparison
cmp [Either (FieldAssignment' Expr) ModuleName]
fs Expr
e Type'' Term Term
t ConOrigin
ConORec

        A.RecUpdate KwRange
kwr ExprInfo
ei Expr
recexpr Assigns
fs -> Comparison
-> KwRange
-> ExprInfo
-> Expr
-> Assigns
-> Expr
-> Type'' Term Term
-> TCMT IO Term
checkRecordUpdate Comparison
cmp KwRange
kwr ExprInfo
ei Expr
recexpr Assigns
fs Expr
e Type'' Term Term
t

        A.RecWhere KwRange
kwr ExprInfo
ei [LetBinding]
decls Assigns
fs           -> Comparison
-> KwRange
-> ExprInfo
-> Maybe Expr
-> [LetBinding]
-> Assigns
-> Expr
-> Type'' Term Term
-> TCMT IO Term
checkRecordWhere Comparison
cmp KwRange
kwr ExprInfo
ei Maybe Expr
forall a. Maybe a
Nothing [LetBinding]
decls Assigns
fs Expr
e Type'' Term Term
t
        A.RecUpdateWhere KwRange
kwr ExprInfo
ei Expr
exp [LetBinding]
decls Assigns
fs -> Comparison
-> KwRange
-> ExprInfo
-> Maybe Expr
-> [LetBinding]
-> Assigns
-> Expr
-> Type'' Term Term
-> TCMT IO Term
checkRecordWhere Comparison
cmp KwRange
kwr ExprInfo
ei (Expr -> Maybe Expr
forall a. a -> Maybe a
Just Expr
exp) [LetBinding]
decls Assigns
fs Expr
e Type'' Term Term
t

        A.DontCare Expr
e -> do
          rel <- Lens' TCEnv Relevance -> TCMT IO Relevance
forall (m :: * -> *) a. MonadTCEnv m => Lens' TCEnv a -> m a
viewTC (Relevance -> f Relevance) -> TCEnv -> f TCEnv
Lens' TCEnv Relevance
eRelevance
          if isIrrelevant rel then dontCare <$> do
            -- resurrect variables
            applyRelevanceToContext rel $ checkExpr' cmp e t
          else
            internalError "DontCare may only appear in irrelevant contexts"

        A.Dot{} -> TypeError -> TCMT IO Term
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError TypeError
InvalidDottedExpression

        -- Application
        Expr
e -> do
          Application hd args <- Expr -> TCM AppView
appViewM Expr
e
          e' <- checkApplication cmp hd args e t
          pure e'

      `catchIlltypedPatternBlockedOnMeta` \ (TCErr
err, Blocker
x) -> do
        -- We could not check the term because the type of some pattern is blocked.
        -- It has to be blocked on some meta, so we can postpone,
        -- being sure it will be retried when a meta is solved
        -- (which might be the blocking meta in which case we actually make progress).
        ArgName -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m ()
reportSDoc ArgName
"tc.term" Int
50 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
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
"checking pattern got stuck on meta: " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Blocker -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Blocker
x ]
        TypeCheckingProblem -> Blocker -> TCMT IO Term
postponeTypeCheckingProblem (Comparison -> Expr -> Type'' Term Term -> TypeCheckingProblem
CheckExpr Comparison
cmp Expr
e Type'' Term Term
t) Blocker
x

  where
  -- Call checkExpr with an hidden lambda inserted if appropriate,
  -- else fallback.
  tryInsertHiddenLambda
    :: A.Expr
    -> Type      -- Reduced.
    -> TCM Term
    -> TCM Term
  tryInsertHiddenLambda :: Expr -> Type'' Term Term -> TCMT IO Term -> TCMT IO Term
tryInsertHiddenLambda Expr
e Type'' Term Term
tReduced TCMT IO Term
fallback
    -- Insert hidden lambda if all of the following conditions are met:
    -- type is a hidden function type, {x : A} -> B or {{x : A}} -> B
    -- expression is not a lambda with the appropriate hiding yet
    | Pi dom :: Dom' Term (Type'' Term Term)
dom@(Dom' Term (Type'' Term Term) -> Type'' Term Term
forall t e. Dom' t e -> e
unDom -> Type'' Term Term
a) Abs (Type'' Term Term)
b <- Type'' Term Term -> Term
forall t a. Type'' t a -> a
unEl Type'' Term Term
tReduced
        , let info :: ArgInfo
info = Dom' Term (Type'' Term Term)
dom Dom' Term (Type'' Term Term)
-> Getting ArgInfo (Dom' Term (Type'' Term Term)) ArgInfo
-> ArgInfo
forall s a. s -> Getting a s a -> a
^. Getting ArgInfo (Dom' Term (Type'' Term Term)) ArgInfo
forall t e (f :: * -> *).
Functor f =>
(ArgInfo -> f ArgInfo) -> Dom' t e -> f (Dom' t e)
dInfo
        , let h :: Hiding
h = ArgInfo -> Hiding
forall a. LensHiding a => a -> Hiding
getHiding ArgInfo
info
        , Hiding -> Bool
forall a. LensHiding a => a -> Bool
notVisible Hiding
h
        -- expression is not a matching hidden lambda or question mark
        , Bool -> Bool
not (Hiding -> Expr -> Bool
forall {a}. LensHiding a => a -> Expr -> Bool
hiddenLambdaOrHole Hiding
h Expr
e)
        = do
      let proceed :: TCMT IO Term
proceed = ArgInfo -> ArgName -> TCMT IO Term
doInsert (Origin -> ArgInfo -> ArgInfo
forall a. LensOrigin a => Origin -> a -> a
setOrigin Origin
Inserted ArgInfo
info) (ArgName -> TCMT IO Term) -> ArgName -> TCMT IO Term
forall a b. (a -> b) -> a -> b
$ Abs (Type'' Term Term) -> ArgName
forall a. Abs a -> ArgName
absName Abs (Type'' Term Term)
b
      expandHidden <- 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
      -- If we skip the lambda insertion for an introduction,
      -- we will hit a dead end, so proceed no matter what.
      if definitelyIntroduction then proceed else
        -- #3019 and #4170: don't insert implicit lambdas in arguments to existing metas
        if expandHidden == ReallyDontExpandLast then fallback else do
        -- Andreas, 2017-01-19, issue #2412:
        -- We do not want to insert a hidden lambda if A is
        -- possibly empty type of sizes, as this will produce an error.
        reduce a >>= isSizeType >>= \case
          Just (BoundedLt Term
u) -> Term
-> (Blocker -> Term -> TCMT IO Term)
-> (NotBlocked -> Term -> TCMT IO Term)
-> TCMT IO Term
forall t (m :: * -> *) a.
(Reduce t, IsMeta t, MonadReduce m) =>
t -> (Blocker -> t -> m a) -> (NotBlocked -> t -> m a) -> m a
ifBlocked Term
u (\ Blocker
_ Term
_ -> TCMT IO Term
fallback) ((NotBlocked -> Term -> TCMT IO Term) -> TCMT IO Term)
-> (NotBlocked -> Term -> TCMT IO Term) -> TCMT IO Term
forall a b. (a -> b) -> a -> b
$ \ NotBlocked
_ Term
v -> do
            TCMT IO Bool -> TCMT IO Term -> TCMT IO Term -> TCMT IO Term
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM (Term -> TCMT IO Bool
checkSizeNeverZero Term
v) TCMT IO Term
proceed TCMT IO Term
fallback
            TCMT IO Term -> (TCErr -> TCMT IO Term) -> TCMT IO Term
forall a. TCMT IO a -> (TCErr -> TCMT IO a) -> TCMT IO a
forall e (m :: * -> *) a.
MonadError e m =>
m a -> (e -> m a) -> m a
`catchError` \TCErr
_ -> TCMT IO Term
fallback
          Maybe BoundedSize
_ -> TCMT IO Term
proceed

    | Bool
otherwise = TCMT IO Term
fallback

    where
    re :: Range' SrcFile
re = Expr -> Range' SrcFile
forall a. HasRange a => a -> Range' SrcFile
getRange Expr
e
    rx :: Range' SrcFile
rx = Maybe (Position' SrcFile)
-> Range' SrcFile
-> (Position' SrcFile -> Range' SrcFile)
-> Range' SrcFile
forall a b. Maybe a -> b -> (a -> b) -> b
caseMaybe (Range' SrcFile -> Maybe (Position' SrcFile)
forall a. Range' a -> Maybe (Position' a)
rStart Range' SrcFile
re) Range' SrcFile
forall a. Range' a
noRange ((Position' SrcFile -> Range' SrcFile) -> Range' SrcFile)
-> (Position' SrcFile -> Range' SrcFile) -> Range' SrcFile
forall a b. (a -> b) -> a -> b
$ \ Position' SrcFile
pos -> Position' SrcFile -> Position' SrcFile -> Range' SrcFile
forall a b. Position' a -> Position' b -> Range' a
posToRange Position' SrcFile
pos Position' SrcFile
pos

    doInsert :: ArgInfo -> ArgName -> TCMT IO Term
doInsert ArgInfo
info ArgName
y = do
      x <- Name -> Name
forall a. LensInScope a => a -> a
C.setNotInScope (Name -> Name) -> TCMT IO Name -> TCMT IO Name
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Range' SrcFile -> ArgName -> TCMT IO Name
forall (m :: * -> *).
MonadFresh NameId m =>
Range' SrcFile -> ArgName -> m Name
freshName Range' SrcFile
rx ArgName
y
      reportSLn "tc.term.expr.impl" 15 $ "Inserting implicit lambda"
      checkExpr' cmp (A.Lam (A.ExprRange re) (domainFree info $ A.mkBinder x) e) tReduced

    hiddenLambdaOrHole :: a -> Expr -> Bool
hiddenLambdaOrHole a
h = \case
      A.AbsurdLam ExprInfo
_ Hiding
h'          -> a -> Hiding -> Bool
forall a b. (LensHiding a, LensHiding b) => a -> b -> Bool
sameHiding a
h Hiding
h'
      A.ExtendedLam ExprInfo
_ DefInfo
_ Erased
_ QName
_ NonEmpty Clause
cls -> (Clause -> Bool) -> NonEmpty Clause -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any Clause -> Bool
hiddenLHS NonEmpty Clause
cls
      A.Lam ExprInfo
_ LamBinding
bind Expr
_            -> a -> LamBinding -> Bool
forall a b. (LensHiding a, LensHiding b) => a -> b -> Bool
sameHiding a
h LamBinding
bind
      A.QuestionMark{}          -> Bool
True
      Expr
_                         -> Bool
False

    hiddenLHS :: Clause -> Bool
hiddenLHS (A.Clause (A.LHS LHSInfo
_ (A.LHSHead QName
_ (NamedArg (Pattern' Expr)
a : [NamedArg (Pattern' Expr)]
_))) [ProblemEq]
_ RHS
_ WhereDeclarations
_ Catchall
_) = NamedArg (Pattern' Expr) -> Bool
forall a. LensHiding a => a -> Bool
notVisible NamedArg (Pattern' Expr)
a
    hiddenLHS Clause
_ = Bool
False

    -- Things with are definitely introductions,
    -- thus, cannot be of hidden Pi-type, unless they are hidden lambdas.
    definitelyIntroduction :: Bool
definitelyIntroduction = case Expr
e of
      A.Lam{}        -> Bool
True
      A.AbsurdLam{}  -> Bool
True
      A.Lit{}        -> Bool
True
      A.Pi{}         -> Bool
True
      A.Fun{}        -> Bool
True
      A.Rec{}        -> Bool
True
      A.RecUpdate{}  -> Bool
True
      A.ScopedExpr{} -> Bool
forall a. HasCallStack => a
__IMPOSSIBLE__
      Expr
_ -> Bool
False

---------------------------------------------------------------------------
-- * Reflection
---------------------------------------------------------------------------

doQuoteTerm :: Comparison -> Term -> Type -> TCM Term
doQuoteTerm :: Comparison -> Term -> Type'' Term Term -> TCMT IO Term
doQuoteTerm Comparison
cmp Term
et Type'' Term Term
t = do
  et'       <- Term -> TCMT IO Term
forall (m :: * -> *) a. (HasConstInfo m, TermLike a) => a -> m a
etaContract (Term -> TCMT IO Term) -> TCMT IO Term -> TCMT IO Term
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Term -> TCMT IO Term
forall a (m :: * -> *).
(InstantiateFull a, MonadReduce m) =>
a -> m a
instantiateFull Term
et
  quoteMetas <- optQuoteMetas <$> pragmaOptions
  let metas = Term -> [MetaId]
forall a. AllMetas a => a -> [MetaId]
allMetasList Term
et'
  if quoteMetas || null metas then do
    q  <- quoteTerm et'
    ty <- el primAgdaTerm
    coerce cmp q ty t
  else
    postponeTypeCheckingProblem (DoQuoteTerm cmp et t) $ unblockOnAllMetas $ Set.fromList metas

-- | Unquote a TCM computation in a given hole.
unquoteM :: A.Expr -> Term -> Type -> TCM ()
unquoteM :: Expr -> Term -> Type'' Term Term -> TCM ()
unquoteM Expr
tacA Term
hole Type'' Term Term
holeType = do
  tac <- Quantity -> TCMT IO Term -> TCMT IO Term
forall (tcm :: * -> *) q a.
(MonadTCEnv tcm, LensQuantity q) =>
q -> tcm a -> tcm a
applyQuantityToJudgement Quantity
zeroQuantity (TCMT IO Term -> TCMT IO Term) -> TCMT IO Term -> TCMT IO Term
forall a b. (a -> b) -> a -> b
$
    Expr -> Type'' Term Term -> TCMT IO Term
checkExpr Expr
tacA (Type'' Term Term -> TCMT IO Term)
-> TCM (Type'' Term Term) -> TCMT IO Term
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< (TCMT IO Term -> TCM (Type'' Term Term)
forall (m :: * -> *). Functor m => m Term -> m (Type'' Term Term)
el TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTerm TCM (Type'' Term Term)
-> TCM (Type'' Term Term) -> TCM (Type'' Term Term)
forall (m :: * -> *).
HasOptions m =>
m (Type'' Term Term)
-> m (Type'' Term Term) -> m (Type'' Term Term)
--> TCMT IO Term -> TCM (Type'' Term Term)
forall (m :: * -> *). Functor m => m Term -> m (Type'' Term Term)
el (TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTCM TCMT IO Term -> TCMT IO Term -> TCMT IO Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primLevelZero TCMT IO Term -> TCMT IO Term -> TCMT IO Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primUnit))
  inFreshModuleIfFreeParams $ unquoteTactic tac hole holeType

-- | Run a tactic `tac : Term → TC ⊤` in a hole (second argument) of the type
--   given by the third argument. Runs the continuation if successful.
unquoteTactic :: Term -> Term -> Type -> TCM ()
unquoteTactic :: Term -> Term -> Type'' Term Term -> TCM ()
unquoteTactic Term
tac Term
hole Type'' Term Term
goal = do
  TCMT IO Bool -> TCM () -> TCM () -> TCM ()
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM (Lens' TCState Bool -> TCMT IO Bool
forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
useTC (Bool -> f Bool) -> TCState -> f TCState
Lens' TCState Bool
stConsideringInstance) (Blocker -> Constraint -> TCM ()
forall (m :: * -> *).
MonadConstraint m =>
Blocker -> Constraint -> m ()
addConstraint Blocker
neverUnblock (Term -> Term -> Type'' Term Term -> Constraint
UnquoteTactic Term
tac Term
hole Type'' Term Term
goal)) do
  ArgName -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m ()
reportSDoc ArgName
"tc.term.tactic" Int
40 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
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
"Running tactic" 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
tac
    , 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
"on" 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
hole 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 -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Type'' Term Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type'' Term Term -> m Doc
prettyTCM Type'' Term Term
goal ]
  ok  <- UnquoteM Term -> TCM (Either UnquoteError (Term, [QName]))
forall a. UnquoteM a -> TCM (Either UnquoteError (a, [QName]))
runUnquoteM (UnquoteM Term -> TCM (Either UnquoteError (Term, [QName])))
-> UnquoteM Term -> TCM (Either UnquoteError (Term, [QName]))
forall a b. (a -> b) -> a -> b
$ Term -> Term -> UnquoteM Term
unquoteTCM Term
tac Term
hole
  case ok of
    Left (BlockedOnMeta TCState
oldState Blocker
blocker) -> do
      TCState -> TCM ()
forall (m :: * -> *). MonadTCState m => TCState -> m ()
putTC TCState
oldState
      let stripFreshMeta :: MetaId -> f Blocker
stripFreshMeta MetaId
x = Blocker
-> (MetaVariable -> Blocker) -> Maybe MetaVariable -> Blocker
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Blocker
neverUnblock (Blocker -> MetaVariable -> Blocker
forall a b. a -> b -> a
const (Blocker -> MetaVariable -> Blocker)
-> Blocker -> MetaVariable -> Blocker
forall a b. (a -> b) -> a -> b
$ MetaId -> Blocker
unblockOnMeta MetaId
x) (Maybe MetaVariable -> Blocker)
-> f (Maybe MetaVariable) -> f Blocker
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> MetaId -> f (Maybe MetaVariable)
forall (m :: * -> *).
ReadTCState m =>
MetaId -> m (Maybe MetaVariable)
lookupLocalMeta' MetaId
x
      blocker' <- (MetaId -> TCMT IO Blocker) -> Blocker -> TCMT IO Blocker
forall (m :: * -> *).
Monad m =>
(MetaId -> m Blocker) -> Blocker -> m Blocker
onBlockingMetasM MetaId -> TCMT IO Blocker
forall {f :: * -> *}. ReadTCState f => MetaId -> f Blocker
stripFreshMeta Blocker
blocker
      r <- case Set.toList $ allBlockingMetas blocker' of
            MetaId
x : [MetaId]
_ -> Maybe MetaVariable -> Range' SrcFile
forall a. HasRange a => a -> Range' SrcFile
getRange (Maybe MetaVariable -> Range' SrcFile)
-> TCMT IO (Maybe MetaVariable) -> TCMT IO (Range' SrcFile)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> MetaId -> TCMT IO (Maybe MetaVariable)
forall (m :: * -> *).
ReadTCState m =>
MetaId -> m (Maybe MetaVariable)
lookupLocalMeta' MetaId
x
            []    -> Range' SrcFile -> TCMT IO (Range' SrcFile)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Range' SrcFile
forall a. Range' a
noRange
      setCurrentRange r $
        addConstraint blocker' (UnquoteTactic tac hole goal)
    Left UnquoteError
err -> TypeError -> TCM ()
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> TCM ()) -> TypeError -> TCM ()
forall a b. (a -> b) -> a -> b
$ UnquoteError -> TypeError
UnquoteFailed UnquoteError
err
    Right (Term, [QName])
_ -> () -> TCM ()
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ()

---------------------------------------------------------------------------
-- * Meta variables
---------------------------------------------------------------------------

-- | Check an interaction point without arguments.
checkQuestionMark
  :: (Comparison -> Type -> TCM (MetaId, Term))
  -> Comparison
  -> Type            -- ^ Not reduced!
  -> A.MetaInfo
  -> InteractionId
  -> TCM Term
checkQuestionMark :: (Comparison -> Type'' Term Term -> TCMT IO (MetaId, Term))
-> Comparison
-> Type'' Term Term
-> MetaInfo
-> InteractionId
-> TCMT IO Term
checkQuestionMark Comparison -> Type'' Term Term -> TCMT IO (MetaId, Term)
new Comparison
cmp Type'' Term Term
t0 MetaInfo
i InteractionId
ii = do
  ArgName -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m ()
reportSDoc ArgName
"tc.interaction" Int
20 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
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
"Found interaction point"
    , ArgName -> TCMT IO Doc
forall (m :: * -> *). Applicative m => ArgName -> m Doc
text (ArgName -> TCMT IO Doc)
-> (IsAbstract -> ArgName) -> IsAbstract -> TCMT IO Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. IsAbstract -> ArgName
forall a. Show a => a -> ArgName
show (IsAbstract -> TCMT IO Doc) -> TCMT IO IsAbstract -> TCMT IO Doc
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< (TCEnv -> IsAbstract) -> TCMT IO IsAbstract
forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
asksTC (TCEnv -> Getting IsAbstract TCEnv IsAbstract -> IsAbstract
forall s a. s -> Getting a s a -> a
^. Getting IsAbstract TCEnv IsAbstract
forall a. LensIsAbstract a => Lens' a IsAbstract
Lens' TCEnv IsAbstract
lensIsAbstract)
    , InteractionId -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty InteractionId
ii
    , TCMT IO Doc
":"
    , Type'' Term Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type'' Term Term -> m Doc
prettyTCM Type'' Term Term
t0
    ]
  ArgName -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m ()
reportSDoc ArgName
"tc.interaction" Int
90 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
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
"Raw:"
    , ArgName -> TCMT IO Doc
forall (m :: * -> *). Applicative m => ArgName -> m Doc
text (Type'' Term Term -> ArgName
forall a. Show a => a -> ArgName
show Type'' Term Term
t0)
    ]
  MetaInfo
-> (Comparison -> Type'' Term Term -> TCMT IO (MetaId, Term))
-> Comparison
-> Type'' Term Term
-> TCMT IO Term
checkMeta MetaInfo
i ((Comparison -> Type'' Term Term -> TCMT IO (MetaId, Term))
-> InteractionId
-> Comparison
-> Type'' Term Term
-> TCMT IO (MetaId, Term)
newQuestionMark' Comparison -> Type'' Term Term -> TCMT IO (MetaId, Term)
new InteractionId
ii) Comparison
cmp Type'' Term Term
t0 -- Andreas, 2013-05-22 use unreduced type t0!

-- | Check an underscore without arguments.
checkUnderscore :: A.MetaInfo -> Comparison -> Type -> TCM Term
checkUnderscore :: MetaInfo -> Comparison -> Type'' Term Term -> TCMT IO Term
checkUnderscore MetaInfo
i = MetaInfo
-> (Comparison -> Type'' Term Term -> TCMT IO (MetaId, Term))
-> Comparison
-> Type'' Term Term
-> TCMT IO Term
checkMeta MetaInfo
i (MetaInfo
-> RunMetaOccursCheck
-> Comparison
-> Type'' Term Term
-> TCMT IO (MetaId, Term)
newValueMetaOfKind MetaInfo
i RunMetaOccursCheck
RunMetaOccursCheck)

-- | Type check a meta variable.
checkMeta :: A.MetaInfo -> (Comparison -> Type -> TCM (MetaId, Term)) -> Comparison -> Type -> TCM Term
checkMeta :: MetaInfo
-> (Comparison -> Type'' Term Term -> TCMT IO (MetaId, Term))
-> Comparison
-> Type'' Term Term
-> TCMT IO Term
checkMeta MetaInfo
i Comparison -> Type'' Term Term -> TCMT IO (MetaId, Term)
newMeta Comparison
cmp Type'' Term Term
t = (Term, Type'' Term Term) -> Term
forall a b. (a, b) -> a
fst ((Term, Type'' Term Term) -> Term)
-> TCM (Term, Type'' Term Term) -> TCMT IO Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> MetaInfo
-> (Comparison -> Type'' Term Term -> TCMT IO (MetaId, Term))
-> Maybe (Comparison, Type'' Term Term)
-> TCM (Term, Type'' Term Term)
checkOrInferMeta MetaInfo
i Comparison -> Type'' Term Term -> TCMT IO (MetaId, Term)
newMeta ((Comparison, Type'' Term Term)
-> Maybe (Comparison, Type'' Term Term)
forall a. a -> Maybe a
Just (Comparison
cmp , Type'' Term Term
t))

-- | Infer the type of a meta variable.
--   If it is a new one, we create a new meta for its type.
inferMeta :: A.MetaInfo -> (Comparison -> Type -> TCM (MetaId, Term)) -> TCM (Elims -> Term, Type)
inferMeta :: MetaInfo
-> (Comparison -> Type'' Term Term -> TCMT IO (MetaId, Term))
-> TCM (Elims -> Term, Type'' Term Term)
inferMeta MetaInfo
i Comparison -> Type'' Term Term -> TCMT IO (MetaId, Term)
newMeta = (Term -> Elims -> Term)
-> (Term, Type'' Term Term) -> (Elims -> Term, Type'' Term Term)
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 -> Elims -> Term
forall t. Apply t => t -> Elims -> t
applyE ((Term, Type'' Term Term) -> (Elims -> Term, Type'' Term Term))
-> TCM (Term, Type'' Term Term)
-> TCM (Elims -> Term, Type'' Term Term)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> MetaInfo
-> (Comparison -> Type'' Term Term -> TCMT IO (MetaId, Term))
-> Maybe (Comparison, Type'' Term Term)
-> TCM (Term, Type'' Term Term)
checkOrInferMeta MetaInfo
i Comparison -> Type'' Term Term -> TCMT IO (MetaId, Term)
newMeta Maybe (Comparison, Type'' Term Term)
forall a. Maybe a
Nothing

-- | Type check a meta variable.
--   If its type is not given, we return its type, or a fresh one, if it is a new meta.
--   If its type is given, we check that the meta has this type, and we return the same
--   type.
checkOrInferMeta
  :: A.MetaInfo
  -> (Comparison -> Type -> TCM (MetaId, Term))
  -> Maybe (Comparison , Type)
  -> TCM (Term, Type)
checkOrInferMeta :: MetaInfo
-> (Comparison -> Type'' Term Term -> TCMT IO (MetaId, Term))
-> Maybe (Comparison, Type'' Term Term)
-> TCM (Term, Type'' Term Term)
checkOrInferMeta MetaInfo
i Comparison -> Type'' Term Term -> TCMT IO (MetaId, Term)
newMeta Maybe (Comparison, Type'' Term Term)
mt = do
  -- We still need to check equational constraints even when checking a meta
  -- because definitions parameterised by a local rewrite rule do not block
  -- on the corresponding argument
  case MetaInfo -> Maybe MetaId
A.metaNumber MetaInfo
i of
    Maybe MetaId
Nothing -> do
      ScopeInfo -> (ScopeInfo -> TCM ()) -> TCM ()
forall (m :: * -> *) a.
(Monad m, Null a) =>
a -> (a -> m ()) -> m ()
unlessNull (MetaInfo -> ScopeInfo
A.metaScope MetaInfo
i) ScopeInfo -> TCM ()
setScope
      (cmp , t) <- TCMT IO (Comparison, Type'' Term Term)
-> ((Comparison, Type'' Term Term)
    -> TCMT IO (Comparison, Type'' Term Term))
-> Maybe (Comparison, Type'' Term Term)
-> TCMT IO (Comparison, Type'' Term Term)
forall b a. b -> (a -> b) -> Maybe a -> b
maybe ((Comparison
CmpEq,) (Type'' Term Term -> (Comparison, Type'' Term Term))
-> TCM (Type'' Term Term) -> TCMT IO (Comparison, Type'' Term Term)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCM (Type'' Term Term) -> TCM (Type'' Term Term)
forall (m :: * -> *) a.
(MonadTCEnv m, HasOptions m, MonadDebug m) =>
m a -> m a
workOnTypes TCM (Type'' Term Term)
newTypeMeta_) (Comparison, Type'' Term Term)
-> TCMT IO (Comparison, Type'' Term Term)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (Comparison, Type'' Term Term)
mt
      (x, v) <- newMeta cmp t
      setMetaNameSuggestion x (A.metaNameSuggestion i)
      return (v, t)
    -- Rechecking an existing metavariable
    Just MetaId
x -> do
      let v :: Term
v = MetaId -> Elims -> Term
MetaV MetaId
x []
      ArgName -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m ()
reportSDoc ArgName
"tc.meta.check" Int
20 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$
        TCMT IO Doc
"checking existing meta " 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
      t' <- MetaId -> TCM (Type'' Term Term)
forall (m :: * -> *).
ReadTCState m =>
MetaId -> m (Type'' Term Term)
metaType MetaId
x
      reportSDoc "tc.meta.check" 20 $
        nest 2 $ "of type " <+> prettyTCM t'
      case mt of
        Maybe (Comparison, Type'' Term Term)
Nothing -> (Term, Type'' Term Term) -> TCM (Term, Type'' Term Term)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Term
v, Type'' Term Term
t')
        Just (Comparison
cmp , Type'' Term Term
t) -> (,Type'' Term Term
t) (Term -> (Term, Type'' Term Term))
-> TCMT IO Term -> TCM (Term, Type'' Term Term)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Comparison
-> Term -> Type'' Term Term -> Type'' Term Term -> TCMT IO Term
coerce Comparison
cmp Term
v Type'' Term Term
t' Type'' Term Term
t

-- | Turn a domain-free binding (e.g. lambda) into a domain-full one,
--   by inserting an underscore for the missing type.
domainFree :: ArgInfo -> A.Binder' A.Name -> A.LamBinding
domainFree :: ArgInfo -> Binder' Name -> LamBinding
domainFree ArgInfo
info Binder' Name
x =
  TypedBinding -> LamBinding
A.DomainFull (TypedBinding -> LamBinding) -> TypedBinding -> LamBinding
forall a b. (a -> b) -> a -> b
$ Range' SrcFile
-> List1 (Arg (Named_ (Binder' BindName))) -> Expr -> TypedBinding
A.mkTBind Range' SrcFile
r (Arg (Named_ (Binder' BindName))
-> List1 (Arg (Named_ (Binder' BindName)))
forall el coll. Singleton el coll => el -> coll
singleton (Arg (Named_ (Binder' BindName))
 -> List1 (Arg (Named_ (Binder' BindName))))
-> Arg (Named_ (Binder' BindName))
-> List1 (Arg (Named_ (Binder' BindName)))
forall a b. (a -> b) -> a -> b
$ ArgInfo -> Binder' BindName -> Arg (Named_ (Binder' BindName))
forall a. ArgInfo -> a -> NamedArg a
unnamedArg ArgInfo
info (Binder' BindName -> Arg (Named_ (Binder' BindName)))
-> Binder' BindName -> Arg (Named_ (Binder' BindName))
forall a b. (a -> b) -> a -> b
$ (Name -> BindName) -> Binder' Name -> Binder' BindName
forall a b. (a -> b) -> Binder' a -> Binder' b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Name -> BindName
A.mkBindName Binder' Name
x)
               (Expr -> TypedBinding) -> Expr -> TypedBinding
forall a b. (a -> b) -> a -> b
$ MetaInfo -> Expr
A.Underscore MetaInfo
underscoreInfo
  where
    r :: Range' SrcFile
r = Binder' Name -> Range' SrcFile
forall a. HasRange a => a -> Range' SrcFile
getRange Binder' Name
x
    underscoreInfo :: MetaInfo
underscoreInfo = A.MetaInfo
      { metaRange :: Range' SrcFile
A.metaRange          = Range' SrcFile
r
      , metaScope :: ScopeInfo
A.metaScope          = ScopeInfo
emptyScopeInfo
      , metaNumber :: Maybe MetaId
A.metaNumber         = Maybe MetaId
forall a. Maybe a
Nothing
      , metaNameSuggestion :: ArgName
A.metaNameSuggestion = Name -> ArgName
forall a. Pretty a => a -> ArgName
prettyShow (Name -> ArgName) -> Name -> ArgName
forall a b. (a -> b) -> a -> b
$ Name -> Name
A.nameConcrete (Name -> Name) -> Name -> Name
forall a b. (a -> b) -> a -> b
$ Binder' Name -> Name
forall a. Binder' a -> a
A.binderName Binder' Name
x
      , metaKind :: MetaKind
A.metaKind           = MetaKind
A.UnificationMeta
      }


-- | Check arguments whose value we already know.
--
--   This function can be used to check user-supplied parameters
--   we have already computed by inference.
--
--   Precondition: The type @t@ of the head has enough domains.

checkKnownArguments
  :: [NamedArg A.Expr]  -- ^ User-supplied arguments (hidden ones may be missing).
  -> Args               -- ^ Inferred arguments (including hidden ones).
  -> Type               -- ^ Type of the head (must be Pi-type with enough domains).
  -> TCM (Args, Type)   -- ^ Remaining inferred arguments, remaining type.
checkKnownArguments :: [Arg (Named_ Expr)]
-> [Arg Term]
-> Type'' Term Term
-> TCM ([Arg Term], Type'' Term Term)
checkKnownArguments []           [Arg Term]
vs Type'' Term Term
t = ([Arg Term], Type'' Term Term)
-> TCM ([Arg Term], Type'' Term Term)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Arg Term]
vs, Type'' Term Term
t)
checkKnownArguments (Arg (Named_ Expr)
arg : [Arg (Named_ Expr)]
args) [Arg Term]
vs Type'' Term Term
t = do
  (vs', t') <- Arg (Named_ Expr)
-> TCM ([Arg Term], Type'' Term Term)
-> TCM ([Arg Term], Type'' Term Term)
forall (m :: * -> *) x a.
(MonadTrace m, HasRange x) =>
x -> m a -> m a
setCurrentRange Arg (Named_ Expr)
arg (TCM ([Arg Term], Type'' Term Term)
 -> TCM ([Arg Term], Type'' Term Term))
-> TCM ([Arg Term], Type'' Term Term)
-> TCM ([Arg Term], Type'' Term Term)
forall a b. (a -> b) -> a -> b
$ Arg (Named_ Expr)
-> [Arg Term]
-> Type'' Term Term
-> TCM ([Arg Term], Type'' Term Term)
checkKnownArgument Arg (Named_ Expr)
arg [Arg Term]
vs Type'' Term Term
t
  checkKnownArguments args vs' t'

-- | Check an argument whose value we already know.

checkKnownArgument
  :: NamedArg A.Expr    -- ^ User-supplied argument.
  -> Args               -- ^ Inferred arguments (including hidden ones).
  -> Type               -- ^ Type of the head (must be Pi-type with enough domains).
  -> TCM (Args, Type)   -- ^ Remaining inferred arguments, remaining type.
checkKnownArgument :: Arg (Named_ Expr)
-> [Arg Term]
-> Type'' Term Term
-> TCM ([Arg Term], Type'' Term Term)
checkKnownArgument Arg (Named_ Expr)
arg [] Type'' Term Term
_ = TypeError -> TCM ([Arg Term], Type'' Term Term)
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> TCM ([Arg Term], Type'' Term Term))
-> TypeError -> TCM ([Arg Term], Type'' Term Term)
forall a b. (a -> b) -> a -> b
$ Arg (Named_ Expr) -> TypeError
InvalidProjectionParameter Arg (Named_ Expr)
arg
-- Andreas, 2019-07-22, while #3353: we should use domName, not absName !!
-- WAS:
-- checkKnownArgument arg@(Arg info e) (Arg _infov v : vs) t = do
--   (dom@Dom{domInfo = info',unDom = a}, b) <- mustBePi t
--   -- Skip the arguments from vs that do not correspond to e
--   if not (sameHiding info info'
--           && (visible info || maybe True (absName b ==) (bareNameOf e)))
checkKnownArgument Arg (Named_ Expr)
arg (Arg ArgInfo
_ Term
v : [Arg Term]
vs) Type'' Term Term
t = do
  -- Skip the arguments from vs that do not correspond to e
  (dom@(unDom -> a), b) <- Type'' Term Term
-> TCMT IO (Dom' Term (Type'' Term Term), Abs (Type'' Term Term))
forall (m :: * -> *).
MonadReduce m =>
Type'' Term Term
-> m (Dom' Term (Type'' Term Term), Abs (Type'' Term Term))
mustBePi Type'' Term Term
t
  if not $ fromMaybe __IMPOSSIBLE__ $ fittingNamedArg arg dom
    -- Continue with the next one
    then checkKnownArgument arg vs (b `absApp` v)
    -- Found the right argument
    else do
      u <- checkNamedArg arg a
      equalTerm a u v
      return (vs, b `absApp` v)

-- | Check a single argument.

checkNamedArg :: NamedArg A.Expr -> Type -> TCM Term
checkNamedArg :: Arg (Named_ Expr) -> Type'' Term Term -> TCMT IO Term
checkNamedArg arg :: Arg (Named_ Expr)
arg@(Arg ArgInfo
info Named_ Expr
e0) Type'' Term Term
t0 = do
  let e :: Expr
e = Named_ Expr -> Expr
forall name a. Named name a -> a
namedThing Named_ Expr
e0
  let x :: ArgName
x = ArgName -> Named_ Expr -> ArgName
forall a.
(LensNamed a, NameOf a ~ WithOrigin (Ranged ArgName)) =>
ArgName -> a -> ArgName
bareNameWithDefault ArgName
"" Named_ Expr
e0
  Call -> TCMT IO Term -> TCMT IO Term
forall a. Call -> TCMT IO a -> TCMT IO a
forall (m :: * -> *) a. MonadTrace m => Call -> m a -> m a
traceCall (Comparison -> Expr -> Type'' Term Term -> Call
CheckExprCall Comparison
CmpLeq Expr
e Type'' Term Term
t0) (TCMT IO Term -> TCMT IO Term) -> TCMT IO Term -> TCMT IO Term
forall a b. (a -> b) -> a -> b
$ do
    ArgName -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m ()
reportSDoc ArgName
"tc.term.args.named" Int
15 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ do
        TCMT IO Doc
"Checking named arg" 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
fsep [ Arg (Named_ Expr) -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Arg (Named_ Expr) -> m Doc
prettyTCM Arg (Named_ Expr)
arg, TCMT IO Doc
":", Type'' Term Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type'' Term Term -> m Doc
prettyTCM Type'' Term Term
t0 ]
          ]
    ArgName -> Int -> ArgName -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> ArgName -> m ()
reportSLn ArgName
"tc.term.args.named" Int
75 (ArgName -> TCM ()) -> ArgName -> TCM ()
forall a b. (a -> b) -> a -> b
$ ArgName
"  arg = " ArgName -> ArgName -> ArgName
forall a. [a] -> [a] -> [a]
++! Arg (Named_ Expr) -> ArgName
forall a. Show a => a -> ArgName
show (Arg (Named_ Expr) -> Arg (Named_ Expr)
forall a. ExprLike a => a -> a
deepUnscope Arg (Named_ Expr)
arg)
    -- Ulf, 2017-03-24: (#2172) Always treat explicit _ and ? as implicit
    -- argument (i.e. solve with unification).
    -- Andreas, 2024-03-07, issue #2829: Except when we don't.
    -- E.g. when 'insertImplicitPatSynArgs' inserted an instance underscore.
    let checkU :: MetaInfo -> TCMT IO Term
checkU MetaInfo
i = MetaInfo
-> (Comparison -> Type'' Term Term -> TCMT IO (MetaId, Term))
-> Comparison
-> Type'' Term Term
-> TCMT IO Term
checkMeta MetaInfo
i
          (\Comparison
cmp -> MetaKind
-> ArgName
-> Comparison
-> Dom' Term (Type'' Term Term)
-> TCMT IO (MetaId, Term)
newMetaArg (MetaInfo -> MetaKind
A.metaKind MetaInfo
i) ArgName
x Comparison
cmp (Dom' Term (Type'' Term Term) -> TCMT IO (MetaId, Term))
-> (Type'' Term Term -> Dom' Term (Type'' Term Term))
-> Type'' Term Term
-> TCMT IO (MetaId, Term)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ArgInfo -> Type'' Term Term -> Dom' Term (Type'' Term Term)
forall a. ArgInfo -> a -> Dom a
defaultArgDom ArgInfo
info)
          Comparison
CmpLeq Type'' Term Term
t0
    let checkQ :: MetaInfo -> InteractionId -> TCMT IO Term
checkQ = (Comparison -> Type'' Term Term -> TCMT IO (MetaId, Term))
-> Comparison
-> Type'' Term Term
-> MetaInfo
-> InteractionId
-> TCMT IO Term
checkQuestionMark (ArgInfo
-> ArgName
-> Comparison
-> Type'' Term Term
-> TCMT IO (MetaId, Term)
newInteractionMetaArg ArgInfo
info ArgName
x) Comparison
CmpLeq Type'' Term Term
t0
    if Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ Expr -> Bool
isHole Expr
e then Expr -> Type'' Term Term -> TCMT IO Term
checkExpr Expr
e Type'' Term Term
t0 else TCMT IO Term -> TCMT IO Term
forall a. TCM a -> TCM a
localScope (TCMT IO Term -> TCMT IO Term) -> TCMT IO Term -> TCMT IO Term
forall a b. (a -> b) -> a -> b
$ do
      -- Note: we need localScope_ here,
      -- as scopedExpr manipulates the scope in the state.
      -- However, we may not pull localScope_ over checkExpr!
      -- This is why we first test for isHole, and only do
      -- scope manipulations if we actually handle the checking
      -- of e here (and not pass it to checkExpr).
      Expr -> TCM Expr
scopedExpr Expr
e TCM Expr -> (Expr -> TCMT IO Term) -> TCMT IO 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
        A.Underscore MetaInfo
i ->  MetaInfo -> TCMT IO Term
checkU MetaInfo
i
        A.QuestionMark MetaInfo
i InteractionId
ii -> MetaInfo -> InteractionId -> TCMT IO Term
checkQ MetaInfo
i InteractionId
ii
        Expr
_ -> TCMT IO Term
forall a. HasCallStack => a
__IMPOSSIBLE__
  where
  isHole :: Expr -> Bool
isHole A.Underscore{} = Bool
True
  isHole A.QuestionMark{} = Bool
True
  isHole (A.ScopedExpr ScopeInfo
_ Expr
e) = Expr -> Bool
isHole Expr
e
  isHole Expr
_ = Bool
False

-- | Infer the type of an expression. Implemented by checking against a meta
--   variable.  Except for neutrals, for them a polymorphic type is inferred.
inferExpr :: A.Expr -> TCM (Term, Type)
-- inferExpr e = inferOrCheck e Nothing
inferExpr :: Expr -> TCM (Term, Type'' Term Term)
inferExpr = ExpandHidden -> Expr -> TCM (Term, Type'' Term Term)
inferExpr' ExpandHidden
DontExpandLast

inferExpr' :: ExpandHidden -> A.Expr -> TCM (Term, Type)
inferExpr' :: ExpandHidden -> Expr -> TCM (Term, Type'' Term Term)
inferExpr' ExpandHidden
exh Expr
e = Call
-> TCM (Term, Type'' Term Term) -> TCM (Term, Type'' Term Term)
forall a. Call -> TCMT IO a -> TCMT IO a
forall (m :: * -> *) a. MonadTrace m => Call -> m a -> m a
traceCall (Expr -> Call
InferExpr Expr
e) (TCM (Term, Type'' Term Term) -> TCM (Term, Type'' Term Term))
-> TCM (Term, Type'' Term Term) -> TCM (Term, Type'' Term Term)
forall a b. (a -> b) -> a -> b
$ do
  Application hd args <- Expr -> TCM AppView
appViewM Expr
e
  reportSDoc "tc.infer" 30 $ vcat
    [ "inferExpr': appView of " <+> prettyA e
    , "  hd   = " <+> prettyA hd
    , "  args = " <+> prettyAs args
    ]
  reportSDoc "tc.infer" 60 $ vcat
    [ text $ "  hd (raw) = " ++! show hd
    ]
  inferApplication exh hd args e

defOrVar :: A.Expr -> Bool
defOrVar :: Expr -> Bool
defOrVar A.Var{} = Bool
True
defOrVar A.Def'{} = Bool
True
defOrVar A.Proj{} = Bool
True
defOrVar (A.ScopedExpr ScopeInfo
_ Expr
e) = Expr -> Bool
defOrVar Expr
e
defOrVar Expr
_     = Bool
False

-- | Used to check aliases @f = e@.
--   Switches off 'ExpandLast' for the checking of top-level application.
checkDontExpandLast :: Comparison -> A.Expr -> Type -> TCM Term
checkDontExpandLast :: Comparison -> Expr -> Type'' Term Term -> TCMT IO Term
checkDontExpandLast Comparison
cmp Expr
e Type'' Term Term
t = do
  Application hd args <- Expr -> TCM AppView
appViewM Expr
e
  if defOrVar hd then
    traceCall (CheckExprCall cmp e t) $ localScope $ dontExpandLast $ do
      checkApplication cmp hd args e t
  else checkExpr' cmp e t -- note that checkExpr always sets ExpandLast

-- | Check whether a de Bruijn index is bound by a module telescope.
isModuleFreeVar :: Int -> TCM Bool
isModuleFreeVar :: Int -> TCMT IO Bool
isModuleFreeVar Int
i = do
  params <- ModuleName -> TCMT IO [Arg Term]
forall (m :: * -> *).
(HasOptions m, MonadTCEnv m, ReadTCState m, MonadDebug m) =>
ModuleName -> m [Arg Term]
moduleParamsToApply (ModuleName -> TCMT IO [Arg Term])
-> TCMT IO ModuleName -> TCMT IO [Arg Term]
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< TCMT IO ModuleName
forall (m :: * -> *). MonadTCEnv m => m ModuleName
currentModule
  return $! any ((== Var i []) . unArg) params

-- | Infer the type of an expression, and if it is of the form
--   @{tel} -> D vs@ for some datatype @D@ then insert the hidden
--   arguments.  Otherwise, leave the type polymorphic.
inferExprForWith :: Arg A.Expr -> TCM (Term, Type)
inferExprForWith :: Arg Expr -> TCM (Term, Type'' Term Term)
inferExprForWith (Arg ArgInfo
info Expr
e) = ArgName
-> Int
-> ArgName
-> TCM (Term, Type'' Term Term)
-> TCM (Term, Type'' Term Term)
forall a. ArgName -> Int -> ArgName -> TCMT IO a -> TCMT IO a
forall (m :: * -> *) a.
MonadDebug m =>
ArgName -> Int -> ArgName -> m a -> m a
verboseBracket ArgName
"tc.with.infer" Int
20 ArgName
"inferExprForWith" (TCM (Term, Type'' Term Term) -> TCM (Term, Type'' Term Term))
-> TCM (Term, Type'' Term Term) -> TCM (Term, Type'' Term Term)
forall a b. (a -> b) -> a -> b
$
  Relevance
-> TCM (Term, Type'' Term Term) -> TCM (Term, Type'' Term Term)
forall (tcm :: * -> *) r a.
(MonadTCEnv tcm, LensRelevance r) =>
r -> tcm a -> tcm a
applyRelevanceToContext (ArgInfo -> Relevance
forall a. LensRelevance a => a -> Relevance
getRelevance ArgInfo
info) (TCM (Term, Type'' Term Term) -> TCM (Term, Type'' Term Term))
-> TCM (Term, Type'' Term Term) -> TCM (Term, Type'' Term Term)
forall a b. (a -> b) -> a -> b
$ do
    ArgName -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m ()
reportSDoc ArgName
"tc.with.infer" Int
20 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"inferExprForWith " 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
e
    ArgName -> Int -> ArgName -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> ArgName -> m ()
reportSLn  ArgName
"tc.with.infer" Int
80 (ArgName -> TCM ()) -> ArgName -> TCM ()
forall a b. (a -> b) -> a -> b
$ ArgName
"inferExprForWith " ArgName -> ArgName -> ArgName
forall a. [a] -> [a] -> [a]
++! Expr -> ArgName
forall a. Show a => a -> ArgName
show (Expr -> Expr
forall a. ExprLike a => a -> a
deepUnscope Expr
e)
    Call
-> TCM (Term, Type'' Term Term) -> TCM (Term, Type'' Term Term)
forall a. Call -> TCMT IO a -> TCMT IO a
forall (m :: * -> *) a. MonadTrace m => Call -> m a -> m a
traceCall (Expr -> Call
InferExpr Expr
e) (TCM (Term, Type'' Term Term) -> TCM (Term, Type'' Term Term))
-> TCM (Term, Type'' Term Term) -> TCM (Term, Type'' Term Term)
forall a b. (a -> b) -> a -> b
$ do
      -- Andreas, 2024-02-26, issue #7148:
      -- The 'instantiateFull' here performs necessary eta-contraction,
      -- both for future with-abstraction,
      -- and for testing whether v is a variable modulo eta.
      (v, t) <- (Term, Type'' Term Term) -> TCM (Term, Type'' Term Term)
forall a (m :: * -> *).
(InstantiateFull a, MonadReduce m) =>
a -> m a
instantiateFull ((Term, Type'' Term Term) -> TCM (Term, Type'' Term Term))
-> TCM (Term, Type'' Term Term) -> TCM (Term, Type'' Term Term)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Expr -> TCM (Term, Type'' Term Term)
inferExpr Expr
e
      v <- reduce v
      -- Andreas 2014-11-06, issue 1342.
      -- Check that we do not `with` on a module parameter!
      case v of
        Var Int
i [] -> TCMT IO Bool -> TCM () -> TCM ()
forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
whenM (Int -> TCMT IO Bool
isModuleFreeVar Int
i) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ do
          ArgName -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m ()
reportSDoc ArgName
"tc.with.infer" Int
80 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
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
            [ ArgName -> TCMT IO Doc
forall (m :: * -> *). Applicative m => ArgName -> m Doc
text (ArgName -> TCMT IO Doc) -> ArgName -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ ArgName
"with expression is variable " ArgName -> ArgName -> ArgName
forall a. [a] -> [a] -> [a]
++! Int -> ArgName
forall a. Show a => a -> ArgName
show Int
i
            , TCMT IO Doc
"current modules = " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> do ArgName -> TCMT IO Doc
forall (m :: * -> *). Applicative m => ArgName -> m Doc
text (ArgName -> TCMT IO Doc)
-> (ModuleName -> ArgName) -> ModuleName -> TCMT IO Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ModuleName -> ArgName
forall a. Show a => a -> ArgName
show (ModuleName -> TCMT IO Doc) -> TCMT IO ModuleName -> TCMT IO Doc
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< TCMT IO ModuleName
forall (m :: * -> *). MonadTCEnv m => m ModuleName
currentModule
            , TCMT IO Doc
"current module free vars = " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> do ArgName -> TCMT IO Doc
forall (m :: * -> *). Applicative m => ArgName -> m Doc
text (ArgName -> TCMT IO Doc) -> (Int -> ArgName) -> Int -> TCMT IO Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> ArgName
forall a. Show a => a -> ArgName
show (Int -> TCMT IO Doc) -> TCMT IO Int -> TCMT IO Doc
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< TCMT IO Int
getCurrentModuleFreeVars
            , TCMT IO Doc
"context size = " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> do ArgName -> TCMT IO Doc
forall (m :: * -> *). Applicative m => ArgName -> m Doc
text (ArgName -> TCMT IO Doc) -> (Int -> ArgName) -> Int -> TCMT IO Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> ArgName
forall a. Show a => a -> ArgName
show (Int -> TCMT IO Doc) -> TCMT IO Int -> TCMT IO Doc
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< TCMT IO Int
forall (m :: * -> *). MonadTCEnv m => m Int
getContextSize
            , TCMT IO Doc
"current context = " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> do Telescope -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Telescope -> m Doc
prettyTCM (Telescope -> TCMT IO Doc) -> TCMT IO Telescope -> TCMT IO Doc
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< TCMT IO Telescope
forall (m :: * -> *). MonadTCEnv m => m Telescope
getContextTelescope
            ]
          TypeError -> TCM ()
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> TCM ()) -> TypeError -> TCM ()
forall a b. (a -> b) -> a -> b
$ Expr -> Term -> TypeError
WithOnFreeVariable Expr
e Term
v
        Term
_        -> () -> TCM ()
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
      -- Possibly insert hidden arguments.
      TelV tel t0 <- telViewUpTo' (-1) (not . visible) t
      (v, t) <- case unEl t0 of
        Def QName
d Elims
vs -> do
          QName -> TCM (Maybe DataOrRecord)
isDataOrRecordType QName
d TCM (Maybe DataOrRecord)
-> (Maybe DataOrRecord -> TCM (Term, Type'' Term Term))
-> TCM (Term, Type'' Term 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
            Maybe DataOrRecord
Nothing -> (Term, Type'' Term Term) -> TCM (Term, Type'' Term Term)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Term
v, Type'' Term Term
t)
            Just{}  -> do
              (args, t1) <- Int
-> (Hiding -> Bool)
-> Type'' Term Term
-> TCM ([Arg Term], Type'' Term Term)
implicitArgs (-Int
1) Hiding -> Bool
forall a. LensHiding a => a -> Bool
notVisible Type'' Term Term
t
              return (v `apply` args, t1)
        Term
_ -> (Term, Type'' Term Term) -> TCM (Term, Type'' Term Term)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Term
v, Type'' Term Term
t)
      -- #6868, #7113: trigger instance search to resolve instances in with-expression
      solveAwakeConstraints
      return (v, t)

---------------------------------------------------------------------------
-- * Let bindings
---------------------------------------------------------------------------

checkLetBindings' :: Foldable t => t A.LetBinding -> TCM a -> TCM a
checkLetBindings' :: forall (t :: * -> *) a.
Foldable t =>
t LetBinding -> TCM a -> TCM a
checkLetBindings' = (LetBinding -> (TCMT IO a -> TCMT IO a) -> TCMT IO a -> TCMT IO a)
-> (TCMT IO a -> TCMT IO a)
-> t LetBinding
-> TCMT IO a
-> TCMT IO a
forall a b. (a -> b -> b) -> b -> t a -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr ((TCMT IO a -> TCMT IO a)
-> (TCMT IO a -> TCMT IO a) -> TCMT IO a -> TCMT IO a
forall b c a. (b -> c) -> (a -> b) -> a -> c
(.) ((TCMT IO a -> TCMT IO a)
 -> (TCMT IO a -> TCMT IO a) -> TCMT IO a -> TCMT IO a)
-> (LetBinding -> TCMT IO a -> TCMT IO a)
-> LetBinding
-> (TCMT IO a -> TCMT IO a)
-> TCMT IO a
-> TCMT IO a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LetBinding -> TCMT IO a -> TCMT IO a
forall a. LetBinding -> TCM a -> TCM a
checkLetBinding') TCMT IO a -> TCMT IO a
forall a. a -> a
id

checkLetBinding' :: A.LetBinding -> TCM a -> TCM a

checkLetBinding' :: forall a. LetBinding -> TCM a -> TCM a
checkLetBinding' b :: LetBinding
b@(A.LetBind LetInfo
i ArgInfo
info BindName
x Expr
t Expr
e) TCM a
ret = do
  -- #4131: Only DontExpandLast if no user written type signature
  let
    check :: Comparison -> Expr -> Type'' Term Term -> TCMT IO Term
check
      | ArgInfo -> Origin
forall a. LensOrigin a => a -> Origin
getOrigin ArgInfo
info Origin -> Origin -> Bool
forall a. Eq a => a -> a -> Bool
== Origin
Inserted = Comparison -> Expr -> Type'' Term Term -> TCMT IO Term
checkDontExpandLast
      | Bool
otherwise                  = Comparison -> Expr -> Type'' Term Term -> TCMT IO Term
checkExpr'

  t <- TCM (Type'' Term Term) -> TCM (Type'' Term Term)
forall (m :: * -> *) a.
(MonadTCEnv m, HasOptions m, MonadDebug m) =>
m a -> m a
workOnTypes (TCM (Type'' Term Term) -> TCM (Type'' Term Term))
-> TCM (Type'' Term Term) -> TCM (Type'' Term Term)
forall a b. (a -> b) -> a -> b
$ Expr -> TCM (Type'' Term Term)
isType_ Expr
t
  v <- applyModalityToContext info $ check CmpLeq e t

  addLetBinding info UserWritten (A.unBind x) v t ret

checkLetBinding' b :: LetBinding
b@(A.LetAxiom LetInfo
i ArgInfo
info BindName
x Expr
t) TCM a
ret = do
  t <- TCM (Type'' Term Term) -> TCM (Type'' Term Term)
forall (m :: * -> *) a.
(MonadTCEnv m, HasOptions m, MonadDebug m) =>
m a -> m a
workOnTypes (TCM (Type'' Term Term) -> TCM (Type'' Term Term))
-> TCM (Type'' Term Term) -> TCM (Type'' Term Term)
forall a b. (a -> b) -> a -> b
$ Expr -> TCM (Type'' Term Term)
isType_ Expr
t
  current <- currentModule

  -- Note: if addConstant is called under a nontrivial context then
  -- it'll automatically quantify the type we give it over the context
  axn <- qualify current <$> freshName_ (A.unBind x)
  addConstant' axn info t defaultAxiom

  val <- Def axn . fmap Apply <$> getContextArgs
  addLetAxiom info UserWritten (A.unBind x) val t ret

checkLetBinding' b :: LetBinding
b@(A.LetPatBind LetInfo
i ArgInfo
ai Pattern' Expr
p Expr
e) TCM a
ret = do
    p <- Pattern' Expr -> TCM (Pattern' Expr)
forall a. ExpandPatternSynonyms a => a -> TCM a
expandPatternSynonyms Pattern' Expr
p
    (v, t) <- applyModalityToContext ai $ inferExpr' ExpandLast e
    let -- construct a type  t -> dummy  for use in checkLeftHandSide
        t0 = Sort' Term -> Term -> Type'' Term Term
forall t a. Sort' t -> a -> Type'' t a
El (Type'' Term Term -> Sort' Term
forall a. LensSort a => a -> Sort' Term
getSort Type'' Term Term
t) (Term -> Type'' Term Term) -> Term -> Type'' Term Term
forall a b. (a -> b) -> a -> b
$ Dom' Term (Type'' Term Term) -> Abs (Type'' Term Term) -> Term
Pi (ArgInfo -> Type'' Term Term -> Dom' Term (Type'' Term Term)
forall a. ArgInfo -> a -> Dom a
defaultArgDom ArgInfo
ai Type'' Term Term
t) (ArgName -> Type'' Term Term -> Abs (Type'' Term Term)
forall a. ArgName -> a -> Abs a
NoAbs ArgName
forall a. Underscore a => a
underscore Type'' Term Term
HasCallStack => Type'' Term Term
__DUMMY_TYPE__)
        p0 = ArgInfo
-> Named (WithOrigin (Ranged ArgName)) (Pattern' Expr)
-> NamedArg (Pattern' Expr)
forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
ai (Maybe (WithOrigin (Ranged ArgName))
-> Pattern' Expr
-> Named (WithOrigin (Ranged ArgName)) (Pattern' Expr)
forall name a. Maybe name -> a -> Named name a
Named Maybe (WithOrigin (Ranged ArgName))
forall a. Maybe a
Nothing Pattern' Expr
p)
    reportSDoc "tc.term.let.pattern" 10 $ vcat
      [ "let-binding pattern p at type t"
      , nest 2 $ vcat
        [ "p (A) =" <+> prettyA p
        , "t     =" <+> prettyTCM t
        , "cxtRel=" <+> do pretty =<< viewTC eRelevance
        , "cxtQnt=" <+> do pretty =<< viewTC eQuantityZeroHardCompile
        ]
      ]
    fvs <- getContextSize
    checkLeftHandSide (CheckPattern p EmptyTel t) noRange LetLHS [p0] t0 NoWithFunction [] $ \ (LHSResult Int
_ Telescope
delta0 NAPs
ps Bool
_ Arg (Type'' Term Term)
_t Substitution
_ [AsBinding]
asb IntSet
_ Bool
_) -> Pattern' Expr -> TCM a -> TCM a
forall (m :: * -> *) x a.
(MonadTrace m, HasRange x) =>
x -> m a -> m a
setCurrentRange Pattern' Expr
p (TCM a -> TCM a) -> TCM a -> TCM a
forall a b. (a -> b) -> a -> b
$ [AsBinding] -> TCM a -> TCM a
forall a. [AsBinding] -> TCM a -> TCM a
bindAsPatterns [AsBinding]
asb (TCM a -> TCM a) -> TCM a -> TCM a
forall a b. (a -> b) -> a -> b
$ do
          -- After dropping the free variable patterns there should be a single pattern left.
      let p :: DeBruijnPattern
p = case Int -> NAPs -> NAPs
forall a. Int -> [a] -> [a]
drop Int
fvs NAPs
ps of [Arg (Named_ DeBruijnPattern)
p] -> Arg (Named_ DeBruijnPattern) -> DeBruijnPattern
forall a. NamedArg a -> a
namedArg Arg (Named_ DeBruijnPattern)
p; NAPs
_ -> DeBruijnPattern
forall a. HasCallStack => a
__IMPOSSIBLE__
          -- Also strip the context variables from the telescope
          delta :: Telescope
delta = ListTel -> Telescope
telFromList (ListTel -> Telescope) -> ListTel -> Telescope
forall a b. (a -> b) -> a -> b
$ Int -> ListTel -> ListTel
forall a. Int -> [a] -> [a]
drop Int
fvs (ListTel -> ListTel) -> ListTel -> ListTel
forall a b. (a -> b) -> a -> b
$ Telescope -> ListTel
forall t. Tele (Dom t) -> [Dom (ArgName, t)]
telToList Telescope
delta0
      ArgName -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m ()
reportSDoc ArgName
"tc.term.let.pattern" Int
20 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
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
        [ TCMT IO Doc
"p (I) =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> DeBruijnPattern -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => DeBruijnPattern -> m Doc
prettyTCM DeBruijnPattern
p
        , TCMT IO Doc
"delta =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Telescope -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Telescope -> m Doc
prettyTCM Telescope
delta
        , TCMT IO Doc
"cxtRel=" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> do Relevance -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty (Relevance -> TCMT IO Doc) -> TCMT IO Relevance -> TCMT IO Doc
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Lens' TCEnv Relevance -> TCMT IO Relevance
forall (m :: * -> *) a. MonadTCEnv m => Lens' TCEnv a -> m a
viewTC (Relevance -> f Relevance) -> TCEnv -> f TCEnv
Lens' TCEnv Relevance
eRelevance
        , TCMT IO Doc
"cxtQnt=" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> do Quantity -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty (Quantity -> TCMT IO Doc) -> TCMT IO Quantity -> TCMT IO Doc
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Lens' TCEnv Quantity -> TCMT IO Quantity
forall (m :: * -> *) a. MonadTCEnv m => Lens' TCEnv a -> m a
viewTC (Quantity -> f Quantity) -> TCEnv -> f TCEnv
Lens' TCEnv Quantity
eQuantityZeroHardCompile
        ]
      ArgName -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m ()
reportSDoc ArgName
"tc.term.let.pattern" Int
80 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
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
        [ TCMT IO Doc
"p (I) =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> (ArgName -> TCMT IO Doc
forall (m :: * -> *). Applicative m => ArgName -> m Doc
text (ArgName -> TCMT IO Doc)
-> (DeBruijnPattern -> ArgName) -> DeBruijnPattern -> TCMT IO Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DeBruijnPattern -> ArgName
forall a. Show a => a -> ArgName
show) DeBruijnPattern
p
        ]
      -- We translate it into a list of projections.
      fs <- DeBruijnPattern -> TCM [Term -> Term]
recordPatternToProjections DeBruijnPattern
p
      -- We remove the bindings for the pattern variables from the context.
      cxt0 <- getContext
      let binds  = Int -> Context' ContextEntry -> [ContextEntry]
cxTake (Telescope -> Int
forall a. Sized a => a -> Int
size Telescope
delta) Context' ContextEntry
cxt0
          toDrop = [ContextEntry] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [ContextEntry]
binds

          -- We create a substitution for the let-bound variables
          -- (unfortunately, we cannot refer to x in internal syntax
          -- so we have to copy v).
          sigma = ((Term -> Term) -> Term) -> [Term -> Term] -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map' ((Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ Term
v) [Term -> Term]
fs
          -- We apply the types of the let bound-variables to this substitution.
          -- The 0th variable in a context is the last one, so we reverse.
          -- Further, we need to lower all other de Bruijn indices by
          -- the size of delta, so we append the identity substitution.
          sub    = [Term] -> Substitution
forall a. DeBruijn a => [a] -> Substitution' a
parallelS ([Term] -> [Term]
forall a. [a] -> [a]
reverse [Term]
sigma)

      updateContext sub (cxDrop toDrop) $ do
        reportSDoc "tc.term.let.pattern" 20 $ nest 2 $ vcat
          [ "delta =" <+> prettyTCM delta
          , "binds =" <+> prettyTCM binds
          ]
        let fdelta = Telescope -> [Dom' Term (Type'' Term Term)]
forall a. TermSubst a => Tele (Dom a) -> [Dom a]
flattenTel Telescope
delta
        reportSDoc "tc.term.let.pattern" 20 $ nest 2 $ vcat
          [ "fdelta =" <+> addContext delta (prettyTCM fdelta)
          ]
        let tsl  = Substitution' (SubstArg [Dom' Term (Type'' Term Term)])
-> [Dom' Term (Type'' Term Term)] -> [Dom' Term (Type'' Term Term)]
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution
Substitution' (SubstArg [Dom' Term (Type'' Term Term)])
sub [Dom' Term (Type'' Term Term)]
fdelta
        -- We get a list of types
        let ts   = (Dom' Term (Type'' Term Term) -> Type'' Term Term)
-> [Dom' Term (Type'' Term Term)] -> [Type'' Term Term]
forall a b. (a -> b) -> [a] -> [b]
map' Dom' Term (Type'' Term Term) -> Type'' Term Term
forall t e. Dom' t e -> e
unDom [Dom' Term (Type'' Term Term)]
tsl
        -- and relevances.
        let infos = (Dom' Term (Type'' Term Term) -> ArgInfo)
-> [Dom' Term (Type'' Term Term)] -> [ArgInfo]
forall a b. (a -> b) -> [a] -> [b]
map' Dom' Term (Type'' Term Term) -> ArgInfo
forall t e. Dom' t e -> ArgInfo
domInfo [Dom' Term (Type'' Term Term)]
tsl
        -- We get list of names of the let-bound vars from the context.
        let xs   = (ContextEntry -> Name) -> [ContextEntry] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map' ContextEntry -> Name
ctxEntryName ([ContextEntry] -> [Name]) -> [ContextEntry] -> [Name]
forall a b. (a -> b) -> a -> b
$ [ContextEntry] -> [ContextEntry]
forall a. [a] -> [a]
reverse [ContextEntry]
binds
        -- We add all the bindings to the context.
        foldr (uncurry4 $ flip addLetBinding UserWritten) ret $ List.zip4 infos xs sigma ts

checkLetBinding' (A.LetApply ModuleInfo
i Erased
erased ModuleName
x ModuleApplication
modapp ScopeCopyInfo
copyInfo ImportDirective
dir) TCM a
ret = do
  -- Any variables in the context that doesn't belong to the current
  -- module should go with the new module.
  -- Example: @f x y = let open M t in u@.
  -- There are 2 @new@ variables, @x@ and @y@, going into the anonynous module
  -- @module _ (x : _) (y : _) = M t@.
  fv   <- TCMT IO Int
getCurrentModuleFreeVars
  n    <- getContextSize
  let new = Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
fv
  reportSDoc "tc.term.let.apply" 10 $ "Applying" <+> pretty x <+> prettyA modapp <?> ("with" <+> pshow new <+> "free variables")
  reportSDoc "tc.term.let.apply" 20 $ vcat
    [ "context =" <+> (prettyTCM =<< getContextTelescope)
    , "module  =" <+> (prettyTCM =<< currentModule)
    , "fv      =" <+> text (show fv)
    , "copy    =" <+> pretty copyInfo
    ]
  checkSectionApplication i erased x modapp copyInfo
    -- Some other part of the code ensures that "open public" is
    -- ignored in let expressions. Thus there is no need for
    -- checkSectionApplication to throw an error if the import
    -- directive does contain "open public".
    dir{ publicOpen = Nothing }
  withAnonymousModule x new ret
-- LetOpen and (WAS:) LetDeclaredVariable are only used for highlighting.
checkLetBinding' A.LetOpen{} TCM a
ret = TCM a
ret

-- | Version of checkLetBinding which traces the fact that we're
-- checking each binding in the Call.
checkLetBinding :: A.LetBinding -> TCM a -> TCM a
checkLetBinding :: forall a. LetBinding -> TCM a -> TCM a
checkLetBinding LetBinding
b = Call -> (TCMT IO a -> TCMT IO a) -> TCMT IO a -> TCMT IO a
forall (m :: * -> *) b.
MonadTrace m =>
Call -> (m b -> m b) -> m b -> m b
traceCallCPS' (LetBinding -> Call
CheckLetBinding LetBinding
b) (LetBinding -> TCMT IO a -> TCMT IO a
forall a. LetBinding -> TCM a -> TCM a
checkLetBinding' LetBinding
b)

checkLetBindings :: Foldable t => t A.LetBinding -> TCM a -> TCM a
checkLetBindings :: forall (t :: * -> *) a.
Foldable t =>
t LetBinding -> TCM a -> TCM a
checkLetBindings = (LetBinding -> (TCMT IO a -> TCMT IO a) -> TCMT IO a -> TCMT IO a)
-> (TCMT IO a -> TCMT IO a)
-> t LetBinding
-> TCMT IO a
-> TCMT IO a
forall a b. (a -> b -> b) -> b -> t a -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr ((TCMT IO a -> TCMT IO a)
-> (TCMT IO a -> TCMT IO a) -> TCMT IO a -> TCMT IO a
forall b c a. (b -> c) -> (a -> b) -> a -> c
(.) ((TCMT IO a -> TCMT IO a)
 -> (TCMT IO a -> TCMT IO a) -> TCMT IO a -> TCMT IO a)
-> (LetBinding -> TCMT IO a -> TCMT IO a)
-> LetBinding
-> (TCMT IO a -> TCMT IO a)
-> TCMT IO a
-> TCMT IO a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LetBinding -> TCMT IO a -> TCMT IO a
forall a. LetBinding -> TCM a -> TCM a
checkLetBinding) TCMT IO a -> TCMT IO a
forall a. a -> a
id