{-# LANGUAGE NondecreasingIndentation #-}

module Agda.TypeChecking.Rules.Term where

import Prelude hiding ( null )

import Control.Monad         ( (<=<), forM )
import Control.Monad.Except
import Control.Monad.Reader

import Data.Maybe
import Data.Either (partitionEithers, lefts)
import qualified Data.List as List
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))
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)
import qualified Agda.Syntax.Concrete.Name as C
import Agda.Syntax.Common
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, AbstractName
                              , 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.Irrelevance
import Agda.TypeChecking.IApplyConfluence
import Agda.TypeChecking.Level
import Agda.TypeChecking.Lock (requireGuarded)
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.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.Functor
import Agda.Utils.Lens
import Agda.Utils.List
import Agda.Utils.List1  ( List1, pattern (:|) )
import qualified Agda.Utils.List1 as List1
import Agda.Utils.Maybe
import Agda.Utils.Monad
import Agda.Utils.Null
import Agda.Utils.Pretty ( prettyShow )
import qualified Agda.Utils.Pretty as P
import Agda.Utils.Singleton
import Agda.Utils.Size
import Agda.Utils.Tuple

import Agda.Utils.Impossible

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

-- | Check that an expression is a type.
isType :: A.Expr -> Sort -> TCM Type
isType :: Expr -> Sort' Term -> TCM Type
isType = Comparison -> Expr -> Sort' Term -> TCM Type
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
isType' Comparison
c Expr
e Sort' Term
s =
    forall (m :: * -> *) a. MonadTrace m => Call -> m a -> m a
traceCall (Comparison -> Expr -> Sort' Term -> Call
IsTypeCall Comparison
c Expr
e Sort' Term
s) forall a b. (a -> b) -> a -> b
$ do
    Term
v <- Comparison -> Expr -> Type -> TCM Term
checkExpr' Comparison
c Expr
e (Sort' Term -> Type
sort Sort' Term
s)
    forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall t a. Sort' t -> a -> Type'' t a
El Sort' Term
s Term
v

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

    A.Generalized Set QName
s Expr
e -> do
      ([Maybe QName]
_, Type
t') <- Set QName -> TCM Type -> TCM ([Maybe QName], Type)
generalizeType Set QName
s forall a b. (a -> b) -> a -> b
$ Expr -> TCM Type
isType_ Expr
e
      --noFunctionsIntoSize t'
      forall (m :: * -> *) a. Monad m => a -> m a
return Type
t'

    -- Setᵢ
    A.Def' QName
x Suffix
suffix | QName
x forall a. Eq a => a -> a -> Bool
== QName
nameOfSet -> case Suffix
suffix of
      Suffix
NoSuffix -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Sort' Term -> Type
sort (Integer -> Sort' Term
mkType Integer
0)
      Suffix Integer
i -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Sort' Term -> Type
sort (Integer -> Sort' Term
mkType Integer
i)

    -- Propᵢ
    A.Def' QName
x Suffix
suffix | QName
x forall a. Eq a => a -> a -> Bool
== QName
nameOfProp -> do
      forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
unlessM forall (m :: * -> *). HasOptions m => m Bool
isPropEnabled forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError TypeError
NeedOptionProp
      case Suffix
suffix of
        Suffix
NoSuffix -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Sort' Term -> Type
sort (Integer -> Sort' Term
mkProp Integer
0)
        Suffix Integer
i -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Sort' Term -> Type
sort (Integer -> Sort' Term
mkProp Integer
i)

    -- Setᵢ
    A.Def' QName
x Suffix
suffix | QName
x forall a. Eq a => a -> a -> Bool
== QName
nameOfSSet -> do
      forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
unlessM forall (m :: * -> *). HasOptions m => m Bool
isTwoLevelEnabled forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError TypeError
NeedOptionTwoLevel
      case Suffix
suffix of
        Suffix
NoSuffix -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Sort' Term -> Type
sort (Integer -> Sort' Term
mkSSet Integer
0)
        Suffix Integer
i -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Sort' Term -> Type
sort (Integer -> Sort' Term
mkSSet Integer
i)

    -- Setωᵢ
    A.Def' QName
x Suffix
suffix | QName
x forall a. Eq a => a -> a -> Bool
== IsFibrant -> QName
nameOfSetOmega IsFibrant
IsFibrant -> case Suffix
suffix of
      Suffix
NoSuffix -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Sort' Term -> Type
sort (forall t. IsFibrant -> Integer -> Sort' t
Inf IsFibrant
IsFibrant Integer
0)
      Suffix Integer
i -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Sort' Term -> Type
sort (forall t. IsFibrant -> Integer -> Sort' t
Inf IsFibrant
IsFibrant Integer
i)

    -- SSetωᵢ
    A.Def' QName
x Suffix
suffix | QName
x forall a. Eq a => a -> a -> Bool
== IsFibrant -> QName
nameOfSetOmega IsFibrant
IsStrict -> do
      forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
unlessM forall (m :: * -> *). HasOptions m => m Bool
isTwoLevelEnabled forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError TypeError
NeedOptionTwoLevel
      case Suffix
suffix of
        Suffix
NoSuffix -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Sort' Term -> Type
sort (forall t. IsFibrant -> Integer -> Sort' t
Inf IsFibrant
IsStrict Integer
0)
        Suffix Integer
i -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Sort' Term -> Type
sort (forall t. IsFibrant -> Integer -> Sort' t
Inf IsFibrant
IsStrict Integer
i)

    -- Set ℓ
    A.App AppInfo
i Expr
s NamedArg Expr
arg
      | forall a. LensHiding a => a -> Bool
visible NamedArg Expr
arg,
        A.Def QName
x <- Expr -> Expr
unScope Expr
s,
        QName
x forall a. Eq a => a -> a -> Bool
== QName
nameOfSet -> do
      forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
unlessM forall (m :: * -> *). HasOptions m => m Bool
hasUniversePolymorphism forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
ArgName -> m a
genericError
        ArgName
"Use --universe-polymorphism to enable level arguments to Set"
      -- allow NonStrict variables when checking level
      --   Set : (NonStrict) Level -> Set\omega
      forall (tcm :: * -> *) r a.
(MonadTCEnv tcm, LensRelevance r) =>
r -> tcm a -> tcm a
applyRelevanceToContext Relevance
NonStrict forall a b. (a -> b) -> a -> b
$
        Sort' Term -> Type
sort forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t. Level' t -> Sort' t
Type forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> NamedArg Expr -> TCM (Level' Term)
checkLevel NamedArg Expr
arg

    -- Prop ℓ
    A.App AppInfo
i Expr
s NamedArg Expr
arg
      | forall a. LensHiding a => a -> Bool
visible NamedArg Expr
arg,
        A.Def QName
x <- Expr -> Expr
unScope Expr
s,
        QName
x forall a. Eq a => a -> a -> Bool
== QName
nameOfProp -> do
      forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
unlessM forall (m :: * -> *). HasOptions m => m Bool
isPropEnabled forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError TypeError
NeedOptionProp
      forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
unlessM forall (m :: * -> *). HasOptions m => m Bool
hasUniversePolymorphism forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
ArgName -> m a
genericError
        ArgName
"Use --universe-polymorphism to enable level arguments to Prop"
      forall (tcm :: * -> *) r a.
(MonadTCEnv tcm, LensRelevance r) =>
r -> tcm a -> tcm a
applyRelevanceToContext Relevance
NonStrict forall a b. (a -> b) -> a -> b
$
        Sort' Term -> Type
sort forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t. Level' t -> Sort' t
Prop forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> NamedArg Expr -> TCM (Level' Term)
checkLevel NamedArg Expr
arg

    -- SSet ℓ
    A.App AppInfo
i Expr
s NamedArg Expr
arg
      | forall a. LensHiding a => a -> Bool
visible NamedArg Expr
arg,
        A.Def QName
x <- Expr -> Expr
unScope Expr
s,
        QName
x forall a. Eq a => a -> a -> Bool
== QName
nameOfSSet -> do
      forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
unlessM forall (m :: * -> *). HasOptions m => m Bool
isTwoLevelEnabled forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError TypeError
NeedOptionTwoLevel
      forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
unlessM forall (m :: * -> *). HasOptions m => m Bool
hasUniversePolymorphism forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
ArgName -> m a
genericError
        ArgName
"Use --universe-polymorphism to enable level arguments to SSet"
      forall (tcm :: * -> *) r a.
(MonadTCEnv tcm, LensRelevance r) =>
r -> tcm a -> tcm a
applyRelevanceToContext Relevance
NonStrict forall a b. (a -> b) -> a -> b
$
        Sort' Term -> Type
sort forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t. Level' t -> Sort' t
SSet forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> NamedArg Expr -> TCM (Level' Term)
checkLevel NamedArg Expr
arg

    -- Issue #707: Check an existing interaction point
    A.QuestionMark MetaInfo
minfo InteractionId
ii -> forall (m :: * -> *) a b.
Monad m =>
m (Maybe a) -> m b -> (a -> m b) -> m b
caseMaybeM (forall (m :: * -> *).
ReadTCState m =>
InteractionId -> m (Maybe MetaId)
lookupInteractionMeta InteractionId
ii) TCM Type
fallback forall a b. (a -> b) -> a -> b
$ \ MetaId
x -> do
      -- -- | Just x <- A.metaNumber minfo -> do
      forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m ()
reportSDoc ArgName
"tc.ip" Int
20 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep
        [ TCMT IO Doc
"Rechecking meta "
        , forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM MetaId
x
        , forall (m :: * -> *). Applicative m => ArgName -> m Doc
text forall a b. (a -> b) -> a -> b
$ ArgName
" for interaction point " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> ArgName
show InteractionId
ii
        ]
      MetaVariable
mv <- forall (m :: * -> *).
(HasCallStack, MonadDebug m, ReadTCState m) =>
MetaId -> m MetaVariable
lookupLocalMeta MetaId
x
      let s0 :: Type
s0 = forall a. Judgement a -> Type
jMetaType forall b c a. (b -> c) -> (a -> b) -> a -> c
. MetaVariable -> Judgement MetaId
mvJudgement 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 :: Int
n  = forall (t :: * -> *) a. Foldable t => t a -> Int
length forall b c a. (b -> c) -> (a -> b) -> a -> c
. TCEnv -> [ContextEntry]
envContext forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Closure a -> TCEnv
clEnv forall b c a. (b -> c) -> (a -> b) -> a -> c
. MetaInfo -> Closure Range
miClosRange forall b c a. (b -> c) -> (a -> b) -> a -> c
. MetaVariable -> MetaInfo
mvInfo forall a b. (a -> b) -> a -> b
$ MetaVariable
mv
      ([Arg Term]
vs, [Arg Term]
rest) <- forall a. Int -> [a] -> ([a], [a])
splitAt Int
n forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m [Arg Term]
getContextArgs
      forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m ()
reportSDoc ArgName
"tc.ip" Int
20 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
        [ TCMT IO Doc
"  s0   = " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
s0
        , TCMT IO Doc
"  vs   = " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM [Arg Term]
vs
        , TCMT IO Doc
"  rest = " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM [Arg Term]
rest
        ]
      -- 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 (forall (t :: * -> *) a. Foldable t => t a -> Int
length [Arg Term]
vs forall a. Eq a => a -> a -> Bool
/= Int
n) then TCM Type
fallback else do
      Type
s1  <- forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall a (m :: * -> *).
(PiApplyM a, MonadReduce m, HasBuiltins m) =>
Type -> a -> m Type
piApplyM Type
s0 [Arg Term]
vs
      forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m ()
reportSDoc ArgName
"tc.ip" Int
20 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
        [ TCMT IO Doc
"  s1   = " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
s1
        ]
      forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m ()
reportSDoc ArgName
"tc.ip" Int
70 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
        [ TCMT IO Doc
"  s1   = " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *). Applicative m => ArgName -> m Doc
text (forall a. Show a => a -> ArgName
show Type
s1)
        ]
      case forall t a. Type'' t a -> a
unEl Type
s1 of
        Sort Sort' Term
s -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall t a. Sort' t -> a -> Type'' t a
El Sort' Term
s forall a b. (a -> b) -> a -> b
$ MetaId -> Elims -> Term
MetaV MetaId
x forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall a. Arg a -> Elim' a
Apply [Arg Term]
vs
        Term
_ -> forall a. HasCallStack => a
__IMPOSSIBLE__

    Expr
_ -> TCM Type
fallback

checkLevel :: NamedArg A.Expr -> TCM Level
checkLevel :: NamedArg Expr -> TCM (Level' Term)
checkLevel NamedArg Expr
arg = do
  Type
lvl <- forall (m :: * -> *). (HasBuiltins m, MonadTCError m) => m Type
levelType
  forall (m :: * -> *). PureTCM m => Term -> m (Level' Term)
levelView forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< NamedArg Expr -> Type -> TCM Term
checkNamedArg NamedArg Expr
arg Type
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 -> TCM Type
isTypeEqualTo Expr
e0 Type
t = Expr -> TCM Expr
scopedExpr Expr
e0 forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
  A.ScopedExpr{} -> forall a. HasCallStack => a
__IMPOSSIBLE__
  A.Underscore MetaInfo
i | forall a. Maybe a -> Bool
isNothing (MetaInfo -> Maybe MetaId
A.metaNumber MetaInfo
i) -> forall (m :: * -> *) a. Monad m => a -> m a
return Type
t
  Expr
e -> forall (m :: * -> *) a.
(MonadTCEnv m, HasOptions m, MonadDebug m) =>
m a -> m a
workOnTypes forall a b. (a -> b) -> a -> b
$ do
    Type
t' <- Expr -> Sort' Term -> TCM Type
isType Expr
e (forall a. LensSort a => a -> Sort' Term
getSort Type
t)
    Type
t' forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ forall (m :: * -> *). MonadConversion m => Type -> Type -> m ()
leqType Type
t Type
t'

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

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

checkGeneralizeTelescope :: A.GeneralizeTelescope -> ([Maybe Name] -> Telescope -> TCM a) -> TCM a
checkGeneralizeTelescope :: forall a.
GeneralizeTelescope
-> ([Maybe Name] -> Telescope -> TCM a) -> TCM a
checkGeneralizeTelescope (A.GeneralizeTel Map QName Name
vars Telescope
tel) [Maybe Name] -> Telescope -> TCM a
k =
  forall a.
Map QName Name
-> (forall a1. (Telescope -> TCM a1) -> TCM a1)
-> ([Maybe Name] -> Telescope -> TCM a)
-> TCM a
generalizeTelescope Map QName Name
vars (forall a. Telescope -> (Telescope -> TCM a) -> TCM a
checkTelescope Telescope
tel) [Maybe Name] -> Telescope -> TCM a
k

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

-- | 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 = forall a. LamOrPi -> Telescope -> (Telescope -> TCM a) -> TCM a
checkTelescope' LamOrPi
PiNotLam

-- | Flag to control resurrection on domains.
data LamOrPi
  = LamNotPi -- ^ 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
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: LamOrPi -> LamOrPi -> Bool
$c/= :: LamOrPi -> LamOrPi -> Bool
== :: LamOrPi -> LamOrPi -> Bool
$c== :: LamOrPi -> LamOrPi -> Bool
Eq, Int -> LamOrPi -> ShowS
[LamOrPi] -> ShowS
LamOrPi -> ArgName
forall a.
(Int -> a -> ShowS) -> (a -> ArgName) -> ([a] -> ShowS) -> Show a
showList :: [LamOrPi] -> ShowS
$cshowList :: [LamOrPi] -> ShowS
show :: LamOrPi -> ArgName
$cshow :: LamOrPi -> ArgName
showsPrec :: Int -> LamOrPi -> ShowS
$cshowsPrec :: Int -> LamOrPi -> ShowS
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 forall a. Tele a
EmptyTel
checkTelescope' LamOrPi
lamOrPi (TypedBinding
b : Telescope
tel) Telescope -> TCM a
ret =
    forall a. LamOrPi -> TypedBinding -> (Telescope -> TCM a) -> TCM a
checkTypedBindings LamOrPi
lamOrPi TypedBinding
b forall a b. (a -> b) -> a -> b
$ \Telescope
tel1 ->
    forall a. LamOrPi -> Telescope -> (Telescope -> TCM a) -> TCM a
checkTelescope' LamOrPi
lamOrPi Telescope
tel  forall a b. (a -> b) -> a -> b
$ \Telescope
tel2 ->
        Telescope -> TCM a
ret forall a b. (a -> b) -> a -> b
$ 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) => LamOrPi -> List1 a -> A.Expr -> TCM Type
checkDomain :: forall a.
(LensLock a, LensModality a) =>
LamOrPi -> List1 a -> Expr -> TCM Type
checkDomain LamOrPi
lamOrPi List1 a
xs Expr
e = do
    let (Cohesion
c :| [Cohesion]
cs) = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall a. LensCohesion a => a -> Cohesion
getCohesion forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. LensModality a => a -> Modality
getModality) List1 a
xs
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (Cohesion
c forall a. Eq a => a -> a -> Bool
==) [Cohesion]
cs) forall a b. (a -> b) -> a -> b
$ forall a. HasCallStack => a
__IMPOSSIBLE__

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

    Type
t <- forall (tcm :: * -> *) q a.
(MonadTCEnv tcm, LensQuantity q) =>
q -> tcm a -> tcm a
applyQuantityToContext Quantity
q forall a b. (a -> b) -> a -> b
$
         forall (tcm :: * -> *) m a.
(MonadTCEnv tcm, LensCohesion m) =>
m -> tcm a -> tcm a
applyCohesionToContext Cohesion
c forall a b. (a -> b) -> a -> b
$
         forall {m :: * -> *} {a}.
(MonadTCEnv m, HasOptions m, MonadDebug m) =>
LamOrPi -> m a -> m a
modEnv LamOrPi
lamOrPi forall a b. (a -> b) -> a -> b
$ Expr -> TCM Type
isType_ Expr
e
    -- Andrea TODO: also make sure that LockUniv implies IsLock
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (\ a
x -> forall a. LensLock a => a -> Lock
getLock a
x forall a. Eq a => a -> a -> Bool
== Lock
IsLock) List1 a
xs) forall a b. (a -> b) -> a -> b
$ do
        ArgName -> TCM ()
requireGuarded ArgName
"which is needed for @tick/@lock attributes."
         -- Solves issue #5033
        forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
unlessM (forall a. Maybe a -> Bool
isJust forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasBuiltins m => ArgName -> m (Maybe QName)
getName' ArgName
builtinLockUniv) forall a b. (a -> b) -> a -> b
$ do
          forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
Doc -> m a
genericDocError forall a b. (a -> b) -> a -> b
$ Doc
"Missing binding for primLockUniv primitive."

        forall (m :: * -> *).
MonadConversion m =>
Sort' Term -> Sort' Term -> m ()
equalSort (forall a. LensSort a => a -> Sort' Term
getSort Type
t) forall t. Sort' t
LockUniv

    forall (m :: * -> *) a. Monad m => a -> m a
return Type
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 LamOrPi
LamNotPi = forall (m :: * -> *) a.
(MonadTCEnv m, HasOptions m, MonadDebug m) =>
m a -> m a
workOnTypes
        modEnv LamOrPi
_        = forall a. a -> a
id

checkPiDomain :: (LensLock a, LensModality a) => List1 a -> A.Expr -> TCM Type
checkPiDomain :: forall a.
(LensLock a, LensModality a) =>
List1 a -> Expr -> TCM Type
checkPiDomain = forall a.
(LensLock a, LensModality a) =>
LamOrPi -> List1 a -> Expr -> TCM Type
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 wether 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
r TypedBindingInfo
tac List1 (NamedArg (Binder' BindName))
xps Expr
e) Telescope -> TCM a
ret = do
    let xs :: NonEmpty (NamedArg Name)
xs = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall a b. (a -> b) -> NamedArg a -> NamedArg b
updateNamedArg forall a b. (a -> b) -> a -> b
$ BindName -> Name
A.unBind forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Binder' a -> a
A.binderName) List1 (NamedArg (Binder' BindName))
xps
    Maybe Term
tac <- forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (LamOrPi -> Expr -> TCM Term
checkTacticAttribute LamOrPi
lamOrPi) (TypedBindingInfo -> Maybe Expr
tbTacticAttr TypedBindingInfo
tac)
    forall (m :: * -> *) a. Monad m => Maybe a -> (a -> m ()) -> m ()
whenJust Maybe Term
tac forall a b. (a -> b) -> a -> b
$ \ Term
t -> forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m ()
reportSDoc ArgName
"tc.term.tactic" Int
30 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"Checked tactic attribute:" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<?> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> 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
    Bool
experimental <- PragmaOptions -> Bool
optExperimentalIrrelevance forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasOptions m => m PragmaOptions
pragmaOptions

    Type
t <- forall a.
(LensLock a, LensModality a) =>
LamOrPi -> List1 a -> Expr -> TCM Type
checkDomain LamOrPi
lamOrPi List1 (NamedArg (Binder' BindName))
xps Expr
e

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

    let setTac :: Maybe t -> Tele (Dom' t e) -> Tele (Dom' t e)
setTac Maybe t
tac Tele (Dom' t e)
EmptyTel            = forall a. Tele a
EmptyTel
        setTac Maybe t
tac (ExtendTel Dom' t e
dom Abs (Tele (Dom' t e))
tel) = forall a. a -> Abs (Tele a) -> Tele a
ExtendTel Dom' t e
dom{ domTactic :: Maybe t
domTactic = Maybe t
tac } forall a b. (a -> b) -> a -> b
$ Maybe t -> Tele (Dom' t e) -> Tele (Dom' t e)
setTac (forall a. Subst a => Int -> a -> a
raise Int
1 Maybe t
tac) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Abs (Tele (Dom' t e))
tel
        xs' :: NonEmpty (NamedArg Name)
xs' = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall {a}. LensRelevance a => LamOrPi -> Bool -> a -> a
modMod LamOrPi
lamOrPi Bool
experimental) NonEmpty (NamedArg Name)
xs
    let tel :: Telescope
tel = forall {t} {t} {e}.
Subst t =>
Maybe t -> Tele (Dom' t e) -> Tele (Dom' t e)
setTac Maybe Term
tac forall a b. (a -> b) -> a -> b
$ NonEmpty (NamedArg Name) -> Type -> Telescope
namedBindsToTel1 NonEmpty (NamedArg Name)
xs Type
t

    forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext (NonEmpty (NamedArg Name)
xs', Type
t) forall a b. (a -> b) -> a -> b
$ forall a. List1 (NamedArg (Binder' BindName)) -> TCM a -> TCM a
addTypedPatterns List1 (NamedArg (Binder' BindName))
xps (Telescope -> TCM a
ret Telescope
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
        modEnv :: LamOrPi -> m a -> m a
modEnv LamOrPi
LamNotPi = forall (m :: * -> *) a.
(MonadTCEnv m, HasOptions m, MonadDebug m) =>
m a -> m a
workOnTypes
        modEnv LamOrPi
_        = forall a. a -> a
id
        modMod :: LamOrPi -> Bool -> a -> a
modMod LamOrPi
PiNotLam Bool
xp = (if Bool
xp then forall a. LensRelevance a => (Relevance -> Relevance) -> a -> a
mapRelevance Relevance -> Relevance
irrToNonStrict else forall a. a -> a
id)
        modMod LamOrPi
_        Bool
_  = forall a. a -> a
id

checkTypedBindings LamOrPi
lamOrPi (A.TLet Range
_ List1 LetBinding
lbs) Telescope -> TCM a
ret = do
    forall (t :: * -> *) a.
Foldable t =>
t LetBinding -> TCM a -> TCM a
checkLetBindings List1 LetBinding
lbs (Telescope -> TCM a
ret 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 (NamedArg (Binder' BindName)) -> TCM a -> TCM a
addTypedPatterns List1 (NamedArg (Binder' BindName))
xps TCM a
ret = do
  let ps :: [(Pattern, BindName)]
ps  = forall a b. (a -> Maybe b) -> List1 a -> [b]
List1.mapMaybe (forall a. Binder' a -> Maybe (Pattern, a)
A.extractPattern forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. NamedArg a -> a
namedArg) List1 (NamedArg (Binder' BindName))
xps
  let lbs :: [LetBinding]
lbs = forall a b. (a -> b) -> [a] -> [b]
map (Pattern, BindName) -> LetBinding
letBinding [(Pattern, BindName)]
ps
  forall (t :: * -> *) a.
Foldable t =>
t LetBinding -> TCM a -> TCM a
checkLetBindings [LetBinding]
lbs TCM a
ret
  where
    letBinding :: (A.Pattern, A.BindName) -> A.LetBinding
    letBinding :: (Pattern, BindName) -> LetBinding
letBinding (Pattern
p, BindName
n) = LetInfo -> Pattern -> Expr -> LetBinding
A.LetPatBind (Range -> LetInfo
A.LetRange Range
r) Pattern
p (Name -> Expr
A.Var forall a b. (a -> b) -> a -> b
$ BindName -> Name
A.unBind BindName
n)
      where r :: Range
r = forall u t. (HasRange u, HasRange t) => u -> t -> Range
fuseRange Pattern
p BindName
n

-- | Check a tactic attribute. Should have type Term → TC ⊤.
checkTacticAttribute :: LamOrPi -> A.Expr -> TCM Term
checkTacticAttribute :: LamOrPi -> Expr -> TCM Term
checkTacticAttribute LamOrPi
LamNotPi Expr
e = forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
Doc -> m a
genericDocError forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< TCMT IO Doc
"The @tactic attribute is not allowed here"
checkTacticAttribute LamOrPi
PiNotLam Expr
e = do
  Type
expectedType <- forall (m :: * -> *). Functor m => m Term -> m Type
el forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTerm forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> forall (m :: * -> *). Functor m => m Term -> m Type
el (forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTCM forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primLevelZero forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primUnit)
  Expr -> Type -> TCM Term
checkExpr Expr
e Type
expectedType

checkPath :: A.TypedBinding -> A.Expr -> Type -> TCM Term
checkPath :: TypedBinding -> Expr -> Type -> TCM Term
checkPath b :: TypedBinding
b@(A.TBind Range
_r TypedBindingInfo
_tac (NamedArg (Binder' BindName)
xp :| []) Expr
typ) Expr
body Type
ty = do
 forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m ()
reportSDoc ArgName
"tc.term.lambda" Int
30 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
hsep [ TCMT IO Doc
"checking path lambda", forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA NamedArg (Binder' BindName)
xp ]
 case (forall a. Binder' a -> Maybe (Pattern, a)
A.extractPattern forall a b. (a -> b) -> a -> b
$ forall a. NamedArg a -> a
namedArg NamedArg (Binder' BindName)
xp) of
  Just{}  -> forall (m :: * -> *) x a.
(MonadTrace m, HasRange x) =>
x -> m a -> m a
setCurrentRange NamedArg (Binder' BindName)
xp forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
ArgName -> m a
genericError forall a b. (a -> b) -> a -> b
$ ArgName
"Patterns are not allowed in Path-lambdas"
  Maybe (Pattern, BindName)
Nothing -> do
    let x :: NamedArg Name
x    = forall a b. (a -> b) -> NamedArg a -> NamedArg b
updateNamedArg (BindName -> Name
A.unBind forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Binder' a -> a
A.binderName) NamedArg (Binder' BindName)
xp
        info :: ArgInfo
info = forall a. LensArgInfo a => a -> ArgInfo
getArgInfo NamedArg Name
x
    PathType Sort' Term
s QName
path Arg Term
level Arg Term
typ Arg Term
lhs Arg Term
rhs <- forall (m :: * -> *). HasBuiltins m => Type -> m PathView
pathView Type
ty
    Type
interval <- forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Type
primIntervalType
    Term
v <- forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext ([NamedArg Name
x], Type
interval) forall a b. (a -> b) -> a -> b
$
           Expr -> Type -> TCM Term
checkExpr Expr
body (forall t a. Sort' t -> a -> Type'' t a
El (forall a. Subst a => Int -> a -> a
raise Int
1 Sort' Term
s) (forall a. Subst a => Int -> a -> a
raise Int
1 (forall e. Arg e -> e
unArg Arg Term
typ) forall t. Apply t => t -> [Arg Term] -> t
`apply` [forall e. e -> Arg e
argN forall a b. (a -> b) -> a -> b
$ Int -> Term
var Int
0]))
    Term
iZero <- forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primIZero
    Term
iOne  <- forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primIOne
    let lhs' :: Term
lhs' = forall a. Subst a => Int -> SubstArg a -> a -> a
subst Int
0 Term
iZero Term
v
        rhs' :: Term
rhs' = forall a. Subst a => Int -> SubstArg a -> a -> a
subst Int
0 Term
iOne  Term
v
    let t :: Term
t = ArgInfo -> Abs Term -> Term
Lam ArgInfo
info forall a b. (a -> b) -> a -> b
$ forall a. ArgName -> a -> Abs a
Abs (NamedArg Name -> ArgName
namedArgName NamedArg Name
x) Term
v
    let btyp :: Term -> Type
btyp Term
i = forall t a. Sort' t -> a -> Type'' t a
El Sort' Term
s (forall e. Arg e -> e
unArg Arg Term
typ forall t. Apply t => t -> [Arg Term] -> t
`apply` [forall e. e -> Arg e
argN Term
i])
    forall (m :: * -> *) a b.
MonadTCEnv m =>
Lens' a TCEnv -> (a -> a) -> m b -> m b
locallyTC Lens' Range TCEnv
eRange (forall a b. a -> b -> a
const forall a. Range' a
noRange) forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
(MonadMetaSolver m, MonadConstraint m, MonadFresh Int m,
 MonadFresh ProblemId m) =>
Type -> m Term -> m Term
blockTerm Type
ty forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) x a.
(MonadTrace m, HasRange x) =>
x -> m a -> m a
setCurrentRange Expr
body forall a b. (a -> b) -> a -> b
$ do
      forall (m :: * -> *).
MonadConversion m =>
Type -> Term -> Term -> m ()
equalTerm (Term -> Type
btyp Term
iZero) Term
lhs' (forall e. Arg e -> e
unArg Arg Term
lhs)
      forall (m :: * -> *).
MonadConversion m =>
Type -> Term -> Term -> m ()
equalTerm (Term -> Type
btyp Term
iOne) Term
rhs' (forall e. Arg e -> e
unArg Arg Term
rhs)
      forall (m :: * -> *) a. Monad m => a -> m a
return Term
t
checkPath TypedBinding
b Expr
body Type
ty = forall a. HasCallStack => a
__IMPOSSIBLE__

---------------------------------------------------------------------------
-- * 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 -> TCM Term
checkLambda Comparison
cmp (A.TLet Range
_ List1 LetBinding
lbs) Expr
body Type
target =
  forall (t :: * -> *) a.
Foldable t =>
t LetBinding -> TCM a -> TCM a
checkLetBindings List1 LetBinding
lbs (Expr -> Type -> TCM Term
checkExpr Expr
body Type
target)
checkLambda Comparison
cmp b :: TypedBinding
b@(A.TBind Range
r TypedBindingInfo
tac List1 (NamedArg (Binder' BindName))
xps0 Expr
typ) Expr
body Type
target = do
  forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m ()
reportSDoc ArgName
"tc.term.lambda" Int
30 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
    [ TCMT IO Doc
"checkLambda before insertion xs =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA List1 (NamedArg (Binder' BindName))
xps0
    ]
  -- Andreas, 2020-03-25, issue #4481: since we have named lambdas now,
  -- we need to insert skipped hidden arguments.
  List1 (NamedArg (Binder' BindName))
xps <- forall (m :: * -> *).
(PureTCM m, MonadError TCErr m, MonadFresh NameId m,
 MonadTrace m) =>
List1 (NamedArg (Binder' BindName))
-> Type -> m (List1 (NamedArg (Binder' BindName)))
insertImplicitBindersT1 List1 (NamedArg (Binder' BindName))
xps0 Type
target
  Comparison
-> TypedBinding
-> List1 (NamedArg (Binder' BindName))
-> Expr
-> Expr
-> Type
-> TCM Term
checkLambda' Comparison
cmp (Range
-> TypedBindingInfo
-> List1 (NamedArg (Binder' BindName))
-> Expr
-> TypedBinding
A.TBind Range
r TypedBindingInfo
tac List1 (NamedArg (Binder' BindName))
xps Expr
typ) List1 (NamedArg (Binder' BindName))
xps Expr
typ Expr
body Type
target

checkLambda'
  :: Comparison          -- ^ @cmp@
  -> A.TypedBinding      -- ^ @TBind _ _ xps typ@
  -> List1 (NamedArg Binder)   -- ^ @xps@
  -> A.Expr              -- ^ @typ@
  -> A.Expr              -- ^ @body@
  -> Type                -- ^ @target@
  -> TCM Term
checkLambda' :: Comparison
-> TypedBinding
-> List1 (NamedArg (Binder' BindName))
-> Expr
-> Expr
-> Type
-> TCM Term
checkLambda' Comparison
cmp TypedBinding
b List1 (NamedArg (Binder' BindName))
xps Expr
typ Expr
body Type
target = do
  forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m ()
reportSDoc ArgName
"tc.term.lambda" Int
30 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
    [ TCMT IO Doc
"checkLambda xs =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA List1 (NamedArg (Binder' BindName))
xps
    , TCMT IO Doc
"possiblePath   =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Bool
possiblePath
    , TCMT IO Doc
"numbinds       =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Int
numbinds
    , TCMT IO Doc
"typ            =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA   (Expr -> Expr
unScope Expr
typ)
    ]
  forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m ()
reportSDoc ArgName
"tc.term.lambda" Int
60 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
    [ TCMT IO Doc
"info           =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> (forall (m :: * -> *). Applicative m => ArgName -> m Doc
text forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => a -> ArgName
show) ArgInfo
info
    ]
  TelV Telescope
tel Type
btyp <- forall (m :: * -> *).
(MonadReduce m, MonadAddContext m) =>
Int -> Type -> m (TelV Type)
telViewUpTo Int
numbinds Type
target
  if forall a. Sized a => a -> Int
size Telescope
tel forall a. Ord a => a -> a -> Bool
< Int
numbinds Bool -> Bool -> Bool
|| Int
numbinds forall a. Eq a => a -> a -> Bool
/= Int
1
    then (if Bool
possiblePath then TCM Term
trySeeingIfPath else TCM Term
dontUseTargetType)
    else Telescope -> Type -> TCM Term
useTargetType Telescope
tel Type
btyp

  where

    xs :: NonEmpty (NamedArg Name)
xs = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall a b. (a -> b) -> NamedArg a -> NamedArg b
updateNamedArg (BindName -> Name
A.unBind forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Binder' a -> a
A.binderName)) List1 (NamedArg (Binder' BindName))
xps
    numbinds :: Int
numbinds = forall (t :: * -> *) a. Foldable t => t a -> Int
length List1 (NamedArg (Binder' BindName))
xps
    isUnderscore :: Expr -> Bool
isUnderscore = \case { A.Underscore{} -> Bool
True; Expr
_ -> Bool
False }
    possiblePath :: Bool
possiblePath = Int
numbinds forall a. Eq a => a -> a -> Bool
== Int
1 Bool -> Bool -> Bool
&& Expr -> Bool
isUnderscore (Expr -> Expr
unScope Expr
typ)
                   Bool -> Bool -> Bool
&& forall a. LensRelevance a => a -> Bool
isRelevant ArgInfo
info Bool -> Bool -> Bool
&& forall a. LensHiding a => a -> Bool
visible ArgInfo
info
    info :: ArgInfo
info = forall a. LensArgInfo a => a -> ArgInfo
getArgInfo forall a b. (a -> b) -> a -> b
$ forall a. NonEmpty a -> a
List1.head NonEmpty (NamedArg Name)
xs

    trySeeingIfPath :: TCM Term
trySeeingIfPath = do
      Bool
cubical <- forall a. Maybe a -> Bool
isJust forall b c a. (b -> c) -> (a -> b) -> a -> c
. PragmaOptions -> Maybe Cubical
optCubical forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasOptions m => m PragmaOptions
pragmaOptions
      forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> ArgName -> m ()
reportSLn ArgName
"tc.term.lambda" Int
60 forall a b. (a -> b) -> a -> b
$ ArgName
"trySeeingIfPath for " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> ArgName
show List1 (NamedArg (Binder' BindName))
xps
      let postpone' :: Blocker -> Type -> TCM Term
postpone' = if Bool
cubical then Blocker -> Type -> TCM Term
postpone else \ Blocker
_ Type
_ -> TCM Term
dontUseTargetType
      forall t (m :: * -> *) a.
(Reduce t, IsMeta t, MonadReduce m) =>
t -> (Blocker -> t -> m a) -> (NotBlocked -> t -> m a) -> m a
ifBlocked Type
target Blocker -> Type -> TCM Term
postpone' forall a b. (a -> b) -> a -> b
$ \ NotBlocked
_ Type
t -> do
        forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifNotM (PathView -> Bool
isPathType forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasBuiltins m => Type -> m PathView
pathView Type
t) TCM Term
dontUseTargetType {-else-} forall a b. (a -> b) -> a -> b
$ if Bool
cubical
          then TypedBinding -> Expr -> Type -> TCM Term
checkPath TypedBinding
b Expr
body Type
t
          else forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
ArgName -> m a
genericError forall a b. (a -> b) -> a -> b
$ [ArgName] -> ArgName
unwords
                 [ ArgName
"Option --cubical/--erased-cubical needed to build"
                 , ArgName
"a path with a lambda abstraction"
                 ]

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

    dontUseTargetType :: TCM Term
dontUseTargetType = do
      -- Checking λ (xs : argsT) → body : target
      forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> m () -> m ()
verboseS ArgName
"tc.term.lambda" Int
5 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). MonadStatistics m => ArgName -> m ()
tick ArgName
"lambda-no-target-type"

      -- First check that argsT is a valid type
      Type
argsT <- forall (m :: * -> *) a.
(MonadTCEnv m, HasOptions m, MonadDebug m) =>
m a -> m a
workOnTypes forall a b. (a -> b) -> a -> b
$ Expr -> TCM Type
isType_ Expr
typ
      let tel :: Telescope
tel = NonEmpty (NamedArg Name) -> Type -> Telescope
namedBindsToTel1 NonEmpty (NamedArg Name)
xs Type
argsT
      forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m ()
reportSDoc ArgName
"tc.term.lambda" Int
30 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"dontUseTargetType tel =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Telescope
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?
      Term -> TCM ()
checkSizeLtSat forall a b. (a -> b) -> a -> b
$ forall t a. Type'' t a -> a
unEl Type
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 :: TCM (Type, Term) -> TCM (Type, Term)
postponeOnBlockedPattern TCM (Type, Term)
m = TCM (Type, Term)
m forall a. TCM a -> ((TCErr, Blocker) -> TCM a) -> TCM a
`catchIlltypedPatternBlockedOnMeta` \(TCErr
err , Blocker
x) -> do
            forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m ()
reportSDoc ArgName
"tc.term" Int
50 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat forall a b. (a -> b) -> a -> b
$
              [ TCMT IO Doc
"checking record pattern stuck on meta: " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *). Applicative m => ArgName -> m Doc
text (forall a. Show a => a -> ArgName
show Blocker
x) ]
            Type
t1 <- forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext (NonEmpty (NamedArg Name)
xs, Type
argsT) forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a.
(MonadTCEnv m, HasOptions m, MonadDebug m) =>
m a -> m a
workOnTypes TCM Type
newTypeMeta_
            let e :: Expr
e    = ExprInfo -> LamBinding -> Expr -> Expr
A.Lam ExprInfo
A.exprNoRange (TypedBinding -> LamBinding
A.DomainFull TypedBinding
b) Expr
body
                tgt' :: Type
tgt' = Telescope -> Type -> Type
telePi Telescope
tel Type
t1
            Term
w <- TypeCheckingProblem -> Blocker -> TCM Term
postponeTypeCheckingProblem (Comparison -> Expr -> Type -> TypeCheckingProblem
CheckExpr Comparison
cmp Expr
e Type
tgt') Blocker
x
            forall (m :: * -> *) a. Monad m => a -> m a
return (Type
tgt' , Term
w)

      -- Now check body : ?t₁
      -- DONT USE tel for addContext, as it loses NameIds.
      -- WRONG: v <- addContext tel $ checkExpr body t1
      (Type
target0 , Term
w) <- TCM (Type, Term) -> TCM (Type, Term)
postponeOnBlockedPattern forall a b. (a -> b) -> a -> b
$
         forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext (NonEmpty (NamedArg Name)
xs, Type
argsT) forall a b. (a -> b) -> a -> b
$ forall a. List1 (NamedArg (Binder' BindName)) -> TCM a -> TCM a
addTypedPatterns List1 (NamedArg (Binder' BindName))
xps forall a b. (a -> b) -> a -> b
$ do
           Type
t1 <- forall (m :: * -> *) a.
(MonadTCEnv m, HasOptions m, MonadDebug m) =>
m a -> m a
workOnTypes TCM Type
newTypeMeta_
           Term
v  <- Comparison -> Expr -> Type -> TCM Term
checkExpr' Comparison
cmp Expr
body Type
t1
           forall (m :: * -> *) a. Monad m => a -> m a
return (Telescope -> Type -> Type
telePi Telescope
tel Type
t1 , Telescope -> Term -> Term
teleLam Telescope
tel Term
v)

      -- Do not coerce hidden lambdas
      if forall a. LensHiding a => a -> Bool
notVisible ArgInfo
info Bool -> Bool -> Bool
|| forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any forall a. LensHiding a => a -> Bool
notVisible NonEmpty (NamedArg Name)
xs then do
        ProblemId
pid <- forall (m :: * -> *) a.
(MonadFresh ProblemId m, MonadConstraint m) =>
m a -> m ProblemId
newProblem_ forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). MonadConversion m => Type -> Type -> m ()
leqType Type
target0 Type
target
        forall (m :: * -> *).
(MonadMetaSolver m, MonadFresh Int m) =>
Type -> Term -> ProblemId -> m Term
blockTermOnProblem Type
target Term
w ProblemId
pid
      else do
        forall (m :: * -> *).
(MonadConversion m, MonadTCM m) =>
Comparison -> Term -> Type -> Type -> m Term
coerce Comparison
cmp Term
w Type
target0 Type
target


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

        let (NamedArg Name
x :| []) = NonEmpty (NamedArg Name)
xs
        forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (forall a b. (LensHiding a, LensHiding b) => a -> b -> Bool
sameHiding Dom Type
dom ArgInfo
info) forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError forall a b. (a -> b) -> a -> b
$ Type -> TypeError
WrongHidingInLambda Type
target
        forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (forall a. Maybe a -> Bool
isJust forall a b. (a -> b) -> a -> b
$ forall a. LensNamed a => a -> Maybe (NameOf a)
getNameOf NamedArg Name
x) forall a b. (a -> b) -> a -> b
$
          -- Andreas, 2020-03-25, issue #4481: check for correct name
          forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (forall a b.
(LensNamed a, LensNamed b, NameOf a ~ WithOrigin (Ranged ArgName),
 NameOf b ~ WithOrigin (Ranged ArgName)) =>
a -> b -> Bool
namedSame Dom Type
dom NamedArg Name
x) forall a b. (a -> b) -> a -> b
$
            forall (m :: * -> *) x a.
(MonadTrace m, HasRange x) =>
x -> m a -> m a
setCurrentRange NamedArg Name
x forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError forall a b. (a -> b) -> a -> b
$ TypeError
WrongHidingInLHS
        -- Andreas, 2011-10-01 ignore relevance in lambda if not explicitly given
        ArgInfo
info <- forall dom.
(LensAnnotation dom, LensModality dom) =>
dom -> ArgInfo -> TCM ArgInfo
lambdaModalityCheck Dom Type
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 :: Type
a = forall t e. Dom' t e -> e
unDom Dom Type
dom
        Term -> TCM ()
checkSizeLtSat forall a b. (a -> b) -> a -> b
$ forall t a. Type'' t a -> a
unEl Type
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.
        (ProblemId
pid, Type
argT) <- forall (m :: * -> *) a.
(MonadFresh ProblemId m, MonadConstraint m) =>
m a -> m (ProblemId, a)
newProblem forall a b. (a -> b) -> a -> b
$ Expr -> Type -> TCM Type
isTypeEqualTo Expr
typ Type
a
        -- Andreas, Issue 630: take name from function type if lambda name is "_"
        Term
v <- forall a. Name -> ArgName -> Dom Type -> TCM a -> TCM a
lambdaAddContext (forall a. NamedArg a -> a
namedArg NamedArg Name
x) ArgName
y (forall a. ArgInfo -> a -> Dom a
defaultArgDom ArgInfo
info Type
argT) forall a b. (a -> b) -> a -> b
$
               forall a. List1 (NamedArg (Binder' BindName)) -> TCM a -> TCM a
addTypedPatterns List1 (NamedArg (Binder' BindName))
xps forall a b. (a -> b) -> a -> b
$ Comparison -> Expr -> Type -> TCM Term
checkExpr' Comparison
cmp Expr
body Type
btyp
        forall (m :: * -> *).
(MonadMetaSolver m, MonadFresh Int m) =>
Type -> Term -> ProblemId -> m Term
blockTermOnProblem Type
target (ArgInfo -> Abs Term -> Term
Lam ArgInfo
info forall a b. (a -> b) -> a -> b
$ forall a. ArgName -> a -> Abs a
Abs (NamedArg Name -> ArgName
namedArgName NamedArg Name
x) Term
v) ProblemId
pid

    useTargetType Telescope
_ Type
_ = forall a. HasCallStack => a
__IMPOSSIBLE__

-- | 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 = forall dom. LensAnnotation dom => dom -> ArgInfo -> TCM ArgInfo
lambdaAnnotationCheck (forall a. LensAnnotation a => a -> Annotation
getAnnotation dom
dom) forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< forall dom. LensCohesion dom => dom -> ArgInfo -> TCM ArgInfo
lambdaCohesionCheck Modality
m forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< forall dom. LensQuantity dom => dom -> ArgInfo -> TCM ArgInfo
lambdaQuantityCheck Modality
m forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< forall dom. LensRelevance dom => dom -> ArgInfo -> TCM ArgInfo
lambdaIrrelevanceCheck Modality
m
  where m :: Modality
m = 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
  | forall a. LensRelevance a => a -> Relevance
getRelevance ArgInfo
info forall a. Eq a => a -> a -> Bool
== Relevance
defaultRelevance = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. LensRelevance a => Relevance -> a -> a
setRelevance (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  = forall a. LensRelevance a => a -> Relevance
getRelevance dom
dom  -- relevance of function type
      let rLam :: Relevance
rLam = forall a. LensRelevance a => a -> Relevance
getRelevance ArgInfo
info -- relevance of lambda
      forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Relevance -> Relevance -> Bool
sameRelevance Relevance
rPi Relevance
rLam) forall a b. (a -> b) -> a -> b
$
        forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError TypeError
WrongIrrelevanceInLambda
      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
  | forall a. LensQuantity a => a -> Bool
noUserQuantity ArgInfo
info = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. LensQuantity a => Quantity -> a -> a
setQuantity (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  = forall a. LensQuantity a => a -> Quantity
getQuantity dom
dom  -- quantity of function type
      let qLam :: Quantity
qLam = forall a. LensQuantity a => a -> Quantity
getQuantity ArgInfo
info -- quantity of lambda
      forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Quantity
qPi Quantity -> Quantity -> Bool
`sameQuantity` Quantity
qLam) forall a b. (a -> b) -> a -> b
$ do
        forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError TypeError
WrongQuantityInLambda
      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
  | forall a. LensAnnotation a => a -> Annotation
getAnnotation ArgInfo
info forall a. Eq a => a -> a -> Bool
== Annotation
defaultAnnotation = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. LensAnnotation a => Annotation -> a -> a
setAnnotation (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  = forall a. LensAnnotation a => a -> Annotation
getAnnotation dom
dom  -- annotation of function type
      let aLam :: Annotation
aLam = forall a. LensAnnotation a => a -> Annotation
getAnnotation ArgInfo
info -- annotation of lambda
      forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Annotation
aPi forall a. Eq a => a -> a -> Bool
== Annotation
aLam) forall a b. (a -> b) -> a -> b
$ do
        forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError forall a b. (a -> b) -> a -> b
$ ArgName -> TypeError
GenericError forall a b. (a -> b) -> a -> b
$ ArgName
"Wrong annotation in lambda"
      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
  | forall a. LensCohesion a => a -> Cohesion
getCohesion ArgInfo
info forall a. Eq a => a -> a -> Bool
== Cohesion
defaultCohesion = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. LensCohesion a => Cohesion -> a -> a
setCohesion (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  = forall a. LensCohesion a => a -> Cohesion
getCohesion dom
dom  -- cohesion of function type
      let cLam :: Cohesion
cLam = forall a. LensCohesion a => a -> Cohesion
getCohesion ArgInfo
info -- cohesion of lambda
      forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Cohesion
cPi Cohesion -> Cohesion -> Bool
`sameCohesion` Cohesion
cLam) forall a b. (a -> b) -> a -> b
$ do
        -- if there is a cohesion annotation then
        -- it better match the domain.
        forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError TypeError
WrongCohesionInLambda
      forall (m :: * -> *) a. Monad m => a -> m a
return ArgInfo
info

-- Andreas, issue #630: take name from function type if lambda name is "_".
lambdaAddContext :: Name -> ArgName -> Dom Type -> TCM a -> TCM a
lambdaAddContext :: forall a. Name -> ArgName -> Dom Type -> TCM a -> TCM a
lambdaAddContext Name
x ArgName
y Dom Type
dom
  | forall a. IsNoName a => a -> Bool
isNoName Name
x = forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext (ArgName
y, Dom Type
dom)                 -- Note: String instance
  | Bool
otherwise  = forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext (Name
x, Dom Type
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)
-> Expr
-> Type
-> TCM Term
checkPostponedLambda Comparison
cmp args :: Arg (List1 (WithHiding Name), Maybe Type)
args@(Arg ArgInfo
info (WithHiding Hiding
h Name
x :| [WithHiding Name]
xs, Maybe Type
mt)) Expr
body Type
target = do
  let postpone :: Blocker -> Type -> TCM Term
postpone Blocker
_ Type
t = TypeCheckingProblem -> TCM Term
postponeTypeCheckingProblem_ forall a b. (a -> b) -> a -> b
$ Comparison
-> Arg (List1 (WithHiding Name), Maybe Type)
-> Expr
-> Type
-> TypeCheckingProblem
CheckLambda Comparison
cmp Arg (List1 (WithHiding Name), Maybe Type)
args Expr
body Type
t
      lamHiding :: Hiding
lamHiding = forall a. Monoid a => a -> a -> a
mappend Hiding
h forall a b. (a -> b) -> a -> b
$ forall a. LensHiding a => a -> Hiding
getHiding ArgInfo
info
  Hiding
-> Type
-> (Blocker -> Type -> TCM Term)
-> (Type -> TCM Term)
-> TCM Term
insertHiddenLambdas Hiding
lamHiding Type
target Blocker -> Type -> TCM Term
postpone forall a b. (a -> b) -> a -> b
$ \ t :: Type
t@(El Sort' Term
_ (Pi Dom Type
dom Abs Type
b)) -> do
    -- Andreas, 2011-10-01 ignore relevance in lambda if not explicitly given
    ArgInfo
info' <- forall a. LensHiding a => Hiding -> a -> a
setHiding Hiding
lamHiding forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall dom.
(LensAnnotation dom, LensModality dom) =>
dom -> ArgInfo -> TCM ArgInfo
lambdaModalityCheck Dom Type
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.
    Maybe ProblemId
mpid <- forall a b. Maybe a -> b -> (a -> b) -> b
caseMaybe Maybe Type
mt (forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing) forall a b. (a -> b) -> a -> b
$ \ Type
ascribedType -> forall a. a -> Maybe a
Just forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do
      forall (m :: * -> *) a.
(MonadFresh ProblemId m, MonadConstraint m) =>
m a -> m ProblemId
newProblem_ forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). MonadConversion m => Type -> Type -> m ()
leqType (forall t e. Dom' t e -> e
unDom Dom Type
dom) Type
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' :: Dom Type
dom' = forall a. LensRelevance a => Relevance -> a -> a
setRelevance (forall a. LensRelevance a => a -> Relevance
getRelevance ArgInfo
info') forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. LensHiding a => Hiding -> a -> a
setHiding Hiding
lamHiding forall a b. (a -> b) -> a -> b
$
          forall b a. b -> (a -> b) -> Maybe a -> b
maybe Dom Type
dom (Dom Type
dom forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$>) Maybe Type
mt
    Term
v <- forall a. Name -> ArgName -> Dom Type -> TCM a -> TCM a
lambdaAddContext Name
x (forall a. Abs a -> ArgName
absName Abs Type
b) Dom Type
dom'  forall a b. (a -> b) -> a -> b
$
      Comparison
-> Arg ([WithHiding Name], Maybe Type) -> Expr -> Type -> TCM Term
checkPostponedLambda0 Comparison
cmp (forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
info ([WithHiding Name]
xs, Maybe Type
mt)) Expr
body forall a b. (a -> b) -> a -> b
$ forall a. Subst a => Abs a -> a
absBody Abs Type
b
    let v' :: Term
v' = ArgInfo -> Abs Term -> Term
Lam ArgInfo
info' forall a b. (a -> b) -> a -> b
$ forall a. ArgName -> a -> Abs a
Abs (Name -> ArgName
nameToArgName Name
x) Term
v
    forall b a. b -> (a -> b) -> Maybe a -> b
maybe (forall (m :: * -> *) a. Monad m => a -> m a
return Term
v') (forall (m :: * -> *).
(MonadMetaSolver m, MonadFresh Int m) =>
Type -> Term -> ProblemId -> m Term
blockTermOnProblem Type
t Term
v') Maybe ProblemId
mpid

checkPostponedLambda0 :: Comparison -> Arg ([WithHiding Name], Maybe Type) -> A.Expr -> Type -> TCM Term
checkPostponedLambda0 :: Comparison
-> Arg ([WithHiding Name], Maybe Type) -> Expr -> Type -> TCM Term
checkPostponedLambda0 Comparison
cmp (Arg ArgInfo
_    ([]    , Maybe Type
_ )) Expr
body Type
target =
  Comparison -> Expr -> Type -> TCM Term
checkExpr' Comparison
cmp Expr
body Type
target
checkPostponedLambda0 Comparison
cmp (Arg ArgInfo
info (WithHiding Name
x : [WithHiding Name]
xs, Maybe Type
mt)) Expr
body Type
target =
  Comparison
-> Arg (List1 (WithHiding Name), Maybe Type)
-> Expr
-> Type
-> TCM Term
checkPostponedLambda Comparison
cmp (forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
info (WithHiding Name
x forall a. a -> [a] -> NonEmpty a
:| [WithHiding Name]
xs, Maybe Type
mt)) Expr
body Type
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
-> (Blocker -> Type -> TCM Term)
-> (Type -> TCM Term)
-> TCM Term
insertHiddenLambdas Hiding
h Type
target Blocker -> Type -> TCM Term
postpone Type -> TCM Term
ret = do
  -- If the target type is blocked, we postpone,
  -- because we do not know if a hidden lambda needs to be inserted.
  forall t (m :: * -> *) a.
(Reduce t, IsMeta t, MonadReduce m) =>
t -> (Blocker -> t -> m a) -> (NotBlocked -> t -> m a) -> m a
ifBlocked Type
target Blocker -> Type -> TCM Term
postpone forall a b. (a -> b) -> a -> b
$ \ NotBlocked
_ Type
t -> do
    case forall t a. Type'' t a -> a
unEl Type
t of

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

      Term
_ -> forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> TypeError
GenericDocError forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< do
        TCMT IO Doc
"Expected " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
target forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
" to be a function type"

-- | @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 -> TCM Term
checkAbsurdLambda Comparison
cmp ExprInfo
i Hiding
h Expr
e Type
t = forall (m :: * -> *) a.
MonadTCEnv m =>
(TCEnv -> TCEnv) -> m a -> m a
localTC (forall i o. Lens' i o -> LensSet i o
set Lens' Quantity TCEnv
eQuantity Quantity
topQuantity) forall a b. (a -> b) -> a -> b
$ do
      -- Andreas, 2019-10-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.
  Type
t <- forall a (m :: * -> *).
(InstantiateFull a, MonadReduce m) =>
a -> m a
instantiateFull Type
t
  forall t (m :: * -> *) a.
(Reduce t, IsMeta t, MonadReduce m) =>
t -> (Blocker -> t -> m a) -> (NotBlocked -> t -> m a) -> m a
ifBlocked Type
t (\ Blocker
blocker Type
t' -> TypeCheckingProblem -> Blocker -> TCM Term
postponeTypeCheckingProblem (Comparison -> Expr -> Type -> TypeCheckingProblem
CheckExpr Comparison
cmp Expr
e Type
t') Blocker
blocker) forall a b. (a -> b) -> a -> b
$ \ NotBlocked
_ Type
t' -> do
    case forall t a. Type'' t a -> a
unEl Type
t' of
      Pi dom :: Dom Type
dom@(Dom{domInfo :: forall t e. Dom' t e -> ArgInfo
domInfo = ArgInfo
info', unDom :: forall t e. Dom' t e -> e
unDom = Type
a}) Abs Type
b
        | Bool -> Bool
not (forall a b. (LensHiding a, LensHiding b) => a -> b -> Bool
sameHiding Hiding
h ArgInfo
info') -> forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError forall a b. (a -> b) -> a -> b
$ Type -> TypeError
WrongHidingInLambda Type
t'
        | Bool
otherwise -> forall (m :: * -> *).
(MonadMetaSolver m, MonadConstraint m, MonadFresh Int m,
 MonadFresh ProblemId m) =>
Type -> m Term -> m Term
blockTerm Type
t' forall a b. (a -> b) -> a -> b
$ do
          Range -> Type -> TCM ()
ensureEmptyType (forall a. HasRange a => a -> Range
getRange ExprInfo
i) Type
a
          -- Add helper function
          ModuleName
top <- forall (m :: * -> *). MonadTCEnv m => m ModuleName
currentModule
          QName
aux <- ModuleName -> Name -> QName
qualify ModuleName
top forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a (m :: * -> *).
(FreshName a, MonadFresh NameId m) =>
a -> m Name
freshName_ (forall a. HasRange a => a -> Range
getRange ExprInfo
i, ArgName
absurdLambdaName)
          -- if we are in irrelevant / erased position, the helper function
          -- is added as irrelevant / erased
          Modality
mod <- forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
asksTC forall a. LensModality a => a -> Modality
getModality
          forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m ()
reportSDoc ArgName
"tc.term.absurd" Int
10 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
            [ (TCMT IO Doc
"Adding absurd function" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Modality
mod) forall a. Semigroup a => a -> a -> a
<> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
aux
            , forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"of type" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
t'
            ]
          Language
lang <- forall (m :: * -> *). HasOptions m => m Language
getLanguage
          QName -> Definition -> TCM ()
addConstant QName
aux forall a b. (a -> b) -> a -> b
$
            (\ Defn
d -> (ArgInfo -> QName -> Type -> Language -> Defn -> Definition
defaultDefn (forall a. LensModality a => Modality -> a -> a
setModality Modality
mod ArgInfo
info') QName
aux Type
t' Language
lang Defn
d)
                    { defPolarity :: [Polarity]
defPolarity       = [Polarity
Nonvariant]
                    , defArgOccurrences :: [Occurrence]
defArgOccurrences = [Occurrence
Unused] })
            forall a b. (a -> b) -> a -> b
$ FunctionData -> Defn
FunctionDefn FunctionData
emptyFunctionData
              { _funClauses :: [Clause]
_funClauses        =
                  [ Clause
                    { clauseLHSRange :: Range
clauseLHSRange  = forall a. HasRange a => a -> Range
getRange Expr
e
                    , clauseFullRange :: Range
clauseFullRange = forall a. HasRange a => a -> Range
getRange Expr
e
                    , clauseTel :: Telescope
clauseTel       = ListTel -> Telescope
telFromList [forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (ArgName
absurdPatternName,) Dom Type
dom]
                    , namedClausePats :: NAPs
namedClausePats = [forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
info' forall a b. (a -> b) -> a -> b
$ forall name a. Maybe name -> a -> Named name a
Named (forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall a. Origin -> a -> WithOrigin a
WithOrigin Origin
Inserted forall a b. (a -> b) -> a -> b
$ forall a. a -> Ranged a
unranged forall a b. (a -> b) -> a -> b
$ forall a. Abs a -> ArgName
absName Abs Type
b) forall a b. (a -> b) -> a -> b
$ Int -> DeBruijnPattern
absurdP Int
0]
                    , clauseBody :: Maybe Term
clauseBody      = forall a. Maybe a
Nothing
                    , clauseType :: Maybe (Arg Type)
clauseType      = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall a. LensModality a => Modality -> a -> a
setModality Modality
mod forall a b. (a -> b) -> a -> b
$ forall e. e -> Arg e
defaultArg forall a b. (a -> b) -> a -> b
$ forall a. Subst a => Abs a -> a
absBody Abs Type
b
                    , clauseCatchall :: Bool
clauseCatchall    = Bool
True      -- absurd clauses are safe as catch-alls
                    , clauseExact :: Maybe Bool
clauseExact       = forall a. a -> Maybe a
Just Bool
False
                    , clauseRecursive :: Maybe Bool
clauseRecursive   = forall a. a -> Maybe a
Just Bool
False
                    , clauseUnreachable :: Maybe Bool
clauseUnreachable = forall a. a -> Maybe a
Just Bool
True -- absurd clauses are unreachable
                    , clauseEllipsis :: ExpandedEllipsis
clauseEllipsis    = ExpandedEllipsis
NoEllipsis
                    , clauseWhereModule :: Maybe ModuleName
clauseWhereModule = forall a. Maybe a
Nothing
                    }
                  ]
              , _funCompiled :: Maybe CompiledClauses
_funCompiled       = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall a. [Arg ArgName] -> CompiledClauses' a
Fail [forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
info' ArgName
"()"]
              , _funSplitTree :: Maybe SplitTree
_funSplitTree      = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall a. Int -> SplitTree' a
SplittingDone Int
0
              , _funMutual :: Maybe [QName]
_funMutual         = forall a. a -> Maybe a
Just []
              , _funTerminates :: Maybe Bool
_funTerminates     = forall a. a -> Maybe a
Just Bool
True
              , _funExtLam :: Maybe ExtLamInfo
_funExtLam         = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ ModuleName -> Bool -> Maybe System -> ExtLamInfo
ExtLamInfo ModuleName
top Bool
True forall a. Null a => a
empty
              }
          -- Andreas 2012-01-30: since aux is lifted to toplevel
          -- it needs to be applied to the current telescope (issue 557)
          QName -> Elims -> Term
Def QName
aux forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map forall a. Arg a -> Elim' a
Apply forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a t. DeBruijn a => Tele (Dom t) -> [Arg a]
teleArgs forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Telescope
getContextTelescope
      Term
_ -> forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError forall a b. (a -> b) -> a -> b
$ Type -> TypeError
ShouldBePi Type
t'

-- | @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
-> List1 Clause
-> Expr
-> Type
-> TCM Term
checkExtendedLambda Comparison
cmp ExprInfo
i DefInfo
di Erased
erased QName
qname List1 Clause
cs Expr
e Type
t = do
  Modality
mod <- forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
asksTC forall a. LensModality a => a -> Modality
getModality
  if Erased -> Bool
isErased Erased
erased Bool -> Bool -> Bool
&& Bool -> Bool
not (forall a. LensQuantity a => a -> Bool
hasQuantity0 Modality
mod) then
    forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
ArgName -> m a
genericError forall a b. (a -> b) -> a -> b
$ [ArgName] -> ArgName
unwords
      [ ArgName
"Erased pattern-matching lambdas may only be used in erased"
      , ArgName
"contexts"
      ]
   else forall (m :: * -> *) a.
MonadTCEnv m =>
(TCEnv -> TCEnv) -> m a -> m a
localTC (forall i o. Lens' i o -> LensSet i o
set Lens' Quantity TCEnv
eQuantity forall a b. (a -> b) -> a -> b
$ Erased -> Quantity
asQuantity Erased
erased) forall a b. (a -> b) -> a -> b
$ do
   -- 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
   DefaultToInfty -> TCM ()
solveSizeConstraints DefaultToInfty
DontDefaultToInfty
   ModuleName
lamMod <- forall a. TCM a -> TCM a
inFreshModuleIfFreeParams forall (m :: * -> *). MonadTCEnv m => m ModuleName
currentModule  -- #2883: need a fresh module if refined params
   Type
t <- forall a (m :: * -> *).
(InstantiateFull a, MonadReduce m) =>
a -> m a
instantiateFull Type
t
   forall t (m :: * -> *) a.
(Reduce t, IsMeta t, MonadReduce m) =>
t -> (Blocker -> t -> m a) -> (NotBlocked -> t -> m a) -> m a
ifBlocked Type
t (\ Blocker
m Type
t' -> TypeCheckingProblem -> TCM Term
postponeTypeCheckingProblem_ forall a b. (a -> b) -> a -> b
$ Comparison -> Expr -> Type -> TypeCheckingProblem
CheckExpr Comparison
cmp Expr
e Type
t') forall a b. (a -> b) -> a -> b
$ \ NotBlocked
_ Type
t -> do
     MutualId
j   <- TCM MutualId
currentOrFreshMutualBlock
     Modality
mod <- forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
asksTC forall a. LensModality a => a -> Modality
getModality
     let info :: ArgInfo
info = forall a. LensModality a => Modality -> a -> a
setModality Modality
mod ArgInfo
defaultArgInfo

     forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m ()
reportSDoc ArgName
"tc.term.exlam" Int
20 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
       [ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
hsep
         [ forall (m :: * -> *). Applicative m => ArgName -> m Doc
text forall a b. (a -> b) -> a -> b
$ forall a. Show a => a -> ArgName
show forall a b. (a -> b) -> a -> b
$ forall t. DefInfo' t -> IsAbstract
A.defAbstract DefInfo
di
         , TCMT IO Doc
"extended lambda's implementation"
         , forall (m :: * -> *). Functor m => m Doc -> m Doc
doubleQuotes forall a b. (a -> b) -> a -> b
$ forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
qname
         , TCMT IO Doc
"has type:"
         ]
       , forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
t -- <+> " where clauses: " <+> text (show cs)
       ]
     [Arg Term]
args     <- forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m [Arg Term]
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.
     forall {m :: * -> *} {a}. MonadTCEnv m => IsAbstract -> m a -> m a
abstract (forall t. DefInfo' t -> IsAbstract
A.defAbstract DefInfo
di) forall a b. (a -> b) -> a -> b
$ do
       -- Andreas, 2013-12-28: add extendedlambda as @Function@, not as @Axiom@;
       -- otherwise, @addClause@ in @checkFunDef'@ fails (see issue 1009).
       QName -> Definition -> TCM ()
addConstant QName
qname forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< do
         Language
lang <- forall (m :: * -> *). HasOptions m => m Language
getLanguage
         Definition -> TCMT IO Definition
useTerPragma forall a b. (a -> b) -> a -> b
$
           (ArgInfo -> QName -> Type -> Language -> Defn -> Definition
defaultDefn ArgInfo
info QName
qname Type
t Language
lang Defn
emptyFunction)
             { defMutual :: MutualId
defMutual = MutualId
j }
       Type
-> ArgInfo
-> Delayed
-> Maybe ExtLamInfo
-> Maybe QName
-> DefInfo
-> QName
-> [Clause]
-> TCM ()
checkFunDef' Type
t ArgInfo
info Delayed
NotDelayed (forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ ModuleName -> Bool -> Maybe System -> ExtLamInfo
ExtLamInfo ModuleName
lamMod Bool
False forall a. Null a => a
empty) forall a. Maybe a
Nothing DefInfo
di QName
qname forall a b. (a -> b) -> a -> b
$
         forall l. IsList l => l -> [Item l]
List1.toList List1 Clause
cs
       forall (m :: * -> *) a. Monad m => m (Maybe a) -> m () -> m ()
whenNothingM (forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
asksTC TCEnv -> Maybe MutualId
envMutualBlock) forall a b. (a -> b) -> a -> b
$
         -- Andrea 10-03-2018: Should other checks be performed here too? e.g. termination/positivity/..
         QName -> TCM ()
checkIApplyConfluence_ QName
qname
       forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ QName -> Elims -> Term
Def QName
qname forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall a. Arg a -> Elim' a
Apply [Arg Term]
args
  where
    -- Concrete definitions cannot use information about abstract things.
    abstract :: IsAbstract -> m a -> m a
abstract IsAbstract
ConcreteDef = forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
inConcreteMode
    abstract IsAbstract
AbstractDef = 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.
  TCState
st <- forall (m :: * -> *). MonadTCState m => m TCState
getTC

  TCM a
m forall e (m :: * -> *) a.
MonadError e m =>
m a -> (e -> m a) -> m a
`catchError` \ TCErr
err -> do

    let reraise :: MonadError TCErr m => m a
        reraise :: forall (m :: * -> *) a. MonadError TCErr m => m a
reraise = 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
blocker <- forall b a. b -> (a -> b) -> Maybe a -> b
maybe forall (m :: * -> *) a. MonadError TCErr m => m a
reraise forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ case TCErr
err of
      TypeError CallStack
_ TCState
s Closure TypeError
cl -> case 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
aClosure)           -> forall a. a -> Maybe a
Just Blocker
b
        CannotEliminateWithPattern Maybe Blocker
b NamedArg Pattern
p Type
a              -> Maybe Blocker
b
        -- Andrea: TODO look for blocking meta in tClosure and its Sort.
        -- SplitError (CannotCreateMissingClause _ _ _ tClosure) ->
        TypeError
_                                             -> forall a. Maybe a
Nothing
      TCErr
_ -> forall a. Maybe a
Nothing

    forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m ()
reportSDoc ArgName
"tc.postpone" Int
20 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat forall a b. (a -> b) -> a -> b
$
      [ TCMT IO Doc
"checking definition blocked on: " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Blocker
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!
    forall (m :: * -> *). MonadTCState m => TCState -> m ()
putTC TCState
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
blocker <- (forall (m :: * -> *).
Monad m =>
(MetaId -> m Blocker) -> Blocker -> m Blocker
`onBlockingMetasM` Blocker
blocker) forall a b. (a -> b) -> a -> b
$ \ MetaId
x ->
                forall (m :: * -> *).
ReadTCState m =>
MetaId -> m (Maybe (Either RemoteMetaVariable MetaVariable))
lookupMeta MetaId
x 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 -> 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{} -> forall (m :: * -> *) a. Monad m => a -> m a
return Blocker
alwaysUnblock
      Just (Right MetaVariable
m)
        | InstV{} <- MetaVariable -> MetaInstantiation
mvInstantiation MetaVariable
m -> forall (m :: * -> *) a. Monad m => a -> m a
return Blocker
alwaysUnblock
        | Bool
otherwise                    -> forall (m :: * -> *) a. Monad m => a -> m a
return 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
blocker forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Blocker
neverUnblock, Blocker
alwaysUnblock] then forall (m :: * -> *) a. MonadError TCErr m => m a
reraise else (TCErr, Blocker) -> TCM a
handle (TCErr
err, Blocker
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) = 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@.
  [Maybe (FieldAssignment' Expr)]
fs' <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM ([Name]
xs forall a. Eq a => [a] -> [a] -> [a]
List.\\ forall a b. (a -> b) -> [a] -> [b]
map (forall o (m :: * -> *) i. MonadReader o m => Lens' i o -> m i
view forall a. Lens' Name (FieldAssignment' a)
nameFieldA) Assigns
fs) forall a b. (a -> b) -> a -> b
$ \ Name
f -> do

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

    -- If we have several matching assignments, that's an error.
    case forall a. [Maybe a] -> [a]
catMaybes [Maybe (ModuleName, FieldAssignment' Expr)]
pms of
      []        -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing
      [(ModuleName
_, FieldAssignment' Expr
fa)] -> forall (m :: * -> *) a. Monad m => a -> m a
return (forall a. a -> Maybe a
Just FieldAssignment' Expr
fa)
      [(ModuleName, FieldAssignment' Expr)]
mfas      -> forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> TypeError
GenericDocError forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< do
        forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat forall a b. (a -> b) -> a -> b
$
          TCMT IO Doc
"Ambiguity: the field" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Name
f
            forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
"appears in the following modules: " forall a. a -> [a] -> [a]
: forall a b. (a -> b) -> [a] -> [b]
map (forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> a
fst) [(ModuleName, FieldAssignment' Expr)]
mfas
  forall (m :: * -> *) a. Monad m => a -> m a
return (Assigns
fs forall a. [a] -> [a] -> [a]
++ forall a. [Maybe a] -> [a]
catMaybes [Maybe (FieldAssignment' Expr)]
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.
  -> TCM Term         -- ^ Record value in internal syntax.
checkRecordExpression :: Comparison
-> [Either (FieldAssignment' Expr) ModuleName]
-> Expr
-> Type
-> TCM Term
checkRecordExpression Comparison
cmp [Either (FieldAssignment' Expr) ModuleName]
mfs Expr
e Type
t = do
  forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m ()
reportSDoc ArgName
"tc.term.rec" Int
10 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep
    [ TCMT IO Doc
"checking record expression"
    , forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA Expr
e
    ]
  forall t (m :: * -> *) a.
(Reduce t, IsMeta t, MonadReduce m) =>
t -> (Blocker -> t -> m a) -> (NotBlocked -> t -> m a) -> m a
ifBlocked Type
t (\ Blocker
_ Type
t -> Type -> TCM Term
guessRecordType Type
t) {-else-} forall a b. (a -> b) -> a -> b
$ \ NotBlocked
_ Type
t -> do
  case forall t a. Type'' t a -> a
unEl Type
t of
    -- Case: We know the type of the record already.
    Def QName
r Elims
es  -> do
      let ~(Just [Arg Term]
vs) = forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims Elims
es
      forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m ()
reportSDoc ArgName
"tc.term.rec" Int
20 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). Applicative m => ArgName -> m Doc
text forall a b. (a -> b) -> a -> b
$ ArgName
"  r   = " forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> ArgName
prettyShow QName
r

      forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m ()
reportSDoc ArgName
"tc.term.rec" Int
30 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"  xs  = " forall a. Semigroup a => a -> a -> a
<> do
        forall (m :: * -> *). Applicative m => ArgName -> m Doc
text forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall a. Pretty a => a -> ArgName
prettyShow forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map forall t e. Dom' t e -> e
unDom forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *).
(HasConstInfo m, ReadTCState m, MonadError TCErr m) =>
QName -> m [Dom' Term Name]
getRecordFieldNames QName
r
      forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m ()
reportSDoc ArgName
"tc.term.rec" Int
30 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"  ftel= " forall a. Semigroup a => a -> a -> a
<> do
        forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< QName -> TCM Telescope
getRecordFieldTypes QName
r
      forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m ()
reportSDoc ArgName
"tc.term.rec" Int
30 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"  con = " forall a. Semigroup a => a -> a -> a
<> do
        forall (m :: * -> *). Applicative m => ArgName -> m Doc
text forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall a. Pretty a => a -> ArgName
prettyShow forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *).
(HasConstInfo m, ReadTCState m, MonadError TCErr m) =>
QName -> m ConHead
getRecordConstructor QName
r

      Defn
def <- forall (m :: * -> *).
(HasConstInfo m, ReadTCState m, MonadError TCErr m) =>
QName -> m Defn
getRecordDef QName
r
      let -- Field names (C.Name) with ArgInfo from record type definition.
          cxs :: [Arg Name]
cxs  = forall a b. (a -> b) -> [a] -> [b]
map forall t a. Dom' t a -> Arg a
argFromDom forall a b. (a -> b) -> a -> b
$ Defn -> [Dom' Term Name]
recordFieldNames Defn
def
          -- Just field names.
          xs :: [Name]
xs   = forall a b. (a -> b) -> [a] -> [b]
map forall e. Arg e -> e
unArg [Arg Name]
cxs
          -- Record constructor.
          con :: ConHead
con  = forall a. KillRange a => KillRangeT a
killRange forall a b. (a -> b) -> a -> b
$ Defn -> ConHead
recConHead Defn
def
      forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m ()
reportSDoc ArgName
"tc.term.rec" Int
20 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
        [ TCMT IO Doc
"  xs  = " forall a. Semigroup a => a -> a -> a
<> forall (m :: * -> *) a. Monad m => a -> m a
return (forall a. Pretty a => a -> Doc
P.pretty [Name]
xs)
        , TCMT IO Doc
"  ftel= " forall a. Semigroup a => a -> a -> a
<> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM (Defn -> Telescope
recTel Defn
def)
        , TCMT IO Doc
"  con = " forall a. Semigroup a => a -> a -> a
<> forall (m :: * -> *) a. Monad m => a -> m a
return (forall a. Pretty a => a -> Doc
P.pretty ConHead
con)
        ]

      -- Record expressions corresponding to erased record
      -- constructors can only be used in compile-time mode.
      Quantity
constructorQ <- forall a. LensQuantity a => a -> Quantity
getQuantity forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo (ConHead -> QName
conName ConHead
con)
      Quantity
currentQ     <- forall (m :: * -> *) a. MonadTCEnv m => Lens' a TCEnv -> m a
viewTC Lens' Quantity TCEnv
eQuantity
      forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Quantity
constructorQ Quantity -> Quantity -> Bool
`moreQuantity` Quantity
currentQ) forall a b. (a -> b) -> a -> b
$
        forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError forall a b. (a -> b) -> a -> b
$ ArgName -> TypeError
GenericError forall a b. (a -> b) -> a -> b
$
        ArgName
"A record expression corresponding to an erased record " forall a. [a] -> [a] -> [a]
++
        ArgName
"constructor must only be used in erased settings"

      -- 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.
      [Name] -> [QName] -> TCM ()
disambiguateRecordFields (forall a b. (a -> b) -> [a] -> [b]
map forall a. FieldAssignment' a -> Name
_nameFieldA forall a b. (a -> b) -> a -> b
$ forall a b. [Either a b] -> [a]
lefts [Either (FieldAssignment' Expr) ModuleName]
mfs) (forall a b. (a -> b) -> [a] -> [b]
map forall t e. Dom' t e -> e
unDom forall a b. (a -> b) -> a -> b
$ Defn -> [Dom QName]
recFields Defn
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.
      Assigns
fs <- [Either (FieldAssignment' Expr) ModuleName]
-> [Name] -> TCM Assigns
expandModuleAssigns [Either (FieldAssignment' Expr) ModuleName]
mfs (forall a b. (a -> b) -> [a] -> [b]
map forall e. Arg e -> e
unArg [Arg Name]
cxs)

      -- Compute a list of metas for the missing visible fields.
      ScopeInfo
scope <- forall (m :: * -> *). ReadTCState m => m ScopeInfo
getScope
      let re :: Range
re = forall a. HasRange a => a -> Range
getRange Expr
e
          meta :: Name -> Expr
meta Name
x = MetaInfo -> Expr
A.Underscore forall a b. (a -> b) -> a -> b
$ Range -> ScopeInfo -> Maybe MetaId -> ArgName -> MetaInfo
A.MetaInfo Range
re ScopeInfo
scope forall a. Maybe a
Nothing (forall a. Pretty a => a -> ArgName
prettyShow Name
x)
      -- In @es@ omitted explicit fields are replaced by underscores.
      -- Omitted implicit or instance fields
      -- are still left out and inserted later by checkArguments_.
      [NamedArg Expr]
es <- forall a.
HasRange a =>
QName
-> (Name -> a)
-> [FieldAssignment' a]
-> [Arg Name]
-> TCM [NamedArg a]
insertMissingFieldsWarn QName
r Name -> Expr
meta Assigns
fs [Arg Name]
cxs

      [Arg Term]
args <- Comparison
-> ExpandHidden
-> Range
-> [NamedArg Expr]
-> Telescope
-> TCM (Elims, Telescope)
checkArguments_ Comparison
cmp ExpandHidden
ExpandLast Range
re [NamedArg Expr]
es (Defn -> Telescope
recTel Defn
def forall t. Apply t => t -> [Arg Term] -> t
`apply` [Arg Term]
vs) forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
        (Elims
elims, Telescope
remainingTel) | forall a. Null a => a -> Bool
null Telescope
remainingTel
                              , Just [Arg Term]
args <- forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims Elims
elims -> forall (m :: * -> *) a. Monad m => a -> m a
return [Arg Term]
args
        (Elims, Telescope)
_ -> forall a. HasCallStack => a
__IMPOSSIBLE__
      -- Don't need to block here!
      forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m ()
reportSDoc ArgName
"tc.term.rec" Int
20 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). Applicative m => ArgName -> m Doc
text forall a b. (a -> b) -> a -> b
$ ArgName
"finished record expression"
      forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ ConHead -> ConInfo -> Elims -> Term
Con ConHead
con ConInfo
ConORec (forall a b. (a -> b) -> [a] -> [b]
map forall a. Arg a -> Elim' a
Apply [Arg Term]
args)
    Term
_ -> forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError forall a b. (a -> b) -> a -> b
$ Type -> TypeError
ShouldBeRecordType Type
t

  where
    -- Case: We don't know the type of the record.
    guessRecordType :: Type -> TCM Term
guessRecordType Type
t = do
      let fields :: [Name]
fields = [ Name
x | Left (FieldAssignment Name
x Expr
_) <- [Either (FieldAssignment' Expr) ModuleName]
mfs ]
      [QName]
rs <- [Name] -> TCM [QName]
findPossibleRecords [Name]
fields
      forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m ()
reportSDoc ArgName
"tc.term.rec" Int
30 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"Possible records for" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
t forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
"are" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<?> forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty [QName]
rs
      case [QName]
rs of
          -- If there are no records with the right fields we might as well fail right away.
        [] -> case [Name]
fields of
          []  -> forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
ArgName -> m a
genericError ArgName
"There are no records in scope"
          [Name
f] -> forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
ArgName -> m a
genericError forall a b. (a -> b) -> a -> b
$ ArgName
"There is no known record with the field " forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> ArgName
prettyShow Name
f
          [Name]
_   -> forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
ArgName -> m a
genericError forall a b. (a -> b) -> a -> b
$ ArgName
"There is no known record with the fields " forall a. [a] -> [a] -> [a]
++ [ArgName] -> ArgName
unwords (forall a b. (a -> b) -> [a] -> [b]
map forall a. Pretty a => a -> ArgName
prettyShow [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.
          Definition
def <- forall (m :: * -> *).
(Functor m, HasConstInfo m, HasOptions m, ReadTCState m,
 MonadTCEnv m, MonadDebug m) =>
Definition -> m Definition
instantiateDef forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
r
          [Arg Term]
ps  <- forall (m :: * -> *).
(Functor m, HasConstInfo m, HasOptions m, ReadTCState m,
 MonadTCEnv m, MonadDebug m) =>
QName -> m [Arg Term]
freeVarsToApply QName
r
          let rt :: Type
rt = Definition -> Type
defType Definition
def
          forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m ()
reportSDoc ArgName
"tc.term.rec" Int
30 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"Type of unique record" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
rt
          [Arg Term]
vs  <- forall (m :: * -> *). MonadMetaSolver m => Type -> m [Arg Term]
newArgsMeta Type
rt
          Type
target <- forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce forall a b. (a -> b) -> a -> b
$ Type -> [Arg Term] -> Type
piApply Type
rt [Arg Term]
vs
          Sort' Term
s  <- case forall t a. Type'' t a -> a
unEl Type
target of
                  Sort Sort' Term
s  -> forall (m :: * -> *) a. Monad m => a -> m a
return Sort' Term
s
                  Term
v       -> do
                    forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m ()
reportSDoc ArgName
"impossible" Int
10 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
                      [ TCMT IO Doc
"The impossible happened when checking record expression against meta"
                      , TCMT IO Doc
"Candidate record type r = " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
r
                      , TCMT IO Doc
"Type of r               = " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
rt
                      , TCMT IO Doc
"Ends in (should be sort)= " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
v
                      , forall (m :: * -> *). Applicative m => ArgName -> m Doc
text forall a b. (a -> b) -> a -> b
$ ArgName
"  Raw                   =  " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> ArgName
show Term
v
                      ]
                    forall a. HasCallStack => a
__IMPOSSIBLE__
          let inferred :: Type
inferred = forall t a. Sort' t -> a -> Type'' t a
El Sort' Term
s forall a b. (a -> b) -> a -> b
$ QName -> Elims -> Term
Def QName
r forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall a. Arg a -> Elim' a
Apply ([Arg Term]
ps forall a. [a] -> [a] -> [a]
++ [Arg Term]
vs)
          Term
v <- Expr -> Type -> TCM Term
checkExpr Expr
e Type
inferred
          forall (m :: * -> *).
(MonadConversion m, MonadTCM m) =>
Comparison -> Term -> Type -> Type -> m Term
coerce Comparison
cmp Term
v Type
inferred Type
t
          -- Andreas 2012-04-21: OLD CODE, WRONG DIRECTION, I GUESS:
          -- blockTerm t $ v <$ leqType_ t inferred

          -- If there are more than one possible record we postpone
        QName
_:QName
_:[QName]
_ -> do
          forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m ()
reportSDoc ArgName
"tc.term.expr.rec" Int
10 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep
            [ TCMT IO Doc
"Postponing type checking of"
            , forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA Expr
e forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
":" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
t
            ]
          TypeCheckingProblem -> TCM Term
postponeTypeCheckingProblem_ forall a b. (a -> b) -> a -> b
$ Comparison -> Expr -> Type -> TypeCheckingProblem
CheckExpr Comparison
cmp Expr
e Type
t

-- | @checkRecordUpdate cmp ei recexpr fs e t@
--
-- Preconditions: @e = RecUpdate ei recexpr fs@ and @t@ is reduced.
--
checkRecordUpdate
  :: Comparison   -- ^ @cmp@
  -> 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
-> ExprInfo -> Expr -> Assigns -> Expr -> Type -> TCM Term
checkRecordUpdate Comparison
cmp ExprInfo
ei Expr
recexpr Assigns
fs Expr
eupd Type
t = do
  forall t (m :: * -> *) a.
(Reduce t, IsMeta t, MonadReduce m) =>
t -> (Blocker -> t -> m a) -> (NotBlocked -> t -> m a) -> m a
ifBlocked Type
t (\ Blocker
_ Type
_ -> TCM Term
tryInfer) forall a b. (a -> b) -> a -> b
$ {-else-} \ NotBlocked
_ Type
t' -> do
    forall (m :: * -> *) a b.
Monad m =>
m (Maybe a) -> m b -> (a -> m b) -> m b
caseMaybeM (forall (m :: * -> *).
PureTCM m =>
Type -> m (Maybe (QName, [Arg Term], Defn))
isRecordType Type
t') TCM Term
should forall a b. (a -> b) -> a -> b
$ \ (QName
r, [Arg Term]
_pars, Defn
defn) -> do
      -- Bind the record value (before update) to a fresh @name@.
      Term
v <- Comparison -> Expr -> Type -> TCM Term
checkExpr' Comparison
cmp Expr
recexpr Type
t'
      Name
name <- forall (m :: * -> *). MonadFresh NameId m => Range -> m Name
freshNoName forall a b. (a -> b) -> a -> b
$ forall a. HasRange a => a -> Range
getRange Expr
recexpr
      forall (m :: * -> *) a.
MonadAddContext m =>
ArgInfo -> Name -> Term -> Type -> m a -> m a
addLetBinding ArgInfo
defaultArgInfo Name
name Term
v Type
t' forall a b. (a -> b) -> a -> b
$ do

        let projs :: [Arg QName]
projs = forall a b. (a -> b) -> [a] -> [b]
map forall t a. Dom' t a -> Arg a
argFromDom forall a b. (a -> b) -> a -> b
$ Defn -> [Dom QName]
recFields Defn
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.
        [Name] -> [QName] -> TCM ()
disambiguateRecordFields (forall a b. (a -> b) -> [a] -> [b]
map forall a. FieldAssignment' a -> Name
_nameFieldA Assigns
fs) (forall a b. (a -> b) -> [a] -> [b]
map forall e. Arg e -> e
unArg [Arg QName]
projs)

        -- Desugar record update expression into record expression.
        let fs' :: [(Name, Maybe Expr)]
fs' = forall a b. (a -> b) -> [a] -> [b]
map (\ (FieldAssignment Name
x Expr
e) -> (Name
x, forall a. a -> Maybe a
Just Expr
e)) Assigns
fs
        [Arg Name]
axs <- forall a b. (a -> b) -> [a] -> [b]
map forall t a. Dom' t a -> Arg a
argFromDom forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *).
(HasConstInfo m, ReadTCState m, MonadError TCErr m) =>
QName -> m [Dom' Term Name]
getRecordFieldNames QName
r
        [Maybe Expr]
es  <- forall a.
HasRange a =>
QName -> (Arg Name -> a) -> [Arg Name] -> [(Name, a)] -> TCM [a]
orderFieldsWarn QName
r (forall a b. a -> b -> a
const forall a. Maybe a
Nothing) [Arg Name]
axs [(Name, Maybe Expr)]
fs'
        let es' :: [Maybe Expr]
es'  = 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 :: Expr
erec = ExprInfo -> [Either (FieldAssignment' Expr) ModuleName] -> Expr
A.Rec ExprInfo
ei [ forall a b. a -> Either a b
Left (forall a. Name -> a -> FieldAssignment' a
FieldAssignment Name
x Expr
e) | (Arg ArgInfo
_ Name
x, Just Expr
e) <- forall a b. [a] -> [b] -> [(a, b)]
zip [Arg Name]
axs [Maybe Expr]
es' ]
        -- Call the type checker on the desugared syntax.
        Comparison -> Expr -> Type -> TCM Term
checkExpr' Comparison
cmp Expr
erec Type
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 | forall a. LensHiding a => a -> Bool
visible ArgInfo
ai = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$
      -- omitted visible fields remain unchanged: @{ ...; p = p name; ...}@
      -- (hidden fields are supposed to be inferred)
      AppInfo -> Expr -> NamedArg Expr -> Expr
A.App
        (Range -> AppInfo
A.defaultAppInfo forall a b. (a -> b) -> a -> b
$ forall a. HasRange a => a -> Range
getRange ExprInfo
ei)
        (ProjOrigin -> AmbiguousQName -> Expr
A.Proj ProjOrigin
ProjSystem forall a b. (a -> b) -> a -> b
$ QName -> AmbiguousQName
unambiguous QName
p)
        (forall a. a -> NamedArg a
defaultNamedArg 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 :: TCM Term
tryInfer = do
      (Term
_, Type
trec) <- Expr -> TCM (Term, Type)
inferExpr Expr
recexpr
      forall t (m :: * -> *) a.
(Reduce t, IsMeta t, MonadReduce m) =>
t -> (Blocker -> t -> m a) -> (NotBlocked -> t -> m a) -> m a
ifBlocked Type
trec (\ Blocker
_ Type
_ -> TCM Term
postpone) forall a b. (a -> b) -> a -> b
$ {-else-} \ NotBlocked
_ Type
_ -> do
        Term
v <- Comparison -> Expr -> Type -> TCM Term
checkExpr' Comparison
cmp Expr
eupd Type
trec
        forall (m :: * -> *).
(MonadConversion m, MonadTCM m) =>
Comparison -> Term -> Type -> Type -> m Term
coerce Comparison
cmp Term
v Type
trec Type
t

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

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

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

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

-- | 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 forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Expr -> TCM Expr
scopedExpr Expr
e
scopedExpr Expr
e                      = forall (m :: * -> *) a. Monad m => a -> m a
return Expr
e

-- | Type check an expression.
checkExpr :: A.Expr -> Type -> TCM Term
checkExpr :: Expr -> Type -> TCM Term
checkExpr = Comparison -> Expr -> Type -> TCM 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 -> TCM Term
checkExpr' Comparison
cmp Expr
e Type
t =
  forall (m :: * -> *) a.
MonadDebug m =>
ArgName -> Int -> ArgName -> m a -> m a
verboseBracket ArgName
"tc.term.expr.top" Int
5 ArgName
"checkExpr" forall a b. (a -> b) -> a -> b
$
  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 -> forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
                                              [ TCMT IO Doc
"checkExpr" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<?> forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep [ forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Expr
e, TCMT IO Doc
":", forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
t ]
                                              , TCMT IO Doc
"  returns" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<?> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
v ]) forall a b. (a -> b) -> a -> b
$
  forall (m :: * -> *) a. MonadTrace m => Call -> m a -> m a
traceCall (Comparison -> Expr -> Type -> Call
CheckExprCall Comparison
cmp Expr
e Type
t) forall a b. (a -> b) -> a -> b
$ forall a. TCM a -> TCM a
localScope forall a b. (a -> b) -> a -> b
$ forall a. TCM a -> TCM a
doExpandLast forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). PureTCM m => Term -> m Term
unfoldInlined forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< do
    forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m ()
reportSDoc ArgName
"tc.term.expr.top" Int
15 forall a b. (a -> b) -> a -> b
$
        TCMT IO Doc
"Checking" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep
          [ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep [ forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Expr
e, TCMT IO Doc
":", forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
t ]
          , forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"at " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> (forall (m :: * -> *). Applicative m => ArgName -> m Doc
text forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Pretty a => a -> ArgName
prettyShow forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (m :: * -> *). MonadTCEnv m => m Range
getCurrentRange)
          ]
    forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m ()
reportSDoc ArgName
"tc.term.expr.top.detailed" Int
80 forall a b. (a -> b) -> a -> b
$
      TCMT IO Doc
"Checking" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep [ forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Expr
e, TCMT IO Doc
":", forall (m :: * -> *). Applicative m => ArgName -> m Doc
text (forall a. Show a => a -> ArgName
show Type
t) ]
    Type
tReduced <- forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce Type
t
    forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m ()
reportSDoc ArgName
"tc.term.expr.top" Int
15 forall a b. (a -> b) -> a -> b
$
        TCMT IO Doc
"    --> " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
tReduced

    Expr
e <- Expr -> TCM Expr
scopedExpr Expr
e

    TCM Term -> TCM Term
irrelevantIfProp <- (forall (m :: * -> *) a.
Monad m =>
BlockT m a -> m (Either Blocker a)
runBlocked forall a b. (a -> b) -> a -> b
$ forall a (m :: * -> *).
(LensSort a, PrettyTCM a, PureTCM m, MonadBlock m) =>
a -> m Bool
isPropM Type
t) forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
      Right Bool
True  -> do
        let mod :: Modality
mod = Modality
defaultModality { modRelevance :: Relevance
modRelevance = Relevance
Irrelevant }
        forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Term -> Term
dontCare forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (tcm :: * -> *) m a.
(MonadTCEnv tcm, LensModality m) =>
m -> tcm a -> tcm a
applyModalityToContext Modality
mod
      Either Blocker Bool
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a. a -> a
id

    TCM Term -> TCM Term
irrelevantIfProp forall a b. (a -> b) -> a -> b
$ Expr -> Type -> TCM Term -> TCM Term
tryInsertHiddenLambda Expr
e Type
tReduced forall a b. (a -> b) -> a -> b
$ case Expr
e of

        A.ScopedExpr ScopeInfo
scope Expr
e -> 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 -> TCM (MetaId, Term))
-> Comparison -> Type -> MetaInfo -> InteractionId -> TCM Term
checkQuestionMark (forall (m :: * -> *).
MonadMetaSolver m =>
RunMetaOccursCheck -> Comparison -> Type -> m (MetaId, Term)
newValueMeta' RunMetaOccursCheck
RunMetaOccursCheck) Comparison
cmp Type
t MetaInfo
i InteractionId
ii
        A.Underscore MetaInfo
i -> Comparison -> Type -> MetaInfo -> TCM Term
checkUnderscore Comparison
cmp Type
t MetaInfo
i

        A.WithApp ExprInfo
_ Expr
e [Expr]
es -> forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError 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, forall a. LensHiding a => a -> Bool
visible ArgInfo
ai -> do
          QName
x <- forall (m :: * -> *).
(MonadTCError m, MonadAbsToCon m) =>
Expr -> m QName
quotedName forall a b. (a -> b) -> a -> b
$ forall name a. Named name a -> a
namedThing Named_ Expr
e
          Type
ty <- TCM Type
qNameType
          forall (m :: * -> *).
(MonadConversion m, MonadTCM m) =>
Comparison -> Term -> Type -> Type -> m Term
coerce Comparison
cmp (QName -> Term
quoteName QName
x) Type
ty Type
t

          | A.QuoteTerm ExprInfo
_ <- Expr -> Expr
unScope Expr
q -> do
             (Term
et, Type
_) <- Expr -> TCM (Term, Type)
inferExpr (forall name a. Named name a -> a
namedThing Named_ Expr
e)
             Comparison -> Term -> Type -> TCM Term
doQuoteTerm Comparison
cmp Term
et Type
t

        A.Quote{}     -> forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
ArgName -> m a
genericError ArgName
"quote must be applied to a defined name"
        A.QuoteTerm{} -> forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
ArgName -> m a
genericError ArgName
"quoteTerm must be applied to a term"
        A.Unquote{}   -> forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
ArgName -> m a
genericError ArgName
"unquote must be applied to a term"

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

        A.ExtendedLam ExprInfo
i DefInfo
di Erased
erased QName
qname List1 Clause
cs ->
          Comparison
-> ExprInfo
-> DefInfo
-> Erased
-> QName
-> List1 Clause
-> Expr
-> Type
-> TCM Term
checkExtendedLambda Comparison
cmp ExprInfo
i DefInfo
di Erased
erased QName
qname List1 Clause
cs Expr
e Type
t

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

        A.Lam ExprInfo
i (A.DomainFree Maybe Expr
_ NamedArg (Binder' BindName)
x) Expr
e0
          | forall a. Maybe a -> Bool
isNothing (forall name a. Named name a -> Maybe name
nameOf forall a b. (a -> b) -> a -> b
$ forall e. Arg e -> e
unArg NamedArg (Binder' BindName)
x) Bool -> Bool -> Bool
&& forall a. Maybe a -> Bool
isNothing (forall a. Binder' a -> Maybe Pattern
A.binderPattern forall a b. (a -> b) -> a -> b
$ forall a. NamedArg a -> a
namedArg NamedArg (Binder' BindName)
x) ->
              Comparison -> Expr -> Type -> TCM Term
checkExpr' Comparison
cmp (ExprInfo -> LamBinding -> Expr -> Expr
A.Lam ExprInfo
i (ArgInfo -> Binder' Name -> LamBinding
domainFree (forall a. LensArgInfo a => a -> ArgInfo
getArgInfo NamedArg (Binder' BindName)
x) forall a b. (a -> b) -> a -> b
$ BindName -> Name
A.unBind forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. NamedArg a -> a
namedArg NamedArg (Binder' BindName)
x) Expr
e0) Type
t
          | Bool
otherwise -> forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError forall a b. (a -> b) -> a -> b
$ ArgName -> TypeError
NotImplemented ArgName
"named arguments in lambdas"

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

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

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

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

        A.RecUpdate ExprInfo
ei Expr
recexpr Assigns
fs -> Comparison
-> ExprInfo -> Expr -> Assigns -> Expr -> Type -> TCM Term
checkRecordUpdate Comparison
cmp ExprInfo
ei Expr
recexpr Assigns
fs Expr
e Type
t

        A.DontCare Expr
e -> -- resurrect vars
          forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM ((Relevance
Irrelevant forall a. Eq a => a -> a -> Bool
==) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
asksTC forall a. LensRelevance a => a -> Relevance
getRelevance)
            (Term -> Term
dontCare forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do forall (tcm :: * -> *) r a.
(MonadTCEnv tcm, LensRelevance r) =>
r -> tcm a -> tcm a
applyRelevanceToContext Relevance
Irrelevant forall a b. (a -> b) -> a -> b
$ Comparison -> Expr -> Type -> TCM Term
checkExpr' Comparison
cmp Expr
e Type
t)
            (forall (tcm :: * -> *) a.
(HasCallStack, MonadTCM tcm) =>
ArgName -> tcm a
internalError ArgName
"DontCare may only appear in irrelevant contexts")

        A.Dot{} -> forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
ArgName -> m a
genericError ArgName
"Invalid dotted expression"

        -- Application
        Expr
_   | Application Expr
hd [NamedArg Expr]
args <- Expr -> AppView' Expr
appView Expr
e -> Comparison -> Expr -> [NamedArg Expr] -> Expr -> Type -> TCM Term
checkApplication Comparison
cmp Expr
hd [NamedArg Expr]
args Expr
e Type
t

      forall a. TCM a -> ((TCErr, Blocker) -> TCM a) -> TCM a
`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).
        forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m ()
reportSDoc ArgName
"tc.term" Int
50 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat forall a b. (a -> b) -> a -> b
$
          [ TCMT IO Doc
"checking pattern got stuck on meta: " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Blocker
x ]
        TypeCheckingProblem -> Blocker -> TCM Term
postponeTypeCheckingProblem (Comparison -> Expr -> Type -> TypeCheckingProblem
CheckExpr Comparison
cmp Expr
e Type
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 -> TCM Term -> TCM Term
tryInsertHiddenLambda Expr
e Type
tReduced TCM 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{domInfo :: forall t e. Dom' t e -> ArgInfo
domInfo = ArgInfo
info, unDom :: forall t e. Dom' t e -> e
unDom = Type
a}) Abs Type
b <- forall t a. Type'' t a -> a
unEl Type
tReduced
        , let h :: Hiding
h = forall a. LensHiding a => a -> Hiding
getHiding ArgInfo
info
        , forall a. LensHiding a => a -> Bool
notVisible Hiding
h
        -- expression is not a matching hidden lambda or question mark
        , Bool -> Bool
not (forall {a}. LensHiding a => a -> Expr -> Bool
hiddenLambdaOrHole Hiding
h Expr
e)
        = do
      let proceed :: TCM Term
proceed = ArgInfo -> ArgName -> TCM Term
doInsert (forall a. LensOrigin a => Origin -> a -> a
setOrigin Origin
Inserted ArgInfo
info) forall a b. (a -> b) -> a -> b
$ forall a. Abs a -> ArgName
absName Abs Type
b
      ExpandHidden
expandHidden <- forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
asksTC TCEnv -> ExpandHidden
envExpandLast
      -- If we skip the lambda insertion for an introduction,
      -- we will hit a dead end, so proceed no matter what.
      if Bool
definitelyIntroduction then TCM Term
proceed else
        -- #3019 and #4170: don't insert implicit lambdas in arguments to existing metas
        if ExpandHidden
expandHidden forall a. Eq a => a -> a -> Bool
== ExpandHidden
ReallyDontExpandLast then TCM Term
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.
        forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce Type
a forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall a (m :: * -> *).
(IsSizeType a, HasOptions m, HasBuiltins m) =>
a -> m (Maybe BoundedSize)
isSizeType forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
          Just (BoundedLt Term
u) -> 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
_ -> TCM Term
fallback) forall a b. (a -> b) -> a -> b
$ \ NotBlocked
_ Term
v -> do
            forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM (Term -> TCMT IO Bool
checkSizeNeverZero Term
v) TCM Term
proceed TCM Term
fallback
            forall e (m :: * -> *) a.
MonadError e m =>
m a -> (e -> m a) -> m a
`catchError` \TCErr
_ -> TCM Term
fallback
          Maybe BoundedSize
_ -> TCM Term
proceed

    | Bool
otherwise = TCM Term
fallback

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

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

    hiddenLambdaOrHole :: a -> Expr -> Bool
hiddenLambdaOrHole a
h = \case
      A.AbsurdLam ExprInfo
_ Hiding
h'          -> forall a b. (LensHiding a, LensHiding b) => a -> b -> Bool
sameHiding a
h Hiding
h'
      A.ExtendedLam ExprInfo
_ DefInfo
_ Erased
_ QName
_ List1 Clause
cls -> forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any Clause -> Bool
hiddenLHS List1 Clause
cls
      A.Lam ExprInfo
_ LamBinding
bind Expr
_            -> 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
a : [NamedArg Pattern]
_))) [ProblemEq]
_ RHS
_ WhereDeclarations
_ Bool
_) = forall a. LensHiding a => a -> Bool
notVisible NamedArg Pattern
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{} -> forall a. HasCallStack => a
__IMPOSSIBLE__
      Expr
_ -> Bool
False

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

doQuoteTerm :: Comparison -> Term -> Type -> TCM Term
doQuoteTerm :: Comparison -> Term -> Type -> TCM Term
doQuoteTerm Comparison
cmp Term
et Type
t = do
  Term
et'       <- forall (m :: * -> *) a.
(MonadTCEnv m, HasConstInfo m, HasOptions m, TermLike a) =>
a -> m a
etaContract forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall a (m :: * -> *).
(InstantiateFull a, MonadReduce m) =>
a -> m a
instantiateFull Term
et
  case forall a. AllMetas a => a -> [MetaId]
allMetasList Term
et' of
    []  -> do
      Term
q  <- Term -> TCM Term
quoteTerm Term
et'
      Type
ty <- forall (m :: * -> *). Functor m => m Term -> m Type
el forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTerm
      forall (m :: * -> *).
(MonadConversion m, MonadTCM m) =>
Comparison -> Term -> Type -> Type -> m Term
coerce Comparison
cmp Term
q Type
ty Type
t
    [MetaId]
metas -> TypeCheckingProblem -> Blocker -> TCM Term
postponeTypeCheckingProblem (Comparison -> Term -> Type -> TypeCheckingProblem
DoQuoteTerm Comparison
cmp Term
et Type
t) forall a b. (a -> b) -> a -> b
$ Set MetaId -> Blocker
unblockOnAllMetas forall a b. (a -> b) -> a -> b
$ forall a. Ord a => [a] -> Set a
Set.fromList [MetaId]
metas

-- | Unquote a TCM computation in a given hole.
unquoteM :: A.Expr -> Term -> Type -> TCM ()
unquoteM :: Expr -> Term -> Type -> TCM ()
unquoteM Expr
tacA Term
hole Type
holeType = do
  Term
tac <- forall (tcm :: * -> *) q a.
(MonadTCEnv tcm, LensQuantity q) =>
q -> tcm a -> tcm a
applyQuantityToContext Quantity
zeroQuantity forall a b. (a -> b) -> a -> b
$
    Expr -> Type -> TCM Term
checkExpr Expr
tacA forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< (forall (m :: * -> *). Functor m => m Term -> m Type
el forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTerm forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> forall (m :: * -> *). Functor m => m Term -> m Type
el (forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTCM forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primLevelZero forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primUnit))
  forall a. TCM a -> TCM a
inFreshModuleIfFreeParams forall a b. (a -> b) -> a -> b
$ Term -> Term -> Type -> TCM ()
unquoteTactic Term
tac Term
hole Type
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 -> TCM ()
unquoteTactic Term
tac Term
hole Type
goal = do
  forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m ()
reportSDoc ArgName
"tc.term.tactic" Int
40 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep
    [ TCMT IO Doc
"Running tactic" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
tac
    , forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"on" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
hole forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
":" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
goal ]
  Either UnquoteError (Term, [QName])
ok  <- forall a. UnquoteM a -> TCM (Either UnquoteError (a, [QName]))
runUnquoteM forall a b. (a -> b) -> a -> b
$ Term -> Term -> UnquoteM Term
unquoteTCM Term
tac Term
hole
  case Either UnquoteError (Term, [QName])
ok of
    Left (BlockedOnMeta TCState
oldState Blocker
blocker) -> do
      forall (m :: * -> *). MonadTCState m => TCState -> m ()
putTC TCState
oldState
      let stripFreshMeta :: MetaId -> f Blocker
stripFreshMeta MetaId
x = forall b a. b -> (a -> b) -> Maybe a -> b
maybe Blocker
neverUnblock (forall a b. a -> b -> a
const forall a b. (a -> b) -> a -> b
$ MetaId -> Blocker
unblockOnMeta MetaId
x) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *).
ReadTCState m =>
MetaId -> m (Maybe MetaVariable)
lookupLocalMeta' MetaId
x
      Blocker
blocker' <- forall (m :: * -> *).
Monad m =>
(MetaId -> m Blocker) -> Blocker -> m Blocker
onBlockingMetasM forall {f :: * -> *}. ReadTCState f => MetaId -> f Blocker
stripFreshMeta Blocker
blocker
      Range
r <- case forall a. Set a -> [a]
Set.toList forall a b. (a -> b) -> a -> b
$ Blocker -> Set MetaId
allBlockingMetas Blocker
blocker' of
            MetaId
x : [MetaId]
_ -> forall a. HasRange a => a -> Range
getRange forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *).
ReadTCState m =>
MetaId -> m (Maybe MetaVariable)
lookupLocalMeta' MetaId
x
            []    -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Range' a
noRange
      forall (m :: * -> *) x a.
(MonadTrace m, HasRange x) =>
x -> m a -> m a
setCurrentRange Range
r forall a b. (a -> b) -> a -> b
$
        forall (m :: * -> *).
MonadConstraint m =>
Blocker -> Constraint -> m ()
addConstraint Blocker
blocker' (Term -> Term -> Type -> Constraint
UnquoteTactic Term
tac Term
hole Type
goal)
    Left UnquoteError
err -> forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError forall a b. (a -> b) -> a -> b
$ UnquoteError -> TypeError
UnquoteFailed UnquoteError
err
    Right (Term, [QName])
_ -> 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 -> TCM (MetaId, Term))
-> Comparison -> Type -> MetaInfo -> InteractionId -> TCM Term
checkQuestionMark Comparison -> Type -> TCM (MetaId, Term)
new Comparison
cmp Type
t0 MetaInfo
i InteractionId
ii = do
  forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m ()
reportSDoc ArgName
"tc.interaction" Int
20 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep
    [ TCMT IO Doc
"Found interaction point"
    , forall (m :: * -> *). Applicative m => ArgName -> m Doc
text forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => a -> ArgName
show forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
asksTC (forall o i. o -> Lens' i o -> i
^. forall a. LensIsAbstract a => Lens' IsAbstract a
lensIsAbstract)
    , forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty InteractionId
ii
    , TCMT IO Doc
":"
    , forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
t0
    ]
  forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m ()
reportSDoc ArgName
"tc.interaction" Int
60 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep
    [ TCMT IO Doc
"Raw:"
    , forall (m :: * -> *). Applicative m => ArgName -> m Doc
text (forall a. Show a => a -> ArgName
show Type
t0)
    ]
  (Comparison -> Type -> TCM (MetaId, Term))
-> Comparison -> Type -> MetaInfo -> TCM Term
checkMeta ((Comparison -> Type -> TCM (MetaId, Term))
-> InteractionId -> Comparison -> Type -> TCM (MetaId, Term)
newQuestionMark' Comparison -> Type -> TCM (MetaId, Term)
new InteractionId
ii) Comparison
cmp Type
t0 MetaInfo
i -- Andreas, 2013-05-22 use unreduced type t0!

-- | Check an underscore without arguments.
checkUnderscore :: Comparison -> Type -> A.MetaInfo -> TCM Term
checkUnderscore :: Comparison -> Type -> MetaInfo -> TCM Term
checkUnderscore = (Comparison -> Type -> TCM (MetaId, Term))
-> Comparison -> Type -> MetaInfo -> TCM Term
checkMeta (forall (m :: * -> *).
MonadMetaSolver m =>
RunMetaOccursCheck -> Comparison -> Type -> m (MetaId, Term)
newValueMeta RunMetaOccursCheck
RunMetaOccursCheck)

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

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

-- | 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
  :: (Comparison -> Type -> TCM (MetaId, Term))
  -> Maybe (Comparison , Type)
  -> A.MetaInfo
  -> TCM (Term, Type)
checkOrInferMeta :: (Comparison -> Type -> TCM (MetaId, Term))
-> Maybe (Comparison, Type) -> MetaInfo -> TCM (Term, Type)
checkOrInferMeta Comparison -> Type -> TCM (MetaId, Term)
newMeta Maybe (Comparison, Type)
mt MetaInfo
i = do
  case MetaInfo -> Maybe MetaId
A.metaNumber MetaInfo
i of
    Maybe MetaId
Nothing -> do
      ScopeInfo -> TCM ()
setScope (MetaInfo -> ScopeInfo
A.metaScope MetaInfo
i)
      (Comparison
cmp , Type
t) <- forall b a. b -> (a -> b) -> Maybe a -> b
maybe ((Comparison
CmpEq,) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *) a.
(MonadTCEnv m, HasOptions m, MonadDebug m) =>
m a -> m a
workOnTypes TCM Type
newTypeMeta_) forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (Comparison, Type)
mt
      (MetaId
x, Term
v) <- Comparison -> Type -> TCM (MetaId, Term)
newMeta Comparison
cmp Type
t
      forall (m :: * -> *).
MonadMetaSolver m =>
MetaId -> ArgName -> m ()
setMetaNameSuggestion MetaId
x (MetaInfo -> ArgName
A.metaNameSuggestion MetaInfo
i)
      forall (m :: * -> *) a. Monad m => a -> m a
return (Term
v, Type
t)
    -- Rechecking an existing metavariable
    Just MetaId
x -> do
      let v :: Term
v = MetaId -> Elims -> Term
MetaV MetaId
x []
      forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m ()
reportSDoc ArgName
"tc.meta.check" Int
20 forall a b. (a -> b) -> a -> b
$
        TCMT IO Doc
"checking existing meta " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
v
      Type
t' <- forall (m :: * -> *). ReadTCState m => MetaId -> m Type
metaType MetaId
x
      forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m ()
reportSDoc ArgName
"tc.meta.check" Int
20 forall a b. (a -> b) -> a -> b
$
        forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"of type " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
t'
      case Maybe (Comparison, Type)
mt of
        Maybe (Comparison, Type)
Nothing -> forall (m :: * -> *) a. Monad m => a -> m a
return (Term
v, Type
t')
        Just (Comparison
cmp , Type
t) -> (,Type
t) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *).
(MonadConversion m, MonadTCM m) =>
Comparison -> Term -> Type -> Type -> m Term
coerce Comparison
cmp Term
v Type
t' Type
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 forall a b. (a -> b) -> a -> b
$ Range
-> List1 (NamedArg (Binder' BindName)) -> Expr -> TypedBinding
A.mkTBind Range
r (forall el coll. Singleton el coll => el -> coll
singleton forall a b. (a -> b) -> a -> b
$ forall a. ArgInfo -> a -> NamedArg a
unnamedArg ArgInfo
info forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Name -> BindName
A.mkBindName Binder' Name
x)
               forall a b. (a -> b) -> a -> b
$ MetaInfo -> Expr
A.Underscore MetaInfo
underscoreInfo
  where
    r :: Range
r = forall a. HasRange a => a -> Range
getRange Binder' Name
x
    underscoreInfo :: MetaInfo
underscoreInfo = A.MetaInfo
      { metaRange :: Range
A.metaRange          = Range
r
      , metaScope :: ScopeInfo
A.metaScope          = ScopeInfo
emptyScopeInfo
      , metaNumber :: Maybe MetaId
A.metaNumber         = forall a. Maybe a
Nothing
      , metaNameSuggestion :: ArgName
A.metaNameSuggestion = forall a. Pretty a => a -> ArgName
prettyShow forall a b. (a -> b) -> a -> b
$ Name -> Name
A.nameConcrete forall a b. (a -> b) -> a -> b
$ forall a. Binder' a -> a
A.binderName Binder' Name
x
      }


-- | 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 :: [NamedArg Expr] -> [Arg Term] -> Type -> TCM ([Arg Term], Type)
checkKnownArguments []           [Arg Term]
vs Type
t = forall (m :: * -> *) a. Monad m => a -> m a
return ([Arg Term]
vs, Type
t)
checkKnownArguments (NamedArg Expr
arg : [NamedArg Expr]
args) [Arg Term]
vs Type
t = do
  ([Arg Term]
vs', Type
t') <- forall (m :: * -> *) x a.
(MonadTrace m, HasRange x) =>
x -> m a -> m a
setCurrentRange NamedArg Expr
arg forall a b. (a -> b) -> a -> b
$ NamedArg Expr -> [Arg Term] -> Type -> TCM ([Arg Term], Type)
checkKnownArgument NamedArg Expr
arg [Arg Term]
vs Type
t
  [NamedArg Expr] -> [Arg Term] -> Type -> TCM ([Arg Term], Type)
checkKnownArguments [NamedArg Expr]
args [Arg Term]
vs' Type
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 :: NamedArg Expr -> [Arg Term] -> Type -> TCM ([Arg Term], Type)
checkKnownArgument NamedArg Expr
arg [] Type
_ = forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
Doc -> m a
genericDocError forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< do
  TCMT IO Doc
"Invalid projection parameter " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA NamedArg 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 NamedArg Expr
arg (Arg ArgInfo
_ Term
v : [Arg Term]
vs) Type
t = do
  -- Skip the arguments from vs that do not correspond to e
  (dom :: Dom Type
dom@Dom{ unDom :: forall t e. Dom' t e -> e
unDom = Type
a }, Abs Type
b) <- forall (m :: * -> *).
MonadReduce m =>
Type -> m (Dom Type, Abs Type)
mustBePi Type
t
  if Bool -> Bool
not forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a -> a
fromMaybe forall a. HasCallStack => a
__IMPOSSIBLE__ forall a b. (a -> b) -> a -> b
$ forall arg dom.
(LensNamed arg, NameOf arg ~ WithOrigin (Ranged ArgName),
 LensHiding arg, LensNamed dom,
 NameOf dom ~ WithOrigin (Ranged ArgName), LensHiding dom) =>
arg -> dom -> Maybe Bool
fittingNamedArg NamedArg Expr
arg Dom Type
dom
    -- Continue with the next one
    then NamedArg Expr -> [Arg Term] -> Type -> TCM ([Arg Term], Type)
checkKnownArgument NamedArg Expr
arg [Arg Term]
vs (Abs Type
b forall a. Subst a => Abs a -> SubstArg a -> a
`absApp` Term
v)
    -- Found the right argument
    else do
      Term
u <- NamedArg Expr -> Type -> TCM Term
checkNamedArg NamedArg Expr
arg Type
a
      forall (m :: * -> *).
MonadConversion m =>
Type -> Term -> Term -> m ()
equalTerm Type
a Term
u Term
v
      forall (m :: * -> *) a. Monad m => a -> m a
return ([Arg Term]
vs, Abs Type
b forall a. Subst a => Abs a -> SubstArg a -> a
`absApp` Term
v)

-- | Check a single argument.

checkNamedArg :: NamedArg A.Expr -> Type -> TCM Term
checkNamedArg :: NamedArg Expr -> Type -> TCM Term
checkNamedArg arg :: NamedArg Expr
arg@(Arg ArgInfo
info Named_ Expr
e0) Type
t0 = do
  let e :: Expr
e = forall name a. Named name a -> a
namedThing Named_ Expr
e0
  let x :: ArgName
x = forall a.
(LensNamed a, NameOf a ~ WithOrigin (Ranged ArgName)) =>
ArgName -> a -> ArgName
bareNameWithDefault ArgName
"" Named_ Expr
e0
  forall (m :: * -> *) a. MonadTrace m => Call -> m a -> m a
traceCall (Comparison -> Expr -> Type -> Call
CheckExprCall Comparison
CmpLeq Expr
e Type
t0) forall a b. (a -> b) -> a -> b
$ do
    forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m ()
reportSDoc ArgName
"tc.term.args.named" Int
15 forall a b. (a -> b) -> a -> b
$ do
        TCMT IO Doc
"Checking named arg" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep
          [ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep [ forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM NamedArg Expr
arg, TCMT IO Doc
":", forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
t0 ]
          ]
    forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> ArgName -> m ()
reportSLn ArgName
"tc.term.args.named" Int
75 forall a b. (a -> b) -> a -> b
$ ArgName
"  arg = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> ArgName
show (forall a. ExprLike a => a -> a
deepUnscope NamedArg Expr
arg)
    -- Ulf, 2017-03-24: (#2172) Always treat explicit _ and ? as implicit
    -- argument (i.e. solve with unification).
    let checkU :: MetaInfo -> TCM Term
checkU = (Comparison -> Type -> TCM (MetaId, Term))
-> Comparison -> Type -> MetaInfo -> TCM Term
checkMeta (forall (m :: * -> *).
(PureTCM m, MonadMetaSolver m) =>
ArgInfo -> ArgName -> Comparison -> Type -> m (MetaId, Term)
newMetaArg (forall a. LensHiding a => Hiding -> a -> a
setHiding Hiding
Hidden ArgInfo
info) ArgName
x) Comparison
CmpLeq Type
t0
    let checkQ :: MetaInfo -> InteractionId -> TCM Term
checkQ = (Comparison -> Type -> TCM (MetaId, Term))
-> Comparison -> Type -> MetaInfo -> InteractionId -> TCM Term
checkQuestionMark (ArgInfo -> ArgName -> Comparison -> Type -> TCM (MetaId, Term)
newInteractionMetaArg (forall a. LensHiding a => Hiding -> a -> a
setHiding Hiding
Hidden ArgInfo
info) ArgName
x) Comparison
CmpLeq Type
t0
    if Bool -> Bool
not forall a b. (a -> b) -> a -> b
$ Expr -> Bool
isHole Expr
e then Expr -> Type -> TCM Term
checkExpr Expr
e Type
t0 else forall a. TCM a -> TCM a
localScope 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 forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
        A.Underscore MetaInfo
i ->  MetaInfo -> TCM Term
checkU MetaInfo
i
        A.QuestionMark MetaInfo
i InteractionId
ii -> MetaInfo -> InteractionId -> TCM Term
checkQ MetaInfo
i InteractionId
ii
        Expr
_ -> 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)
inferExpr = ExpandHidden -> Expr -> TCM (Term, Type)
inferExpr' ExpandHidden
DontExpandLast

inferExpr' :: ExpandHidden -> A.Expr -> TCM (Term, Type)
inferExpr' :: ExpandHidden -> Expr -> TCM (Term, Type)
inferExpr' ExpandHidden
exh Expr
e = forall (m :: * -> *) a. MonadTrace m => Call -> m a -> m a
traceCall (Expr -> Call
InferExpr Expr
e) forall a b. (a -> b) -> a -> b
$ do
  let Application Expr
hd [NamedArg Expr]
args = Expr -> AppView' Expr
appView Expr
e
  forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m ()
reportSDoc ArgName
"tc.infer" Int
30 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
    [ TCMT IO Doc
"inferExpr': appView of " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA Expr
e
    , TCMT IO Doc
"  hd   = " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA Expr
hd
    , TCMT IO Doc
"  args = " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a ce (m :: * -> *).
(ToConcrete a, ConOfAbs a ~ [ce], Pretty ce, MonadAbsToCon m) =>
a -> m Doc
prettyAs [NamedArg Expr]
args
    ]
  forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m ()
reportSDoc ArgName
"tc.infer" Int
60 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
    [ forall (m :: * -> *). Applicative m => ArgName -> m Doc
text forall a b. (a -> b) -> a -> b
$ ArgName
"  hd (raw) = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> ArgName
show Expr
hd
    ]
  ExpandHidden -> Expr -> [NamedArg Expr] -> Expr -> TCM (Term, Type)
inferApplication ExpandHidden
exh Expr
hd [NamedArg Expr]
args Expr
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 -> TCM Term
checkDontExpandLast Comparison
cmp Expr
e Type
t = case Expr
e of
  Expr
_ | Application Expr
hd [NamedArg Expr]
args <- Expr -> AppView' Expr
appView Expr
e,  Expr -> Bool
defOrVar Expr
hd ->
    forall (m :: * -> *) a. MonadTrace m => Call -> m a -> m a
traceCall (Comparison -> Expr -> Type -> Call
CheckExprCall Comparison
cmp Expr
e Type
t) forall a b. (a -> b) -> a -> b
$ forall a. TCM a -> TCM a
localScope forall a b. (a -> b) -> a -> b
$ forall a. TCM a -> TCM a
dontExpandLast forall a b. (a -> b) -> a -> b
$ do
      Comparison -> Expr -> [NamedArg Expr] -> Expr -> Type -> TCM Term
checkApplication Comparison
cmp Expr
hd [NamedArg Expr]
args Expr
e Type
t
  Expr
_ -> Comparison -> Expr -> Type -> TCM Term
checkExpr' Comparison
cmp Expr
e Type
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
  [Arg Term]
params <- forall (m :: * -> *).
(Functor m, Applicative m, HasOptions m, MonadTCEnv m,
 ReadTCState m, MonadDebug m) =>
ModuleName -> m [Arg Term]
moduleParamsToApply forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (m :: * -> *). MonadTCEnv m => m ModuleName
currentModule
  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any ((forall a. Eq a => a -> a -> Bool
== Int -> Elims -> Term
Var Int
i []) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall e. Arg e -> e
unArg) [Arg Term]
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)
inferExprForWith (Arg ArgInfo
info Expr
e) = forall (m :: * -> *) a.
MonadDebug m =>
ArgName -> Int -> ArgName -> m a -> m a
verboseBracket ArgName
"tc.with.infer" Int
20 ArgName
"inferExprForWith" forall a b. (a -> b) -> a -> b
$
  forall (tcm :: * -> *) r a.
(MonadTCEnv tcm, LensRelevance r) =>
r -> tcm a -> tcm a
applyRelevanceToContext (forall a. LensRelevance a => a -> Relevance
getRelevance ArgInfo
info) forall a b. (a -> b) -> a -> b
$ do
    forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m ()
reportSDoc ArgName
"tc.with.infer" Int
20 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"inferExprforWith " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Expr
e
    forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> ArgName -> m ()
reportSLn  ArgName
"tc.with.infer" Int
80 forall a b. (a -> b) -> a -> b
$ ArgName
"inferExprforWith " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> ArgName
show (forall a. ExprLike a => a -> a
deepUnscope Expr
e)
    forall (m :: * -> *) a. MonadTrace m => Call -> m a -> m a
traceCall (Expr -> Call
InferExpr Expr
e) forall a b. (a -> b) -> a -> b
$ do
      -- With wants type and term fully instantiated!
      (Term
v, Type
t) <- forall a (m :: * -> *).
(InstantiateFull a, MonadReduce m) =>
a -> m a
instantiateFull forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Expr -> TCM (Term, Type)
inferExpr Expr
e
      Term
v0 <- forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce Term
v
      -- Andreas 2014-11-06, issue 1342.
      -- Check that we do not `with` on a module parameter!
      case Term
v0 of
        Var Int
i [] -> forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
whenM (Int -> TCMT IO Bool
isModuleFreeVar Int
i) forall a b. (a -> b) -> a -> b
$ do
          forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m ()
reportSDoc ArgName
"tc.with.infer" Int
80 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
            [ forall (m :: * -> *). Applicative m => ArgName -> m Doc
text forall a b. (a -> b) -> a -> b
$ ArgName
"with expression is variable " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> ArgName
show Int
i
            , TCMT IO Doc
"current modules = " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> do forall (m :: * -> *). Applicative m => ArgName -> m Doc
text forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => a -> ArgName
show forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (m :: * -> *). MonadTCEnv m => m ModuleName
currentModule
            , TCMT IO Doc
"current module free vars = " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> do forall (m :: * -> *). Applicative m => ArgName -> m Doc
text forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => a -> ArgName
show forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< TCM Int
getCurrentModuleFreeVars
            , TCMT IO Doc
"context size = " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> do forall (m :: * -> *). Applicative m => ArgName -> m Doc
text forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => a -> ArgName
show forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Int
getContextSize
            , TCMT IO Doc
"current context = " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> do forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Telescope
getContextTelescope
            ]
          forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError forall a b. (a -> b) -> a -> b
$ Expr -> Term -> TypeError
WithOnFreeVariable Expr
e Term
v0
        Term
_        -> forall (m :: * -> *) a. Monad m => a -> m a
return ()
      -- Possibly insert hidden arguments.
      TelV Telescope
tel Type
t0 <- forall (m :: * -> *).
(MonadReduce m, MonadAddContext m) =>
Int -> (Dom Type -> Bool) -> Type -> m (TelV Type)
telViewUpTo' (-Int
1) (Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. LensHiding a => a -> Bool
visible) Type
t
      case forall t a. Type'' t a -> a
unEl Type
t0 of
        Def QName
d Elims
vs -> do
          Maybe DataOrRecord
res <- QName -> TCM (Maybe DataOrRecord)
isDataOrRecordType QName
d
          case Maybe DataOrRecord
res of
            Maybe DataOrRecord
Nothing -> forall (m :: * -> *) a. Monad m => a -> m a
return (Term
v, Type
t)
            Just{}  -> do
              ([Arg Term]
args, Type
t1) <- forall (m :: * -> *).
(PureTCM m, MonadMetaSolver m, MonadTCM m) =>
Int -> (Hiding -> Bool) -> Type -> m ([Arg Term], Type)
implicitArgs (-Int
1) forall a. LensHiding a => a -> Bool
notVisible Type
t
              forall (m :: * -> *) a. Monad m => a -> m a
return (Term
v forall t. Apply t => t -> [Arg Term] -> t
`apply` [Arg Term]
args, Type
t1)
        Term
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return (Term
v, Type
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 = forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (forall b c a. (b -> c) -> (a -> b) -> a -> c
(.) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. LetBinding -> TCM a -> TCM a
checkLetBinding) 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 =
  forall (m :: * -> *) a. MonadTrace m => Call -> m a -> m a
traceCall (LetBinding -> Call
CheckLetBinding LetBinding
b) forall a b. (a -> b) -> a -> b
$ do
    -- #4131: Only DontExpandLast if no user written type signature
    let check :: Comparison -> Expr -> Type -> TCM Term
check | forall a. LensOrigin a => a -> Origin
getOrigin ArgInfo
info forall a. Eq a => a -> a -> Bool
== Origin
Inserted = Comparison -> Expr -> Type -> TCM Term
checkDontExpandLast
              | Bool
otherwise                  = Comparison -> Expr -> Type -> TCM Term
checkExpr'
    Type
t <- forall (m :: * -> *) a.
(MonadTCEnv m, HasOptions m, MonadDebug m) =>
m a -> m a
workOnTypes forall a b. (a -> b) -> a -> b
$ Expr -> TCM Type
isType_ Expr
t
    Term
v <- forall (tcm :: * -> *) m a.
(MonadTCEnv tcm, LensModality m) =>
m -> tcm a -> tcm a
applyModalityToContext ArgInfo
info forall a b. (a -> b) -> a -> b
$ Comparison -> Expr -> Type -> TCM Term
check Comparison
CmpLeq Expr
e Type
t
    forall (m :: * -> *) a.
MonadAddContext m =>
ArgInfo -> Name -> Term -> Type -> m a -> m a
addLetBinding ArgInfo
info (BindName -> Name
A.unBind BindName
x) Term
v Type
t TCM a
ret

checkLetBinding b :: LetBinding
b@(A.LetPatBind LetInfo
i Pattern
p Expr
e) TCM a
ret =
  forall (m :: * -> *) a. MonadTrace m => Call -> m a -> m a
traceCall (LetBinding -> Call
CheckLetBinding LetBinding
b) forall a b. (a -> b) -> a -> b
$ do
    Pattern
p <- forall a. ExpandPatternSynonyms a => a -> TCM a
expandPatternSynonyms Pattern
p
    (Term
v, Type
t) <- ExpandHidden -> Expr -> TCM (Term, Type)
inferExpr' ExpandHidden
ExpandLast Expr
e
    let -- construct a type  t -> dummy  for use in checkLeftHandSide
        t0 :: Type
t0 = forall t a. Sort' t -> a -> Type'' t a
El (forall a. LensSort a => a -> Sort' Term
getSort Type
t) forall a b. (a -> b) -> a -> b
$ Dom Type -> Abs Type -> Term
Pi (forall a. a -> Dom a
defaultDom Type
t) (forall a. ArgName -> a -> Abs a
NoAbs forall a. Underscore a => a
underscore HasCallStack => Type
__DUMMY_TYPE__)
        p0 :: NamedArg Pattern
p0 = forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
defaultArgInfo (forall name a. Maybe name -> a -> Named name a
Named forall a. Maybe a
Nothing Pattern
p)
    forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m ()
reportSDoc ArgName
"tc.term.let.pattern" Int
10 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
      [ TCMT IO Doc
"let-binding pattern p at type t"
      , forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
        [ TCMT IO Doc
"p (A) =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA Pattern
p
        , TCMT IO Doc
"t     =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
t
        , TCMT IO Doc
"cxtRel=" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> do forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
asksTC forall a. LensRelevance a => a -> Relevance
getRelevance
        , TCMT IO Doc
"cxtQnt=" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> do forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
asksTC forall a. LensQuantity a => a -> Quantity
getQuantity
        ]
      ]
    Int
fvs <- forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Int
getContextSize
    forall a.
Call
-> Maybe QName
-> [NamedArg Pattern]
-> Type
-> Maybe Substitution
-> [ProblemEq]
-> (LHSResult -> TCM a)
-> TCM a
checkLeftHandSide (Pattern -> Telescope -> Type -> Call
CheckPattern Pattern
p forall a. Tele a
EmptyTel Type
t) forall a. Maybe a
Nothing [NamedArg Pattern
p0] Type
t0 forall a. Maybe a
Nothing [] forall a b. (a -> b) -> a -> b
$ \ (LHSResult Int
_ Telescope
delta0 NAPs
ps Bool
_ Arg Type
_t Substitution
_ [AsBinding]
asb IntSet
_ Bool
_) -> forall a. [AsBinding] -> TCM a -> TCM a
bindAsPatterns [AsBinding]
asb 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 forall a. Int -> [a] -> [a]
drop Int
fvs NAPs
ps of [Arg (Named_ DeBruijnPattern)
p] -> forall a. NamedArg a -> a
namedArg Arg (Named_ DeBruijnPattern)
p; NAPs
_ -> forall a. HasCallStack => a
__IMPOSSIBLE__
          -- Also strip the context variables from the telescope
          delta :: Telescope
delta = ListTel -> Telescope
telFromList forall a b. (a -> b) -> a -> b
$ forall a. Int -> [a] -> [a]
drop Int
fvs forall a b. (a -> b) -> a -> b
$ forall t. Tele (Dom t) -> [Dom (ArgName, t)]
telToList Telescope
delta0
      forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m ()
reportSDoc ArgName
"tc.term.let.pattern" Int
20 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
        [ TCMT IO Doc
"p (I) =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM DeBruijnPattern
p
        , TCMT IO Doc
"delta =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Telescope
delta
        , TCMT IO Doc
"cxtRel=" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> do forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
asksTC forall a. LensRelevance a => a -> Relevance
getRelevance
        , TCMT IO Doc
"cxtQnt=" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> do forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
asksTC forall a. LensQuantity a => a -> Quantity
getQuantity
        ]
      forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m ()
reportSDoc ArgName
"tc.term.let.pattern" Int
80 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
        [ TCMT IO Doc
"p (I) =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> (forall (m :: * -> *). Applicative m => ArgName -> m Doc
text forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => a -> ArgName
show) DeBruijnPattern
p
        ]
      -- We translate it into a list of projections.
      [Term -> Term]
fs <- DeBruijnPattern -> TCM [Term -> Term]
recordPatternToProjections DeBruijnPattern
p
      -- We remove the bindings for the pattern variables from the context.
      [ContextEntry]
cxt0 <- forall (m :: * -> *). MonadTCEnv m => m [ContextEntry]
getContext
      let ([ContextEntry]
binds, [ContextEntry]
cxt) = forall a. Int -> [a] -> ([a], [a])
splitAt (forall a. Sized a => a -> Int
size Telescope
delta) [ContextEntry]
cxt0
          toDrop :: Int
toDrop       = 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]
sigma = forall a b. (a -> b) -> [a] -> [b]
map (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 :: Substitution
sub    = forall a. DeBruijn a => [a] -> Substitution' a
parallelS (forall a. [a] -> [a]
reverse [Term]
sigma)

      forall (m :: * -> *) a.
MonadAddContext m =>
Substitution -> ([ContextEntry] -> [ContextEntry]) -> m a -> m a
updateContext Substitution
sub (forall a. Int -> [a] -> [a]
drop Int
toDrop) forall a b. (a -> b) -> a -> b
$ do
        forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m ()
reportSDoc ArgName
"tc.term.let.pattern" Int
20 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
          [ TCMT IO Doc
"delta =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Telescope
delta
          , TCMT IO Doc
"binds =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM [ContextEntry]
binds
          ]
        let fdelta :: [Dom Type]
fdelta = forall a. TermSubst a => Tele (Dom a) -> [Dom a]
flattenTel Telescope
delta
        forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m ()
reportSDoc ArgName
"tc.term.let.pattern" Int
20 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
          [ TCMT IO Doc
"fdelta =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
delta (forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM [Dom Type]
fdelta)
          ]
        let tsl :: [Dom Type]
tsl  = forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution
sub [Dom Type]
fdelta
        -- We get a list of types
        let ts :: [Type]
ts   = forall a b. (a -> b) -> [a] -> [b]
map forall t e. Dom' t e -> e
unDom [Dom Type]
tsl
        -- and relevances.
        let infos :: [ArgInfo]
infos = forall a b. (a -> b) -> [a] -> [b]
map forall t e. Dom' t e -> ArgInfo
domInfo [Dom Type]
tsl
        -- We get list of names of the let-bound vars from the context.
        let xs :: [Name]
xs   = forall a b. (a -> b) -> [a] -> [b]
map (forall a b. (a, b) -> a
fst forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t e. Dom' t e -> e
unDom) (forall a. [a] -> [a]
reverse [ContextEntry]
binds)
        -- We add all the bindings to the context.
        forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (forall a b c d e. (a -> b -> c -> d -> e) -> (a, b, c, d) -> e
uncurry4 forall (m :: * -> *) a.
MonadAddContext m =>
ArgInfo -> Name -> Term -> Type -> m a -> m a
addLetBinding) TCM a
ret forall a b. (a -> b) -> a -> b
$ forall a b c d. [a] -> [b] -> [c] -> [d] -> [(a, b, c, d)]
List.zip4 [ArgInfo]
infos [Name]
xs [Term]
sigma [Type]
ts

checkLetBinding (A.LetApply ModuleInfo
i ModuleName
x ModuleApplication
modapp ScopeCopyInfo
copyInfo ImportDirective
_adir) 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@.
  Int
fv   <- TCM Int
getCurrentModuleFreeVars
  Int
n    <- forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Int
getContextSize
  let new :: Int
new = Int
n forall a. Num a => a -> a -> a
- Int
fv
  forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m ()
reportSDoc ArgName
"tc.term.let.apply" Int
10 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"Applying" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty ModuleName
x forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA ModuleApplication
modapp forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<?> (TCMT IO Doc
"with" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) a. (Applicative m, Show a) => a -> m Doc
pshow Int
new forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
"free variables")
  forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m ()
reportSDoc ArgName
"tc.term.let.apply" Int
20 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
    [ TCMT IO Doc
"context =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> (forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Telescope
getContextTelescope)
    , TCMT IO Doc
"module  =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> (forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (m :: * -> *). MonadTCEnv m => m ModuleName
currentModule)
    , TCMT IO Doc
"fv      =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *). Applicative m => ArgName -> m Doc
text (forall a. Show a => a -> ArgName
show Int
fv)
    ]
  ModuleInfo
-> ModuleName -> ModuleApplication -> ScopeCopyInfo -> TCM ()
checkSectionApplication ModuleInfo
i ModuleName
x ModuleApplication
modapp ScopeCopyInfo
copyInfo
  forall a. ModuleName -> Int -> TCM a -> TCM a
withAnonymousModule ModuleName
x Int
new TCM a
ret
-- LetOpen and LetDeclaredVariable are only used for highlighting.
checkLetBinding A.LetOpen{} TCM a
ret = TCM a
ret
checkLetBinding (A.LetDeclaredVariable BindName
_) TCM a
ret = TCM a
ret