{-# LANGUAGE NondecreasingIndentation #-}

module Agda.TypeChecking.Rules.Term where

import Prelude hiding ( null )

import Control.Monad.Reader

import Data.Maybe
import Data.Either (partitionEithers, lefts)
import Data.Monoid (mappend)
import qualified Data.List as List
import qualified Data.Map as Map

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

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.Syntax.Translation.InternalToAbstract (reify)

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.MetaVars
import Agda.TypeChecking.Monad
import Agda.TypeChecking.Monad.Builtin
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.Except
  (MonadError(catchError, throwError))
import Agda.Utils.Functor
import Agda.Utils.Lens
import Agda.Utils.List
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.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 -> TCM Type
isType = Comparison -> Expr -> Sort -> 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 -> TCM Type
isType' Comparison
c Expr
e Sort
s =
    Call -> TCM Type -> TCM Type
forall (tcm :: * -> *) a.
(MonadTCM tcm, ReadTCState tcm, MonadDebug tcm) =>
Call -> tcm a -> tcm a
traceCall (Comparison -> Expr -> Sort -> Call
IsTypeCall Comparison
c Expr
e Sort
s) (TCM Type -> TCM Type) -> TCM Type -> TCM Type
forall a b. (a -> b) -> a -> b
$ do
    Term
v <- Comparison -> Expr -> Type -> TCM Term
checkExpr' Comparison
c Expr
e (Sort -> Type
sort Sort
s)
    Type -> TCM Type
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> TCM Type) -> Type -> TCM Type
forall a b. (a -> b) -> a -> b
$ Sort -> Term -> Type
forall t a. Sort' t -> a -> Type'' t a
El Sort
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 = Call -> TCM Type -> TCM Type
forall (tcm :: * -> *) a.
(MonadTCM tcm, ReadTCState tcm, MonadDebug tcm) =>
Call -> tcm a -> tcm a
traceCall (Expr -> Call
IsType_ Expr
e) (TCM Type -> TCM Type) -> TCM Type -> TCM Type
forall a b. (a -> b) -> a -> b
$ do
  VerboseKey
-> VerboseLevel -> (Type -> TCM Doc) -> TCM Type -> TCM Type
forall (m :: * -> *) a.
MonadDebug m =>
VerboseKey -> VerboseLevel -> (a -> TCM Doc) -> m a -> m a
reportResult VerboseKey
"tc.term.istype" VerboseLevel
15 (\Type
a -> [TCM Doc] -> TCM Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
vcat
    [ TCM Doc
"isType_" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<?> Expr -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Expr
e
    , VerboseLevel -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest VerboseLevel
2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ TCM Doc
"returns" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<?> Type -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
a
    ]) (TCM Type -> TCM Type) -> TCM Type -> TCM Type
forall a b. (a -> b) -> a -> b
$ do
  let fallback :: TCM Type
fallback = Comparison -> Expr -> Sort -> TCM Type
isType' Comparison
CmpEq Expr
e (Sort -> TCM Type) -> TCMT IO Sort -> TCM Type
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< do TCMT IO Sort -> TCMT IO Sort
forall (m :: * -> *) a.
(MonadTCEnv m, HasOptions m, MonadDebug m) =>
m a -> m a
workOnTypes (TCMT IO Sort -> TCMT IO Sort) -> TCMT IO Sort -> TCMT IO Sort
forall a b. (a -> b) -> a -> b
$ TCMT IO Sort
forall (m :: * -> *). MonadMetaSolver m => m Sort
newSortMeta
  case Expr -> Expr
unScope Expr
e of
    A.Fun ExprInfo
i (Arg ArgInfo
info Expr
t) Expr
b -> do
      Dom Type
a <- ArgInfo -> Dom Type -> Dom Type
forall a. LensArgInfo a => ArgInfo -> a -> a
setArgInfo ArgInfo
info (Dom Type -> Dom Type) -> (Type -> Dom Type) -> Type -> Dom Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> Dom Type
forall a. a -> Dom a
defaultDom (Type -> Dom Type) -> TCM Type -> TCMT IO (Dom Type)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr -> TCM Type
isType_ Expr
t
      Type
b <- Expr -> TCM Type
isType_ Expr
b
      Sort
s <- Sort -> Sort -> TCMT IO Sort
inferFunSort (Dom Type -> Sort
forall a. LensSort a => a -> Sort
getSort Dom Type
a) (Type -> Sort
forall a. LensSort a => a -> Sort
getSort Type
b)
      let t' :: Type
t' = Sort -> Term -> Type
forall t a. Sort' t -> a -> Type'' t a
El Sort
s (Term -> Type) -> Term -> Type
forall a b. (a -> b) -> a -> b
$ Dom Type -> Abs Type -> Term
Pi Dom Type
a (Abs Type -> Term) -> Abs Type -> Term
forall a b. (a -> b) -> a -> b
$ VerboseKey -> Type -> Abs Type
forall a. VerboseKey -> a -> Abs a
NoAbs VerboseKey
forall a. Underscore a => a
underscore Type
b
      Type -> Type -> TCM ()
noFunctionsIntoSize Type
b Type
t'
      Type -> TCM Type
forall (m :: * -> *) a. Monad m => a -> m a
return Type
t'
    A.Pi ExprInfo
_ Telescope
tel Expr
e | Telescope -> Bool
forall a. Null a => a -> Bool
null Telescope
tel -> Expr -> TCM Type
isType_ Expr
e
    A.Pi ExprInfo
_ Telescope
tel Expr
e -> do
      (Type
t0, Type
t') <- Telescope -> (Telescope -> TCM (Type, Type)) -> TCM (Type, Type)
forall a. Telescope -> (Telescope -> TCM a) -> TCM a
checkPiTelescope Telescope
tel ((Telescope -> TCM (Type, Type)) -> TCM (Type, Type))
-> (Telescope -> TCM (Type, Type)) -> TCM (Type, Type)
forall a b. (a -> b) -> a -> b
$ \ Telescope
tel -> do
        Type
t0  <- Type -> TCM Type
forall a (m :: * -> *).
(InstantiateFull a, MonadReduce m) =>
a -> m a
instantiateFull (Type -> TCM Type) -> TCM Type -> TCM Type
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Expr -> TCM Type
isType_ Expr
e
        Telescope
tel <- Telescope -> TCMT IO Telescope
forall a (m :: * -> *).
(InstantiateFull a, MonadReduce m) =>
a -> m a
instantiateFull Telescope
tel
        (Type, Type) -> TCM (Type, Type)
forall (m :: * -> *) a. Monad m => a -> m a
return (Type
t0, Telescope -> Type -> Type
telePi Telescope
tel Type
t0)
      Type -> TCM ()
checkTelePiSort Type
t'
      Type -> Type -> TCM ()
noFunctionsIntoSize Type
t0 Type
t'
      Type -> TCM Type
forall (m :: * -> *) a. Monad m => a -> m a
return Type
t'

    -- Setᵢ
    A.Set ExprInfo
_ Integer
n -> do
      Type -> TCM Type
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> TCM Type) -> Type -> TCM Type
forall a b. (a -> b) -> a -> b
$ Sort -> Type
sort (Integer -> Sort
mkType Integer
n)

    -- Propᵢ
    A.Prop ExprInfo
_ Integer
n -> do
      TCMT IO Bool -> TCM () -> TCM ()
forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
unlessM TCMT IO Bool
forall (m :: * -> *). HasOptions m => m Bool
isPropEnabled (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ TypeError -> TCM ()
forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m, MonadError TCErr m) =>
TypeError -> m a
typeError TypeError
NeedOptionProp
      Type -> TCM Type
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> TCM Type) -> Type -> TCM Type
forall a b. (a -> b) -> a -> b
$ Sort -> Type
sort (Integer -> Sort
mkProp Integer
n)

    -- Set ℓ
    A.App AppInfo
i Expr
s NamedArg Expr
arg
      | NamedArg Expr -> Bool
forall a. LensHiding a => a -> Bool
visible NamedArg Expr
arg,
        A.Set ExprInfo
_ Integer
0 <- Expr -> Expr
unScope Expr
s -> do
      TCMT IO Bool -> TCM () -> TCM ()
forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
unlessM TCMT IO Bool
forall (m :: * -> *). HasOptions m => m Bool
hasUniversePolymorphism (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ VerboseKey -> TCM ()
forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m, MonadError TCErr m) =>
VerboseKey -> m a
genericError
        VerboseKey
"Use --universe-polymorphism to enable level arguments to Set"
      -- allow NonStrict variables when checking level
      --   Set : (NonStrict) Level -> Set\omega
      Relevance -> TCM Type -> TCM Type
forall (tcm :: * -> *) r a.
(MonadTCEnv tcm, LensRelevance r) =>
r -> tcm a -> tcm a
applyRelevanceToContext Relevance
NonStrict (TCM Type -> TCM Type) -> TCM Type -> TCM Type
forall a b. (a -> b) -> a -> b
$
        Sort -> Type
sort (Sort -> Type) -> (Level' Term -> Sort) -> Level' Term -> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Level' Term -> Sort
forall t. Level' t -> Sort' t
Type (Level' Term -> Type) -> TCMT IO (Level' Term) -> TCM Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> NamedArg Expr -> TCMT IO (Level' Term)
checkLevel NamedArg Expr
arg

    -- Prop ℓ
    A.App AppInfo
i Expr
s NamedArg Expr
arg
      | NamedArg Expr -> Bool
forall a. LensHiding a => a -> Bool
visible NamedArg Expr
arg,
        A.Prop ExprInfo
_ Integer
0 <- Expr -> Expr
unScope Expr
s -> do
      TCMT IO Bool -> TCM () -> TCM ()
forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
unlessM TCMT IO Bool
forall (m :: * -> *). HasOptions m => m Bool
isPropEnabled (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ TypeError -> TCM ()
forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m, MonadError TCErr m) =>
TypeError -> m a
typeError TypeError
NeedOptionProp
      TCMT IO Bool -> TCM () -> TCM ()
forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
unlessM TCMT IO Bool
forall (m :: * -> *). HasOptions m => m Bool
hasUniversePolymorphism (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ VerboseKey -> TCM ()
forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m, MonadError TCErr m) =>
VerboseKey -> m a
genericError
        VerboseKey
"Use --universe-polymorphism to enable level arguments to Prop"
      Relevance -> TCM Type -> TCM Type
forall (tcm :: * -> *) r a.
(MonadTCEnv tcm, LensRelevance r) =>
r -> tcm a -> tcm a
applyRelevanceToContext Relevance
NonStrict (TCM Type -> TCM Type) -> TCM Type -> TCM Type
forall a b. (a -> b) -> a -> b
$
        Sort -> Type
sort (Sort -> Type) -> (Level' Term -> Sort) -> Level' Term -> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Level' Term -> Sort
forall t. Level' t -> Sort' t
Prop (Level' Term -> Type) -> TCMT IO (Level' Term) -> TCM Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> NamedArg Expr -> TCMT IO (Level' Term)
checkLevel NamedArg Expr
arg

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

    Expr
_ -> TCM Type
fallback

checkLevel :: NamedArg A.Expr -> TCM Level
checkLevel :: NamedArg Expr -> TCMT IO (Level' Term)
checkLevel NamedArg Expr
arg = do
  Type
lvl <- TCM Type
forall (m :: * -> *). HasBuiltins m => m Type
levelType
  Term -> TCMT IO (Level' Term)
forall (m :: * -> *).
(HasBuiltins m, MonadReduce m, MonadDebug m) =>
Term -> m (Level' Term)
levelView (Term -> TCMT IO (Level' Term))
-> TCM Term -> TCMT IO (Level' Term)
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'.
noFunctionsIntoSize :: Type -> Type -> TCM ()
noFunctionsIntoSize :: Type -> Type -> TCM ()
noFunctionsIntoSize Type
t Type
tBlame = do
  VerboseKey -> VerboseLevel -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.fun" VerboseLevel
20 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ do
    let El Sort
s (Pi Dom Type
dom Abs Type
b) = Type
tBlame
    [TCM Doc] -> TCM Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
sep [ TCM Doc
"created function type " TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Type -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
tBlame
        , TCM Doc
"with pts rule (" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Sort -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM (Dom Type -> Sort
forall a. LensSort a => a -> Sort
getSort Dom Type
dom) TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+>
                        TCM Doc
"," TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Abs Type -> (Type -> TCM Doc) -> TCM Doc
forall t a (m :: * -> *) b.
(Subst t a, MonadAddContext m) =>
Abs a -> (a -> m b) -> m b
underAbstraction_ Abs Type
b (Sort -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM (Sort -> TCM Doc) -> (Type -> Sort) -> Type -> TCM Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> Sort
forall a. LensSort a => a -> Sort
getSort) TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+>
                        TCM Doc
"," TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Sort -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Sort
s TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCM Doc
")"
        ]
  Sort
s <- Sort -> TCMT IO Sort
forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce (Sort -> TCMT IO Sort) -> Sort -> TCMT IO Sort
forall a b. (a -> b) -> a -> b
$ Type -> Sort
forall a. LensSort a => a -> Sort
getSort Type
t
  Bool -> TCM () -> TCM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Sort
s Sort -> Sort -> Bool
forall a. Eq a => a -> a -> Bool
== Sort
forall t. Sort' t
SizeUniv) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ do
    -- Andreas, 2015-02-14
    -- We have constructed a function type in SizeUniv
    -- which is illegal to prevent issue 1428.
    TypeError -> TCM ()
forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m, MonadError TCErr m) =>
TypeError -> m a
typeError (TypeError -> TCM ()) -> TypeError -> TCM ()
forall a b. (a -> b) -> a -> b
$ Term -> TypeError
FunctionTypeInSizeUniv (Term -> TypeError) -> Term -> TypeError
forall a b. (a -> b) -> a -> b
$ Type -> Term
forall t a. Type'' t a -> a
unEl Type
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 TCM Expr -> (Expr -> TCM Type) -> TCM Type
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
  A.ScopedExpr{} -> TCM Type
forall a. HasCallStack => a
__IMPOSSIBLE__
  A.Underscore MetaInfo
i | MetaInfo -> Maybe MetaId
A.metaNumber MetaInfo
i Maybe MetaId -> Maybe MetaId -> Bool
forall a. Eq a => a -> a -> Bool
== Maybe MetaId
forall a. Maybe a
Nothing -> Type -> TCM Type
forall (m :: * -> *) a. Monad m => a -> m a
return Type
t
  Expr
e -> TCM Type -> TCM Type
forall (m :: * -> *) a.
(MonadTCEnv m, HasOptions m, MonadDebug m) =>
m a -> m a
workOnTypes (TCM Type -> TCM Type) -> TCM Type -> TCM Type
forall a b. (a -> b) -> a -> b
$ do
    Type
t' <- Expr -> Sort -> TCM Type
isType Expr
e (Type -> Sort
forall a. LensSort a => a -> Sort
getSort Type
t)
    Type
t' Type -> TCM () -> TCM Type
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Type -> Type -> TCM ()
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' = TCM () -> TCM ()
forall (m :: * -> *) a.
(MonadTCEnv m, HasOptions m, MonadDebug m) =>
m a -> m a
workOnTypes (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ Type -> Type -> TCM ()
forall (m :: * -> *). MonadConversion m => Type -> Type -> m ()
leqType Type
t Type
t'

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

checkGeneralizeTelescope :: A.GeneralizeTelescope -> ([Maybe Name] -> Telescope -> TCM a) -> TCM a
checkGeneralizeTelescope :: GeneralizeTelescope
-> ([Maybe Name] -> Telescope -> TCM a) -> TCM a
checkGeneralizeTelescope (A.GeneralizeTel Map QName Name
vars Telescope
tel) [Maybe Name] -> Telescope -> TCM a
k =
  Map QName Name
-> (forall a1. (Telescope -> TCM a1) -> TCM a1)
-> ([Maybe Name] -> Telescope -> TCM a)
-> TCM a
forall a.
Map QName Name
-> (forall a1. (Telescope -> TCM a1) -> TCM a1)
-> ([Maybe Name] -> Telescope -> TCM a)
-> TCM a
generalizeTelescope Map QName Name
vars (Telescope -> (Telescope -> TCM a1) -> TCM a1
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 :: Telescope -> (Telescope -> TCM a) -> TCM a
checkTelescope = LamOrPi -> Telescope -> (Telescope -> TCM a) -> TCM a
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 :: Telescope -> (Telescope -> TCM a) -> TCM a
checkPiTelescope = LamOrPi -> Telescope -> (Telescope -> TCM a) -> TCM a
forall a. LamOrPi -> Telescope -> (Telescope -> TCM a) -> TCM a
checkTelescope' LamOrPi
PiNotLam

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

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

-- | Check 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 :: LamOrPi -> TypedBinding -> (Telescope -> TCM a) -> TCM a
checkTypedBindings LamOrPi
lamOrPi (A.TBind Range
r TacticAttr
tac [NamedArg Binder]
xps Expr
e) Telescope -> TCM a
ret = do
    let xs :: [NamedArg Name]
xs = (NamedArg Binder -> NamedArg Name)
-> [NamedArg Binder] -> [NamedArg Name]
forall a b. (a -> b) -> [a] -> [b]
map ((Binder -> Name) -> NamedArg Binder -> NamedArg Name
forall a b. (a -> b) -> NamedArg a -> NamedArg b
updateNamedArg ((Binder -> Name) -> NamedArg Binder -> NamedArg Name)
-> (Binder -> Name) -> NamedArg Binder -> NamedArg Name
forall a b. (a -> b) -> a -> b
$ BindName -> Name
A.unBind (BindName -> Name) -> (Binder -> BindName) -> Binder -> Name
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Binder -> BindName
forall a. Binder' a -> a
A.binderName) [NamedArg Binder]
xps
    Maybe Term
tac <- (Expr -> TCM Term) -> TacticAttr -> TCMT IO (Maybe Term)
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) TacticAttr
tac
    Maybe Term -> (Term -> TCM ()) -> TCM ()
forall (m :: * -> *) a. Monad m => Maybe a -> (a -> m ()) -> m ()
whenJust Maybe Term
tac ((Term -> TCM ()) -> TCM ()) -> (Term -> TCM ()) -> TCM ()
forall a b. (a -> b) -> a -> b
$ \ Term
t -> VerboseKey -> VerboseLevel -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.term.tactic" VerboseLevel
30 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ TCM Doc
"Checked tactic attribute:" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<?> Term -> TCM 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 (PragmaOptions -> Bool) -> TCMT IO PragmaOptions -> TCMT IO Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCMT IO PragmaOptions
forall (m :: * -> *). HasOptions m => m PragmaOptions
pragmaOptions

    let cs :: [Cohesion]
cs = (NamedArg Binder -> Cohesion) -> [NamedArg Binder] -> [Cohesion]
forall a b. (a -> b) -> [a] -> [b]
map NamedArg Binder -> Cohesion
forall a. LensCohesion a => a -> Cohesion
getCohesion [NamedArg Binder]
xps
        c :: Cohesion
c = Cohesion -> [Cohesion] -> Cohesion
forall a. a -> [a] -> a
headWithDefault Cohesion
forall a. HasCallStack => a
__IMPOSSIBLE__ [Cohesion]
cs
    Bool -> TCM () -> TCM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless ((Cohesion -> Bool) -> [Cohesion] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (Cohesion
c Cohesion -> Cohesion -> Bool
forall a. Eq a => a -> a -> Bool
==) [Cohesion]
cs) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ TCM ()
forall a. HasCallStack => a
__IMPOSSIBLE__

    Type
t <- Cohesion -> TCM Type -> TCM Type
forall (tcm :: * -> *) m a.
(MonadTCEnv tcm, LensCohesion m) =>
m -> tcm a -> tcm a
applyCohesionToContext Cohesion
c (TCM Type -> TCM Type) -> TCM Type -> TCM Type
forall a b. (a -> b) -> a -> b
$ LamOrPi -> TCM Type -> TCM Type
forall (m :: * -> *) a.
(MonadTCEnv m, HasOptions m, MonadDebug m) =>
LamOrPi -> m a -> m a
modEnv LamOrPi
lamOrPi (TCM Type -> TCM Type) -> TCM Type -> TCM Type
forall a b. (a -> b) -> a -> b
$ Expr -> TCM Type
isType_ Expr
e

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

    let setTac :: Maybe t -> Tele (Dom' t e) -> Tele (Dom' t e)
setTac Maybe t
tac Tele (Dom' t e)
EmptyTel            = Tele (Dom' t e)
forall a. Tele a
EmptyTel
        setTac Maybe t
tac (ExtendTel Dom' t e
dom Abs (Tele (Dom' t e))
tel) = Dom' t e -> Abs (Tele (Dom' t e)) -> Tele (Dom' t e)
forall a. a -> Abs (Tele a) -> Tele a
ExtendTel Dom' t e
dom{ domTactic :: Maybe t
domTactic = Maybe t
tac } (Abs (Tele (Dom' t e)) -> Tele (Dom' t e))
-> Abs (Tele (Dom' t e)) -> Tele (Dom' t e)
forall a b. (a -> b) -> a -> b
$ Maybe t -> Tele (Dom' t e) -> Tele (Dom' t e)
setTac (VerboseLevel -> Maybe t -> Maybe t
forall t a. Subst t a => VerboseLevel -> a -> a
raise VerboseLevel
1 Maybe t
tac) (Tele (Dom' t e) -> Tele (Dom' t e))
-> Abs (Tele (Dom' t e)) -> Abs (Tele (Dom' t e))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Abs (Tele (Dom' t e))
tel
        xs' :: [NamedArg Name]
xs' = (NamedArg Name -> NamedArg Name)
-> [NamedArg Name] -> [NamedArg Name]
forall a b. (a -> b) -> [a] -> [b]
map (LamOrPi -> Bool -> NamedArg Name -> NamedArg Name
forall c.
(LensRelevance c, LensQuantity c) =>
LamOrPi -> Bool -> c -> c
modMod LamOrPi
lamOrPi Bool
experimental) [NamedArg Name]
xs
    let tel :: Telescope
tel = Maybe Term -> Telescope -> Telescope
forall t t t e.
Subst t t =>
Maybe t -> Tele (Dom' t e) -> Tele (Dom' t e)
setTac Maybe Term
tac (Telescope -> Telescope) -> Telescope -> Telescope
forall a b. (a -> b) -> a -> b
$ [NamedArg Name] -> Type -> Telescope
namedBindsToTel [NamedArg Name]
xs Type
t

    ([NamedArg Name], Type) -> TCM a -> TCM a
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext ([NamedArg Name]
xs', Type
t) (TCM a -> TCM a) -> TCM a -> TCM a
forall a b. (a -> b) -> a -> b
$ [NamedArg Binder] -> TCM a -> TCM a
forall a. [NamedArg Binder] -> TCM a -> TCM a
addTypedPatterns [NamedArg Binder]
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 = m a -> m a
forall (m :: * -> *) a.
(MonadTCEnv m, HasOptions m, MonadDebug m) =>
m a -> m a
workOnTypes
        modEnv LamOrPi
_        = m a -> m a
forall a. a -> a
id
        modMod :: LamOrPi -> Bool -> c -> c
modMod LamOrPi
PiNotLam Bool
xp = (if Bool
xp then (Relevance -> Relevance) -> c -> c
forall a. LensRelevance a => (Relevance -> Relevance) -> a -> a
mapRelevance Relevance -> Relevance
irrToNonStrict else c -> c
forall a. a -> a
id)
                           (c -> c) -> (c -> c) -> c -> c
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Quantity -> c -> c
forall a. LensQuantity a => Quantity -> a -> a
setQuantity Quantity
topQuantity)
        modMod LamOrPi
_        Bool
_  = c -> c
forall a. a -> a
id
checkTypedBindings LamOrPi
lamOrPi (A.TLet Range
_ [LetBinding]
lbs) Telescope -> TCM a
ret = do
    [LetBinding] -> TCM a -> TCM a
forall a. [LetBinding] -> TCM a -> TCM a
checkLetBindings [LetBinding]
lbs (Telescope -> TCM a
ret Telescope
forall a. Tele a
EmptyTel)

-- | After a typed binding has been checked, add the patterns it binds
addTypedPatterns :: [NamedArg A.Binder] -> TCM a -> TCM a
addTypedPatterns :: [NamedArg Binder] -> TCM a -> TCM a
addTypedPatterns [NamedArg Binder]
xps TCM a
ret = do
  let ps :: [(Pattern, BindName)]
ps  = (NamedArg Binder -> Maybe (Pattern, BindName))
-> [NamedArg Binder] -> [(Pattern, BindName)]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe (Binder -> Maybe (Pattern, BindName)
forall a. Binder' a -> Maybe (Pattern, a)
A.extractPattern (Binder -> Maybe (Pattern, BindName))
-> (NamedArg Binder -> Binder)
-> NamedArg Binder
-> Maybe (Pattern, BindName)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NamedArg Binder -> Binder
forall a. NamedArg a -> a
namedArg) [NamedArg Binder]
xps
  let lbs :: [LetBinding]
lbs = ((Pattern, BindName) -> LetBinding)
-> [(Pattern, BindName)] -> [LetBinding]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Pattern, BindName) -> LetBinding
letBinding [(Pattern, BindName)]
ps
  [LetBinding] -> TCM a -> TCM a
forall a. [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 (Name -> Expr) -> Name -> Expr
forall a b. (a -> b) -> a -> b
$ BindName -> Name
A.unBind BindName
n)
      where r :: Range
r = Pattern -> BindName -> Range
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 = Doc -> TCM Term
forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m, MonadError TCErr m) =>
Doc -> m a
genericDocError (Doc -> TCM Term) -> TCM Doc -> TCM Term
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< TCM Doc
"The @tactic attribute is not allowed here"
checkTacticAttribute LamOrPi
PiNotLam Expr
e = do
  Type
expectedType <- TCM Term -> TCM Type
forall (tcm :: * -> *). Functor tcm => tcm Term -> tcm Type
el TCM Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTerm TCM Type -> TCM Type -> TCM Type
forall (tcm :: * -> *).
Monad tcm =>
tcm Type -> tcm Type -> tcm Type
--> TCM Term -> TCM Type
forall (tcm :: * -> *). Functor tcm => tcm Term -> tcm Type
el (TCM Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTCM TCM Term -> TCM Term -> TCM Term
forall (tcm :: * -> *).
Monad tcm =>
tcm Term -> tcm Term -> tcm Term
<#> TCM Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primLevelZero TCM Term -> TCM Term -> TCM Term
forall (tcm :: * -> *).
Monad tcm =>
tcm Term -> tcm Term -> tcm Term
<@> TCM Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primUnit)
  Expr -> Type -> TCM Term
checkExpr Expr
e Type
expectedType

ifPath :: Type -> TCM a -> TCM a -> TCM a
ifPath :: Type -> TCM a -> TCM a -> TCM a
ifPath Type
ty TCM a
fallback TCM a
work = do
  PathView
pv <- Type -> TCMT IO PathView
forall (m :: * -> *). HasBuiltins m => Type -> m PathView
pathView Type
ty
  if PathView -> Bool
isPathType PathView
pv then TCM a
work else TCM a
fallback

checkPath :: A.TypedBinding -> A.Expr -> Type -> TCM Term
checkPath :: TypedBinding -> Expr -> Type -> TCM Term
checkPath b :: TypedBinding
b@(A.TBind Range
_ TacticAttr
_ [NamedArg Binder
x'] Expr
typ) Expr
body Type
ty = do
    let x :: NamedArg Name
x    = (Binder -> Name) -> NamedArg Binder -> NamedArg Name
forall a b. (a -> b) -> NamedArg a -> NamedArg b
updateNamedArg (BindName -> Name
A.unBind (BindName -> Name) -> (Binder -> BindName) -> Binder -> Name
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Binder -> BindName
forall a. Binder' a -> a
A.binderName) NamedArg Binder
x'
        info :: ArgInfo
info = NamedArg Name -> ArgInfo
forall a. LensArgInfo a => a -> ArgInfo
getArgInfo NamedArg Name
x
    PathType Sort
s QName
path Arg Term
level Arg Term
typ Arg Term
lhs Arg Term
rhs <- Type -> TCMT IO PathView
forall (m :: * -> *). HasBuiltins m => Type -> m PathView
pathView Type
ty
    Type
interval <- TCM Term -> TCM Type
forall (tcm :: * -> *). Functor tcm => tcm Term -> tcm Type
elInf TCM Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primInterval
    Term
v <- ([NamedArg Name], Type) -> TCM Term -> TCM Term
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext ([NamedArg Name
x], Type
interval) (TCM Term -> TCM Term) -> TCM Term -> TCM Term
forall a b. (a -> b) -> a -> b
$
           Expr -> Type -> TCM Term
checkExpr Expr
body (Sort -> Term -> Type
forall t a. Sort' t -> a -> Type'' t a
El (VerboseLevel -> Sort -> Sort
forall t a. Subst t a => VerboseLevel -> a -> a
raise VerboseLevel
1 Sort
s) (VerboseLevel -> Term -> Term
forall t a. Subst t a => VerboseLevel -> a -> a
raise VerboseLevel
1 (Arg Term -> Term
forall e. Arg e -> e
unArg Arg Term
typ) Term -> [Arg Term] -> Term
forall t. Apply t => t -> [Arg Term] -> t
`apply` [Term -> Arg Term
forall e. e -> Arg e
argN (Term -> Arg Term) -> Term -> Arg Term
forall a b. (a -> b) -> a -> b
$ VerboseLevel -> Term
var VerboseLevel
0]))
    Term
iZero <- TCM Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primIZero
    Term
iOne  <- TCM Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primIOne
    let lhs' :: Term
lhs' = VerboseLevel -> Term -> Term -> Term
forall t a. Subst t a => VerboseLevel -> t -> a -> a
subst VerboseLevel
0 Term
iZero Term
v
        rhs' :: Term
rhs' = VerboseLevel -> Term -> Term -> Term
forall t a. Subst t a => VerboseLevel -> t -> a -> a
subst VerboseLevel
0 Term
iOne  Term
v
    let t :: Term
t = ArgInfo -> Abs Term -> Term
Lam ArgInfo
info (Abs Term -> Term) -> Abs Term -> Term
forall a b. (a -> b) -> a -> b
$ VerboseKey -> Term -> Abs Term
forall a. VerboseKey -> a -> Abs a
Abs (NamedArg Name -> VerboseKey
namedArgName NamedArg Name
x) Term
v
    let btyp :: Term -> Type
btyp Term
i = Sort -> Term -> Type
forall t a. Sort' t -> a -> Type'' t a
El Sort
s (Arg Term -> Term
forall e. Arg e -> e
unArg Arg Term
typ Term -> [Arg Term] -> Term
forall t. Apply t => t -> [Arg Term] -> t
`apply` [Term -> Arg Term
forall e. e -> Arg e
argN Term
i])
    Lens' Range TCEnv -> (Range -> Range) -> TCM Term -> TCM Term
forall (m :: * -> *) a b.
MonadTCEnv m =>
Lens' a TCEnv -> (a -> a) -> m b -> m b
locallyTC Lens' Range TCEnv
eRange (Range -> Range -> Range
forall a b. a -> b -> a
const Range
forall a. Range' a
noRange) (TCM Term -> TCM Term) -> TCM Term -> TCM Term
forall a b. (a -> b) -> a -> b
$ Type -> TCM Term -> TCM Term
forall (m :: * -> *).
(MonadMetaSolver m, MonadConstraint m, MonadFresh VerboseLevel m,
 MonadFresh ProblemId m) =>
Type -> m Term -> m Term
blockTerm Type
ty (TCM Term -> TCM Term) -> TCM Term -> TCM Term
forall a b. (a -> b) -> a -> b
$ Call -> TCM Term -> TCM Term
forall (tcm :: * -> *) a.
(MonadTCM tcm, ReadTCState tcm, MonadDebug tcm) =>
Call -> tcm a -> tcm a
traceCall (Range -> Call
SetRange (Range -> Call) -> Range -> Call
forall a b. (a -> b) -> a -> b
$ Expr -> Range
forall t. HasRange t => t -> Range
getRange Expr
body) (TCM Term -> TCM Term) -> TCM Term -> TCM Term
forall a b. (a -> b) -> a -> b
$ do
      Type -> Term -> Term -> TCM ()
forall (m :: * -> *).
MonadConversion m =>
Type -> Term -> Term -> m ()
equalTerm (Term -> Type
btyp Term
iZero) Term
lhs' (Arg Term -> Term
forall e. Arg e -> e
unArg Arg Term
lhs)
      Type -> Term -> Term -> TCM ()
forall (m :: * -> *).
MonadConversion m =>
Type -> Term -> Term -> m ()
equalTerm (Term -> Type
btyp Term
iOne) Term
rhs' (Arg Term -> Term
forall e. Arg e -> e
unArg Arg Term
rhs)
      Term -> TCM Term
forall (m :: * -> *) a. Monad m => a -> m a
return Term
t
checkPath TypedBinding
b Expr
body Type
ty = TCM Term
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
_ [LetBinding]
lbs) Expr
body Type
target =
  [LetBinding] -> TCM Term -> TCM Term
forall a. [LetBinding] -> TCM a -> TCM a
checkLetBindings [LetBinding]
lbs (Expr -> Type -> TCM Term
checkExpr Expr
body Type
target)
checkLambda Comparison
cmp b :: TypedBinding
b@(A.TBind Range
_ TacticAttr
_ [NamedArg Binder]
xps Expr
typ) Expr
body Type
target = do
  VerboseKey -> VerboseLevel -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.term.lambda" VerboseLevel
60 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
vcat
    [ TCM Doc
"checkLambda xs = " TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [NamedArg Binder] -> TCM Doc
forall c a (m :: * -> *).
(Pretty c, ToConcrete a c, MonadAbsToCon m) =>
a -> m Doc
prettyA [NamedArg Binder]
xps
    , TCM Doc
"possiblePath = " TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> VerboseKey -> TCM Doc
forall (m :: * -> *). Monad m => VerboseKey -> m Doc
text ((Bool, VerboseLevel, Expr, ArgInfo) -> VerboseKey
forall a. Show a => a -> VerboseKey
show (Bool
possiblePath, VerboseLevel
numbinds, Expr -> Expr
unScope Expr
typ, ArgInfo
info))
    ]
  TelV Telescope
tel Type
btyp <- VerboseLevel -> Type -> TCMT IO (TelV Type)
forall (m :: * -> *).
(MonadReduce m, MonadAddContext m) =>
VerboseLevel -> Type -> m (TelV Type)
telViewUpTo VerboseLevel
numbinds Type
target
  if Telescope -> VerboseLevel
forall a. Sized a => a -> VerboseLevel
size Telescope
tel VerboseLevel -> VerboseLevel -> Bool
forall a. Ord a => a -> a -> Bool
< VerboseLevel
numbinds Bool -> Bool -> Bool
|| VerboseLevel
numbinds VerboseLevel -> VerboseLevel -> Bool
forall a. Eq a => a -> a -> Bool
/= VerboseLevel
1
    then (if Bool
possiblePath then TCM Term
trySeeingIfPath else TCM Term
dontUseTargetType)
    else Telescope -> Type -> TCM Term
forall t. Tele (Dom' t Type) -> Type -> TCM Term
useTargetType Telescope
tel Type
btyp

  where

    xs :: [NamedArg Name]
xs = (NamedArg Binder -> NamedArg Name)
-> [NamedArg Binder] -> [NamedArg Name]
forall a b. (a -> b) -> [a] -> [b]
map ((Binder -> Name) -> NamedArg Binder -> NamedArg Name
forall a b. (a -> b) -> NamedArg a -> NamedArg b
updateNamedArg (BindName -> Name
A.unBind (BindName -> Name) -> (Binder -> BindName) -> Binder -> Name
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Binder -> BindName
forall a. Binder' a -> a
A.binderName)) [NamedArg Binder]
xps
    numbinds :: VerboseLevel
numbinds = [NamedArg Binder] -> VerboseLevel
forall (t :: * -> *) a. Foldable t => t a -> VerboseLevel
length [NamedArg Binder]
xps
    isUnderscore :: Expr -> Bool
isUnderscore Expr
e = case Expr
e of { A.Underscore{} -> Bool
True; Expr
_ -> Bool
False }
    possiblePath :: Bool
possiblePath = VerboseLevel
numbinds VerboseLevel -> VerboseLevel -> Bool
forall a. Eq a => a -> a -> Bool
== VerboseLevel
1 Bool -> Bool -> Bool
&& Expr -> Bool
isUnderscore (Expr -> Expr
unScope Expr
typ)
                   Bool -> Bool -> Bool
&& ArgInfo -> Bool
forall a. LensRelevance a => a -> Bool
isRelevant ArgInfo
info Bool -> Bool -> Bool
&& ArgInfo -> Bool
forall a. LensHiding a => a -> Bool
visible ArgInfo
info
    info :: ArgInfo
info = NamedArg Name -> ArgInfo
forall a. LensArgInfo a => a -> ArgInfo
getArgInfo (NamedArg Name -> [NamedArg Name] -> NamedArg Name
forall a. a -> [a] -> a
headWithDefault NamedArg Name
forall a. HasCallStack => a
__IMPOSSIBLE__ [NamedArg Name]
xs)

    trySeeingIfPath :: TCM Term
trySeeingIfPath = do
      Bool
cubical <- PragmaOptions -> Bool
optCubical (PragmaOptions -> Bool) -> TCMT IO PragmaOptions -> TCMT IO Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCMT IO PragmaOptions
forall (m :: * -> *). HasOptions m => m PragmaOptions
pragmaOptions
      VerboseKey -> VerboseLevel -> VerboseKey -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> VerboseKey -> m ()
reportSLn VerboseKey
"tc.term.lambda" VerboseLevel
60 (VerboseKey -> TCM ()) -> VerboseKey -> TCM ()
forall a b. (a -> b) -> a -> b
$ VerboseKey
"trySeeingIfPath for " VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ [NamedArg Binder] -> VerboseKey
forall a. Show a => a -> VerboseKey
show [NamedArg Binder]
xps
      let postpone' :: p -> Type -> TCM Term
postpone' = if Bool
cubical then p -> Type -> TCM Term
forall p. p -> Type -> TCM Term
postpone else \ p
_ Type
_ -> TCM Term
dontUseTargetType
      Type
-> (MetaId -> Type -> TCM Term)
-> (NotBlocked -> Type -> TCM Term)
-> TCM Term
forall t (m :: * -> *) a.
(Reduce t, IsMeta t, MonadReduce m, HasBuiltins m) =>
t -> (MetaId -> t -> m a) -> (NotBlocked -> t -> m a) -> m a
ifBlocked Type
target MetaId -> Type -> TCM Term
forall p. p -> Type -> TCM Term
postpone' ((NotBlocked -> Type -> TCM Term) -> TCM Term)
-> (NotBlocked -> Type -> TCM Term) -> TCM Term
forall a b. (a -> b) -> a -> b
$ \ NotBlocked
_ Type
t -> do
        Type -> TCM Term -> TCM Term -> TCM Term
forall a. Type -> TCM a -> TCM a -> TCM a
ifPath Type
t TCM Term
dontUseTargetType (TCM Term -> TCM Term) -> TCM Term -> TCM Term
forall a b. (a -> b) -> a -> b
$ if Bool
cubical
          then TypedBinding -> Expr -> Type -> TCM Term
checkPath TypedBinding
b Expr
body Type
t
          else VerboseKey -> TCM Term
forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m, MonadError TCErr m) =>
VerboseKey -> m a
genericError VerboseKey
"Option --cubical needed to build a path with a lambda abstraction"

    postpone :: p -> Type -> TCM Term
postpone p
m Type
tgt = TypeCheckingProblem -> TCM Term
postponeTypeCheckingProblem_ (TypeCheckingProblem -> TCM Term)
-> TypeCheckingProblem -> TCM Term
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
      VerboseKey -> VerboseLevel -> TCM () -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> m () -> m ()
verboseS VerboseKey
"tc.term.lambda" VerboseLevel
5 (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ VerboseKey -> TCM ()
forall (m :: * -> *). MonadStatistics m => VerboseKey -> m ()
tick VerboseKey
"lambda-no-target-type"

      -- First check that argsT is a valid type
      Type
argsT <- TCM Type -> TCM Type
forall (m :: * -> *) a.
(MonadTCEnv m, HasOptions m, MonadDebug m) =>
m a -> m a
workOnTypes (TCM Type -> TCM Type) -> TCM Type -> TCM Type
forall a b. (a -> b) -> a -> b
$ Expr -> TCM Type
isType_ Expr
typ
      let tel :: Telescope
tel = [NamedArg Name] -> Type -> Telescope
namedBindsToTel [NamedArg Name]
xs Type
argsT
      VerboseKey -> VerboseLevel -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.term.lambda" VerboseLevel
60 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ TCM Doc
"dontUseTargetType tel =" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Telescope -> TCM Doc
forall (m :: * -> *) a. (Monad 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 (Term -> TCM ()) -> Term -> TCM ()
forall a b. (a -> b) -> a -> b
$ Type -> Term
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 TCM (Type, Term)
-> ((TCErr, MetaId) -> TCM (Type, Term)) -> TCM (Type, Term)
forall a. TCM a -> ((TCErr, MetaId) -> TCM a) -> TCM a
`catchIlltypedPatternBlockedOnMeta` \(TCErr
err , MetaId
x) -> do
            VerboseKey -> VerboseLevel -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.term" VerboseLevel
50 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
vcat ([TCM Doc] -> TCM Doc) -> [TCM Doc] -> TCM Doc
forall a b. (a -> b) -> a -> b
$
              [ TCM Doc
"checking record pattern stuck on meta: " TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> VerboseKey -> TCM Doc
forall (m :: * -> *). Monad m => VerboseKey -> m Doc
text (MetaId -> VerboseKey
forall a. Show a => a -> VerboseKey
show MetaId
x) ]
            Type
t1 <- ([NamedArg Name], Type) -> TCM Type -> TCM Type
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext ([NamedArg Name]
xs, Type
argsT) (TCM Type -> TCM Type) -> TCM Type -> TCM Type
forall a b. (a -> b) -> a -> b
$ TCM Type -> TCM Type
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 -> TCMT IO Bool -> TCM Term
postponeTypeCheckingProblem (Comparison -> Expr -> Type -> TypeCheckingProblem
CheckExpr Comparison
cmp Expr
e Type
tgt') (TCMT IO Bool -> TCM Term) -> TCMT IO Bool -> TCM Term
forall a b. (a -> b) -> a -> b
$ MetaId -> TCMT IO Bool
forall a (m :: * -> *).
(IsInstantiatedMeta a, MonadFail m, ReadTCState m) =>
a -> m Bool
isInstantiatedMeta MetaId
x
            (Type, Term) -> TCM (Type, Term)
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 (TCM (Type, Term) -> TCM (Type, Term))
-> TCM (Type, Term) -> TCM (Type, Term)
forall a b. (a -> b) -> a -> b
$
         ([NamedArg Name], Type) -> TCM (Type, Term) -> TCM (Type, Term)
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext ([NamedArg Name]
xs, Type
argsT) (TCM (Type, Term) -> TCM (Type, Term))
-> TCM (Type, Term) -> TCM (Type, Term)
forall a b. (a -> b) -> a -> b
$ [NamedArg Binder] -> TCM (Type, Term) -> TCM (Type, Term)
forall a. [NamedArg Binder] -> TCM a -> TCM a
addTypedPatterns [NamedArg Binder]
xps (TCM (Type, Term) -> TCM (Type, Term))
-> TCM (Type, Term) -> TCM (Type, Term)
forall a b. (a -> b) -> a -> b
$ do
           Type
t1 <- TCM Type -> TCM Type
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
           (Type, Term) -> TCM (Type, Term)
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 ArgInfo -> Bool
forall a. LensHiding a => a -> Bool
notVisible ArgInfo
info Bool -> Bool -> Bool
|| (NamedArg Name -> Bool) -> [NamedArg Name] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any NamedArg Name -> Bool
forall a. LensHiding a => a -> Bool
notVisible [NamedArg Name]
xs then do
        ProblemId
pid <- TCM () -> TCMT IO ProblemId
forall (m :: * -> *) a.
(MonadFresh ProblemId m, MonadConstraint m) =>
m a -> m ProblemId
newProblem_ (TCM () -> TCMT IO ProblemId) -> TCM () -> TCMT IO ProblemId
forall a b. (a -> b) -> a -> b
$ Type -> Type -> TCM ()
forall (m :: * -> *). MonadConversion m => Type -> Type -> m ()
leqType Type
target0 Type
target
        Type -> Term -> ProblemId -> TCM Term
forall (m :: * -> *).
(MonadMetaSolver m, MonadFresh VerboseLevel m) =>
Type -> Term -> ProblemId -> m Term
blockTermOnProblem Type
target Term
w ProblemId
pid
      else do
        Comparison -> Term -> Type -> Type -> TCM Term
forall (m :: * -> *).
(MonadConversion m, MonadTCM m) =>
Comparison -> Term -> Type -> Type -> m Term
coerce Comparison
cmp Term
w Type
target0 Type
target


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

        let [NamedArg Name
x] = [NamedArg Name]
xs
        Bool -> TCM () -> TCM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Dom' t Type -> ArgInfo -> Bool
forall a b. (LensHiding a, LensHiding b) => a -> b -> Bool
sameHiding Dom' t Type
dom ArgInfo
info) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ TypeError -> TCM ()
forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m, MonadError TCErr m) =>
TypeError -> m a
typeError (TypeError -> TCM ()) -> TypeError -> TCM ()
forall a b. (a -> b) -> a -> b
$ Type -> TypeError
WrongHidingInLambda Type
target
        -- Andreas, 2011-10-01 ignore relevance in lambda if not explicitly given
        ArgInfo
info <- Dom' t Type -> ArgInfo -> TCM ArgInfo
forall dom. LensModality dom => dom -> ArgInfo -> TCM ArgInfo
lambdaModalityCheck Dom' t 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 = Dom' t Type -> Type
forall t e. Dom' t e -> e
unDom Dom' t Type
dom
        Term -> TCM ()
checkSizeLtSat (Term -> TCM ()) -> Term -> TCM ()
forall a b. (a -> b) -> a -> b
$ Type -> Term
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) <- TCM Type -> TCMT IO (ProblemId, Type)
forall (m :: * -> *) a.
(MonadFresh ProblemId m, MonadConstraint m) =>
m a -> m (ProblemId, a)
newProblem (TCM Type -> TCMT IO (ProblemId, Type))
-> TCM Type -> TCMT IO (ProblemId, Type)
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 <- Name -> VerboseKey -> Dom Type -> TCM Term -> TCM Term
forall a. Name -> VerboseKey -> Dom Type -> TCM a -> TCM a
lambdaAddContext (NamedArg Name -> Name
forall a. NamedArg a -> a
namedArg NamedArg Name
x) VerboseKey
y (ArgInfo -> Type -> Dom Type
forall a. ArgInfo -> a -> Dom a
defaultArgDom ArgInfo
info Type
argT) (TCM Term -> TCM Term) -> TCM Term -> TCM Term
forall a b. (a -> b) -> a -> b
$
               [NamedArg Binder] -> TCM Term -> TCM Term
forall a. [NamedArg Binder] -> TCM a -> TCM a
addTypedPatterns [NamedArg Binder]
xps (TCM Term -> TCM Term) -> TCM Term -> TCM Term
forall a b. (a -> b) -> a -> b
$ Comparison -> Expr -> Type -> TCM Term
checkExpr' Comparison
cmp Expr
body Type
btyp
        Type -> Term -> ProblemId -> TCM Term
forall (m :: * -> *).
(MonadMetaSolver m, MonadFresh VerboseLevel m) =>
Type -> Term -> ProblemId -> m Term
blockTermOnProblem Type
target (ArgInfo -> Abs Term -> Term
Lam ArgInfo
info (Abs Term -> Term) -> Abs Term -> Term
forall a b. (a -> b) -> a -> b
$ VerboseKey -> Term -> Abs Term
forall a. VerboseKey -> a -> Abs a
Abs (NamedArg Name -> VerboseKey
namedArgName NamedArg Name
x) Term
v) ProblemId
pid

    useTargetType Tele (Dom' t Type)
_ Type
_ = TCM Term
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 :: LensModality dom => dom -> ArgInfo -> TCM ArgInfo
lambdaModalityCheck :: dom -> ArgInfo -> TCM ArgInfo
lambdaModalityCheck dom
dom = Modality -> ArgInfo -> TCM ArgInfo
forall dom. LensCohesion dom => dom -> ArgInfo -> TCM ArgInfo
lambdaCohesionCheck Modality
m (ArgInfo -> TCM ArgInfo)
-> (ArgInfo -> TCM ArgInfo) -> ArgInfo -> TCM ArgInfo
forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< Modality -> ArgInfo -> TCM ArgInfo
forall dom. LensQuantity dom => dom -> ArgInfo -> TCM ArgInfo
lambdaQuantityCheck Modality
m (ArgInfo -> TCM ArgInfo)
-> (ArgInfo -> TCM ArgInfo) -> ArgInfo -> TCM ArgInfo
forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< Modality -> ArgInfo -> TCM ArgInfo
forall dom. LensRelevance dom => dom -> ArgInfo -> TCM ArgInfo
lambdaIrrelevanceCheck Modality
m
  where m :: Modality
m = dom -> Modality
forall a. LensModality a => a -> Modality
getModality dom
dom

-- | Check that irrelevance info in lambda is compatible with irrelevance
--   coming from the function type.
--   If lambda has no user-given relevance, copy that of function type.
lambdaIrrelevanceCheck :: LensRelevance dom => dom -> ArgInfo -> TCM ArgInfo
lambdaIrrelevanceCheck :: dom -> ArgInfo -> TCM ArgInfo
lambdaIrrelevanceCheck dom
dom ArgInfo
info
    -- Case: no specific user annotation: use relevance of function type
  | ArgInfo -> Relevance
forall a. LensRelevance a => a -> Relevance
getRelevance ArgInfo
info Relevance -> Relevance -> Bool
forall a. Eq a => a -> a -> Bool
== Relevance
defaultRelevance = ArgInfo -> TCM ArgInfo
forall (m :: * -> *) a. Monad m => a -> m a
return (ArgInfo -> TCM ArgInfo) -> ArgInfo -> TCM ArgInfo
forall a b. (a -> b) -> a -> b
$ Relevance -> ArgInfo -> ArgInfo
forall a. LensRelevance a => Relevance -> a -> a
setRelevance (dom -> Relevance
forall a. LensRelevance a => a -> Relevance
getRelevance dom
dom) ArgInfo
info
    -- Case: explicit user annotation is taken seriously
  | Bool
otherwise = do
      let rPi :: Relevance
rPi  = dom -> Relevance
forall a. LensRelevance a => a -> Relevance
getRelevance dom
dom  -- relevance of function type
      let rLam :: Relevance
rLam = ArgInfo -> Relevance
forall a. LensRelevance a => a -> Relevance
getRelevance ArgInfo
info -- relevance of lambda
        -- Andreas, 2017-01-24, issue #2429
        -- we should report an error if we try to check a relevant function
        -- against an irrelevant function type (subtyping violation)
      Bool -> TCM () -> TCM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Relevance -> Relevance -> Bool
moreRelevant Relevance
rPi Relevance
rLam) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ do
        -- @rLam == Relevant@ is impossible here
        -- @rLam == Irrelevant@ is impossible here (least relevant)
        -- this error can only happen if @rLam == NonStrict@ and @rPi == Irrelevant@
        Bool -> TCM () -> TCM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Relevance
rLam Relevance -> Relevance -> Bool
forall a. Eq a => a -> a -> Bool
== Relevance
NonStrict) TCM ()
forall a. HasCallStack => a
__IMPOSSIBLE__  -- separate tests for separate line nums
        Bool -> TCM () -> TCM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Relevance
rPi Relevance -> Relevance -> Bool
forall a. Eq a => a -> a -> Bool
== Relevance
Irrelevant) TCM ()
forall a. HasCallStack => a
__IMPOSSIBLE__
        TypeError -> TCM ()
forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m, MonadError TCErr m) =>
TypeError -> m a
typeError TypeError
WrongIrrelevanceInLambda
      ArgInfo -> TCM ArgInfo
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 :: dom -> ArgInfo -> TCM ArgInfo
lambdaQuantityCheck dom
dom ArgInfo
info
    -- Case: no specific user annotation: use quantity of function type
  | ArgInfo -> Bool
forall a. LensQuantity a => a -> Bool
noUserQuantity ArgInfo
info = ArgInfo -> TCM ArgInfo
forall (m :: * -> *) a. Monad m => a -> m a
return (ArgInfo -> TCM ArgInfo) -> ArgInfo -> TCM ArgInfo
forall a b. (a -> b) -> a -> b
$ Quantity -> ArgInfo -> ArgInfo
forall a. LensQuantity a => Quantity -> a -> a
setQuantity (dom -> Quantity
forall a. LensQuantity a => a -> Quantity
getQuantity dom
dom) ArgInfo
info
    -- Case: explicit user annotation is taken seriously
  | Bool
otherwise = do
      let qPi :: Quantity
qPi  = dom -> Quantity
forall a. LensQuantity a => a -> Quantity
getQuantity dom
dom  -- quantity of function type
      let qLam :: Quantity
qLam = ArgInfo -> Quantity
forall a. LensQuantity a => a -> Quantity
getQuantity ArgInfo
info -- quantity of lambda
      Bool -> TCM () -> TCM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Quantity
qPi Quantity -> Quantity -> Bool
`moreQuantity` Quantity
qLam) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ do
        TypeError -> TCM ()
forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m, MonadError TCErr m) =>
TypeError -> m a
typeError TypeError
WrongQuantityInLambda
      ArgInfo -> TCM ArgInfo
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 :: dom -> ArgInfo -> TCM ArgInfo
lambdaCohesionCheck dom
dom ArgInfo
info
    -- Case: no specific user annotation: use cohesion of function type
  | ArgInfo -> Cohesion
forall a. LensCohesion a => a -> Cohesion
getCohesion ArgInfo
info Cohesion -> Cohesion -> Bool
forall a. Eq a => a -> a -> Bool
== Cohesion
defaultCohesion = ArgInfo -> TCM ArgInfo
forall (m :: * -> *) a. Monad m => a -> m a
return (ArgInfo -> TCM ArgInfo) -> ArgInfo -> TCM ArgInfo
forall a b. (a -> b) -> a -> b
$ Cohesion -> ArgInfo -> ArgInfo
forall a. LensCohesion a => Cohesion -> a -> a
setCohesion (dom -> Cohesion
forall a. LensCohesion a => a -> Cohesion
getCohesion dom
dom) ArgInfo
info
    -- Case: explicit user annotation is taken seriously
  | Bool
otherwise = do
      let cPi :: Cohesion
cPi  = dom -> Cohesion
forall a. LensCohesion a => a -> Cohesion
getCohesion dom
dom  -- cohesion of function type
      let cLam :: Cohesion
cLam = ArgInfo -> Cohesion
forall a. LensCohesion a => a -> Cohesion
getCohesion ArgInfo
info -- cohesion of lambda
      Bool -> TCM () -> TCM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Cohesion
cPi Cohesion -> Cohesion -> Bool
`sameCohesion` Cohesion
cLam) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ do
        -- if there is a cohesion annotation then
        -- it better match the domain.
        TypeError -> TCM ()
forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m, MonadError TCErr m) =>
TypeError -> m a
typeError TypeError
WrongCohesionInLambda
      ArgInfo -> TCM ArgInfo
forall (m :: * -> *) a. Monad m => a -> m a
return ArgInfo
info

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


-- | 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.
  -> (MetaId -> 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
-> (MetaId -> Type -> TCM Term)
-> (Type -> TCM Term)
-> TCM Term
insertHiddenLambdas Hiding
h Type
target MetaId -> 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.
  Type
-> (MetaId -> Type -> TCM Term)
-> (NotBlocked -> Type -> TCM Term)
-> TCM Term
forall t (m :: * -> *) a.
(Reduce t, IsMeta t, MonadReduce m, HasBuiltins m) =>
t -> (MetaId -> t -> m a) -> (NotBlocked -> t -> m a) -> m a
ifBlocked Type
target MetaId -> Type -> TCM Term
postpone ((NotBlocked -> Type -> TCM Term) -> TCM Term)
-> (NotBlocked -> Type -> TCM Term) -> TCM Term
forall a b. (a -> b) -> a -> b
$ \ NotBlocked
_ Type
t -> do
    case Type -> Term
forall t a. Type'' t a -> a
unEl Type
t of

      Pi Dom Type
dom Abs Type
b -> do
        let h' :: Hiding
h' = Dom Type -> Hiding
forall a. LensHiding a => a -> Hiding
getHiding Dom Type
dom
        -- Found expected hiding: return function type.
        if Hiding -> Hiding -> Bool
forall a b. (LensHiding a, LensHiding b) => a -> b -> Bool
sameHiding Hiding
h Hiding
h' then Type -> 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 Hiding -> Bool
forall a. LensHiding a => a -> Bool
visible Hiding
h' then TypeError -> TCM Term
forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m, MonadError TCErr m) =>
TypeError -> m a
typeError (TypeError -> TCM Term) -> TypeError -> TCM Term
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 :: VerboseKey
x    = Abs Type -> VerboseKey
forall a. Abs a -> VerboseKey
absName Abs Type
b
            ArgInfo -> Abs Term -> Term
Lam (Origin -> ArgInfo -> ArgInfo
forall a. LensOrigin a => Origin -> a -> a
setOrigin Origin
Inserted (ArgInfo -> ArgInfo) -> ArgInfo -> ArgInfo
forall a b. (a -> b) -> a -> b
$ Dom Type -> ArgInfo
forall t e. Dom' t e -> ArgInfo
domInfo Dom Type
dom) (Abs Term -> Term) -> (Term -> Abs Term) -> Term -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. VerboseKey -> Term -> Abs Term
forall a. VerboseKey -> a -> Abs a
Abs VerboseKey
x (Term -> Term) -> TCM Term -> TCM Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do
              (VerboseKey, Dom Type) -> TCM Term -> TCM Term
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext (VerboseKey
x, Dom Type
dom) (TCM Term -> TCM Term) -> TCM Term -> TCM Term
forall a b. (a -> b) -> a -> b
$ Hiding
-> Type
-> (MetaId -> Type -> TCM Term)
-> (Type -> TCM Term)
-> TCM Term
insertHiddenLambdas Hiding
h (Abs Type -> Type
forall t a. Subst t a => Abs a -> a
absBody Abs Type
b) MetaId -> Type -> TCM Term
postpone Type -> TCM Term
ret

      Term
_ -> TypeError -> TCM Term
forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m, MonadError TCErr m) =>
TypeError -> m a
typeError (TypeError -> TCM Term) -> (Doc -> TypeError) -> Doc -> TCM Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> TypeError
GenericDocError (Doc -> TCM Term) -> TCM Doc -> TCM Term
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< do
        TCM Doc
"Expected " TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Type -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
target TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCM 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 = (TCEnv -> TCEnv) -> TCM Term -> TCM Term
forall (m :: * -> *) a.
MonadTCEnv m =>
(TCEnv -> TCEnv) -> m a -> m a
localTC (Lens' Quantity TCEnv -> LensSet Quantity TCEnv
forall i o. Lens' i o -> LensSet i o
set Lens' Quantity TCEnv
eQuantity Quantity
topQuantity) (TCM Term -> TCM Term) -> TCM Term -> TCM Term
forall a b. (a -> b) -> a -> b
$ do
      -- Andreas, 2019-10-01: check absurd lambdas in non-erased mode.
      -- Otherwise, they are not usable in meta-solutions in the term world.
      -- See test/Succeed/Issue3176.agda for an absurd lambda
      -- created in types.
  Type
t <- Type -> TCM Type
forall a (m :: * -> *).
(InstantiateFull a, MonadReduce m) =>
a -> m a
instantiateFull Type
t
  Type
-> (MetaId -> Type -> TCM Term)
-> (NotBlocked -> Type -> TCM Term)
-> TCM Term
forall t (m :: * -> *) a.
(Reduce t, IsMeta t, MonadReduce m, HasBuiltins m) =>
t -> (MetaId -> t -> m a) -> (NotBlocked -> t -> m a) -> m a
ifBlocked Type
t (\ MetaId
m Type
t' -> TypeCheckingProblem -> TCM Term
postponeTypeCheckingProblem_ (TypeCheckingProblem -> TCM Term)
-> TypeCheckingProblem -> TCM Term
forall a b. (a -> b) -> a -> b
$ Comparison -> Expr -> Type -> TypeCheckingProblem
CheckExpr Comparison
cmp Expr
e Type
t') ((NotBlocked -> Type -> TCM Term) -> TCM Term)
-> (NotBlocked -> Type -> TCM Term) -> TCM Term
forall a b. (a -> b) -> a -> b
$ \ NotBlocked
_ Type
t' -> do
    case Type -> Term
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 (Hiding -> ArgInfo -> Bool
forall a b. (LensHiding a, LensHiding b) => a -> b -> Bool
sameHiding Hiding
h ArgInfo
info') -> TypeError -> TCM Term
forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m, MonadError TCErr m) =>
TypeError -> m a
typeError (TypeError -> TCM Term) -> TypeError -> TCM Term
forall a b. (a -> b) -> a -> b
$ Type -> TypeError
WrongHidingInLambda Type
t'
        | Bool -> Bool
not (Type -> Bool
forall a. TermLike a => a -> Bool
noMetas Type
a) ->
            TypeCheckingProblem -> TCMT IO Bool -> TCM Term
postponeTypeCheckingProblem (Comparison -> Expr -> Type -> TypeCheckingProblem
CheckExpr Comparison
cmp Expr
e Type
t') (TCMT IO Bool -> TCM Term) -> TCMT IO Bool -> TCM Term
forall a b. (a -> b) -> a -> b
$
              Type -> Bool
forall a. TermLike a => a -> Bool
noMetas (Type -> Bool) -> TCM Type -> TCMT IO Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type -> TCM Type
forall a (m :: * -> *).
(InstantiateFull a, MonadReduce m) =>
a -> m a
instantiateFull Type
a
        | Bool
otherwise -> Type -> TCM Term -> TCM Term
forall (m :: * -> *).
(MonadMetaSolver m, MonadConstraint m, MonadFresh VerboseLevel m,
 MonadFresh ProblemId m) =>
Type -> m Term -> m Term
blockTerm Type
t' (TCM Term -> TCM Term) -> TCM Term -> TCM Term
forall a b. (a -> b) -> a -> b
$ do
          Range -> Type -> TCM ()
ensureEmptyType (ExprInfo -> Range
forall t. HasRange t => t -> Range
getRange ExprInfo
i) Type
a
          -- Add helper function
          ModuleName
top <- TCMT IO ModuleName
forall (m :: * -> *). MonadTCEnv m => m ModuleName
currentModule
          QName
aux <- ModuleName -> Name -> QName
qualify ModuleName
top (Name -> QName) -> TCMT IO Name -> TCMT IO QName
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Range, VerboseKey) -> TCMT IO Name
forall a (m :: * -> *).
(FreshName a, MonadFresh NameId m) =>
a -> m Name
freshName_ (ExprInfo -> Range
forall t. HasRange t => t -> Range
getRange ExprInfo
i, VerboseKey
absurdLambdaName)
          -- if we are in irrelevant / erased position, the helper function
          -- is added as irrelevant / erased
          Modality
mod <- (TCEnv -> Modality) -> TCMT IO Modality
forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
asksTC TCEnv -> Modality
forall a. LensModality a => a -> Modality
getModality
          VerboseKey -> VerboseLevel -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.term.absurd" VerboseLevel
10 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
vcat
            [ (TCM Doc
"Adding absurd function" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Modality -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Modality
mod) TCM Doc -> TCM Doc -> TCM Doc
forall a. Semigroup a => a -> a -> a
<> QName -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
aux
            , VerboseLevel -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest VerboseLevel
2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ TCM Doc
"of type" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Type -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
t'
            ]
          QName -> Definition -> TCM ()
addConstant QName
aux (Definition -> TCM ()) -> Definition -> TCM ()
forall a b. (a -> b) -> a -> b
$
            (\ Defn
d -> (ArgInfo -> QName -> Type -> Defn -> Definition
defaultDefn (Modality -> ArgInfo -> ArgInfo
forall a. LensModality a => Modality -> a -> a
setModality Modality
mod ArgInfo
info') QName
aux Type
t' Defn
d)
                    { defPolarity :: [Polarity]
defPolarity       = [Polarity
Nonvariant]
                    , defArgOccurrences :: [Occurrence]
defArgOccurrences = [Occurrence
Unused] })
            (Defn -> Definition) -> Defn -> Definition
forall a b. (a -> b) -> a -> b
$ Defn
emptyFunction
              { funClauses :: [Clause]
funClauses        =
                  [ Clause :: Range
-> Range
-> Telescope
-> NAPs
-> Maybe Term
-> Maybe (Arg Type)
-> Bool
-> Maybe Bool
-> Maybe Bool
-> ExpandedEllipsis
-> Clause
Clause
                    { clauseLHSRange :: Range
clauseLHSRange  = Expr -> Range
forall t. HasRange t => t -> Range
getRange Expr
e
                    , clauseFullRange :: Range
clauseFullRange = Expr -> Range
forall t. HasRange t => t -> Range
getRange Expr
e
                    , clauseTel :: Telescope
clauseTel       = ListTel -> Telescope
telFromList [(Type -> (VerboseKey, Type))
-> Dom Type -> Dom' Term (VerboseKey, Type)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (VerboseKey
absurdPatternName,) Dom Type
dom]
                    , namedClausePats :: NAPs
namedClausePats = [ArgInfo
-> Named (WithOrigin (Ranged VerboseKey)) DeBruijnPattern
-> Arg (Named (WithOrigin (Ranged VerboseKey)) DeBruijnPattern)
forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
info' (Named (WithOrigin (Ranged VerboseKey)) DeBruijnPattern
 -> Arg (Named (WithOrigin (Ranged VerboseKey)) DeBruijnPattern))
-> Named (WithOrigin (Ranged VerboseKey)) DeBruijnPattern
-> Arg (Named (WithOrigin (Ranged VerboseKey)) DeBruijnPattern)
forall a b. (a -> b) -> a -> b
$ Maybe (WithOrigin (Ranged VerboseKey))
-> DeBruijnPattern
-> Named (WithOrigin (Ranged VerboseKey)) DeBruijnPattern
forall name a. Maybe name -> a -> Named name a
Named (WithOrigin (Ranged VerboseKey)
-> Maybe (WithOrigin (Ranged VerboseKey))
forall a. a -> Maybe a
Just (WithOrigin (Ranged VerboseKey)
 -> Maybe (WithOrigin (Ranged VerboseKey)))
-> WithOrigin (Ranged VerboseKey)
-> Maybe (WithOrigin (Ranged VerboseKey))
forall a b. (a -> b) -> a -> b
$ Origin -> Ranged VerboseKey -> WithOrigin (Ranged VerboseKey)
forall a. Origin -> a -> WithOrigin a
WithOrigin Origin
Inserted (Ranged VerboseKey -> WithOrigin (Ranged VerboseKey))
-> Ranged VerboseKey -> WithOrigin (Ranged VerboseKey)
forall a b. (a -> b) -> a -> b
$ VerboseKey -> Ranged VerboseKey
forall a. a -> Ranged a
unranged (VerboseKey -> Ranged VerboseKey)
-> VerboseKey -> Ranged VerboseKey
forall a b. (a -> b) -> a -> b
$ Abs Type -> VerboseKey
forall a. Abs a -> VerboseKey
absName Abs Type
b) (DeBruijnPattern
 -> Named (WithOrigin (Ranged VerboseKey)) DeBruijnPattern)
-> DeBruijnPattern
-> Named (WithOrigin (Ranged VerboseKey)) DeBruijnPattern
forall a b. (a -> b) -> a -> b
$ VerboseLevel -> DeBruijnPattern
absurdP VerboseLevel
0]
                    , clauseBody :: Maybe Term
clauseBody      = Maybe Term
forall a. Maybe a
Nothing
                    , clauseType :: Maybe (Arg Type)
clauseType      = Arg Type -> Maybe (Arg Type)
forall a. a -> Maybe a
Just (Arg Type -> Maybe (Arg Type)) -> Arg Type -> Maybe (Arg Type)
forall a b. (a -> b) -> a -> b
$ Modality -> Arg Type -> Arg Type
forall a. LensModality a => Modality -> a -> a
setModality Modality
mod (Arg Type -> Arg Type) -> Arg Type -> Arg Type
forall a b. (a -> b) -> a -> b
$ Type -> Arg Type
forall e. e -> Arg e
defaultArg (Type -> Arg Type) -> Type -> Arg Type
forall a b. (a -> b) -> a -> b
$ Abs Type -> Type
forall t a. Subst t a => Abs a -> a
absBody Abs Type
b
                    , clauseCatchall :: Bool
clauseCatchall  = Bool
False
                    , clauseRecursive :: Maybe Bool
clauseRecursive   = Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
False
                    , clauseUnreachable :: Maybe Bool
clauseUnreachable = Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
True -- absurd clauses are unreachable
                    , clauseEllipsis :: ExpandedEllipsis
clauseEllipsis  = ExpandedEllipsis
NoEllipsis
                    }
                  ]
              , funCompiled :: Maybe CompiledClauses
funCompiled       = CompiledClauses -> Maybe CompiledClauses
forall a. a -> Maybe a
Just CompiledClauses
forall a. CompiledClauses' a
Fail
              , funSplitTree :: Maybe SplitTree
funSplitTree      = SplitTree -> Maybe SplitTree
forall a. a -> Maybe a
Just (SplitTree -> Maybe SplitTree) -> SplitTree -> Maybe SplitTree
forall a b. (a -> b) -> a -> b
$ VerboseLevel -> SplitTree
forall a. VerboseLevel -> SplitTree' a
SplittingDone VerboseLevel
0
              , funMutual :: Maybe [QName]
funMutual         = [QName] -> Maybe [QName]
forall a. a -> Maybe a
Just []
              , funTerminates :: Maybe Bool
funTerminates     = Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
True
              }
          -- Andreas 2012-01-30: since aux is lifted to toplevel
          -- it needs to be applied to the current telescope (issue 557)
          Telescope
tel <- TCMT IO Telescope
forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Telescope
getContextTelescope
          Term -> TCM Term
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> TCM Term) -> Term -> TCM Term
forall a b. (a -> b) -> a -> b
$ QName -> Elims -> Term
Def QName
aux (Elims -> Term) -> Elims -> Term
forall a b. (a -> b) -> a -> b
$ (Arg Term -> Elim' Term) -> [Arg Term] -> Elims
forall a b. (a -> b) -> [a] -> [b]
map Arg Term -> Elim' Term
forall a. Arg a -> Elim' a
Apply ([Arg Term] -> Elims) -> [Arg Term] -> Elims
forall a b. (a -> b) -> a -> b
$ Telescope -> [Arg Term]
forall a t. DeBruijn a => Tele (Dom t) -> [Arg a]
teleArgs Telescope
tel
      Term
_ -> TypeError -> TCM Term
forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m, MonadError TCErr m) =>
TypeError -> m a
typeError (TypeError -> TCM Term) -> TypeError -> TCM Term
forall a b. (a -> b) -> a -> b
$ Type -> TypeError
ShouldBePi Type
t'

-- | @checkExtendedLambda i di qname cs e t@ check pattern matching lambda.
-- Precondition: @e = ExtendedLam i di qname cs@
checkExtendedLambda :: Comparison -> A.ExprInfo -> A.DefInfo -> QName -> [A.Clause] ->
                       A.Expr -> Type -> TCM Term
checkExtendedLambda :: Comparison
-> ExprInfo
-> DefInfo
-> QName
-> [Clause]
-> Expr
-> Type
-> TCM Term
checkExtendedLambda Comparison
cmp ExprInfo
i DefInfo
di QName
qname [Clause]
cs Expr
e Type
t = (TCEnv -> TCEnv) -> TCM Term -> TCM Term
forall (m :: * -> *) a.
MonadTCEnv m =>
(TCEnv -> TCEnv) -> m a -> m a
localTC (Lens' Quantity TCEnv -> LensSet Quantity TCEnv
forall i o. Lens' i o -> LensSet i o
set Lens' Quantity TCEnv
eQuantity Quantity
topQuantity) (TCM Term -> TCM Term) -> TCM Term -> TCM Term
forall a b. (a -> b) -> a -> b
$ do
      -- Andreas, 2019-10-01: check extended lambdas in non-erased mode.
      -- Otherwise, they are not usable in meta-solutions in the term world.
      -- See test/Succeed/Issue{3581}.agda for an extended lambda
      -- created in a type.
   -- 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 <- TCMT IO ModuleName -> TCMT IO ModuleName
forall a. TCM a -> TCM a
inFreshModuleIfFreeParams TCMT IO ModuleName
forall (m :: * -> *). MonadTCEnv m => m ModuleName
currentModule  -- #2883: need a fresh module if refined params
   Type
t <- Type -> TCM Type
forall a (m :: * -> *).
(InstantiateFull a, MonadReduce m) =>
a -> m a
instantiateFull Type
t
   Type
-> (MetaId -> Type -> TCM Term)
-> (NotBlocked -> Type -> TCM Term)
-> TCM Term
forall t (m :: * -> *) a.
(Reduce t, IsMeta t, MonadReduce m, HasBuiltins m) =>
t -> (MetaId -> t -> m a) -> (NotBlocked -> t -> m a) -> m a
ifBlocked Type
t (\ MetaId
m Type
t' -> TypeCheckingProblem -> TCM Term
postponeTypeCheckingProblem_ (TypeCheckingProblem -> TCM Term)
-> TypeCheckingProblem -> TCM Term
forall a b. (a -> b) -> a -> b
$ Comparison -> Expr -> Type -> TypeCheckingProblem
CheckExpr Comparison
cmp Expr
e Type
t') ((NotBlocked -> Type -> TCM Term) -> TCM Term)
-> (NotBlocked -> Type -> TCM Term) -> TCM Term
forall a b. (a -> b) -> a -> b
$ \ NotBlocked
_ Type
t -> do
     MutualId
j   <- TCM MutualId
currentOrFreshMutualBlock
     Modality
mod <- (TCEnv -> Modality) -> TCMT IO Modality
forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
asksTC TCEnv -> Modality
forall a. LensModality a => a -> Modality
getModality
     let info :: ArgInfo
info = Modality -> ArgInfo -> ArgInfo
forall a. LensModality a => Modality -> a -> a
setModality Modality
mod ArgInfo
defaultArgInfo

     VerboseKey -> VerboseLevel -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.term.exlam" VerboseLevel
20 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$
       (VerboseKey -> TCM Doc
forall (m :: * -> *). Monad m => VerboseKey -> m Doc
text (IsAbstract -> VerboseKey
forall a. Show a => a -> VerboseKey
show (IsAbstract -> VerboseKey) -> IsAbstract -> VerboseKey
forall a b. (a -> b) -> a -> b
$ DefInfo -> IsAbstract
forall t. DefInfo' t -> IsAbstract
A.defAbstract DefInfo
di) TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+>
       TCM Doc
"extended lambda's implementation \"") TCM Doc -> TCM Doc -> TCM Doc
forall a. Semigroup a => a -> a -> a
<> QName -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
qname TCM Doc -> TCM Doc -> TCM Doc
forall a. Semigroup a => a -> a -> a
<>
       TCM Doc
"\" has type: " TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
$$ Type -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
t -- <+> " where clauses: " <+> text (show cs)
     [Arg Term]
args     <- TCMT IO [Arg Term]
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.
     (IsAbstract -> TCM Term -> TCM Term
forall (m :: * -> *) a. MonadTCEnv m => IsAbstract -> m a -> m a
abstract (DefInfo -> IsAbstract
forall t. DefInfo' t -> IsAbstract
A.defAbstract DefInfo
di) (TCM Term -> TCM Term) -> TCM Term -> TCM Term
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 (Definition -> TCM ()) -> TCMT IO Definition -> TCM ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< do
         Definition -> TCMT IO Definition
useTerPragma (Definition -> TCMT IO Definition)
-> Definition -> TCMT IO Definition
forall a b. (a -> b) -> a -> b
$
           (ArgInfo -> QName -> Type -> Defn -> Definition
defaultDefn ArgInfo
info QName
qname Type
t 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 (ExtLamInfo -> Maybe ExtLamInfo
forall a. a -> Maybe a
Just (ExtLamInfo -> Maybe ExtLamInfo) -> ExtLamInfo -> Maybe ExtLamInfo
forall a b. (a -> b) -> a -> b
$ ModuleName -> Maybe System -> ExtLamInfo
ExtLamInfo ModuleName
lamMod Maybe System
forall a. Null a => a
empty) Maybe QName
forall a. Maybe a
Nothing DefInfo
di QName
qname [Clause]
cs
       TCMT IO (Maybe MutualId) -> TCM () -> TCM ()
forall (m :: * -> *) a. Monad m => m (Maybe a) -> m () -> m ()
whenNothingM ((TCEnv -> Maybe MutualId) -> TCMT IO (Maybe MutualId)
forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
asksTC TCEnv -> Maybe MutualId
envMutualBlock) (TCM () -> TCM ()) -> TCM () -> TCM ()
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
       Term -> TCM Term
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> TCM Term) -> Term -> TCM Term
forall a b. (a -> b) -> a -> b
$ QName -> Elims -> Term
Def QName
qname (Elims -> Term) -> Elims -> Term
forall a b. (a -> b) -> a -> b
$ (Arg Term -> Elim' Term) -> [Arg Term] -> Elims
forall a b. (a -> b) -> [a] -> [b]
map Arg Term -> Elim' Term
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 = m a -> m a
forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
inConcreteMode
    abstract IsAbstract
AbstractDef = m a -> m a
forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
inAbstractMode

-- | Run a computation.
--
--   * If successful, that's it, we are done.
--
--   * If @IlltypedPattern p a@, @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, MetaId) -> TCM a) -> TCM a
catchIlltypedPatternBlockedOnMeta :: TCM a -> ((TCErr, MetaId) -> TCM a) -> TCM a
catchIlltypedPatternBlockedOnMeta TCM a
m (TCErr, MetaId) -> TCM a
handle = do

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

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

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

    -- Get the blocking meta responsible for the type error.
    -- If we do not find such a meta or the error should not be handled,
    -- we reraise the error.
    MetaId
x <- TCMT IO MetaId
-> (MetaId -> TCMT IO MetaId) -> Maybe MetaId -> TCMT IO MetaId
forall b a. b -> (a -> b) -> Maybe a -> b
maybe TCMT IO MetaId
forall a. TCMT IO a
reraise MetaId -> TCMT IO MetaId
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe MetaId -> TCMT IO MetaId)
-> TCMT IO (Maybe MetaId) -> TCMT IO MetaId
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< do
      case TCErr
err of
        TypeError TCState
s Closure TypeError
cl -> TCMT IO (Maybe MetaId) -> TCMT IO (Maybe MetaId)
forall a. TCM a -> TCM a
localTCState (TCMT IO (Maybe MetaId) -> TCMT IO (Maybe MetaId))
-> TCMT IO (Maybe MetaId) -> TCMT IO (Maybe MetaId)
forall a b. (a -> b) -> a -> b
$ do
          TCState -> TCM ()
forall (m :: * -> *). MonadTCState m => TCState -> m ()
putTC TCState
s
          Closure TypeError
-> (TypeError -> TCMT IO (Maybe MetaId)) -> TCMT IO (Maybe MetaId)
forall (m :: * -> *) a c b.
(MonadTCEnv m, ReadTCState m, LensClosure a c) =>
c -> (a -> m b) -> m b
enterClosure Closure TypeError
cl ((TypeError -> TCMT IO (Maybe MetaId)) -> TCMT IO (Maybe MetaId))
-> (TypeError -> TCMT IO (Maybe MetaId)) -> TCMT IO (Maybe MetaId)
forall a b. (a -> b) -> a -> b
$ \case
            IlltypedPattern Pattern
p Type
a -> Type -> TCMT IO (Maybe MetaId)
forall t (m :: * -> *).
(Reduce t, IsMeta t, MonadReduce m, HasBuiltins m) =>
t -> m (Maybe MetaId)
isBlocked Type
a

            SplitError (UnificationStuck QName
c Telescope
tel [Arg Term]
us [Arg Term]
vs [UnificationFailure]
_) -> do
              -- Andreas, 2018-11-23, re issue #3403
              -- The following computation of meta-variables and picking
              -- of the first one, seems a bit brittle.
              -- I do not understand why there is a single @reduce@ here
              -- (seems to archieve a bit along @normalize@, but how much??).
              ([Dom Type], [Arg Term], [Arg Term])
problem <- ([Dom Type], [Arg Term], [Arg Term])
-> TCMT IO ([Dom Type], [Arg Term], [Arg Term])
forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce (([Dom Type], [Arg Term], [Arg Term])
 -> TCMT IO ([Dom Type], [Arg Term], [Arg Term]))
-> TCMT IO ([Dom Type], [Arg Term], [Arg Term])
-> TCMT IO ([Dom Type], [Arg Term], [Arg Term])
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< ([Dom Type], [Arg Term], [Arg Term])
-> TCMT IO ([Dom Type], [Arg Term], [Arg Term])
forall a (m :: * -> *).
(InstantiateFull a, MonadReduce m) =>
a -> m a
instantiateFull (Telescope -> [Dom Type]
forall a. Subst Term a => Tele (Dom a) -> [Dom a]
flattenTel Telescope
tel, [Arg Term]
us, [Arg Term]
vs)
              -- over-approximating the set of metas actually blocking unification
              Maybe MetaId -> TCMT IO (Maybe MetaId)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe MetaId -> TCMT IO (Maybe MetaId))
-> Maybe MetaId -> TCMT IO (Maybe MetaId)
forall a b. (a -> b) -> a -> b
$ ([Dom Type], [Arg Term], [Arg Term]) -> Maybe MetaId
forall a. TermLike a => a -> Maybe MetaId
firstMeta ([Dom Type], [Arg Term], [Arg Term])
problem

            SplitError (NotADatatype Closure Type
aClosure) ->
              Closure Type
-> (Type -> TCMT IO (Maybe MetaId)) -> TCMT IO (Maybe MetaId)
forall (m :: * -> *) a c b.
(MonadTCEnv m, ReadTCState m, LensClosure a c) =>
c -> (a -> m b) -> m b
enterClosure Closure Type
aClosure ((Type -> TCMT IO (Maybe MetaId)) -> TCMT IO (Maybe MetaId))
-> (Type -> TCMT IO (Maybe MetaId)) -> TCMT IO (Maybe MetaId)
forall a b. (a -> b) -> a -> b
$ \ Type
a -> Type -> TCMT IO (Maybe MetaId)
forall t (m :: * -> *).
(Reduce t, IsMeta t, MonadReduce m, HasBuiltins m) =>
t -> m (Maybe MetaId)
isBlocked Type
a

            -- Andrea: TODO look for blocking meta in tClosure and its Sort.
            -- SplitError (CannotCreateMissingClause _ _ _ tClosure) ->

            CannotEliminateWithPattern NamedArg Pattern
p Type
a -> Type -> TCMT IO (Maybe MetaId)
forall t (m :: * -> *).
(Reduce t, IsMeta t, MonadReduce m, HasBuiltins m) =>
t -> m (Maybe MetaId)
isBlocked Type
a

            TypeError
_ -> Maybe MetaId -> TCMT IO (Maybe MetaId)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe MetaId
forall a. Maybe a
Nothing
        TCErr
_ -> Maybe MetaId -> TCMT IO (Maybe MetaId)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe MetaId
forall a. Maybe a
Nothing

    VerboseKey -> VerboseLevel -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.postpone" VerboseLevel
20 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
vcat ([TCM Doc] -> TCM Doc) -> [TCM Doc] -> TCM Doc
forall a b. (a -> b) -> a -> b
$
      [ TCM Doc
"checking definition blocked on meta: " TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> MetaId -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM MetaId
x ]

    -- 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!
    TCState -> TCM ()
forall (m :: * -> *). MonadTCState m => TCState -> m ()
putTC TCState
st

    -- The meta might not be known in the reset state, as it could have been created
    -- somewhere on the way to the type error.
    MetaId -> TCMT IO (Maybe MetaVariable)
forall (m :: * -> *).
ReadTCState m =>
MetaId -> m (Maybe MetaVariable)
lookupMeta' MetaId
x TCMT IO (Maybe MetaVariable)
-> (Maybe MetaVariable -> TCM a) -> TCM a
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
      -- Case: we do not know the meta, so we reraise.
      Maybe MetaVariable
Nothing -> TCM a
forall a. TCMT IO a
reraise
      -- Case: we know the meta here.
      -- 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
      -- Just m | InstV{} <- mvInstantiation m -> __IMPOSSIBLE__  -- It cannot be instantiated yet.
      Just MetaVariable
m | InstV{} <- MetaVariable -> MetaInstantiation
mvInstantiation MetaVariable
m -> TCM a
forall a. TCMT IO a
reraise
      -- Case: the meta is frozen (and not an interaction meta).
      -- Postponing doesn't make sense, so we reraise.
      Just MetaVariable
m | Frozen
Frozen  <- MetaVariable -> Frozen
mvFrozen MetaVariable
m -> MetaId -> TCMT IO (Maybe InteractionId)
forall (m :: * -> *).
ReadTCState m =>
MetaId -> m (Maybe InteractionId)
isInteractionMeta MetaId
x TCMT IO (Maybe InteractionId)
-> (Maybe InteractionId -> TCM a) -> TCM a
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
        Maybe InteractionId
Nothing -> TCM a
forall a. TCMT IO a
reraise
      -- Remaining cases: the meta is known and can still be instantiated.
        Just{}  -> (TCErr, MetaId) -> TCM a
handle (TCErr
err, MetaId
x)
      Just{} -> (TCErr, MetaId) -> TCM a
handle (TCErr
err, MetaId
x)

---------------------------------------------------------------------------
-- * 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 Assign ModuleName] -> [Name] -> TCM Assigns
expandModuleAssigns [Either Assign ModuleName]
mfs [Name]
xs = do
  let (Assigns
fs , [ModuleName]
ms) = [Either Assign ModuleName] -> (Assigns, [ModuleName])
forall a b. [Either a b] -> ([a], [b])
partitionEithers [Either Assign 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 Assign]
fs' <- [Name]
-> (Name -> TCMT IO (Maybe Assign)) -> TCMT IO [Maybe Assign]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM ([Name]
xs [Name] -> [Name] -> [Name]
forall a. Eq a => [a] -> [a] -> [a]
List.\\ (Assign -> Name) -> Assigns -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map (Lens' Name Assign -> Assign -> Name
forall o (m :: * -> *) i. MonadReader o m => Lens' i o -> m i
view forall a. Lens' Name (FieldAssignment' a)
Lens' Name Assign
nameFieldA) Assigns
fs) ((Name -> TCMT IO (Maybe Assign)) -> TCMT IO [Maybe Assign])
-> (Name -> TCMT IO (Maybe Assign)) -> TCMT IO [Maybe Assign]
forall a b. (a -> b) -> a -> b
$ \ Name
f -> do

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

    -- If we have several matching assignments, that's an error.
    case [Maybe (ModuleName, Assign)] -> [(ModuleName, Assign)]
forall a. [Maybe a] -> [a]
catMaybes [Maybe (ModuleName, Assign)]
pms of
      []        -> Maybe Assign -> TCMT IO (Maybe Assign)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe Assign
forall a. Maybe a
Nothing
      [(ModuleName
_, Assign
fa)] -> Maybe Assign -> TCMT IO (Maybe Assign)
forall (m :: * -> *) a. Monad m => a -> m a
return (Assign -> Maybe Assign
forall a. a -> Maybe a
Just Assign
fa)
      [(ModuleName, Assign)]
mfas      -> TypeError -> TCMT IO (Maybe Assign)
forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m, MonadError TCErr m) =>
TypeError -> m a
typeError (TypeError -> TCMT IO (Maybe Assign))
-> (Doc -> TypeError) -> Doc -> TCMT IO (Maybe Assign)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> TypeError
GenericDocError (Doc -> TCMT IO (Maybe Assign))
-> TCM Doc -> TCMT IO (Maybe Assign)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< do
        [TCM Doc] -> TCM Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
vcat ([TCM Doc] -> TCM Doc) -> [TCM Doc] -> TCM Doc
forall a b. (a -> b) -> a -> b
$
          [ TCM Doc
"Ambiguity: the field" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Name -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Name
f
            TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCM Doc
"appears in the following modules: " ]
          [TCM Doc] -> [TCM Doc] -> [TCM Doc]
forall a. [a] -> [a] -> [a]
++ ((ModuleName, Assign) -> TCM Doc)
-> [(ModuleName, Assign)] -> [TCM Doc]
forall a b. (a -> b) -> [a] -> [b]
map (ModuleName -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM (ModuleName -> TCM Doc)
-> ((ModuleName, Assign) -> ModuleName)
-> (ModuleName, Assign)
-> TCM Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ModuleName, Assign) -> ModuleName
forall a b. (a, b) -> a
fst) [(ModuleName, Assign)]
mfas
  Assigns -> TCM Assigns
forall (m :: * -> *) a. Monad m => a -> m a
return (Assigns
fs Assigns -> Assigns -> Assigns
forall a. [a] -> [a] -> [a]
++ [Maybe Assign] -> Assigns
forall a. [Maybe a] -> [a]
catMaybes [Maybe Assign]
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 Assign ModuleName] -> Expr -> Type -> TCM Term
checkRecordExpression Comparison
cmp [Either Assign ModuleName]
mfs Expr
e Type
t = do
  VerboseKey -> VerboseLevel -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.term.rec" VerboseLevel
10 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
sep
    [ TCM Doc
"checking record expression"
    , Expr -> TCM Doc
forall c a (m :: * -> *).
(Pretty c, ToConcrete a c, MonadAbsToCon m) =>
a -> m Doc
prettyA Expr
e
    ]
  Type
-> (MetaId -> Type -> TCM Term)
-> (NotBlocked -> Type -> TCM Term)
-> TCM Term
forall t (m :: * -> *) a.
(Reduce t, IsMeta t, MonadReduce m, HasBuiltins m) =>
t -> (MetaId -> t -> m a) -> (NotBlocked -> t -> m a) -> m a
ifBlocked Type
t (\ MetaId
_ Type
t -> Type -> TCM Term
guessRecordType Type
t) {-else-} ((NotBlocked -> Type -> TCM Term) -> TCM Term)
-> (NotBlocked -> Type -> TCM Term) -> TCM Term
forall a b. (a -> b) -> a -> b
$ \ NotBlocked
_ Type
t -> do
  case Type -> Term
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) = Elims -> Maybe [Arg Term]
forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims Elims
es
      VerboseKey -> VerboseLevel -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.term.rec" VerboseLevel
20 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ VerboseKey -> TCM Doc
forall (m :: * -> *). Monad m => VerboseKey -> m Doc
text (VerboseKey -> TCM Doc) -> VerboseKey -> TCM Doc
forall a b. (a -> b) -> a -> b
$ VerboseKey
"  r   = " VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ QName -> VerboseKey
forall a. Pretty a => a -> VerboseKey
prettyShow QName
r

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

      Defn
def <- QName -> TCMT IO Defn
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  = (Dom' Term Name -> Arg Name) -> [Dom' Term Name] -> [Arg Name]
forall a b. (a -> b) -> [a] -> [b]
map Dom' Term Name -> Arg Name
forall t a. Dom' t a -> Arg a
argFromDom ([Dom' Term Name] -> [Arg Name]) -> [Dom' Term Name] -> [Arg Name]
forall a b. (a -> b) -> a -> b
$ Defn -> [Dom' Term Name]
recordFieldNames Defn
def
          -- Just field names.
          xs :: [Name]
xs   = (Arg Name -> Name) -> [Arg Name] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map Arg Name -> Name
forall e. Arg e -> e
unArg [Arg Name]
cxs
          -- Record constructor.
          con :: ConHead
con  = KillRangeT ConHead
forall a. KillRange a => KillRangeT a
killRange KillRangeT ConHead -> KillRangeT ConHead
forall a b. (a -> b) -> a -> b
$ Defn -> ConHead
recConHead Defn
def
      VerboseKey -> VerboseLevel -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.term.rec" VerboseLevel
20 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
vcat
        [ TCM Doc
"  xs  = " TCM Doc -> TCM Doc -> TCM Doc
forall a. Semigroup a => a -> a -> a
<> Doc -> TCM Doc
forall (m :: * -> *) a. Monad m => a -> m a
return ([Name] -> Doc
forall a. Pretty a => a -> Doc
P.pretty [Name]
xs)
        , TCM Doc
"  ftel= " TCM Doc -> TCM Doc -> TCM Doc
forall a. Semigroup a => a -> a -> a
<> Telescope -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM (Defn -> Telescope
recTel Defn
def)
        , TCM Doc
"  con = " TCM Doc -> TCM Doc -> TCM Doc
forall a. Semigroup a => a -> a -> a
<> Doc -> TCM Doc
forall (m :: * -> *) a. Monad m => a -> m a
return (ConHead -> Doc
forall a. Pretty a => a -> Doc
P.pretty ConHead
con)
        ]

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

      -- Compute a list of metas for the missing visible fields.
      ScopeInfo
scope <- TCMT IO ScopeInfo
forall (m :: * -> *). ReadTCState m => m ScopeInfo
getScope
      let re :: Range
re = Expr -> Range
forall t. HasRange t => t -> Range
getRange Expr
e
          meta :: a -> Expr
meta a
x = MetaInfo -> Expr
A.Underscore (MetaInfo -> Expr) -> MetaInfo -> Expr
forall a b. (a -> b) -> a -> b
$ Range -> ScopeInfo -> Maybe MetaId -> VerboseKey -> MetaInfo
A.MetaInfo Range
re ScopeInfo
scope Maybe MetaId
forall a. Maybe a
Nothing (a -> VerboseKey
forall a. Pretty a => a -> VerboseKey
prettyShow a
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 <- QName
-> (Name -> Expr) -> Assigns -> [Arg Name] -> TCM [NamedArg Expr]
forall a.
QName
-> (Name -> a)
-> [FieldAssignment' a]
-> [Arg Name]
-> TCM [NamedArg a]
insertMissingFields QName
r Name -> Expr
forall a. Pretty a => a -> Expr
meta Assigns
fs [Arg Name]
cxs

      [Arg Term]
args <- ExpandHidden
-> Range -> [NamedArg Expr] -> Telescope -> TCM (Elims, Telescope)
checkArguments_ ExpandHidden
ExpandLast Range
re [NamedArg Expr]
es (Defn -> Telescope
recTel Defn
def Telescope -> [Arg Term] -> Telescope
forall t. Apply t => t -> [Arg Term] -> t
`apply` [Arg Term]
vs) TCM (Elims, Telescope)
-> ((Elims, Telescope) -> TCMT IO [Arg Term]) -> TCMT IO [Arg Term]
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
        (Elims
elims, Telescope
remainingTel) | Telescope -> Bool
forall a. Null a => a -> Bool
null Telescope
remainingTel
                              , Just [Arg Term]
args <- Elims -> Maybe [Arg Term]
forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims Elims
elims -> [Arg Term] -> TCMT IO [Arg Term]
forall (m :: * -> *) a. Monad m => a -> m a
return [Arg Term]
args
        (Elims, Telescope)
_ -> TCMT IO [Arg Term]
forall a. HasCallStack => a
__IMPOSSIBLE__
      -- Don't need to block here!
      VerboseKey -> VerboseLevel -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.term.rec" VerboseLevel
20 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ VerboseKey -> TCM Doc
forall (m :: * -> *). Monad m => VerboseKey -> m Doc
text (VerboseKey -> TCM Doc) -> VerboseKey -> TCM Doc
forall a b. (a -> b) -> a -> b
$ VerboseKey
"finished record expression"
      Term -> TCM Term
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> TCM Term) -> Term -> TCM Term
forall a b. (a -> b) -> a -> b
$ ConHead -> ConInfo -> Elims -> Term
Con ConHead
con ConInfo
ConORec ((Arg Term -> Elim' Term) -> [Arg Term] -> Elims
forall a b. (a -> b) -> [a] -> [b]
map Arg Term -> Elim' Term
forall a. Arg a -> Elim' a
Apply [Arg Term]
args)
    Term
_         -> TypeError -> TCM Term
forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m, MonadError TCErr m) =>
TypeError -> m a
typeError (TypeError -> TCM Term) -> TypeError -> TCM Term
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 Assign ModuleName]
mfs ]
      [QName]
rs <- [Name] -> TCM [QName]
findPossibleRecords [Name]
fields
      case [QName]
rs of
          -- If there are no records with the right fields we might as well fail right away.
        [] -> case [Name]
fields of
          []  -> VerboseKey -> TCM Term
forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m, MonadError TCErr m) =>
VerboseKey -> m a
genericError VerboseKey
"There are no records in scope"
          [Name
f] -> VerboseKey -> TCM Term
forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m, MonadError TCErr m) =>
VerboseKey -> m a
genericError (VerboseKey -> TCM Term) -> VerboseKey -> TCM Term
forall a b. (a -> b) -> a -> b
$ VerboseKey
"There is no known record with the field " VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ Name -> VerboseKey
forall a. Pretty a => a -> VerboseKey
prettyShow Name
f
          [Name]
_   -> VerboseKey -> TCM Term
forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m, MonadError TCErr m) =>
VerboseKey -> m a
genericError (VerboseKey -> TCM Term) -> VerboseKey -> TCM Term
forall a b. (a -> b) -> a -> b
$ VerboseKey
"There is no known record with the fields " VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ [VerboseKey] -> VerboseKey
unwords ((Name -> VerboseKey) -> [Name] -> [VerboseKey]
forall a b. (a -> b) -> [a] -> [b]
map Name -> VerboseKey
forall a. Pretty a => a -> VerboseKey
prettyShow [Name]
fields)
          -- If there's only one record with the appropriate fields, go with that.
        [QName
r] -> do
          Definition
def <- QName -> TCMT IO Definition
forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
r
          let rt :: Type
rt = Definition -> Type
defType Definition
def
          [Arg Term]
vs  <- Type -> TCMT IO [Arg Term]
forall (m :: * -> *). MonadMetaSolver m => Type -> m [Arg Term]
newArgsMeta Type
rt
          Type
target <- Type -> TCM Type
forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce (Type -> TCM Type) -> Type -> TCM Type
forall a b. (a -> b) -> a -> b
$ Type -> [Arg Term] -> Type
piApply Type
rt [Arg Term]
vs
          Sort
s  <- case Type -> Term
forall t a. Type'' t a -> a
unEl Type
target of
                  Sort Sort
s  -> Sort -> TCMT IO Sort
forall (m :: * -> *) a. Monad m => a -> m a
return Sort
s
                  Term
v       -> do
                    VerboseKey -> VerboseLevel -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"impossible" VerboseLevel
10 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
vcat
                      [ TCM Doc
"The impossible happened when checking record expression against meta"
                      , TCM Doc
"Candidate record type r = " TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> QName -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
r
                      , TCM Doc
"Type of r               = " TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Type -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
rt
                      , TCM Doc
"Ends in (should be sort)= " TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Term -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
v
                      , VerboseKey -> TCM Doc
forall (m :: * -> *). Monad m => VerboseKey -> m Doc
text (VerboseKey -> TCM Doc) -> VerboseKey -> TCM Doc
forall a b. (a -> b) -> a -> b
$ VerboseKey
"  Raw                   =  " VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ Term -> VerboseKey
forall a. Show a => a -> VerboseKey
show Term
v
                      ]
                    TCMT IO Sort
forall a. HasCallStack => a
__IMPOSSIBLE__
          let inferred :: Type
inferred = Sort -> Term -> Type
forall t a. Sort' t -> a -> Type'' t a
El Sort
s (Term -> Type) -> Term -> Type
forall a b. (a -> b) -> a -> b
$ QName -> Elims -> Term
Def QName
r (Elims -> Term) -> Elims -> Term
forall a b. (a -> b) -> a -> b
$ (Arg Term -> Elim' Term) -> [Arg Term] -> Elims
forall a b. (a -> b) -> [a] -> [b]
map Arg Term -> Elim' Term
forall a. Arg a -> Elim' a
Apply [Arg Term]
vs
          Term
v <- Expr -> Type -> TCM Term
checkExpr Expr
e Type
inferred
          Comparison -> Term -> Type -> Type -> TCM Term
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
          VerboseKey -> VerboseLevel -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.term.expr.rec" VerboseLevel
10 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
sep
            [ TCM Doc
"Postponing type checking of"
            , VerboseLevel -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest VerboseLevel
2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ Expr -> TCM Doc
forall c a (m :: * -> *).
(Pretty c, ToConcrete a c, MonadAbsToCon m) =>
a -> m Doc
prettyA Expr
e TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCM Doc
":" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Type -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
t
            ]
          TypeCheckingProblem -> TCM Term
postponeTypeCheckingProblem_ (TypeCheckingProblem -> TCM Term)
-> TypeCheckingProblem -> TCM Term
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         -- ^ Reduced.
  -> TCM Term
checkRecordUpdate :: Comparison
-> ExprInfo -> Expr -> Assigns -> Expr -> Type -> TCM Term
checkRecordUpdate Comparison
cmp ExprInfo
ei Expr
recexpr Assigns
fs Expr
e Type
t = do
  case Type -> Term
forall t a. Type'' t a -> a
unEl Type
t of
    Def QName
r Elims
vs  -> do
      Term
v <- Comparison -> Expr -> Type -> TCM Term
checkExpr' Comparison
cmp Expr
recexpr Type
t
      Name
name <- Range -> TCMT IO Name
forall (m :: * -> *). MonadFresh NameId m => Range -> m Name
freshNoName (Expr -> Range
forall t. HasRange t => t -> Range
getRange Expr
recexpr)
      ArgInfo -> Name -> Term -> Type -> TCM Term -> TCM Term
forall (m :: * -> *) a.
MonadAddContext m =>
ArgInfo -> Name -> Term -> Type -> m a -> m a
addLetBinding ArgInfo
defaultArgInfo Name
name Term
v Type
t (TCM Term -> TCM Term) -> TCM Term -> TCM Term
forall a b. (a -> b) -> a -> b
$ do
        [Arg QName]
projs <- (Dom' Term QName -> Arg QName) -> [Dom' Term QName] -> [Arg QName]
forall a b. (a -> b) -> [a] -> [b]
map Dom' Term QName -> Arg QName
forall t a. Dom' t a -> Arg a
argFromDom ([Dom' Term QName] -> [Arg QName])
-> (Defn -> [Dom' Term QName]) -> Defn -> [Arg QName]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Defn -> [Dom' Term QName]
recFields (Defn -> [Arg QName]) -> TCMT IO Defn -> TCMT IO [Arg QName]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> TCMT IO Defn
forall (m :: * -> *).
(HasConstInfo m, ReadTCState m, MonadError TCErr m) =>
QName -> m Defn
getRecordDef QName
r

        -- 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 ((Assign -> Name) -> Assigns -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map Assign -> Name
forall a. FieldAssignment' a -> Name
_nameFieldA Assigns
fs) ((Arg QName -> QName) -> [Arg QName] -> [QName]
forall a b. (a -> b) -> [a] -> [b]
map Arg QName -> QName
forall e. Arg e -> e
unArg [Arg QName]
projs)

        [Arg Name]
axs <- (Dom' Term Name -> Arg Name) -> [Dom' Term Name] -> [Arg Name]
forall a b. (a -> b) -> [a] -> [b]
map Dom' Term Name -> Arg Name
forall t a. Dom' t a -> Arg a
argFromDom ([Dom' Term Name] -> [Arg Name])
-> TCMT IO [Dom' Term Name] -> TCMT IO [Arg Name]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> TCMT IO [Dom' Term Name]
forall (m :: * -> *).
(HasConstInfo m, ReadTCState m, MonadError TCErr m) =>
QName -> m [Dom' Term Name]
getRecordFieldNames QName
r
        let xs :: [Name]
xs = (Arg Name -> Name) -> [Arg Name] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map Arg Name -> Name
forall e. Arg e -> e
unArg [Arg Name]
axs
        [TacticAttr]
es <- QName
-> (Arg Name -> TacticAttr)
-> [Arg Name]
-> [(Name, TacticAttr)]
-> TCM [TacticAttr]
forall a.
QName -> (Arg Name -> a) -> [Arg Name] -> [(Name, a)] -> TCM [a]
orderFields QName
r (\ Arg Name
_ -> TacticAttr
forall a. Maybe a
Nothing) [Arg Name]
axs ([(Name, TacticAttr)] -> TCM [TacticAttr])
-> [(Name, TacticAttr)] -> TCM [TacticAttr]
forall a b. (a -> b) -> a -> b
$ (Assign -> (Name, TacticAttr)) -> Assigns -> [(Name, TacticAttr)]
forall a b. (a -> b) -> [a] -> [b]
map (\ (FieldAssignment Name
x Expr
e) -> (Name
x, Expr -> TacticAttr
forall a. a -> Maybe a
Just Expr
e)) Assigns
fs
        let es' :: [TacticAttr]
es' = (Arg QName -> TacticAttr -> TacticAttr)
-> [Arg QName] -> [TacticAttr] -> [TacticAttr]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (Name -> ExprInfo -> Arg QName -> TacticAttr -> TacticAttr
replaceFields Name
name ExprInfo
ei) [Arg QName]
projs [TacticAttr]
es
        Comparison -> Expr -> Type -> TCM Term
checkExpr' Comparison
cmp (ExprInfo -> [Either Assign ModuleName] -> Expr
A.Rec ExprInfo
ei [ Assign -> Either Assign ModuleName
forall a b. a -> Either a b
Left (Name -> Expr -> Assign
forall a. Name -> a -> FieldAssignment' a
FieldAssignment Name
x Expr
e) | (Name
x, Just Expr
e) <- [Name] -> [TacticAttr] -> [(Name, TacticAttr)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Name]
xs [TacticAttr]
es' ]) Type
t

    MetaV MetaId
_ Elims
_ -> do
      Type
inferred <- Expr -> TCM (Term, Type)
inferExpr Expr
recexpr TCM (Term, Type) -> ((Term, Type) -> TCM Type) -> TCM Type
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Type -> TCM Type
forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce (Type -> TCM Type)
-> ((Term, Type) -> Type) -> (Term, Type) -> TCM Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Term, Type) -> Type
forall a b. (a, b) -> b
snd
      case Type -> Term
forall t a. Type'' t a -> a
unEl Type
inferred of
        MetaV MetaId
_ Elims
_ -> TypeCheckingProblem -> TCM Term
postponeTypeCheckingProblem_ (TypeCheckingProblem -> TCM Term)
-> TypeCheckingProblem -> TCM Term
forall a b. (a -> b) -> a -> b
$ Comparison -> Expr -> Type -> TypeCheckingProblem
CheckExpr Comparison
cmp Expr
e Type
t
        Term
_         -> do
          Term
v <- Comparison -> Expr -> Type -> TCM Term
checkExpr' Comparison
cmp Expr
e Type
inferred
          Comparison -> Term -> Type -> Type -> TCM Term
forall (m :: * -> *).
(MonadConversion m, MonadTCM m) =>
Comparison -> Term -> Type -> Type -> m Term
coerce Comparison
cmp Term
v Type
inferred Type
t
    Term
_         -> TypeError -> TCM Term
forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m, MonadError TCErr m) =>
TypeError -> m a
typeError (TypeError -> TCM Term) -> TypeError -> TCM Term
forall a b. (a -> b) -> a -> b
$ Type -> TypeError
ShouldBeRecordType Type
t
  where
    replaceFields :: Name -> A.ExprInfo -> Arg A.QName -> Maybe A.Expr -> Maybe A.Expr
    replaceFields :: Name -> ExprInfo -> Arg QName -> TacticAttr -> TacticAttr
replaceFields Name
n ExprInfo
ei a :: Arg QName
a@(Arg ArgInfo
_ QName
p) TacticAttr
Nothing | Arg QName -> Bool
forall a. LensHiding a => a -> Bool
visible Arg QName
a =
        Expr -> TacticAttr
forall a. a -> Maybe a
Just (Expr -> TacticAttr) -> Expr -> TacticAttr
forall a b. (a -> b) -> a -> b
$ AppInfo -> Expr -> NamedArg Expr -> Expr
A.App (Range -> AppInfo
A.defaultAppInfo (Range -> AppInfo) -> Range -> AppInfo
forall a b. (a -> b) -> a -> b
$ ExprInfo -> Range
forall t. HasRange t => t -> Range
getRange ExprInfo
ei) (QName -> Expr
A.Def QName
p) (NamedArg Expr -> Expr) -> NamedArg Expr -> Expr
forall a b. (a -> b) -> a -> b
$ Expr -> NamedArg Expr
forall a. a -> NamedArg a
defaultNamedArg (Expr -> NamedArg Expr) -> Expr -> NamedArg Expr
forall a b. (a -> b) -> a -> b
$ Name -> Expr
A.Var Name
n
    replaceFields Name
_ ExprInfo
_  (Arg ArgInfo
_ QName
_) TacticAttr
Nothing  = TacticAttr
forall a. Maybe a
Nothing
    replaceFields Name
_ ExprInfo
_  Arg QName
_         (Just Expr
e) = Expr -> TacticAttr
forall a. a -> Maybe a
Just (Expr -> TacticAttr) -> Expr -> TacticAttr
forall a b. (a -> b) -> a -> b
$ Expr
e

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

checkLiteral :: Literal -> Type -> TCM Term
checkLiteral :: Literal -> Type -> TCM Term
checkLiteral Literal
lit Type
t = do
  Type
t' <- Literal -> TCM Type
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
Literal -> m Type
litType Literal
lit
  Comparison -> Term -> Type -> Type -> TCM Term
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 TCM () -> TCM Expr -> TCM Expr
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Expr -> TCM Expr
scopedExpr Expr
e
scopedExpr Expr
e                      = Expr -> TCM Expr
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 =
  VerboseKey -> VerboseLevel -> VerboseKey -> TCM Term -> TCM Term
forall (m :: * -> *) a.
MonadDebug m =>
VerboseKey -> VerboseLevel -> VerboseKey -> m a -> m a
verboseBracket VerboseKey
"tc.term.expr.top" VerboseLevel
5 VerboseKey
"checkExpr" (TCM Term -> TCM Term) -> TCM Term -> TCM Term
forall a b. (a -> b) -> a -> b
$
  VerboseKey
-> VerboseLevel -> (Term -> TCM Doc) -> TCM Term -> TCM Term
forall (m :: * -> *) a.
MonadDebug m =>
VerboseKey -> VerboseLevel -> (a -> TCM Doc) -> m a -> m a
reportResult VerboseKey
"tc.term.expr.top" VerboseLevel
15 (\ Term
v -> [TCM Doc] -> TCM Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
vcat
                                              [ TCM Doc
"checkExpr" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<?> [TCM Doc] -> TCM Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
fsep [ Expr -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Expr
e, TCM Doc
":", Type -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
t ]
                                              , TCM Doc
"  returns" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<?> Term -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
v ]) (TCM Term -> TCM Term) -> TCM Term -> TCM Term
forall a b. (a -> b) -> a -> b
$
  Call -> TCM Term -> TCM Term
forall (tcm :: * -> *) a.
(MonadTCM tcm, ReadTCState tcm, MonadDebug tcm) =>
Call -> tcm a -> tcm a
traceCall (Comparison -> Expr -> Type -> Call
CheckExprCall Comparison
cmp Expr
e Type
t) (TCM Term -> TCM Term) -> TCM Term -> TCM Term
forall a b. (a -> b) -> a -> b
$ TCM Term -> TCM Term
forall a. TCM a -> TCM a
localScope (TCM Term -> TCM Term) -> TCM Term -> TCM Term
forall a b. (a -> b) -> a -> b
$ TCM Term -> TCM Term
forall a. TCM a -> TCM a
doExpandLast (TCM Term -> TCM Term) -> TCM Term -> TCM Term
forall a b. (a -> b) -> a -> b
$ Term -> TCM Term
forall (m :: * -> *).
(HasConstInfo m, MonadReduce m) =>
Term -> m Term
unfoldInlined (Term -> TCM Term) -> TCM Term -> TCM Term
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< do
    VerboseKey -> VerboseLevel -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.term.expr.top" VerboseLevel
15 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$
        TCM Doc
"Checking" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [TCM Doc] -> TCM Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
sep
          [ [TCM Doc] -> TCM Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
fsep [ Expr -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Expr
e, TCM Doc
":", Type -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
t ]
          , VerboseLevel -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest VerboseLevel
2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ TCM Doc
"at " TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> (VerboseKey -> TCM Doc
forall (m :: * -> *). Monad m => VerboseKey -> m Doc
text (VerboseKey -> TCM Doc)
-> (Range -> VerboseKey) -> Range -> TCM Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Range -> VerboseKey
forall a. Pretty a => a -> VerboseKey
prettyShow (Range -> TCM Doc) -> TCMT IO Range -> TCM Doc
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< TCMT IO Range
forall (m :: * -> *). MonadTCEnv m => m Range
getCurrentRange)
          ]
    VerboseKey -> VerboseLevel -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.term.expr.top.detailed" VerboseLevel
80 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$
      TCM Doc
"Checking" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [TCM Doc] -> TCM Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
fsep [ Expr -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Expr
e, TCM Doc
":", VerboseKey -> TCM Doc
forall (m :: * -> *). Monad m => VerboseKey -> m Doc
text (Type -> VerboseKey
forall a. Show a => a -> VerboseKey
show Type
t) ]
    Type
tReduced <- Type -> TCM Type
forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce Type
t
    VerboseKey -> VerboseLevel -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.term.expr.top" VerboseLevel
15 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$
        TCM Doc
"    --> " TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Type -> TCM 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 <- Type -> TCMT IO Bool
forall a (m :: * -> *).
(LensSort a, PrettyTCM a, MonadReduce m, MonadDebug m) =>
a -> m Bool
isPropM Type
t TCMT IO Bool
-> (Bool -> TCMT IO (TCM Term -> TCM Term))
-> TCMT IO (TCM Term -> TCM Term)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
      Bool
True  -> do
        let mod :: Modality
mod = Modality
defaultModality { modRelevance :: Relevance
modRelevance = Relevance
Irrelevant }
        (TCM Term -> TCM Term) -> TCMT IO (TCM Term -> TCM Term)
forall (m :: * -> *) a. Monad m => a -> m a
return ((TCM Term -> TCM Term) -> TCMT IO (TCM Term -> TCM Term))
-> (TCM Term -> TCM Term) -> TCMT IO (TCM Term -> TCM Term)
forall a b. (a -> b) -> a -> b
$ (Term -> Term) -> TCM Term -> TCM Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Term -> Term
dontCare (TCM Term -> TCM Term)
-> (TCM Term -> TCM Term) -> TCM Term -> TCM Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Modality -> TCM Term -> TCM Term
forall (tcm :: * -> *) m a.
(MonadTCEnv tcm, LensModality m) =>
m -> tcm a -> tcm a
applyModalityToContext Modality
mod
      Bool
False -> (TCM Term -> TCM Term) -> TCMT IO (TCM Term -> TCM Term)
forall (m :: * -> *) a. Monad m => a -> m a
return TCM Term -> TCM Term
forall a. a -> a
id

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

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

        -- a meta variable without arguments: type check directly for efficiency
        A.QuestionMark MetaInfo
i InteractionId
ii -> (Comparison -> Type -> TCM (MetaId, Term))
-> Comparison -> Type -> MetaInfo -> InteractionId -> TCM Term
checkQuestionMark (RunMetaOccursCheck -> Comparison -> Type -> TCM (MetaId, Term)
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 -> TypeError -> TCM Term
forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m, MonadError TCErr m) =>
TypeError -> m a
typeError (TypeError -> TCM Term) -> TypeError -> TCM Term
forall a b. (a -> b) -> a -> b
$ VerboseKey -> TypeError
NotImplemented VerboseKey
"type checking of with application"

        -- check |- Set l : t  (requires universe polymorphism)
        A.App AppInfo
i Expr
s arg :: NamedArg Expr
arg@(Arg ArgInfo
ai Named_ Expr
l)
          | A.Set ExprInfo
_ Integer
0 <- Expr -> Expr
unScope Expr
s, ArgInfo -> Bool
forall a. LensHiding a => a -> Bool
visible ArgInfo
ai ->
          TCMT IO Bool -> TCM Term -> TCM Term -> TCM Term
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifNotM TCMT IO Bool
forall (m :: * -> *). HasOptions m => m Bool
hasUniversePolymorphism
              (VerboseKey -> TCM Term
forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m, MonadError TCErr m) =>
VerboseKey -> m a
genericError VerboseKey
"Use --universe-polymorphism to enable level arguments to Set")
          (TCM Term -> TCM Term) -> TCM Term -> TCM Term
forall a b. (a -> b) -> a -> b
$ {- else -} do
            -- allow NonStrict variables when checking level
            --   Set : (NonStrict) Level -> Set\omega
            Level' Term
n <- Relevance -> TCMT IO (Level' Term) -> TCMT IO (Level' Term)
forall (tcm :: * -> *) r a.
(MonadTCEnv tcm, LensRelevance r) =>
r -> tcm a -> tcm a
applyRelevanceToContext Relevance
NonStrict (TCMT IO (Level' Term) -> TCMT IO (Level' Term))
-> TCMT IO (Level' Term) -> TCMT IO (Level' Term)
forall a b. (a -> b) -> a -> b
$ NamedArg Expr -> TCMT IO (Level' Term)
checkLevel NamedArg Expr
arg
            -- check that Set (l+1) <= t
            VerboseKey -> VerboseLevel -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.univ.poly" VerboseLevel
10 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$
              TCM Doc
"checking Set " TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Level' Term -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Level' Term
n TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+>
              TCM Doc
"against" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Type -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
t
            Comparison -> Term -> Type -> Type -> TCM Term
forall (m :: * -> *).
(MonadConversion m, MonadTCM m) =>
Comparison -> Term -> Type -> Type -> m Term
coerce Comparison
cmp (Sort -> Term
Sort (Sort -> Term) -> Sort -> Term
forall a b. (a -> b) -> a -> b
$ Level' Term -> Sort
forall t. Level' t -> Sort' t
Type Level' Term
n) (Sort -> Type
sort (Sort -> Type) -> Sort -> Type
forall a b. (a -> b) -> a -> b
$ Level' Term -> Sort
forall t. Level' t -> Sort' t
Type (Level' Term -> Sort) -> Level' Term -> Sort
forall a b. (a -> b) -> a -> b
$ Level' Term -> Level' Term
levelSuc Level' Term
n) Type
t

        -- check |- Prop l : t  (requires universe polymorphism)
        A.App AppInfo
i Expr
s arg :: NamedArg Expr
arg@(Arg ArgInfo
ai Named_ Expr
l)
          | A.Prop ExprInfo
_ Integer
0 <- Expr -> Expr
unScope Expr
s, ArgInfo -> Bool
forall a. LensHiding a => a -> Bool
visible ArgInfo
ai ->
          TCMT IO Bool -> TCM Term -> TCM Term -> TCM Term
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifNotM TCMT IO Bool
forall (m :: * -> *). HasOptions m => m Bool
hasUniversePolymorphism
              (VerboseKey -> TCM Term
forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m, MonadError TCErr m) =>
VerboseKey -> m a
genericError VerboseKey
"Use --universe-polymorphism to enable level arguments to Prop")
          (TCM Term -> TCM Term) -> TCM Term -> TCM Term
forall a b. (a -> b) -> a -> b
$ {- else -} do
            Level' Term
n <- Relevance -> TCMT IO (Level' Term) -> TCMT IO (Level' Term)
forall (tcm :: * -> *) r a.
(MonadTCEnv tcm, LensRelevance r) =>
r -> tcm a -> tcm a
applyRelevanceToContext Relevance
NonStrict (TCMT IO (Level' Term) -> TCMT IO (Level' Term))
-> TCMT IO (Level' Term) -> TCMT IO (Level' Term)
forall a b. (a -> b) -> a -> b
$ NamedArg Expr -> TCMT IO (Level' Term)
checkLevel NamedArg Expr
arg
            VerboseKey -> VerboseLevel -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.univ.poly" VerboseLevel
10 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$
              TCM Doc
"checking Prop " TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Level' Term -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Level' Term
n TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+>
              TCM Doc
"against" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Type -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
t
            Comparison -> Term -> Type -> Type -> TCM Term
forall (m :: * -> *).
(MonadConversion m, MonadTCM m) =>
Comparison -> Term -> Type -> Type -> m Term
coerce Comparison
cmp (Sort -> Term
Sort (Sort -> Term) -> Sort -> Term
forall a b. (a -> b) -> a -> b
$ Level' Term -> Sort
forall t. Level' t -> Sort' t
Prop Level' Term
n) (Sort -> Type
sort (Sort -> Type) -> Sort -> Type
forall a b. (a -> b) -> a -> b
$ Level' Term -> Sort
forall t. Level' t -> Sort' t
Type (Level' Term -> Sort) -> Level' Term -> Sort
forall a b. (a -> b) -> a -> b
$ Level' Term -> Level' Term
levelSuc Level' Term
n) Type
t

        e0 :: Expr
e0@(A.App AppInfo
i Expr
q (Arg ArgInfo
ai Named_ Expr
e))
          | A.Quote ExprInfo
_ <- Expr -> Expr
unScope Expr
q, ArgInfo -> Bool
forall a. LensHiding a => a -> Bool
visible ArgInfo
ai -> do
          let quoted :: Expr -> m QName
quoted (A.Def QName
x) = QName -> m QName
forall (m :: * -> *) a. Monad m => a -> m a
return QName
x
              quoted (A.Macro QName
x) = QName -> m QName
forall (m :: * -> *) a. Monad m => a -> m a
return QName
x
              quoted (A.Proj ProjOrigin
o AmbiguousQName
p) | Just QName
x <- AmbiguousQName -> Maybe QName
getUnambiguous AmbiguousQName
p = QName -> m QName
forall (m :: * -> *) a. Monad m => a -> m a
return QName
x
              quoted (A.Proj ProjOrigin
o AmbiguousQName
p)  =
                VerboseKey -> m QName
forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m, MonadError TCErr m) =>
VerboseKey -> m a
genericError (VerboseKey -> m QName) -> VerboseKey -> m QName
forall a b. (a -> b) -> a -> b
$ VerboseKey
"quote: Ambigous name: " VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ NonEmpty QName -> VerboseKey
forall a. Pretty a => a -> VerboseKey
prettyShow (AmbiguousQName -> NonEmpty QName
unAmbQ AmbiguousQName
p)
              quoted (A.Con AmbiguousQName
c) | Just QName
x <- AmbiguousQName -> Maybe QName
getUnambiguous AmbiguousQName
c = QName -> m QName
forall (m :: * -> *) a. Monad m => a -> m a
return QName
x
              quoted (A.Con AmbiguousQName
c)  =
                VerboseKey -> m QName
forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m, MonadError TCErr m) =>
VerboseKey -> m a
genericError (VerboseKey -> m QName) -> VerboseKey -> m QName
forall a b. (a -> b) -> a -> b
$ VerboseKey
"quote: Ambigous name: " VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ NonEmpty QName -> VerboseKey
forall a. Pretty a => a -> VerboseKey
prettyShow (AmbiguousQName -> NonEmpty QName
unAmbQ AmbiguousQName
c)
              quoted (A.ScopedExpr ScopeInfo
_ Expr
e) = Expr -> m QName
quoted Expr
e
              quoted Expr
_                  =
                VerboseKey -> m QName
forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m, MonadError TCErr m) =>
VerboseKey -> m a
genericError VerboseKey
"quote: not a defined name"
          QName
x <- Expr -> TCMT IO QName
forall (m :: * -> *).
(MonadTCEnv m, ReadTCState m, MonadError TCErr m) =>
Expr -> m QName
quoted (Named_ Expr -> Expr
forall name a. Named name a -> a
namedThing Named_ Expr
e)
          Type
ty <- TCM Type
qNameType
          Comparison -> Term -> Type -> Type -> TCM Term
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 (Named_ Expr -> Expr
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{}     -> VerboseKey -> TCM Term
forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m, MonadError TCErr m) =>
VerboseKey -> m a
genericError VerboseKey
"quote must be applied to a defined name"
        A.QuoteTerm{} -> VerboseKey -> TCM Term
forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m, MonadError TCErr m) =>
VerboseKey -> m a
genericError VerboseKey
"quoteTerm must be applied to a term"
        A.Unquote{}   -> VerboseKey -> TCM Term
forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m, MonadError TCErr m) =>
VerboseKey -> m a
genericError VerboseKey
"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 QName
qname [Clause]
cs -> Comparison
-> ExprInfo
-> DefInfo
-> QName
-> [Clause]
-> Expr
-> Type
-> TCM Term
checkExtendedLambda Comparison
cmp ExprInfo
i DefInfo
di QName
qname [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 TacticAttr
_ NamedArg Binder
x) Expr
e0
          | Maybe (WithOrigin (Ranged VerboseKey)) -> Bool
forall a. Maybe a -> Bool
isNothing (Named (WithOrigin (Ranged VerboseKey)) Binder
-> Maybe (WithOrigin (Ranged VerboseKey))
forall name a. Named name a -> Maybe name
nameOf (Named (WithOrigin (Ranged VerboseKey)) Binder
 -> Maybe (WithOrigin (Ranged VerboseKey)))
-> Named (WithOrigin (Ranged VerboseKey)) Binder
-> Maybe (WithOrigin (Ranged VerboseKey))
forall a b. (a -> b) -> a -> b
$ NamedArg Binder -> Named (WithOrigin (Ranged VerboseKey)) Binder
forall e. Arg e -> e
unArg NamedArg Binder
x) Bool -> Bool -> Bool
&& Maybe Pattern -> Bool
forall a. Maybe a -> Bool
isNothing (Binder -> Maybe Pattern
forall a. Binder' a -> Maybe Pattern
A.binderPattern (Binder -> Maybe Pattern) -> Binder -> Maybe Pattern
forall a b. (a -> b) -> a -> b
$ NamedArg Binder -> Binder
forall a. NamedArg a -> a
namedArg NamedArg Binder
x) ->
              Comparison -> Expr -> Type -> TCM Term
checkExpr' Comparison
cmp (ExprInfo -> LamBinding -> Expr -> Expr
A.Lam ExprInfo
i (ArgInfo -> Binder' Name -> LamBinding
domainFree (NamedArg Binder -> ArgInfo
forall a. LensArgInfo a => a -> ArgInfo
getArgInfo NamedArg Binder
x) (Binder' Name -> LamBinding) -> Binder' Name -> LamBinding
forall a b. (a -> b) -> a -> b
$ (BindName -> Name) -> Binder -> Binder' Name
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap BindName -> Name
A.unBind (Binder -> Binder' Name) -> Binder -> Binder' Name
forall a b. (a -> b) -> a -> b
$ NamedArg Binder -> Binder
forall a. NamedArg a -> a
namedArg NamedArg Binder
x) Expr
e0) Type
t
          | Bool
otherwise -> TypeError -> TCM Term
forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m, MonadError TCErr m) =>
TypeError -> m a
typeError (TypeError -> TCM Term) -> TypeError -> TCM Term
forall a b. (a -> b) -> a -> b
$ VerboseKey -> TypeError
NotImplemented VerboseKey
"named arguments in lambdas"

        A.Lit Literal
lit    -> Literal -> Type -> TCM Term
checkLiteral Literal
lit Type
t
        A.Let ExprInfo
i [LetBinding]
ds Expr
e -> [LetBinding] -> TCM Term -> TCM Term
forall a. [LetBinding] -> TCM a -> TCM a
checkLetBindings [LetBinding]
ds (TCM Term -> TCM Term) -> TCM Term -> TCM Term
forall a b. (a -> b) -> a -> b
$ Comparison -> Expr -> Type -> TCM Term
checkExpr' Comparison
cmp Expr
e Type
t
        A.Pi ExprInfo
_ Telescope
tel Expr
e | Telescope -> Bool
forall a. Null a => a -> Bool
null Telescope
tel -> Comparison -> Expr -> Type -> TCM Term
checkExpr' Comparison
cmp Expr
e Type
t
        A.Pi ExprInfo
_ Telescope
tel Expr
e -> do
            (Type
t0, Type
t') <- Telescope -> (Telescope -> TCM (Type, Type)) -> TCM (Type, Type)
forall a. Telescope -> (Telescope -> TCM a) -> TCM a
checkPiTelescope Telescope
tel ((Telescope -> TCM (Type, Type)) -> TCM (Type, Type))
-> (Telescope -> TCM (Type, Type)) -> TCM (Type, Type)
forall a b. (a -> b) -> a -> b
$ \ Telescope
tel -> do
                    Type
t0  <- Type -> TCM Type
forall a (m :: * -> *).
(InstantiateFull a, MonadReduce m) =>
a -> m a
instantiateFull (Type -> TCM Type) -> TCM Type -> TCM Type
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Expr -> TCM Type
isType_ Expr
e
                    Telescope
tel <- Telescope -> TCMT IO Telescope
forall a (m :: * -> *).
(InstantiateFull a, MonadReduce m) =>
a -> m a
instantiateFull Telescope
tel
                    (Type, Type) -> TCM (Type, Type)
forall (m :: * -> *) a. Monad m => a -> m a
return (Type
t0, Telescope -> Type -> Type
telePi Telescope
tel Type
t0)
            Type -> TCM ()
checkTelePiSort Type
t'
            Type -> Type -> TCM ()
noFunctionsIntoSize Type
t0 Type
t'
            let s :: Sort
s = Type -> Sort
forall a. LensSort a => a -> Sort
getSort Type
t'
                v :: Term
v = Type -> Term
forall t a. Type'' t a -> a
unEl Type
t'
            Bool -> TCM () -> TCM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Sort
s Sort -> Sort -> Bool
forall a. Eq a => a -> a -> Bool
== Sort
forall t. Sort' t
Inf) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ VerboseKey -> VerboseLevel -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.term.sort" VerboseLevel
20 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$
              [TCM Doc] -> TCM Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
vcat [ VerboseKey -> TCM Doc
forall (m :: * -> *). Monad m => VerboseKey -> m Doc
text (VerboseKey
"reduced to omega:")
                   , VerboseLevel -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest VerboseLevel
2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ TCM Doc
"t   =" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Type -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
t'
                   , VerboseLevel -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest VerboseLevel
2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ TCM Doc
"cxt =" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> (Telescope -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM (Telescope -> TCM Doc) -> TCMT IO Telescope -> TCM Doc
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< TCMT IO Telescope
forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Telescope
getContextTelescope)
                   ]
            Comparison -> Term -> Type -> Type -> TCM Term
forall (m :: * -> *).
(MonadConversion m, MonadTCM m) =>
Comparison -> Term -> Type -> Type -> m Term
coerce Comparison
cmp Term
v (Sort -> Type
sort Sort
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 (TCM Type -> TCM ([Maybe QName], Type))
-> TCM Type -> TCM ([Maybe QName], Type)
forall a b. (a -> b) -> a -> b
$ Expr -> TCM Type
isType_ Expr
e
            Type -> Type -> TCM ()
noFunctionsIntoSize Type
t' Type
t'
            let s :: Sort
s = Type -> Sort
forall a. LensSort a => a -> Sort
getSort Type
t'
                v :: Term
v = Type -> Term
forall t a. Type'' t a -> a
unEl Type
t'
            Bool -> TCM () -> TCM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Sort
s Sort -> Sort -> Bool
forall a. Eq a => a -> a -> Bool
== Sort
forall t. Sort' t
Inf) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ VerboseKey -> VerboseLevel -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.term.sort" VerboseLevel
20 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$
              [TCM Doc] -> TCM Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
vcat [ VerboseKey -> TCM Doc
forall (m :: * -> *). Monad m => VerboseKey -> m Doc
text (VerboseKey
"reduced to omega:")
                   , VerboseLevel -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest VerboseLevel
2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ TCM Doc
"t   =" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Type -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
t'
                   , VerboseLevel -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest VerboseLevel
2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ TCM Doc
"cxt =" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> (Telescope -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM (Telescope -> TCM Doc) -> TCMT IO Telescope -> TCM Doc
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< TCMT IO Telescope
forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Telescope
getContextTelescope)
                   ]
            Comparison -> Term -> Type -> Type -> TCM Term
forall (m :: * -> *).
(MonadConversion m, MonadTCM m) =>
Comparison -> Term -> Type -> Type -> m Term
coerce Comparison
cmp Term
v (Sort -> Type
sort Sort
s) Type
t

        A.Fun ExprInfo
_ (Arg ArgInfo
info Expr
a) Expr
b -> do
            Type
a' <- Expr -> TCM Type
isType_ Expr
a
            let adom :: Dom Type
adom = ArgInfo -> Type -> Dom Type
forall a. ArgInfo -> a -> Dom a
defaultArgDom ArgInfo
info Type
a'
            Type
b' <- Expr -> TCM Type
isType_ Expr
b
            Sort
s  <- Sort -> Sort -> TCMT IO Sort
inferFunSort (Type -> Sort
forall a. LensSort a => a -> Sort
getSort Type
a') (Type -> Sort
forall a. LensSort a => a -> Sort
getSort Type
b')
            let v :: Term
v = Dom Type -> Abs Type -> Term
Pi Dom Type
adom (VerboseKey -> Type -> Abs Type
forall a. VerboseKey -> a -> Abs a
NoAbs VerboseKey
forall a. Underscore a => a
underscore Type
b')
            Type -> Type -> TCM ()
noFunctionsIntoSize Type
b' (Type -> TCM ()) -> Type -> TCM ()
forall a b. (a -> b) -> a -> b
$ Sort -> Term -> Type
forall t a. Sort' t -> a -> Type'' t a
El Sort
s Term
v
            Comparison -> Term -> Type -> Type -> TCM Term
forall (m :: * -> *).
(MonadConversion m, MonadTCM m) =>
Comparison -> Term -> Type -> Type -> m Term
coerce Comparison
cmp Term
v (Sort -> Type
sort Sort
s) Type
t
        A.Set ExprInfo
_ Integer
n    -> do
          Comparison -> Term -> Type -> Type -> TCM Term
forall (m :: * -> *).
(MonadConversion m, MonadTCM m) =>
Comparison -> Term -> Type -> Type -> m Term
coerce Comparison
cmp (Sort -> Term
Sort (Sort -> Term) -> Sort -> Term
forall a b. (a -> b) -> a -> b
$ Integer -> Sort
mkType Integer
n) (Sort -> Type
sort (Sort -> Type) -> Sort -> Type
forall a b. (a -> b) -> a -> b
$ Integer -> Sort
mkType (Integer -> Sort) -> Integer -> Sort
forall a b. (a -> b) -> a -> b
$ Integer
n Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
1) Type
t
        A.Prop ExprInfo
_ Integer
n   -> do
          TCMT IO Bool -> TCM () -> TCM ()
forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
unlessM TCMT IO Bool
forall (m :: * -> *). HasOptions m => m Bool
isPropEnabled (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ TypeError -> TCM ()
forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m, MonadError TCErr m) =>
TypeError -> m a
typeError TypeError
NeedOptionProp
          Comparison -> Term -> Type -> Type -> TCM Term
forall (m :: * -> *).
(MonadConversion m, MonadTCM m) =>
Comparison -> Term -> Type -> Type -> m Term
coerce Comparison
cmp (Sort -> Term
Sort (Sort -> Term) -> Sort -> Term
forall a b. (a -> b) -> a -> b
$ Integer -> Sort
mkProp Integer
n) (Sort -> Type
sort (Sort -> Type) -> Sort -> Type
forall a b. (a -> b) -> a -> b
$ Integer -> Sort
mkType (Integer -> Sort) -> Integer -> Sort
forall a b. (a -> b) -> a -> b
$ Integer
n Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
1) Type
t

        A.Rec ExprInfo
_ [Either Assign ModuleName]
fs  -> Comparison
-> [Either Assign ModuleName] -> Expr -> Type -> TCM Term
checkRecordExpression Comparison
cmp [Either Assign 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
tReduced

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

        A.ETel Telescope
_   -> TCM Term
forall a. HasCallStack => a
__IMPOSSIBLE__

        A.Dot{} -> VerboseKey -> TCM Term
forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m, MonadError TCErr m) =>
VerboseKey -> m a
genericError VerboseKey
"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

      TCM Term -> ((TCErr, MetaId) -> TCM Term) -> TCM Term
forall a. TCM a -> ((TCErr, MetaId) -> TCM a) -> TCM a
`catchIlltypedPatternBlockedOnMeta` \ (TCErr
err, MetaId
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).
        VerboseKey -> VerboseLevel -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.term" VerboseLevel
50 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
vcat ([TCM Doc] -> TCM Doc) -> [TCM Doc] -> TCM Doc
forall a b. (a -> b) -> a -> b
$
          [ TCM Doc
"checking pattern got stuck on meta: " TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> VerboseKey -> TCM Doc
forall (m :: * -> *). Monad m => VerboseKey -> m Doc
text (MetaId -> VerboseKey
forall a. Show a => a -> VerboseKey
show MetaId
x) ]
        TypeCheckingProblem -> TCMT IO Bool -> TCM Term
postponeTypeCheckingProblem (Comparison -> Expr -> Type -> TypeCheckingProblem
CheckExpr Comparison
cmp Expr
e Type
t) (TCMT IO Bool -> TCM Term) -> TCMT IO Bool -> TCM Term
forall a b. (a -> b) -> a -> b
$ MetaId -> TCMT IO Bool
forall a (m :: * -> *).
(IsInstantiatedMeta a, MonadFail m, ReadTCState m) =>
a -> m Bool
isInstantiatedMeta MetaId
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 <- Type -> Term
forall t a. Type'' t a -> a
unEl Type
tReduced
        , let h :: Hiding
h = ArgInfo -> Hiding
forall a. LensHiding a => a -> Hiding
getHiding ArgInfo
info
        , Hiding -> Bool
forall a. LensHiding a => a -> Bool
notVisible Hiding
h
        -- expression is not a matching hidden lambda or question mark
        , Bool -> Bool
not (Hiding -> Expr -> Bool
forall a. LensHiding a => a -> Expr -> Bool
hiddenLambdaOrHole Hiding
h Expr
e)
        = do
      let proceed :: TCM Term
proceed = ArgInfo -> VerboseKey -> TCM Term
doInsert (Origin -> ArgInfo -> ArgInfo
forall a. LensOrigin a => Origin -> a -> a
setOrigin Origin
Inserted ArgInfo
info) (VerboseKey -> TCM Term) -> VerboseKey -> TCM Term
forall a b. (a -> b) -> a -> b
$ Abs Type -> VerboseKey
forall a. Abs a -> VerboseKey
absName Abs Type
b
      ExpandHidden
expandHidden <- (TCEnv -> ExpandHidden) -> TCMT IO 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 ExpandHidden -> ExpandHidden -> Bool
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.
        Type -> TCM Type
forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce Type
a TCM Type
-> (Type -> TCMT IO (Maybe BoundedSize))
-> TCMT IO (Maybe BoundedSize)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Type -> TCMT IO (Maybe BoundedSize)
forall a (m :: * -> *).
(IsSizeType a, HasOptions m, HasBuiltins m) =>
a -> m (Maybe BoundedSize)
isSizeType TCMT IO (Maybe BoundedSize)
-> (Maybe BoundedSize -> TCM Term) -> TCM Term
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
          Just (BoundedLt Term
u) -> Term
-> (MetaId -> Term -> TCM Term)
-> (NotBlocked -> Term -> TCM Term)
-> TCM Term
forall t (m :: * -> *) a.
(Reduce t, IsMeta t, MonadReduce m, HasBuiltins m) =>
t -> (MetaId -> t -> m a) -> (NotBlocked -> t -> m a) -> m a
ifBlocked Term
u (\ MetaId
_ Term
_ -> TCM Term
fallback) ((NotBlocked -> Term -> TCM Term) -> TCM Term)
-> (NotBlocked -> Term -> TCM Term) -> TCM Term
forall a b. (a -> b) -> a -> b
$ \ NotBlocked
_ Term
v -> do
            TCMT IO Bool -> TCM Term -> TCM Term -> TCM Term
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
            TCM Term -> (TCErr -> TCM Term) -> TCM Term
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 = Expr -> Range
forall t. HasRange t => t -> Range
getRange Expr
e
    rx :: Range
rx = Maybe (Position' SrcFile)
-> Range -> (Position' SrcFile -> Range) -> Range
forall a b. Maybe a -> b -> (a -> b) -> b
caseMaybe (Range -> Maybe (Position' SrcFile)
forall a. Range' a -> Maybe (Position' a)
rStart Range
re) Range
forall a. Range' a
noRange ((Position' SrcFile -> Range) -> Range)
-> (Position' SrcFile -> Range) -> Range
forall a b. (a -> b) -> a -> b
$ \ Position' SrcFile
pos -> Position' SrcFile -> Position' SrcFile -> Range
forall a. Position' a -> Position' a -> Range' a
posToRange Position' SrcFile
pos Position' SrcFile
pos

    doInsert :: ArgInfo -> VerboseKey -> TCM Term
doInsert ArgInfo
info VerboseKey
y = do
      Name
x <- Name -> Name
forall a. LensInScope a => a -> a
C.setNotInScope (Name -> Name) -> TCMT IO Name -> TCMT IO Name
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Range -> VerboseKey -> TCMT IO Name
forall (m :: * -> *).
MonadFresh NameId m =>
Range -> VerboseKey -> m Name
freshName Range
rx VerboseKey
y
      VerboseKey -> VerboseLevel -> VerboseKey -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> VerboseKey -> m ()
reportSLn VerboseKey
"tc.term.expr.impl" VerboseLevel
15 (VerboseKey -> TCM ()) -> VerboseKey -> TCM ()
forall a b. (a -> b) -> a -> b
$ VerboseKey
"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 (Binder' Name -> LamBinding) -> Binder' Name -> LamBinding
forall a b. (a -> b) -> a -> b
$ Name -> Binder' Name
forall a. a -> Binder' a
A.mkBinder Name
x) Expr
e) Type
tReduced

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

    hiddenLHS :: Clause -> Bool
hiddenLHS (A.Clause (A.LHS LHSInfo
_ (A.LHSHead QName
_ (NamedArg Pattern
a : [NamedArg Pattern]
_))) [ProblemEq]
_ RHS
_ WhereDeclarations
_ Bool
_) = NamedArg Pattern -> 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.Set{}        -> Bool
True
      A.Prop{}       -> Bool
True
      A.Rec{}        -> Bool
True
      A.RecUpdate{}  -> Bool
True
      A.ScopedExpr{} -> Bool
forall a. HasCallStack => a
__IMPOSSIBLE__
      A.ETel{}       -> Bool
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'       <- Term -> TCM Term
forall (m :: * -> *) a.
(MonadTCEnv m, HasConstInfo m, HasOptions m, TermLike a) =>
a -> m a
etaContract (Term -> TCM Term) -> TCM Term -> TCM Term
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Term -> TCM Term
forall a (m :: * -> *).
(InstantiateFull a, MonadReduce m) =>
a -> m a
instantiateFull Term
et
  case Term -> [MetaId]
forall a. TermLike a => a -> [MetaId]
allMetasList Term
et' of
    []  -> do
      Term
q  <- Term -> TCM Term
quoteTerm Term
et'
      Type
ty <- TCM Term -> TCM Type
forall (tcm :: * -> *). Functor tcm => tcm Term -> tcm Type
el TCM Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTerm
      Comparison -> Term -> Type -> Type -> TCM Term
forall (m :: * -> *).
(MonadConversion m, MonadTCM m) =>
Comparison -> Term -> Type -> Type -> m Term
coerce Comparison
cmp Term
q Type
ty Type
t
    [MetaId]
metas -> TypeCheckingProblem -> TCMT IO Bool -> TCM Term
postponeTypeCheckingProblem (Comparison -> Term -> Type -> TypeCheckingProblem
DoQuoteTerm Comparison
cmp Term
et Type
t) (TCMT IO Bool -> TCM Term) -> TCMT IO Bool -> TCM Term
forall a b. (a -> b) -> a -> b
$ [TCMT IO Bool] -> TCMT IO Bool
forall (f :: * -> *) (m :: * -> *).
(Foldable f, Monad m) =>
f (m Bool) -> m Bool
andM ([TCMT IO Bool] -> TCMT IO Bool) -> [TCMT IO Bool] -> TCMT IO Bool
forall a b. (a -> b) -> a -> b
$ (MetaId -> TCMT IO Bool) -> [MetaId] -> [TCMT IO Bool]
forall a b. (a -> b) -> [a] -> [b]
map MetaId -> TCMT IO Bool
forall a (m :: * -> *).
(IsInstantiatedMeta a, MonadFail m, ReadTCState m) =>
a -> m Bool
isInstantiatedMeta [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 <- Expr -> Type -> TCM Term
checkExpr Expr
tacA (Type -> TCM Term) -> TCM Type -> TCM Term
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< (TCM Term -> TCM Type
forall (tcm :: * -> *). Functor tcm => tcm Term -> tcm Type
el TCM Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTerm TCM Type -> TCM Type -> TCM Type
forall (tcm :: * -> *).
Monad tcm =>
tcm Type -> tcm Type -> tcm Type
--> TCM Term -> TCM Type
forall (tcm :: * -> *). Functor tcm => tcm Term -> tcm Type
el (TCM Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTCM TCM Term -> TCM Term -> TCM Term
forall (tcm :: * -> *).
Monad tcm =>
tcm Term -> tcm Term -> tcm Term
<#> TCM Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primLevelZero TCM Term -> TCM Term -> TCM Term
forall (tcm :: * -> *).
Monad tcm =>
tcm Term -> tcm Term -> tcm Term
<@> TCM Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primUnit))
  TCM () -> TCM ()
forall a. TCM a -> TCM a
inFreshModuleIfFreeParams (TCM () -> TCM ()) -> TCM () -> TCM ()
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
  VerboseKey -> VerboseLevel -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.term.tactic" VerboseLevel
40 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
sep
    [ TCM Doc
"Running tactic" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Term -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
tac
    , VerboseLevel -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest VerboseLevel
2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ TCM Doc
"on" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Term -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
hole TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCM Doc
":" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Type -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
goal ]
  Either UnquoteError (Term, [QName])
ok  <- UnquoteM Term -> TCM (Either UnquoteError (Term, [QName]))
forall a. UnquoteM a -> TCM (Either UnquoteError (a, [QName]))
runUnquoteM (UnquoteM Term -> TCM (Either UnquoteError (Term, [QName])))
-> UnquoteM Term -> TCM (Either UnquoteError (Term, [QName]))
forall a b. (a -> b) -> a -> b
$ Term -> Term -> UnquoteM Term
unquoteTCM Term
tac Term
hole
  case Either UnquoteError (Term, [QName])
ok of
    Left (BlockedOnMeta TCState
oldState MetaId
x) -> do
      TCState -> TCM ()
forall (m :: * -> *). MonadTCState m => TCState -> m ()
putTC TCState
oldState
      Maybe MetaVariable
mi <- MetaId -> TCMT IO (Maybe MetaVariable)
forall (m :: * -> *).
ReadTCState m =>
MetaId -> m (Maybe MetaVariable)
lookupMeta' MetaId
x
      (Range
r, Maybe MetaId
meta) <- case Maybe MetaVariable
mi of
        Maybe MetaVariable
Nothing -> do -- fresh meta: need to block on something else!
          (Range
forall a. Range' a
noRange,) (Maybe MetaId -> (Range, Maybe MetaId))
-> (Type -> Maybe MetaId) -> Type -> (Range, Maybe MetaId)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> Maybe MetaId
forall a. TermLike a => a -> Maybe MetaId
firstMeta (Type -> (Range, Maybe MetaId))
-> TCM Type -> TCMT IO (Range, Maybe MetaId)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type -> TCM Type
forall a (m :: * -> *).
(InstantiateFull a, MonadReduce m) =>
a -> m a
instantiateFull Type
goal
            -- Remark:
            -- Nothing:  Nothing to block on, leave it yellow. Alternative: fail.
            -- Just x:   range?
        Just MetaVariable
mi -> (Range, Maybe MetaId) -> TCMT IO (Range, Maybe MetaId)
forall (m :: * -> *) a. Monad m => a -> m a
return (MetaVariable -> Range
forall t. HasRange t => t -> Range
getRange MetaVariable
mi, MetaId -> Maybe MetaId
forall a. a -> Maybe a
Just MetaId
x)
      Range -> TCM () -> TCM ()
forall (tcm :: * -> *) x a.
(MonadTCM tcm, ReadTCState tcm, MonadDebug tcm, HasRange x) =>
x -> tcm a -> tcm a
setCurrentRange Range
r (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$
        Constraint -> TCM ()
forall (m :: * -> *). MonadConstraint m => Constraint -> m ()
addConstraint (Maybe MetaId -> Term -> Term -> Type -> Constraint
UnquoteTactic Maybe MetaId
meta Term
tac Term
hole Type
goal)
    Left UnquoteError
err -> TypeError -> TCM ()
forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m, MonadError TCErr m) =>
TypeError -> m a
typeError (TypeError -> TCM ()) -> TypeError -> TCM ()
forall a b. (a -> b) -> a -> b
$ UnquoteError -> TypeError
UnquoteFailed UnquoteError
err
    Right (Term, [QName])
_ -> () -> TCM ()
forall (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
  VerboseKey -> VerboseLevel -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.interaction" VerboseLevel
20 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
sep
    [ TCM Doc
"Found interaction point"
    , VerboseKey -> TCM Doc
forall (m :: * -> *). Monad m => VerboseKey -> m Doc
text (VerboseKey -> TCM Doc)
-> (IsAbstract -> VerboseKey) -> IsAbstract -> TCM Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. IsAbstract -> VerboseKey
forall a. Show a => a -> VerboseKey
show (IsAbstract -> TCM Doc) -> TCMT IO IsAbstract -> TCM Doc
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< (TCEnv -> IsAbstract) -> TCMT IO IsAbstract
forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
asksTC (TCEnv -> Lens' IsAbstract TCEnv -> IsAbstract
forall o i. o -> Lens' i o -> i
^. forall a. LensIsAbstract a => Lens' IsAbstract a
Lens' IsAbstract TCEnv
lensIsAbstract)
    , InteractionId -> TCM Doc
forall (m :: * -> *) a. (Monad m, Pretty a) => a -> m Doc
pretty InteractionId
ii
    , TCM Doc
":"
    , Type -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
t0
    ]
  VerboseKey -> VerboseLevel -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.interaction" VerboseLevel
60 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
sep
    [ TCM Doc
"Raw:"
    , VerboseKey -> TCM Doc
forall (m :: * -> *). Monad m => VerboseKey -> m Doc
text (Type -> VerboseKey
forall a. Show a => a -> VerboseKey
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 (RunMetaOccursCheck -> Comparison -> Type -> TCM (MetaId, Term)
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 = (Term, Type) -> Term
forall a b. (a, b) -> a
fst ((Term, Type) -> Term) -> TCM (Term, Type) -> TCM Term
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 ((Comparison, Type) -> Maybe (Comparison, Type)
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 = (Term -> Elims -> Term) -> (Term, Type) -> (Elims -> Term, Type)
forall a c b. (a -> c) -> (a, b) -> (c, b)
mapFst Term -> Elims -> Term
forall t. Apply t => t -> Elims -> t
applyE ((Term, Type) -> (Elims -> Term, Type))
-> TCM (Term, Type) -> TCM (Elims -> Term, Type)
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 Maybe (Comparison, Type)
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) <- TCMT IO (Comparison, Type)
-> ((Comparison, Type) -> TCMT IO (Comparison, Type))
-> Maybe (Comparison, Type)
-> TCMT IO (Comparison, Type)
forall b a. b -> (a -> b) -> Maybe a -> b
maybe ((Comparison
CmpEq,) (Type -> (Comparison, Type))
-> TCM Type -> TCMT IO (Comparison, Type)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCM Type -> TCM Type
forall (m :: * -> *) a.
(MonadTCEnv m, HasOptions m, MonadDebug m) =>
m a -> m a
workOnTypes TCM Type
newTypeMeta_) (Comparison, Type) -> TCMT IO (Comparison, Type)
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
      MetaId -> VerboseKey -> TCM ()
forall (m :: * -> *).
MonadMetaSolver m =>
MetaId -> VerboseKey -> m ()
setMetaNameSuggestion MetaId
x (MetaInfo -> VerboseKey
A.metaNameSuggestion MetaInfo
i)
      (Term, Type) -> TCM (Term, Type)
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 []
      VerboseKey -> VerboseLevel -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.meta.check" VerboseLevel
20 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$
        TCM Doc
"checking existing meta " TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Term -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
v
      Type
t' <- MetaId -> TCM Type
forall (m :: * -> *).
(MonadFail m, ReadTCState m) =>
MetaId -> m Type
metaType MetaId
x
      VerboseKey -> VerboseLevel -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.meta.check" VerboseLevel
20 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$
        VerboseLevel -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest VerboseLevel
2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ TCM Doc
"of type " TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Type -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
t'
      case Maybe (Comparison, Type)
mt of
        Maybe (Comparison, Type)
Nothing -> (Term, Type) -> TCM (Term, Type)
forall (m :: * -> *) a. Monad m => a -> m a
return (Term
v, Type
t')
        Just (Comparison
cmp , Type
t) -> (,Type
t) (Term -> (Term, Type)) -> TCM Term -> TCM (Term, Type)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Comparison -> Term -> Type -> Type -> TCM Term
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 (TypedBinding -> LamBinding) -> TypedBinding -> LamBinding
forall a b. (a -> b) -> a -> b
$ Range -> [NamedArg Binder] -> Expr -> TypedBinding
A.mkTBind Range
r [ArgInfo -> Binder -> NamedArg Binder
forall a. ArgInfo -> a -> NamedArg a
unnamedArg ArgInfo
info (Binder -> NamedArg Binder) -> Binder -> NamedArg Binder
forall a b. (a -> b) -> a -> b
$ (Name -> BindName) -> Binder' Name -> Binder
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Name -> BindName
A.mkBindName Binder' Name
x]
               (Expr -> TypedBinding) -> Expr -> TypedBinding
forall a b. (a -> b) -> a -> b
$ MetaInfo -> Expr
A.Underscore MetaInfo
underscoreInfo
  where
    r :: Range
r = Binder' Name -> Range
forall t. HasRange t => t -> Range
getRange Binder' Name
x
    underscoreInfo :: MetaInfo
underscoreInfo = MetaInfo :: Range -> ScopeInfo -> Maybe MetaId -> VerboseKey -> MetaInfo
A.MetaInfo
      { metaRange :: Range
A.metaRange          = Range
r
      , metaScope :: ScopeInfo
A.metaScope          = ScopeInfo
emptyScopeInfo
      , metaNumber :: Maybe MetaId
A.metaNumber         = Maybe MetaId
forall a. Maybe a
Nothing
      , metaNameSuggestion :: VerboseKey
A.metaNameSuggestion = Name -> VerboseKey
forall a. Pretty a => a -> VerboseKey
prettyShow (Name -> VerboseKey) -> Name -> VerboseKey
forall a b. (a -> b) -> a -> b
$ Name -> Name
A.nameConcrete (Name -> Name) -> Name -> Name
forall a b. (a -> b) -> a -> b
$ Binder' Name -> Name
forall a. Binder' a -> a
A.binderName Binder' Name
x
      }


-- | 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 = ([Arg Term], Type) -> TCM ([Arg Term], Type)
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') <- Call -> TCM ([Arg Term], Type) -> TCM ([Arg Term], Type)
forall (tcm :: * -> *) a.
(MonadTCM tcm, ReadTCState tcm, MonadDebug tcm) =>
Call -> tcm a -> tcm a
traceCall (Range -> Call
SetRange (Range -> Call) -> Range -> Call
forall a b. (a -> b) -> a -> b
$ NamedArg Expr -> Range
forall t. HasRange t => t -> Range
getRange NamedArg Expr
arg) (TCM ([Arg Term], Type) -> TCM ([Arg Term], Type))
-> TCM ([Arg Term], Type) -> TCM ([Arg Term], Type)
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
_ = Doc -> TCM ([Arg Term], Type)
forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m, MonadError TCErr m) =>
Doc -> m a
genericDocError (Doc -> TCM ([Arg Term], Type))
-> TCM Doc -> TCM ([Arg Term], Type)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< do
  TCM Doc
"Invalid projection parameter " TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> NamedArg Expr -> TCM Doc
forall c a (m :: * -> *).
(Pretty c, ToConcrete a c, 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) <- Type -> TCMT IO (Dom Type, Abs Type)
forall (m :: * -> *).
MonadReduce m =>
Type -> m (Dom Type, Abs Type)
mustBePi Type
t
  if Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ Bool -> Maybe Bool -> Bool
forall a. a -> Maybe a -> a
fromMaybe Bool
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe Bool -> Bool) -> Maybe Bool -> Bool
forall a b. (a -> b) -> a -> b
$ NamedArg Expr -> Dom Type -> Maybe Bool
forall arg dom.
(LensNamed (WithOrigin (Ranged VerboseKey)) arg, LensHiding arg,
 LensNamed (WithOrigin (Ranged VerboseKey)) dom, 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 Abs Type -> Term -> Type
forall t a. Subst t a => Abs a -> t -> a
`absApp` Term
v)
    -- Found the right argument
    else do
      Term
u <- NamedArg Expr -> Type -> TCM Term
checkNamedArg NamedArg Expr
arg Type
a
      Type -> Term -> Term -> TCM ()
forall (m :: * -> *).
MonadConversion m =>
Type -> Term -> Term -> m ()
equalTerm Type
a Term
u Term
v
      ([Arg Term], Type) -> TCM ([Arg Term], Type)
forall (m :: * -> *) a. Monad m => a -> m a
return ([Arg Term]
vs, Abs Type
b Abs Type -> Term -> Type
forall t a. Subst t a => Abs a -> t -> 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 = Named_ Expr -> Expr
forall name a. Named name a -> a
namedThing Named_ Expr
e0
  let x :: VerboseKey
x = VerboseKey -> Named_ Expr -> VerboseKey
forall a.
LensNamed (WithOrigin (Ranged VerboseKey)) a =>
VerboseKey -> a -> VerboseKey
bareNameWithDefault VerboseKey
"" Named_ Expr
e0
  Call -> TCM Term -> TCM Term
forall (tcm :: * -> *) a.
(MonadTCM tcm, ReadTCState tcm, MonadDebug tcm) =>
Call -> tcm a -> tcm a
traceCall (Comparison -> Expr -> Type -> Call
CheckExprCall Comparison
CmpLeq Expr
e Type
t0) (TCM Term -> TCM Term) -> TCM Term -> TCM Term
forall a b. (a -> b) -> a -> b
$ do
    VerboseKey -> VerboseLevel -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.term.args.named" VerboseLevel
15 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ do
        TCM Doc
"Checking named arg" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [TCM Doc] -> TCM Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
sep
          [ [TCM Doc] -> TCM Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
fsep [ NamedArg Expr -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM NamedArg Expr
arg, TCM Doc
":", Type -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
t0 ]
          ]
    VerboseKey -> VerboseLevel -> VerboseKey -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> VerboseKey -> m ()
reportSLn VerboseKey
"tc.term.args.named" VerboseLevel
75 (VerboseKey -> TCM ()) -> VerboseKey -> TCM ()
forall a b. (a -> b) -> a -> b
$ VerboseKey
"  arg = " VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ NamedArg Expr -> VerboseKey
forall a. Show a => a -> VerboseKey
show (NamedArg Expr -> NamedArg Expr
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 (ArgInfo -> VerboseKey -> Comparison -> Type -> TCM (MetaId, Term)
forall (m :: * -> *).
MonadMetaSolver m =>
ArgInfo -> VerboseKey -> Comparison -> Type -> m (MetaId, Term)
newMetaArg (Hiding -> ArgInfo -> ArgInfo
forall a. LensHiding a => Hiding -> a -> a
setHiding Hiding
Hidden ArgInfo
info) VerboseKey
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 -> VerboseKey -> Comparison -> Type -> TCM (MetaId, Term)
newInteractionMetaArg (Hiding -> ArgInfo -> ArgInfo
forall a. LensHiding a => Hiding -> a -> a
setHiding Hiding
Hidden ArgInfo
info) VerboseKey
x) Comparison
CmpLeq Type
t0
    if Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ Expr -> Bool
isHole Expr
e then Expr -> Type -> TCM Term
checkExpr Expr
e Type
t0 else TCM Term -> TCM Term
forall a. TCM a -> TCM a
localScope (TCM Term -> TCM Term) -> TCM Term -> TCM Term
forall a b. (a -> b) -> a -> b
$ do
      -- Note: we need localScope here,
      -- as scopedExpr manipulates the scope in the state.
      -- However, we may not pull localScope over checkExpr!
      -- This is why we first test for isHole, and only do
      -- scope manipulations if we actually handle the checking
      -- of e here (and not pass it to checkExpr).
      Expr -> TCM Expr
scopedExpr Expr
e TCM Expr -> (Expr -> TCM Term) -> TCM Term
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
_ -> TCM Term
forall a. HasCallStack => a
__IMPOSSIBLE__
  where
  isHole :: Expr -> Bool
isHole A.Underscore{} = Bool
True
  isHole A.QuestionMark{} = Bool
True
  isHole (A.ScopedExpr ScopeInfo
_ Expr
e) = Expr -> Bool
isHole Expr
e
  isHole Expr
_ = Bool
False

-- | Infer the type of an expression. Implemented by checking against a meta
--   variable.  Except for neutrals, for them a polymorphic type is inferred.
inferExpr :: A.Expr -> TCM (Term, Type)
-- inferExpr e = inferOrCheck e Nothing
inferExpr :: Expr -> TCM (Term, Type)
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 = Call -> TCM (Term, Type) -> TCM (Term, Type)
forall (tcm :: * -> *) a.
(MonadTCM tcm, ReadTCState tcm, MonadDebug tcm) =>
Call -> tcm a -> tcm a
traceCall (Expr -> Call
InferExpr Expr
e) (TCM (Term, Type) -> TCM (Term, Type))
-> TCM (Term, Type) -> TCM (Term, Type)
forall a b. (a -> b) -> a -> b
$ do
  let Application Expr
hd [NamedArg Expr]
args = Expr -> AppView' Expr
appView Expr
e
  VerboseKey -> VerboseLevel -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.infer" VerboseLevel
30 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
vcat
    [ TCM Doc
"inferExpr': appView of " TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Expr -> TCM Doc
forall c a (m :: * -> *).
(Pretty c, ToConcrete a c, MonadAbsToCon m) =>
a -> m Doc
prettyA Expr
e
    , TCM Doc
"  hd   = " TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Expr -> TCM Doc
forall c a (m :: * -> *).
(Pretty c, ToConcrete a c, MonadAbsToCon m) =>
a -> m Doc
prettyA Expr
hd
    , TCM Doc
"  args = " TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [NamedArg Expr] -> TCM Doc
forall c a (m :: * -> *).
(Pretty c, ToConcrete a [c], MonadAbsToCon m) =>
a -> m Doc
prettyAs [NamedArg Expr]
args
    ]
  VerboseKey -> VerboseLevel -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.infer" VerboseLevel
60 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
vcat
    [ VerboseKey -> TCM Doc
forall (m :: * -> *). Monad m => VerboseKey -> m Doc
text (VerboseKey -> TCM Doc) -> VerboseKey -> TCM Doc
forall a b. (a -> b) -> a -> b
$ VerboseKey
"  hd (raw) = " VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ Expr -> VerboseKey
forall a. Show a => a -> VerboseKey
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 ->
    Call -> TCM Term -> TCM Term
forall (tcm :: * -> *) a.
(MonadTCM tcm, ReadTCState tcm, MonadDebug tcm) =>
Call -> tcm a -> tcm a
traceCall (Comparison -> Expr -> Type -> Call
CheckExprCall Comparison
cmp Expr
e Type
t) (TCM Term -> TCM Term) -> TCM Term -> TCM Term
forall a b. (a -> b) -> a -> b
$ TCM Term -> TCM Term
forall a. TCM a -> TCM a
localScope (TCM Term -> TCM Term) -> TCM Term -> TCM Term
forall a b. (a -> b) -> a -> b
$ TCM Term -> TCM Term
forall a. TCM a -> TCM a
dontExpandLast (TCM Term -> TCM Term) -> TCM Term -> TCM Term
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 :: VerboseLevel -> TCMT IO Bool
isModuleFreeVar VerboseLevel
i = do
  [Arg Term]
params <- ModuleName -> TCMT IO [Arg Term]
forall (m :: * -> *).
(Functor m, Applicative m, HasOptions m, MonadTCEnv m,
 ReadTCState m, MonadDebug m) =>
ModuleName -> m [Arg Term]
moduleParamsToApply (ModuleName -> TCMT IO [Arg Term])
-> TCMT IO ModuleName -> TCMT IO [Arg Term]
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< TCMT IO ModuleName
forall (m :: * -> *). MonadTCEnv m => m ModuleName
currentModule
  Bool -> TCMT IO Bool
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool -> TCMT IO Bool) -> Bool -> TCMT IO Bool
forall a b. (a -> b) -> a -> b
$ (Arg Term -> Bool) -> [Arg Term] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any ((Term -> Term -> Bool
forall a. Eq a => a -> a -> Bool
== VerboseLevel -> Elims -> Term
Var VerboseLevel
i []) (Term -> Bool) -> (Arg Term -> Term) -> Arg Term -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Arg Term -> Term
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 :: A.Expr -> TCM (Term, Type)
inferExprForWith :: Expr -> TCM (Term, Type)
inferExprForWith Expr
e = do
  VerboseKey -> VerboseLevel -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.with.infer" VerboseLevel
20 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ TCM Doc
"inferExprforWith " TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Expr -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Expr
e
  VerboseKey -> VerboseLevel -> VerboseKey -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> VerboseKey -> m ()
reportSLn  VerboseKey
"tc.with.infer" VerboseLevel
80 (VerboseKey -> TCM ()) -> VerboseKey -> TCM ()
forall a b. (a -> b) -> a -> b
$ VerboseKey
"inferExprforWith " VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ Expr -> VerboseKey
forall a. Show a => a -> VerboseKey
show (Expr -> Expr
forall a. ExprLike a => a -> a
deepUnscope Expr
e)
  Call -> TCM (Term, Type) -> TCM (Term, Type)
forall (tcm :: * -> *) a.
(MonadTCM tcm, ReadTCState tcm, MonadDebug tcm) =>
Call -> tcm a -> tcm a
traceCall (Expr -> Call
InferExpr Expr
e) (TCM (Term, Type) -> TCM (Term, Type))
-> TCM (Term, Type) -> TCM (Term, Type)
forall a b. (a -> b) -> a -> b
$ do
    -- With wants type and term fully instantiated!
    (Term
v, Type
t) <- (Term, Type) -> TCM (Term, Type)
forall a (m :: * -> *).
(InstantiateFull a, MonadReduce m) =>
a -> m a
instantiateFull ((Term, Type) -> TCM (Term, Type))
-> TCM (Term, Type) -> TCM (Term, Type)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Expr -> TCM (Term, Type)
inferExpr Expr
e
    Term
v0 <- Term -> TCM Term
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 VerboseLevel
i [] -> TCMT IO Bool -> TCM () -> TCM ()
forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
whenM (VerboseLevel -> TCMT IO Bool
isModuleFreeVar VerboseLevel
i) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ do
        VerboseKey -> VerboseLevel -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.with.infer" VerboseLevel
80 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
vcat
          [ VerboseKey -> TCM Doc
forall (m :: * -> *). Monad m => VerboseKey -> m Doc
text (VerboseKey -> TCM Doc) -> VerboseKey -> TCM Doc
forall a b. (a -> b) -> a -> b
$ VerboseKey
"with expression is variable " VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ VerboseLevel -> VerboseKey
forall a. Show a => a -> VerboseKey
show VerboseLevel
i
          , TCM Doc
"current modules = " TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> do VerboseKey -> TCM Doc
forall (m :: * -> *). Monad m => VerboseKey -> m Doc
text (VerboseKey -> TCM Doc)
-> (ModuleName -> VerboseKey) -> ModuleName -> TCM Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ModuleName -> VerboseKey
forall a. Show a => a -> VerboseKey
show (ModuleName -> TCM Doc) -> TCMT IO ModuleName -> TCM Doc
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< TCMT IO ModuleName
forall (m :: * -> *). MonadTCEnv m => m ModuleName
currentModule
          , TCM Doc
"current module free vars = " TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> do VerboseKey -> TCM Doc
forall (m :: * -> *). Monad m => VerboseKey -> m Doc
text (VerboseKey -> TCM Doc)
-> (VerboseLevel -> VerboseKey) -> VerboseLevel -> TCM Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. VerboseLevel -> VerboseKey
forall a. Show a => a -> VerboseKey
show (VerboseLevel -> TCM Doc) -> TCMT IO VerboseLevel -> TCM Doc
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< TCMT IO VerboseLevel
getCurrentModuleFreeVars
          , TCM Doc
"context size = " TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> do VerboseKey -> TCM Doc
forall (m :: * -> *). Monad m => VerboseKey -> m Doc
text (VerboseKey -> TCM Doc)
-> (VerboseLevel -> VerboseKey) -> VerboseLevel -> TCM Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. VerboseLevel -> VerboseKey
forall a. Show a => a -> VerboseKey
show (VerboseLevel -> TCM Doc) -> TCMT IO VerboseLevel -> TCM Doc
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< TCMT IO VerboseLevel
forall (m :: * -> *).
(Applicative m, MonadTCEnv m) =>
m VerboseLevel
getContextSize
          , TCM Doc
"current context = " TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> do Telescope -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM (Telescope -> TCM Doc) -> TCMT IO Telescope -> TCM Doc
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< TCMT IO Telescope
forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Telescope
getContextTelescope
          ]
        TypeError -> TCM ()
forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m, MonadError TCErr m) =>
TypeError -> m a
typeError (TypeError -> TCM ()) -> TypeError -> TCM ()
forall a b. (a -> b) -> a -> b
$ Expr -> Term -> TypeError
WithOnFreeVariable Expr
e Term
v0
      Term
_        -> () -> TCM ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
    -- Possibly insert hidden arguments.
    TelV Telescope
tel Type
t0 <- VerboseLevel -> (Dom Type -> Bool) -> Type -> TCMT IO (TelV Type)
forall (m :: * -> *).
(MonadReduce m, MonadAddContext m) =>
VerboseLevel -> (Dom Type -> Bool) -> Type -> m (TelV Type)
telViewUpTo' (-VerboseLevel
1) (Bool -> Bool
not (Bool -> Bool) -> (Dom Type -> Bool) -> Dom Type -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Dom Type -> Bool
forall a. LensHiding a => a -> Bool
visible) Type
t
    case Type -> Term
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 -> (Term, Type) -> TCM (Term, Type)
forall (m :: * -> *) a. Monad m => a -> m a
return (Term
v, Type
t)
          Just{}  -> do
            ([Arg Term]
args, Type
t1) <- VerboseLevel -> (Hiding -> Bool) -> Type -> TCM ([Arg Term], Type)
forall (m :: * -> *).
(MonadReduce m, MonadMetaSolver m, MonadDebug m, MonadTCM m) =>
VerboseLevel -> (Hiding -> Bool) -> Type -> m ([Arg Term], Type)
implicitArgs (-VerboseLevel
1) Hiding -> Bool
forall a. LensHiding a => a -> Bool
notVisible Type
t
            (Term, Type) -> TCM (Term, Type)
forall (m :: * -> *) a. Monad m => a -> m a
return (Term
v Term -> [Arg Term] -> Term
forall t. Apply t => t -> [Arg Term] -> t
`apply` [Arg Term]
args, Type
t1)
      Term
_ -> (Term, Type) -> TCM (Term, Type)
forall (m :: * -> *) a. Monad m => a -> m a
return (Term
v, Type
t)

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

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

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

checkLetBinding :: LetBinding -> TCM a -> TCM a
checkLetBinding b :: LetBinding
b@(A.LetBind LetInfo
i ArgInfo
info BindName
x Expr
t Expr
e) TCM a
ret =
  Call -> TCM a -> TCM a
forall (tcm :: * -> *) a.
(MonadTCM tcm, ReadTCState tcm, MonadDebug tcm) =>
Call -> tcm a -> tcm a
traceCall (LetBinding -> Call
CheckLetBinding LetBinding
b) (TCM a -> TCM a) -> TCM a -> TCM a
forall a b. (a -> b) -> a -> b
$ do
    Type
t <- Expr -> TCM Type
isType_ Expr
t
    Term
v <- ArgInfo -> TCM Term -> TCM Term
forall (tcm :: * -> *) m a.
(MonadTCEnv tcm, LensModality m) =>
m -> tcm a -> tcm a
applyModalityToContext ArgInfo
info (TCM Term -> TCM Term) -> TCM Term -> TCM Term
forall a b. (a -> b) -> a -> b
$ Comparison -> Expr -> Type -> TCM Term
checkDontExpandLast Comparison
CmpLeq Expr
e Type
t
    ArgInfo -> Name -> Term -> Type -> TCM a -> TCM a
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 =
  Call -> TCM a -> TCM a
forall (tcm :: * -> *) a.
(MonadTCM tcm, ReadTCState tcm, MonadDebug tcm) =>
Call -> tcm a -> tcm a
traceCall (LetBinding -> Call
CheckLetBinding LetBinding
b) (TCM a -> TCM a) -> TCM a -> TCM a
forall a b. (a -> b) -> a -> b
$ do
    Pattern
p <- Pattern -> TCM Pattern
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 = Sort -> Term -> Type
forall t a. Sort' t -> a -> Type'' t a
El (Type -> Sort
forall a. LensSort a => a -> Sort
getSort Type
t) (Term -> Type) -> Term -> Type
forall a b. (a -> b) -> a -> b
$ Dom Type -> Abs Type -> Term
Pi (Type -> Dom Type
forall a. a -> Dom a
defaultDom Type
t) (VerboseKey -> Type -> Abs Type
forall a. VerboseKey -> a -> Abs a
NoAbs VerboseKey
forall a. Underscore a => a
underscore Type
HasCallStack => Type
__DUMMY_TYPE__)
        p0 :: Arg (Named name Pattern)
p0 = ArgInfo -> Named name Pattern -> Arg (Named name Pattern)
forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
defaultArgInfo (Maybe name -> Pattern -> Named name Pattern
forall name a. Maybe name -> a -> Named name a
Named Maybe name
forall a. Maybe a
Nothing Pattern
p)
    VerboseKey -> VerboseLevel -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.term.let.pattern" VerboseLevel
10 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
vcat
      [ TCM Doc
"let-binding pattern p at type t"
      , VerboseLevel -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest VerboseLevel
2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
vcat
        [ TCM Doc
"p (A) =" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Pattern -> TCM Doc
forall c a (m :: * -> *).
(Pretty c, ToConcrete a c, MonadAbsToCon m) =>
a -> m Doc
prettyA Pattern
p
        , TCM Doc
"t     =" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Type -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
t
        , TCM Doc
"cxtRel=" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> do Relevance -> TCM Doc
forall (m :: * -> *) a. (Monad m, Pretty a) => a -> m Doc
pretty (Relevance -> TCM Doc) -> TCMT IO Relevance -> TCM Doc
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< (TCEnv -> Relevance) -> TCMT IO Relevance
forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
asksTC TCEnv -> Relevance
forall a. LensRelevance a => a -> Relevance
getRelevance
        , TCM Doc
"cxtQnt=" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> do Quantity -> TCM Doc
forall (m :: * -> *) a. (Monad m, Pretty a) => a -> m Doc
pretty (Quantity -> TCM Doc) -> TCMT IO Quantity -> TCM Doc
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< (TCEnv -> Quantity) -> TCMT IO Quantity
forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
asksTC TCEnv -> Quantity
forall a. LensQuantity a => a -> Quantity
getQuantity
        ]
      ]
    VerboseLevel
fvs <- TCMT IO VerboseLevel
forall (m :: * -> *).
(Applicative m, MonadTCEnv m) =>
m VerboseLevel
getContextSize
    Call
-> Maybe QName
-> [NamedArg Pattern]
-> Type
-> Maybe Substitution
-> [ProblemEq]
-> (LHSResult -> TCM a)
-> TCM a
forall a.
Call
-> Maybe QName
-> [NamedArg Pattern]
-> Type
-> Maybe Substitution
-> [ProblemEq]
-> (LHSResult -> TCM a)
-> TCM a
checkLeftHandSide (Pattern -> Telescope -> Type -> Call
CheckPattern Pattern
p Telescope
forall a. Tele a
EmptyTel Type
t) Maybe QName
forall a. Maybe a
Nothing [NamedArg Pattern
forall name. Arg (Named name Pattern)
p0] Type
t0 Maybe Substitution
forall a. Maybe a
Nothing [] ((LHSResult -> TCM a) -> TCM a) -> (LHSResult -> TCM a) -> TCM a
forall a b. (a -> b) -> a -> b
$ \ (LHSResult VerboseLevel
_ Telescope
delta0 NAPs
ps Bool
_ Arg Type
_t Substitution
_ [AsBinding]
asb IntSet
_) -> [AsBinding] -> TCM a -> TCM a
forall a. [AsBinding] -> TCM a -> TCM a
bindAsPatterns [AsBinding]
asb (TCM a -> TCM a) -> TCM a -> TCM a
forall a b. (a -> b) -> a -> b
$ do
          -- After dropping the free variable patterns there should be a single pattern left.
      let p :: DeBruijnPattern
p = case VerboseLevel -> NAPs -> NAPs
forall a. VerboseLevel -> [a] -> [a]
drop VerboseLevel
fvs NAPs
ps of [Arg (Named (WithOrigin (Ranged VerboseKey)) DeBruijnPattern)
p] -> Arg (Named (WithOrigin (Ranged VerboseKey)) DeBruijnPattern)
-> DeBruijnPattern
forall a. NamedArg a -> a
namedArg Arg (Named (WithOrigin (Ranged VerboseKey)) DeBruijnPattern)
p; NAPs
_ -> DeBruijnPattern
forall a. HasCallStack => a
__IMPOSSIBLE__
          -- Also strip the context variables from the telescope
          delta :: Telescope
delta = ListTel -> Telescope
telFromList (ListTel -> Telescope) -> ListTel -> Telescope
forall a b. (a -> b) -> a -> b
$ VerboseLevel -> ListTel -> ListTel
forall a. VerboseLevel -> [a] -> [a]
drop VerboseLevel
fvs (ListTel -> ListTel) -> ListTel -> ListTel
forall a b. (a -> b) -> a -> b
$ Telescope -> ListTel
forall t. Tele (Dom t) -> [Dom (VerboseKey, t)]
telToList Telescope
delta0
      VerboseKey -> VerboseLevel -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.term.let.pattern" VerboseLevel
20 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ VerboseLevel -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest VerboseLevel
2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
vcat
        [ TCM Doc
"p (I) =" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> DeBruijnPattern -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM DeBruijnPattern
p
        , TCM Doc
"delta =" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Telescope -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Telescope
delta
        , TCM Doc
"cxtRel=" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> do Relevance -> TCM Doc
forall (m :: * -> *) a. (Monad m, Pretty a) => a -> m Doc
pretty (Relevance -> TCM Doc) -> TCMT IO Relevance -> TCM Doc
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< (TCEnv -> Relevance) -> TCMT IO Relevance
forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
asksTC TCEnv -> Relevance
forall a. LensRelevance a => a -> Relevance
getRelevance
        , TCM Doc
"cxtQnt=" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> do Quantity -> TCM Doc
forall (m :: * -> *) a. (Monad m, Pretty a) => a -> m Doc
pretty (Quantity -> TCM Doc) -> TCMT IO Quantity -> TCM Doc
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< (TCEnv -> Quantity) -> TCMT IO Quantity
forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
asksTC TCEnv -> Quantity
forall a. LensQuantity a => a -> Quantity
getQuantity
        ]
      VerboseKey -> VerboseLevel -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.term.let.pattern" VerboseLevel
80 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ VerboseLevel -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest VerboseLevel
2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
vcat
        [ TCM Doc
"p (I) =" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> (VerboseKey -> TCM Doc
forall (m :: * -> *). Monad m => VerboseKey -> m Doc
text (VerboseKey -> TCM Doc)
-> (DeBruijnPattern -> VerboseKey) -> DeBruijnPattern -> TCM Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DeBruijnPattern -> VerboseKey
forall a. Show a => a -> VerboseKey
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 <- TCMT IO [ContextEntry]
forall (m :: * -> *). MonadTCEnv m => m [ContextEntry]
getContext
      let ([ContextEntry]
binds, [ContextEntry]
cxt) = VerboseLevel -> [ContextEntry] -> ([ContextEntry], [ContextEntry])
forall a. VerboseLevel -> [a] -> ([a], [a])
splitAt (Telescope -> VerboseLevel
forall a. Sized a => a -> VerboseLevel
size Telescope
delta) [ContextEntry]
cxt0
          toDrop :: VerboseLevel
toDrop       = [ContextEntry] -> VerboseLevel
forall (t :: * -> *) a. Foldable t => t a -> VerboseLevel
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 = ((Term -> Term) -> Term) -> [Term -> Term] -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map ((Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ Term
v) [Term -> Term]
fs
          -- We apply the types of the let bound-variables to this substitution.
          -- The 0th variable in a context is the last one, so we reverse.
          -- Further, we need to lower all other de Bruijn indices by
          -- the size of delta, so we append the identity substitution.
          sub :: Substitution
sub    = [Term] -> Substitution
forall a. DeBruijn a => [a] -> Substitution' a
parallelS ([Term] -> [Term]
forall a. [a] -> [a]
reverse [Term]
sigma)

      Substitution
-> ([ContextEntry] -> [ContextEntry]) -> TCM a -> TCM a
forall (m :: * -> *) a.
MonadAddContext m =>
Substitution -> ([ContextEntry] -> [ContextEntry]) -> m a -> m a
updateContext Substitution
sub (VerboseLevel -> [ContextEntry] -> [ContextEntry]
forall a. VerboseLevel -> [a] -> [a]
drop VerboseLevel
toDrop) (TCM a -> TCM a) -> TCM a -> TCM a
forall a b. (a -> b) -> a -> b
$ do
        VerboseKey -> VerboseLevel -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.term.let.pattern" VerboseLevel
20 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ VerboseLevel -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest VerboseLevel
2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
vcat
          [ TCM Doc
"delta =" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Telescope -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Telescope
delta
          , TCM Doc
"binds =" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [ContextEntry] -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM [ContextEntry]
binds
          ]
        let fdelta :: [Dom Type]
fdelta = Telescope -> [Dom Type]
forall a. Subst Term a => Tele (Dom a) -> [Dom a]
flattenTel Telescope
delta
        VerboseKey -> VerboseLevel -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.term.let.pattern" VerboseLevel
20 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ VerboseLevel -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest VerboseLevel
2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
vcat
          [ TCM Doc
"fdelta =" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Telescope -> TCM Doc -> TCM Doc
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
delta ([Dom Type] -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM [Dom Type]
fdelta)
          ]
        let tsl :: [Dom Type]
tsl  = Substitution -> [Dom Type] -> [Dom Type]
forall t a. Subst t a => Substitution' t -> a -> a
applySubst Substitution
sub [Dom Type]
fdelta
        -- We get a list of types
        let ts :: [Type]
ts   = (Dom Type -> Type) -> [Dom Type] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map Dom Type -> Type
forall t e. Dom' t e -> e
unDom [Dom Type]
tsl
        -- and relevances.
        let infos :: [ArgInfo]
infos = (Dom Type -> ArgInfo) -> [Dom Type] -> [ArgInfo]
forall a b. (a -> b) -> [a] -> [b]
map Dom Type -> ArgInfo
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   = (ContextEntry -> Name) -> [ContextEntry] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map ((Name, Type) -> Name
forall a b. (a, b) -> a
fst ((Name, Type) -> Name)
-> (ContextEntry -> (Name, Type)) -> ContextEntry -> Name
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ContextEntry -> (Name, Type)
forall t e. Dom' t e -> e
unDom) ([ContextEntry] -> [ContextEntry]
forall a. [a] -> [a]
reverse [ContextEntry]
binds)
        -- We add all the bindings to the context.
        ((ArgInfo, Name, Term, Type) -> TCM a -> TCM a)
-> TCM a -> [(ArgInfo, Name, Term, Type)] -> TCM a
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr ((ArgInfo -> Name -> Term -> Type -> TCM a -> TCM a)
-> (ArgInfo, Name, Term, Type) -> TCM a -> TCM a
forall a b c d e. (a -> b -> c -> d -> e) -> (a, b, c, d) -> e
uncurry4 ArgInfo -> Name -> Term -> Type -> TCM a -> TCM a
forall (m :: * -> *) a.
MonadAddContext m =>
ArgInfo -> Name -> Term -> Type -> m a -> m a
addLetBinding) TCM a
ret ([(ArgInfo, Name, Term, Type)] -> TCM a)
-> [(ArgInfo, Name, Term, Type)] -> TCM a
forall a b. (a -> b) -> a -> b
$ [ArgInfo]
-> [Name] -> [Term] -> [Type] -> [(ArgInfo, Name, Term, Type)]
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@.
  VerboseLevel
fv   <- TCMT IO VerboseLevel
getCurrentModuleFreeVars
  VerboseLevel
n    <- TCMT IO VerboseLevel
forall (m :: * -> *).
(Applicative m, MonadTCEnv m) =>
m VerboseLevel
getContextSize
  let new :: VerboseLevel
new = VerboseLevel
n VerboseLevel -> VerboseLevel -> VerboseLevel
forall a. Num a => a -> a -> a
- VerboseLevel
fv
  VerboseKey -> VerboseLevel -> VerboseKey -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> VerboseKey -> m ()
reportSLn VerboseKey
"tc.term.let.apply" VerboseLevel
10 (VerboseKey -> TCM ()) -> VerboseKey -> TCM ()
forall a b. (a -> b) -> a -> b
$ VerboseKey
"Applying " VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ ModuleApplication -> VerboseKey
forall a. Show a => a -> VerboseKey
show ModuleApplication
modapp VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ VerboseKey
" with " VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ VerboseLevel -> VerboseKey
forall a. Show a => a -> VerboseKey
show VerboseLevel
new VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ VerboseKey
" free variables"
  VerboseKey -> VerboseLevel -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.term.let.apply" VerboseLevel
20 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
vcat
    [ TCM Doc
"context =" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> (Telescope -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM (Telescope -> TCM Doc) -> TCMT IO Telescope -> TCM Doc
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< TCMT IO Telescope
forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Telescope
getContextTelescope)
    , TCM Doc
"module  =" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> (ModuleName -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM (ModuleName -> TCM Doc) -> TCMT IO ModuleName -> TCM Doc
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< TCMT IO ModuleName
forall (m :: * -> *). MonadTCEnv m => m ModuleName
currentModule)
    , TCM Doc
"fv      =" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> (VerboseKey -> TCM Doc
forall (m :: * -> *). Monad m => VerboseKey -> m Doc
text (VerboseKey -> TCM Doc) -> VerboseKey -> TCM Doc
forall a b. (a -> b) -> a -> b
$ VerboseLevel -> VerboseKey
forall a. Show a => a -> VerboseKey
show VerboseLevel
fv)
    ]
  ModuleInfo
-> ModuleName -> ModuleApplication -> ScopeCopyInfo -> TCM ()
checkSectionApplication ModuleInfo
i ModuleName
x ModuleApplication
modapp ScopeCopyInfo
copyInfo
  ModuleName -> VerboseLevel -> TCM a -> TCM a
forall a. ModuleName -> VerboseLevel -> TCM a -> TCM a
withAnonymousModule ModuleName
x VerboseLevel
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