{-# LANGUAGE CPP #-}
{-# LANGUAGE NondecreasingIndentation #-}
module Agda.TypeChecking.Rules.Term where
#if MIN_VERSION_base(4,11,0)
import Prelude hiding ( (<>), null )
#else
import Prelude hiding ( null )
#endif
import Control.Monad.Trans
import Control.Monad.Trans.Maybe
import Control.Monad.State (get, put)
import Control.Monad.Reader
import Data.Maybe
import Data.Either (partitionEithers)
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 (storeDisambiguatedName)
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 ()
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.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.Datatypes
import Agda.TypeChecking.EtaContract
import Agda.TypeChecking.Implicit
import Agda.TypeChecking.Irrelevance
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 {-# SOURCE #-} Agda.TypeChecking.Empty (isEmptyType)
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
( ExceptT
, MonadError(catchError, throwError)
, runExceptT
)
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.NonemptyList
import Agda.Utils.Pretty ( prettyShow )
import qualified Agda.Utils.Pretty as P
import Agda.Utils.Size
import Agda.Utils.Tuple
#include "undefined.h"
import Agda.Utils.Impossible
isType :: A.Expr -> Sort -> TCM Type
isType e s =
traceCall (IsTypeCall e s) $ do
v <- checkExpr e (sort s)
return $ El s v
isType_ :: A.Expr -> TCM Type
isType_ e = traceCall (IsType_ e) $ do
let fallback = isType e =<< do workOnTypes $ newSortMeta
case unScope e of
A.Fun i (Arg info t) b -> do
a <- Dom info <$> isType_ t
b <- isType_ b
s <- inferFunSort (getSort a) (getSort b)
let t' = El s $ Pi a $ NoAbs underscore b
noFunctionsIntoSize b t'
return t'
A.Pi _ tel e | null tel -> isType_ e
A.Pi _ tel e -> do
(t0, t') <- checkPiTelescope tel $ \ tel -> do
t0 <- instantiateFull =<< isType_ e
tel <- instantiateFull tel
return (t0, telePi tel t0)
checkTelePiSort t'
noFunctionsIntoSize t0 t'
return t'
A.Set _ n -> do
return $ sort (mkType n)
A.App i s arg
| visible arg,
A.Set _ 0 <- unScope s ->
ifNotM hasUniversePolymorphism
(typeError $ GenericError "Use --universe-polymorphism to enable level arguments to Set")
$ do
lvl <- levelType
n <- levelView =<< do
applyRelevanceToContext NonStrict $
checkNamedArg arg lvl
return $ sort (Type n)
A.QuestionMark minfo ii -> caseMaybeM (lookupInteractionMeta ii) fallback $ \ x -> do
reportSDoc "tc.ip" 20 $ fsep
[ text "Rechecking meta "
, prettyTCM x
, text $ " for interaction point " ++ show ii
]
mv <- lookupMeta x
let s0 = jMetaType . mvJudgement $ mv
let n = length . envContext . clEnv . miClosRange . mvInfo $ mv
(vs, rest) <- splitAt n <$> getContextArgs
reportSDoc "tc.ip" 20 $ vcat
[ text " s0 = " <+> prettyTCM s0
, text " vs = " <+> prettyTCM vs
, text " rest = " <+> prettyTCM rest
]
if (length vs /= n) then fallback else do
s1 <- piApplyM s0 vs
case unEl s1 of
Sort s -> return $ El s $ MetaV x $ map Apply vs
_ -> __IMPOSSIBLE__
_ -> fallback
noFunctionsIntoSize :: Type -> Type -> TCM ()
noFunctionsIntoSize t tBlame = do
reportSDoc "tc.fun" 20 $ do
let El s (Pi dom b) = tBlame
sep [ text "created function type " <+> prettyTCM tBlame
, text "with pts rule" <+> prettyTCM (getSort dom, getSort b, s)
]
s <- reduce $ getSort t
when (s == SizeUniv) $ do
typeError $ FunctionTypeInSizeUniv $ unEl tBlame
isTypeEqualTo :: A.Expr -> Type -> TCM Type
isTypeEqualTo e0 t = scopedExpr e0 >>= \case
A.ScopedExpr{} -> __IMPOSSIBLE__
A.Underscore i | A.metaNumber i == Nothing -> return t
e -> workOnTypes $ do
t' <- isType e (getSort t)
t' <$ leqType t t'
leqType_ :: Type -> Type -> TCM ()
leqType_ t t' = workOnTypes $ leqType t t'
checkTelescope :: A.Telescope -> (Telescope -> TCM a) -> TCM a
checkTelescope = checkTelescope' LamNotPi
checkPiTelescope :: A.Telescope -> (Telescope -> TCM a) -> TCM a
checkPiTelescope = checkTelescope' PiNotLam
data LamOrPi
= LamNotPi
| PiNotLam
deriving (Eq, Show)
checkTelescope' :: LamOrPi -> A.Telescope -> (Telescope -> TCM a) -> TCM a
checkTelescope' lamOrPi [] ret = ret EmptyTel
checkTelescope' lamOrPi (b : tel) ret =
checkTypedBindings lamOrPi b $ \tel1 ->
checkTelescope' lamOrPi tel $ \tel2 ->
ret $ abstract tel1 tel2
checkTypedBindings :: LamOrPi -> A.TypedBindings -> (Telescope -> TCM a) -> TCM a
checkTypedBindings lamOrPi (A.TypedBindings i (Arg info b)) ret =
checkTypedBinding lamOrPi info b $ \ bs ->
ret $ telFromList bs
checkTypedBinding :: LamOrPi -> ArgInfo -> A.TypedBinding -> (ListTel -> TCM a) -> TCM a
checkTypedBinding lamOrPi info (A.TBind i xs' e) ret = do
let xs = map (fmap A.unBind) xs'
experimental <- optExperimentalIrrelevance <$> pragmaOptions
t <- modEnv lamOrPi $ isType_ e
let info' = mapRelevance (modRel lamOrPi experimental) info
addContext (xs, Dom info' t) $
ret $ bindsWithHidingToTel xs (Dom info t)
where
modEnv LamNotPi = workOnTypes
modEnv _ = id
modRel PiNotLam xp = if xp then irrToNonStrict . nonStrictToRel else nonStrictToRel
modRel _ _ = id
checkTypedBinding lamOrPi info (A.TLet _ lbs) ret = do
checkLetBindings lbs (ret [])
checkLambda :: Arg A.TypedBinding -> A.Expr -> Type -> TCM Term
checkLambda (Arg _ (A.TLet _ lbs)) body target =
checkLetBindings lbs (checkExpr body target)
checkLambda (Arg info (A.TBind _ xs' typ)) body target = do
reportSLn "tc.term.lambda" 60 $ "checkLambda xs = " ++ prettyShow xs
let numbinds = length xs
TelV tel btyp <- telViewUpTo numbinds target
if size tel < numbinds || numbinds /= 1
then dontUseTargetType
else useTargetType tel btyp
where
xs = map (fmap A.unBind) xs'
dontUseTargetType = do
verboseS "tc.term.lambda" 5 $ tick "lambda-no-target-type"
argsT <- workOnTypes $ Dom info <$> isType_ typ
checkSizeLtSat $ unEl $ unDom argsT
let tel = telFromList $ bindsWithHidingToTel xs argsT
reportSLn "tc.term.lambda" 60 $ "dontUseTargetType tel = " ++ show tel
t1 <- addContext (xs, argsT) $ workOnTypes newTypeMeta_
if notVisible info || any notVisible xs then do
pid <- newProblem_ $ leqType (telePi tel t1) target
v <- addContext (xs, argsT) $ checkExpr body t1
blockTermOnProblem target (teleLam tel v) pid
else do
v <- addContext (xs, argsT) $ checkExpr body t1
coerce (teleLam tel v) (telePi tel t1) target
useTargetType tel@(ExtendTel dom (Abs y EmptyTel)) btyp = do
verboseS "tc.term.lambda" 5 $ tick "lambda-with-target-type"
reportSLn "tc.term.lambda" 60 $ "useTargetType y = " ++ y
let [WithHiding h x] = xs
info <- return $ mapHiding (mappend h) info
unless (sameHiding dom info) $ typeError $ WrongHidingInLambda target
info <- lambdaIrrelevanceCheck info dom
let a = unDom dom
checkSizeLtSat $ unEl a
(pid, argT) <- newProblem $ isTypeEqualTo typ a
v <- lambdaAddContext x y (Dom info argT) $ checkExpr body btyp
blockTermOnProblem target (Lam info $ Abs (nameToArgName x) v) pid
useTargetType _ _ = __IMPOSSIBLE__
lambdaIrrelevanceCheck :: LensRelevance dom => ArgInfo -> dom -> TCM ArgInfo
lambdaIrrelevanceCheck info dom
| isRelevant info = return $ setRelevance (getRelevance dom) info
| otherwise = do
let rPi = getRelevance dom
let rLam = getRelevance info
unless (moreRelevant rPi rLam) $ do
unless (rLam == NonStrict) __IMPOSSIBLE__
unless (rPi == Irrelevant) __IMPOSSIBLE__
typeError WrongIrrelevanceInLambda
return info
lambdaAddContext :: Name -> ArgName -> Dom Type -> TCM a -> TCM a
lambdaAddContext x y dom
| isNoName x = addContext (notInScopeName y, dom)
| otherwise = addContext (x, dom)
checkPostponedLambda :: Arg ([WithHiding Name], Maybe Type) -> A.Expr -> Type -> TCM Term
checkPostponedLambda args@(Arg _ ([] , _ )) body target = do
checkExpr body target
checkPostponedLambda args@(Arg info (WithHiding h x : xs, mt)) body target = do
let postpone _ t = postponeTypeCheckingProblem_ $ CheckLambda args body t
lamHiding = mappend h $ getHiding info
insertHiddenLambdas lamHiding target postpone $ \ t@(El _ (Pi dom b)) -> do
info' <- setHiding lamHiding <$> lambdaIrrelevanceCheck info dom
mpid <- caseMaybe mt (return Nothing) $ \ ascribedType -> Just <$> do
newProblem_ $ leqType (unDom dom) ascribedType
let dom' = setRelevance (getRelevance info') . setHiding lamHiding $
maybe dom (dom $>) mt
v <- lambdaAddContext x (absName b) dom' $
checkPostponedLambda (Arg info (xs, mt)) body $ absBody b
let v' = Lam info' $ Abs (nameToArgName x) v
maybe (return v') (blockTermOnProblem t v') mpid
insertHiddenLambdas
:: Hiding
-> Type
-> (MetaId -> Type -> TCM Term)
-> (Type -> TCM Term)
-> TCM Term
insertHiddenLambdas h target postpone ret = do
ifBlockedType target postpone $ \ _ t -> do
case unEl t of
Pi dom b -> do
let h' = getHiding dom
if sameHiding h h' then ret t else do
if visible h' then typeError $ WrongHidingInLambda target else do
let x = absName b
Lam (domInfo dom) . Abs x <$> do
addContext (x, dom) $ insertHiddenLambdas h (absBody b) postpone ret
_ -> typeError . GenericDocError =<< do
text "Expected " <+> prettyTCM target <+> text " to be a function type"
checkAbsurdLambda :: A.ExprInfo -> Hiding -> A.Expr -> Type -> TCM Term
checkAbsurdLambda i h e t = do
t <- instantiateFull t
ifBlockedType t (\ m t' -> postponeTypeCheckingProblem_ $ CheckExpr e t') $ \ _ t' -> do
case unEl t' of
Pi dom@(Dom info' a) b
| not (sameHiding h info') -> typeError $ WrongHidingInLambda t'
| not (null $ allMetas a) ->
postponeTypeCheckingProblem (CheckExpr e t') $
null . allMetas <$> instantiateFull a
| otherwise -> blockTerm t' $ do
isEmptyType (getRange i) a
top <- currentModule
aux <- qualify top <$> freshName_ (getRange i, absurdLambdaName)
rel <- asks envRelevance
reportSDoc "tc.term.absurd" 10 $ vcat
[ text "Adding absurd function" <+> prettyTCM rel <> prettyTCM aux
, nest 2 $ text "of type" <+> prettyTCM t'
]
addConstant aux $
(\ d -> (defaultDefn (setRelevance rel info') aux t' d)
{ defPolarity = [Nonvariant]
, defArgOccurrences = [Unused] })
$ emptyFunction
{ funClauses =
[ Clause
{ clauseLHSRange = getRange e
, clauseFullRange = getRange e
, clauseTel = telFromList [fmap (absurdPatternName,) dom]
, namedClausePats = [Arg info' $ Named (Just $ unranged $ absName b) $ VarP PatOAbsurd (DBPatVar absurdPatternName 0)]
, clauseBody = Nothing
, clauseType = Just $ setRelevance rel $ defaultArg $ absBody b
, clauseCatchall = False
, clauseUnreachable = Just True
}
]
, funCompiled = Just Fail
, funMutual = Just []
, funTerminates = Just True
}
tel <- getContextTelescope
return $ Def aux $ map Apply $ teleArgs tel
_ -> typeError $ ShouldBePi t'
checkExtendedLambda :: A.ExprInfo -> A.DefInfo -> QName -> [A.Clause] ->
A.Expr -> Type -> TCM Term
checkExtendedLambda i di qname cs e t = do
solveSizeConstraints DontDefaultToInfty
lamMod <- inFreshModuleIfFreeParams currentModule
t <- instantiateFull t
ifBlockedType t (\ m t' -> postponeTypeCheckingProblem_ $ CheckExpr e t') $ \ _ t -> do
j <- currentOrFreshMutualBlock
rel <- asks envRelevance
let info = setRelevance rel defaultArgInfo
reportSDoc "tc.term.exlam" 20 $
text (show $ A.defAbstract di) <+>
text "extended lambda's implementation \"" <> prettyTCM qname <>
text "\" has type: " $$ prettyTCM t
args <- getContextArgs
(abstract (A.defAbstract di) $ do
addConstant qname =<< do
useTerPragma $
(defaultDefn info qname t emptyFunction) { defMutual = j }
checkFunDef' t info NotDelayed (Just $ ExtLamInfo lamMod) Nothing di qname cs
return $ Def qname $ map Apply args)
where
abstract ConcreteDef = inConcreteMode
abstract AbstractDef = inAbstractMode
catchIlltypedPatternBlockedOnMeta :: TCM a -> ((TCErr, MetaId) -> TCM a) -> TCM a
catchIlltypedPatternBlockedOnMeta m handle = do
st <- get
m `catchError` \ err -> do
let reraise = throwError err
x <- maybe reraise return =<< case err of
TypeError s cl -> localState $ put s >> do
enterClosure cl $ \case
IlltypedPattern p a -> isBlockedType a
SplitError (UnificationStuck c tel us vs _) -> do
problem <- reduce =<< instantiateFull (flattenTel tel, us, vs)
return $ listToMaybe $ allMetas problem
SplitError (NotADatatype aClosure) ->
enterClosure aClosure $ \ a -> isBlockedType a
CannotEliminateWithPattern p a -> isBlockedType a
_ -> return Nothing
_ -> return Nothing
reportSDoc "tc.postpone" 20 $ vcat $
[ text "checking definition blocked on meta: " <+> prettyTCM x ]
put st
Map.lookup x <$> getMetaStore >>= \case
Nothing -> reraise
Just m | InstV{} <- mvInstantiation m -> reraise
Just m | Frozen <- mvFrozen m -> isInteractionMeta x >>= \case
Nothing -> reraise
Just{} -> handle (err, x)
Just{} -> handle (err, x)
expandModuleAssigns :: [Either A.Assign A.ModuleName] -> [C.Name] -> TCM A.Assigns
expandModuleAssigns mfs exs = do
let (fs , ms) = partitionEithers mfs
exs' = exs List.\\ map (view nameFieldA) fs
fs' <- forM exs' $ \ f -> do
pms <- forM ms $ \ m -> do
modScope <- getNamedScope m
let names :: ThingsInScope AbstractName
names = exportedNamesInScope modScope
return $
case Map.lookup f names of
Just [n] -> Just (m, FieldAssignment f (A.nameExpr n))
_ -> Nothing
case catMaybes pms of
[] -> return Nothing
[(_, fa)] -> return (Just fa)
mfas -> typeError . GenericDocError =<< do
vcat $
[ text "Ambiguity: the field" <+> prettyTCM f
<+> text "appears in the following modules: " ]
++ map (prettyTCM . fst) mfas
return (fs ++ catMaybes fs')
checkRecordExpression :: A.RecordAssigns -> A.Expr -> Type -> TCM Term
checkRecordExpression mfs e t = do
reportSDoc "tc.term.rec" 10 $ sep
[ text "checking record expression"
, prettyA e
]
ifBlockedType t (\ _ t -> guessRecordType t) $ \ _ t -> do
case unEl t of
Def r es -> do
let ~(Just vs) = allApplyElims es
reportSDoc "tc.term.rec" 20 $ text $ " r = " ++ prettyShow r
reportSDoc "tc.term.rec" 30 $ text " xs = " <> do
text =<< prettyShow . map unArg <$> getRecordFieldNames r
reportSDoc "tc.term.rec" 30 $ text " ftel= " <> do
prettyTCM =<< getRecordFieldTypes r
reportSDoc "tc.term.rec" 30 $ text " con = " <> do
text =<< prettyShow <$> getRecordConstructor r
def <- getRecordDef r
let
axs = recordFieldNames def
exs = filter visible axs
xs = map unArg axs
con = killRange $ recConHead def
reportSDoc "tc.term.rec" 20 $ vcat
[ text " xs = " <> return (P.pretty xs)
, text " ftel= " <> prettyTCM (recTel def)
, text " con = " <> return (P.pretty con)
]
fs <- expandModuleAssigns mfs (map unArg exs)
scope <- getScope
let re = getRange e
meta x = A.Underscore $ A.MetaInfo re scope Nothing (prettyShow x)
es <- insertMissingFields r meta fs axs
args <- checkArguments_ ExpandLast re es (recTel def `apply` vs) >>= \case
(elims, remainingTel) | null remainingTel
, Just args <- allApplyElims elims -> return args
_ -> __IMPOSSIBLE__
reportSDoc "tc.term.rec" 20 $ text $ "finished record expression"
return $ Con con ConORec (map Apply args)
_ -> typeError $ ShouldBeRecordType t
where
guessRecordType t = do
let fields = [ x | Left (FieldAssignment x _) <- mfs ]
rs <- findPossibleRecords fields
case rs of
[] -> case fields of
[] -> typeError $ GenericError "There are no records in scope"
[f] -> typeError $ GenericError $ "There is no known record with the field " ++ prettyShow f
_ -> typeError $ GenericError $ "There is no known record with the fields " ++ unwords (map prettyShow fields)
[r] -> do
def <- getConstInfo r
let rt = defType def
vs <- newArgsMeta rt
target <- reduce $ piApply rt vs
s <- case unEl target of
Sort s -> return s
v -> do
reportSDoc "impossible" 10 $ vcat
[ text "The impossible happened when checking record expression against meta"
, text "Candidate record type r = " <+> prettyTCM r
, text "Type of r = " <+> prettyTCM rt
, text "Ends in (should be sort)= " <+> prettyTCM v
, text $ " Raw = " ++ show v
]
__IMPOSSIBLE__
let inferred = El s $ Def r $ map Apply vs
v <- checkExpr e inferred
coerce v inferred t
_:_:_ -> do
reportSDoc "tc.term.expr.rec" 10 $ sep
[ text "Postponing type checking of"
, nest 2 $ prettyA e <+> text ":" <+> prettyTCM t
]
postponeTypeCheckingProblem_ $ CheckExpr e t
checkRecordUpdate :: A.ExprInfo -> A.Expr -> A.Assigns -> A.Expr -> Type -> TCM Term
checkRecordUpdate ei recexpr fs e t = do
case unEl t of
Def r vs -> do
v <- checkExpr recexpr t
name <- freshNoName (getRange recexpr)
addLetBinding defaultArgInfo name v t $ do
projs <- recFields <$> getRecordDef r
axs <- getRecordFieldNames r
scope <- getScope
let xs = map unArg axs
es <- orderFields r Nothing xs $ map (\ (FieldAssignment x e) -> (x, Just e)) fs
let es' = zipWith (replaceFields name ei) projs es
checkExpr (A.Rec ei [ Left (FieldAssignment x e) | (x, Just e) <- zip xs es' ]) t
MetaV _ _ -> do
inferred <- inferExpr recexpr >>= reduce . snd
case unEl inferred of
MetaV _ _ -> postponeTypeCheckingProblem_ $ CheckExpr e t
_ -> do
v <- checkExpr e inferred
coerce v inferred t
_ -> typeError $ ShouldBeRecordType t
where
replaceFields :: Name -> A.ExprInfo -> Arg A.QName -> Maybe A.Expr -> Maybe A.Expr
replaceFields n ei a@(Arg _ p) Nothing | visible a =
Just $ A.App (A.defaultAppInfo $ getRange ei) (A.Def p) $ defaultNamedArg $ A.Var n
replaceFields _ _ (Arg _ _) Nothing = Nothing
replaceFields _ _ _ (Just e) = Just $ e
checkLiteral :: Literal -> Type -> TCM Term
checkLiteral lit t = do
t' <- litType lit
coerce (Lit lit) t' t
scopedExpr :: A.Expr -> TCM A.Expr
scopedExpr (A.ScopedExpr scope e) = setScope scope >> scopedExpr e
scopedExpr e = return e
checkExpr :: A.Expr -> Type -> TCM Term
checkExpr e t0 =
verboseBracket "tc.term.expr.top" 5 "checkExpr" $
traceCall (CheckExprCall e t0) $ localScope $ doExpandLast $ unfoldInlined =<< do
reportSDoc "tc.term.expr.top" 15 $
text "Checking" <+> sep
[ fsep [ prettyTCM e, text ":", prettyTCM t0 ]
, nest 2 $ text "at " <+> (text . prettyShow =<< getCurrentRange)
]
reportSDoc "tc.term.expr.top.detailed" 80 $
text "Checking" <+> fsep [ prettyTCM e, text ":", text (show t0) ]
t <- reduce t0
reportSDoc "tc.term.expr.top" 15 $
text " --> " <+> prettyTCM t
e <- scopedExpr e
tryInsertHiddenLambda e t $ case e of
A.ScopedExpr scope e -> __IMPOSSIBLE__
A.QuestionMark i ii -> checkQuestionMark (newValueMeta' RunMetaOccursCheck) t0 i ii
A.Underscore i -> checkUnderscore t0 i
A.WithApp _ e es -> typeError $ NotImplemented "type checking of with application"
A.App i s arg@(Arg ai l)
| A.Set _ 0 <- unScope s, visible ai ->
ifNotM hasUniversePolymorphism
(typeError $ GenericError "Use --universe-polymorphism to enable level arguments to Set")
$ do
lvl <- levelType
n <- levelView =<< do
applyRelevanceToContext NonStrict $
checkNamedArg arg lvl
reportSDoc "tc.univ.poly" 10 $
text "checking Set " <+> prettyTCM n <+>
text "against" <+> prettyTCM t
coerce (Sort $ Type n) (sort $ Type $ levelSuc n) t
e0@(A.App i q (Arg ai e))
| A.Quote _ <- unScope q, visible ai -> do
let quoted (A.Def x) = return x
quoted (A.Macro x) = return x
quoted (A.Proj o p) | Just x <- getUnambiguous p = return x
quoted (A.Proj o p) =
typeError $ GenericError $ "quote: Ambigous name: " ++ prettyShow (unAmbQ p)
quoted (A.Con c) | Just x <- getUnambiguous c = return x
quoted (A.Con c) =
typeError $ GenericError $ "quote: Ambigous name: " ++ prettyShow (unAmbQ c)
quoted (A.ScopedExpr _ e) = quoted e
quoted _ =
typeError $ GenericError $ "quote: not a defined name"
x <- quoted (namedThing e)
ty <- qNameType
coerce (quoteName x) ty t
| A.QuoteTerm _ <- unScope q ->
do (et, _) <- inferExpr (namedThing e)
et' <- etaContract =<< instantiateFull et
let metas = allMetas et'
case metas of
_:_ -> postponeTypeCheckingProblem (CheckExpr e0 t) $ andM $ map isInstantiatedMeta metas
[] -> do
q <- quoteTerm et'
ty <- el primAgdaTerm
coerce q ty t
A.Quote _ -> typeError $ GenericError "quote must be applied to a defined name"
A.QuoteTerm _ -> typeError $ GenericError "quoteTerm must be applied to a term"
A.Unquote _ -> typeError $ GenericError "unquote must be applied to a term"
A.AbsurdLam i h -> checkAbsurdLambda i h e t
A.ExtendedLam i di qname cs -> checkExtendedLambda i di qname cs e t
A.Lam i (A.DomainFull (A.TypedBindings _ b)) e -> checkLambda b e t
A.Lam i (A.DomainFree info x) e0 -> checkExpr (A.Lam i (domainFree info $ A.unBind x) e0) t
A.Lit lit -> checkLiteral lit t
A.Let i ds e -> checkLetBindings ds $ checkExpr e t
A.Pi _ tel e | null tel -> checkExpr e t
A.Pi _ tel e -> do
(t0, t') <- checkPiTelescope tel $ \ tel -> do
t0 <- instantiateFull =<< isType_ e
tel <- instantiateFull tel
return (t0, telePi tel t0)
checkTelePiSort t'
noFunctionsIntoSize t0 t'
let s = getSort t'
v = unEl t'
when (s == Inf) $ reportSDoc "tc.term.sort" 20 $
vcat [ text ("reduced to omega:")
, nest 2 $ text "t =" <+> prettyTCM t'
, nest 2 $ text "cxt =" <+> (prettyTCM =<< getContextTelescope)
]
coerce v (sort s) t
A.Fun _ (Arg info a) b -> do
a' <- isType_ a
b' <- isType_ b
s <- inferFunSort (getSort a') (getSort b')
let v = Pi (Dom info a') (NoAbs underscore b')
noFunctionsIntoSize b' $ El s v
coerce v (sort s) t
A.Set _ n -> do
coerce (Sort $ mkType n) (sort $ mkType $ n + 1) t
A.Prop _ -> do
typeError $ GenericError "Prop is no longer supported"
A.Rec _ fs -> checkRecordExpression fs e t
A.RecUpdate ei recexpr fs -> checkRecordUpdate ei recexpr fs e t
A.DontCare e ->
ifM ((Irrelevant ==) <$> asks envRelevance)
(dontCare <$> do applyRelevanceToContext Irrelevant $ checkExpr e t)
(internalError "DontCare may only appear in irrelevant contexts")
e0@(A.QuoteGoal _ x e) -> do
qg <- quoteGoal t
case qg of
Left metas -> postponeTypeCheckingProblem (CheckExpr e0 t) $ andM $ map isInstantiatedMeta metas
Right quoted -> do
tmType <- agdaTermType
(v, ty) <- addLetBinding defaultArgInfo x quoted tmType (inferExpr e)
coerce v ty t
e0@(A.QuoteContext _) -> do
qc <- quoteContext
case qc of
Left metas -> postponeTypeCheckingProblem (CheckExpr e0 t) $ andM $ map isInstantiatedMeta metas
Right quotedContext -> do
ctxType <- el $ list $ primArg <@> (unEl <$> agdaTypeType)
coerce quotedContext ctxType t
e0@(A.Tactic i e xs ys) -> do
qc <- quoteContext
qg <- quoteGoal t
let postpone metas = postponeTypeCheckingProblem (CheckExpr e0 t) $ andM $ map isInstantiatedMeta metas
case (qc, qg) of
(Left metas1, Left metas2) -> postpone $ metas1 ++ metas2
(Left metas , Right _ ) -> postpone $ metas
(Right _ , Left metas ) -> postpone $ metas
(Right quotedCtx, Right quotedGoal) -> do
quotedCtx <- defaultNamedArg <$> reify quotedCtx
quotedGoal <- defaultNamedArg <$> reify quotedGoal
let ai = A.defaultAppInfo (getRange i)
tac = foldl (A.App ai) (A.App ai (A.App ai e quotedCtx) quotedGoal) xs
result = foldl (A.App ai) (A.Unquote i) (defaultNamedArg tac : ys)
checkExpr result t
A.ETel _ -> __IMPOSSIBLE__
A.Dot{} -> typeError $ GenericError $ "Invalid dotted expression"
_ | Application hd args <- appView e -> checkApplication hd args e t
`catchIlltypedPatternBlockedOnMeta` \ (err, x) -> do
reportSDoc "tc.term" 50 $ vcat $
[ text "checking pattern got stuck on meta: " <+> text (show x) ]
postponeTypeCheckingProblem (CheckExpr e t) $ isInstantiatedMeta x
where
tryInsertHiddenLambda :: A.Expr -> Type -> TCM Term -> TCM Term
tryInsertHiddenLambda e t fallback
| Pi (Dom info a) b <- unEl t
, let h = getHiding info
, notVisible h
, not (hiddenLambdaOrHole h e)
= do
let proceed = doInsert info $ absName b
if definitelyIntroduction then proceed else do
reduce a >>= isSizeType >>= \case
Just (BoundedLt u) -> ifBlocked u (\ _ _ -> fallback) $ \ _ v -> do
ifM (checkSizeNeverZero v) proceed fallback
`catchError` \_ -> fallback
_ -> proceed
| otherwise = fallback
where
re = getRange e
rx = caseMaybe (rStart re) noRange $ \ pos -> posToRange pos pos
doInsert info y = do
x <- unshadowName <=< freshName rx $ notInScopeName y
reportSLn "tc.term.expr.impl" 15 $ "Inserting implicit lambda"
checkExpr (A.Lam (A.ExprRange re) (domainFree info x) e) t
hiddenLambdaOrHole h e = case e of
A.AbsurdLam _ h' -> sameHiding h h'
A.ExtendedLam _ _ _ cls -> any hiddenLHS cls
A.Lam _ bind _ -> sameHiding h bind
A.QuestionMark{} -> True
_ -> False
hiddenLHS (A.Clause (A.LHS _ (A.LHSHead _ (a : _))) _ _ _ _) = notVisible a
hiddenLHS _ = False
definitelyIntroduction = case e of
A.Lam{} -> True
A.AbsurdLam{} -> True
A.Lit{} -> True
A.Pi{} -> True
A.Fun{} -> True
A.Set{} -> True
A.Prop{} -> True
A.Rec{} -> True
A.RecUpdate{} -> True
A.ScopedExpr{} -> __IMPOSSIBLE__
A.ETel{} -> __IMPOSSIBLE__
_ -> False
quoteGoal :: Type -> TCM (Either [MetaId] Term)
quoteGoal t = do
t' <- etaContract =<< instantiateFull t
let metas = allMetas t'
case metas of
_:_ -> return $ Left metas
[] -> do
quotedGoal <- quoteTerm (unEl t')
return $ Right quotedGoal
quoteContext :: TCM (Either [MetaId] Term)
quoteContext = do
contextTypes <- map (fmap snd) <$> getContext
contextTypes <- etaContract =<< instantiateFull contextTypes
let metas = allMetas contextTypes
case metas of
_:_ -> return $ Left metas
[] -> do
quotedContext <- buildList <*> mapM quoteDom contextTypes
return $ Right quotedContext
unquoteM :: A.Expr -> Term -> Type -> TCM Term -> TCM Term
unquoteM tac hole holeType k = do
tac <- checkExpr tac =<< (el primAgdaTerm --> el (primAgdaTCM <#> primLevelZero <@> primUnit))
inFreshModuleIfFreeParams $ unquoteTactic tac hole holeType k
unquoteTactic :: Term -> Term -> Type -> TCM Term -> TCM Term
unquoteTactic tac hole goal k = do
ok <- runUnquoteM $ unquoteTCM tac hole
case ok of
Left (BlockedOnMeta oldState x) -> do
put oldState
mi <- Map.lookup x <$> getMetaStore
(r, unblock) <- case mi of
Nothing -> do
otherMetas <- allMetas <$> instantiateFull goal
case otherMetas of
[] -> return (noRange, return False)
x:_ -> return (noRange, isInstantiatedMeta x)
Just mi -> return (getRange mi, isInstantiatedMeta x)
setCurrentRange r $
postponeTypeCheckingProblem (UnquoteTactic tac hole goal) unblock
Left err -> typeError $ UnquoteFailed err
Right _ -> k
checkQuestionMark :: (Type -> TCM (MetaId, Term)) -> Type -> A.MetaInfo -> InteractionId -> TCM Term
checkQuestionMark new t0 i ii = do
reportSDoc "tc.interaction" 20 $ sep
[ text "Found interaction point"
, text (show ii)
, text ":"
, prettyTCM t0
]
reportSDoc "tc.interaction" 60 $ sep
[ text "Raw:"
, text (show t0)
]
checkMeta (newQuestionMark' new ii) t0 i
checkUnderscore :: Type -> A.MetaInfo -> TCM Term
checkUnderscore = checkMeta (newValueMeta RunMetaOccursCheck)
checkMeta :: (Type -> TCM (MetaId, Term)) -> Type -> A.MetaInfo -> TCM Term
checkMeta newMeta t i = fst <$> checkOrInferMeta newMeta (Just t) i
inferMeta :: (Type -> TCM (MetaId, Term)) -> A.MetaInfo -> TCM (Elims -> Term, Type)
inferMeta newMeta i = mapFst applyE <$> checkOrInferMeta newMeta Nothing i
checkOrInferMeta :: (Type -> TCM (MetaId, Term)) -> Maybe Type -> A.MetaInfo -> TCM (Term, Type)
checkOrInferMeta newMeta mt i = do
case A.metaNumber i of
Nothing -> do
setScope (A.metaScope i)
t <- maybe (workOnTypes $ newTypeMeta_) return mt
(x, v) <- newMeta t
setMetaNameSuggestion x (A.metaNameSuggestion i)
return (v, t)
Just x -> do
let v = MetaV x []
reportSDoc "tc.meta.check" 20 $
text "checking existing meta " <+> prettyTCM v
t' <- jMetaType . mvJudgement <$> lookupMeta x
reportSDoc "tc.meta.check" 20 $
nest 2 $ text "of type " <+> prettyTCM t'
case mt of
Nothing -> return (v, t')
Just t -> (,t) <$> coerce v t' t
domainFree :: ArgInfo -> A.Name -> A.LamBinding
domainFree info x =
A.DomainFull $ A.TypedBindings r $ Arg info $ A.TBind r [pure $ A.BindName x] $ A.Underscore underscoreInfo
where
r = getRange x
underscoreInfo = A.MetaInfo
{ A.metaRange = r
, A.metaScope = emptyScopeInfo
, A.metaNumber = Nothing
, A.metaNameSuggestion = prettyShow $ A.nameConcrete x
}
checkKnownArguments
:: [NamedArg A.Expr]
-> Args
-> Type
-> TCM (Args, Type)
checkKnownArguments [] vs t = return (vs, t)
checkKnownArguments (arg : args) vs t = do
(vs', t') <- traceCall (SetRange $ getRange arg) $ checkKnownArgument arg vs t
checkKnownArguments args vs' t'
checkKnownArgument
:: NamedArg A.Expr
-> Args
-> Type
-> TCM (Args, Type)
checkKnownArgument arg [] _ = genericDocError =<< do
text "Invalid projection parameter " <+> prettyA arg
checkKnownArgument arg@(Arg info e) (Arg _infov v : vs) t = do
(Dom info' a, b) <- mustBePi t
if not (sameHiding info info'
&& (visible info || maybe True ((absName b ==) . rangedThing) (nameOf e)))
then checkKnownArgument arg vs (b `absApp` v)
else do
u <- checkNamedArg arg a
equalTerm a u v
return (vs, b `absApp` v)
checkNamedArg :: NamedArg A.Expr -> Type -> TCM Term
checkNamedArg arg@(Arg info e0) t0 = do
let e = namedThing e0
let x = maybe "" rangedThing $ nameOf e0
traceCall (CheckExprCall e t0) $ do
reportSDoc "tc.term.args.named" 15 $ do
text "Checking named arg" <+> sep
[ fsep [ prettyTCM arg, text ":", prettyTCM t0 ]
]
reportSLn "tc.term.args.named" 75 $ " arg = " ++ show (deepUnscope arg)
let checkU = checkMeta (newMetaArg (setHiding Hidden info) x) t0
let checkQ = checkQuestionMark (newInteractionMetaArg (setHiding Hidden info) x) t0
if not $ isHole e then checkExpr e t0 else localScope $ do
scopedExpr e >>= \case
A.Underscore i -> checkU i
A.QuestionMark i ii -> checkQ i ii
_ -> __IMPOSSIBLE__
where
isHole A.Underscore{} = True
isHole A.QuestionMark{} = True
isHole (A.ScopedExpr _ e) = isHole e
isHole _ = False
inferExpr :: A.Expr -> TCM (Term, Type)
inferExpr = inferExpr' DontExpandLast
inferExpr' :: ExpandHidden -> A.Expr -> TCM (Term, Type)
inferExpr' exh e = traceCall (InferExpr e) $ do
let Application hd args = appView e
reportSDoc "tc.infer" 30 $ vcat
[ text "inferExpr': appView of " <+> prettyA e
, text " hd = " <+> prettyA hd
, text " args = " <+> prettyAs args
]
reportSDoc "tc.infer" 60 $ vcat
[ text $ " hd (raw) = " ++ show hd
]
inferApplication exh hd args e
defOrVar :: A.Expr -> Bool
defOrVar A.Var{} = True
defOrVar A.Def{} = True
defOrVar A.Proj{} = True
defOrVar (A.ScopedExpr _ e) = defOrVar e
defOrVar _ = False
checkDontExpandLast :: A.Expr -> Type -> TCM Term
checkDontExpandLast e t = case e of
_ | Application hd args <- appView e, defOrVar hd ->
traceCall (CheckExprCall e t) $ localScope $ dontExpandLast $ do
checkApplication hd args e t
_ -> checkExpr e t
isModuleFreeVar :: Int -> TCM Bool
isModuleFreeVar i = do
params <- moduleParamsToApply =<< currentModule
return $ any ((== Var i []) . unArg) params
inferExprForWith :: A.Expr -> TCM (Term, Type)
inferExprForWith e = do
reportSDoc "tc.with.infer" 20 $ text "inferExprforWith " <+> prettyTCM e
reportSLn "tc.with.infer" 80 $ "inferExprforWith " ++ show (deepUnscope e)
traceCall (InferExpr e) $ do
(v, t) <- instantiateFull =<< inferExpr e
v0 <- reduce v
case v0 of
Var i [] -> whenM (isModuleFreeVar i) $ do
reportSDoc "tc.with.infer" 80 $ vcat
[ text $ "with expression is variable " ++ show i
, text "current modules = " <+> do text . show =<< currentModule
, text "current module free vars = " <+> do text . show =<< getCurrentModuleFreeVars
, text "context size = " <+> do text . show =<< getContextSize
, text "current context = " <+> do prettyTCM =<< getContextTelescope
]
typeError $ WithOnFreeVariable e v0
_ -> return ()
TelV tel t0 <- telViewUpTo' (-1) (not . visible) t
case unEl t0 of
Def d vs -> do
res <- isDataOrRecordType d
case res of
Nothing -> return (v, t)
Just{} -> do
(args, t1) <- implicitArgs (-1) notVisible t
return (v `apply` args, t1)
_ -> return (v, t)
checkLetBindings :: [A.LetBinding] -> TCM a -> TCM a
checkLetBindings = foldr (.) id . map checkLetBinding
checkLetBinding :: A.LetBinding -> TCM a -> TCM a
checkLetBinding b@(A.LetBind i info x t e) ret =
traceCall (CheckLetBinding b) $ do
t <- isType_ t
v <- applyRelevanceToContext (getRelevance info) $ checkDontExpandLast e t
addLetBinding info (A.unBind x) v t ret
checkLetBinding b@(A.LetPatBind i p e) ret =
traceCall (CheckLetBinding b) $ do
p <- expandPatternSynonyms p
(v, t) <- inferExpr' ExpandLast e
let
t0 = El (getSort t) $ Pi (Dom defaultArgInfo t) (NoAbs underscore typeDontCare)
p0 = Arg defaultArgInfo (Named Nothing p)
reportSDoc "tc.term.let.pattern" 10 $ vcat
[ text "let-binding pattern p at type t"
, nest 2 $ vcat
[ text "p (A) =" <+> prettyA p
, text "t =" <+> prettyTCM t
]
]
fvs <- getContextSize
checkLeftHandSide (CheckPattern p EmptyTel t) Nothing [p0] t0 Nothing [] $ \ (LHSResult _ delta0 ps _ _t _ asb) -> bindAsPatterns asb $ do
let p = case drop fvs ps of [p] -> namedArg p; _ -> __IMPOSSIBLE__
delta = telFromList $ drop fvs $ telToList delta0
reportSDoc "tc.term.let.pattern" 20 $ nest 2 $ vcat
[ text "p (I) =" <+> prettyTCM p
, text "delta =" <+> prettyTCM delta
]
fs <- recordPatternToProjections p
cxt0 <- getContext
let (binds, cxt) = splitAt (size delta) cxt0
toDrop = length binds
sigma = map ($ v) fs
sub = parallelS (reverse sigma)
updateContext sub (drop toDrop) $ do
reportSDoc "tc.term.let.pattern" 20 $ nest 2 $ vcat
[ text "delta =" <+> prettyTCM delta
, text "binds =" <+> prettyTCM binds
]
let fdelta = flattenTel delta
reportSDoc "tc.term.let.pattern" 20 $ nest 2 $ vcat
[ text "fdelta =" <+> addContext delta (prettyTCM fdelta)
]
let tsl = applySubst sub fdelta
let ts = map unDom tsl
let infos = map domInfo tsl
let xs = map (fst . unDom) (reverse binds)
foldr (uncurry4 addLetBinding) ret $ List.zip4 infos xs sigma ts
checkLetBinding (A.LetApply i x modapp copyInfo _adir) ret = do
fv <- getCurrentModuleFreeVars
n <- getContextSize
let new = n - fv
reportSLn "tc.term.let.apply" 10 $ "Applying " ++ show modapp ++ " with " ++ show new ++ " free variables"
reportSDoc "tc.term.let.apply" 20 $ vcat
[ text "context =" <+> (prettyTCM =<< getContextTelescope)
, text "module =" <+> (prettyTCM =<< currentModule)
, text "fv =" <+> (text $ show fv)
]
checkSectionApplication i x modapp copyInfo
withAnonymousModule x new ret
checkLetBinding A.LetOpen{} ret = ret
checkLetBinding (A.LetDeclaredVariable _) ret = ret