module Agda.TypeChecking.Rules.Term where
import Control.Applicative
import Control.Monad.Trans
import Control.Monad.Reader
import Data.Maybe
import Data.List hiding (sort)
import qualified Data.Map as Map
import Data.Traversable (sequenceA)
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 qualified Agda.Syntax.Concrete.Name as C
import Agda.Syntax.Common
import Agda.Syntax.Fixity
import Agda.Syntax.Internal as I
import Agda.Syntax.Position
import Agda.Syntax.Literal
import Agda.Syntax.Scope.Base (emptyScopeInfo)
import Agda.Syntax.Translation.InternalToAbstract (reify)
import Agda.TypeChecking.Monad
import Agda.TypeChecking.Monad.Builtin
import Agda.TypeChecking.CompiledClause
import Agda.TypeChecking.Constraints
import Agda.TypeChecking.Conversion
import Agda.TypeChecking.Datatypes
import Agda.TypeChecking.EtaContract
import Agda.TypeChecking.Free (isBinderUsed)
import Agda.TypeChecking.Implicit
import Agda.TypeChecking.InstanceArguments
import Agda.TypeChecking.Irrelevance
import Agda.TypeChecking.Level
import Agda.TypeChecking.MetaVars
import Agda.TypeChecking.Patterns.Abstract
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.Substitute
import Agda.TypeChecking.Telescope
import Agda.TypeChecking.Rules.LHS (checkLeftHandSide, LHSResult(..))
import Agda.TypeChecking.Empty (isEmptyType)
import Agda.TypeChecking.Rules.Decl (checkSectionApplication)
import Agda.TypeChecking.Rules.Def (checkFunDef, checkFunDef', useTerPragma)
import Agda.Utils.Except
( Error(noMsg, strMsg)
, ExceptT
, MonadError(catchError, throwError)
, runExceptT
)
import Agda.Utils.Functor (($>))
import Agda.Utils.Maybe
import Agda.Utils.Monad
import Agda.Utils.Permutation
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) $ sharedType <$>
case unScope e of
A.Fun i (Arg info t) b -> do
a <- Dom info <$> isType_ t
b <- isType_ b
return $ El (sLub (getSort $ unDom a) (getSort b)) (Pi (convColor a) (NoAbs underscore b))
A.Pi _ tel e -> do
checkTelescope_ tel $ \tel -> do
t <- instantiateFull =<< isType_ e
tel <- instantiateFull tel
return $ telePi tel t
A.Set _ n -> do
n <- ifM typeInType (return 0) (return n)
return $ sort (mkType n)
A.App i s (Arg (ArgInfo NotHidden r cs) l)
| 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 $
checkExpr (namedThing l) lvl
return $ sort (Type n)
_ -> do
s <- workOnTypes $ newSortMeta
isType e s
isTypeEqualTo :: A.Expr -> Type -> TCM Type
isTypeEqualTo e t = case e of
A.ScopedExpr _ e -> isTypeEqualTo e t
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_ [] ret = ret EmptyTel
checkTelescope_ (b : tel) ret =
checkTypedBindings_ b $ \tel1 ->
checkTelescope_ tel $ \tel2 ->
ret $ abstract tel1 tel2
checkTypedBindings_ :: A.TypedBindings -> (Telescope -> TCM a) -> TCM a
checkTypedBindings_ = checkTypedBindings PiNotLam
data LamOrPi = LamNotPi | PiNotLam deriving (Eq,Show)
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 -> A.ArgInfo -> A.TypedBinding -> (ListTel -> TCM a) -> TCM a
checkTypedBinding lamOrPi info (A.TBind i xs e) ret = do
allowed <- optExperimentalIrrelevance <$> pragmaOptions
t <- modEnv lamOrPi allowed $ isType_ e
let info' = mapRelevance (modRel lamOrPi allowed) info
addCtxs xs (convColor $ Dom info' t) $ ret $ bindsToTel xs (convColor $ Dom info t)
where
modEnv LamNotPi True = doWorkOnTypes
modEnv _ _ = id
modRel PiNotLam True = irrToNonStrict
modRel _ _ = id
checkTypedBinding lamOrPi info (A.TLet _ lbs) ret = do
checkLetBindings lbs (ret [])
checkLambda :: I.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
let numbinds = length xs
TelV tel btyp <- telViewUpTo numbinds target
if size tel < size xs || numbinds /= 1
then dontUseTargetType
else useTargetType tel btyp
where
dontUseTargetType = do
verboseS "tc.term.lambda" 5 $ tick "lambda-no-target-type"
argsT <- workOnTypes $ Dom info <$> isType_ typ
t1 <- addCtxs xs argsT $ workOnTypes newTypeMeta_
let tel = telFromList $ bindsToTel xs argsT
if (getHiding info /= NotHidden) then do
pid <- newProblem_ $ leqType (telePi tel t1) target
v <- addCtxs xs argsT $ checkExpr body t1
blockTermOnProblem target (teleLam tel v) pid
else do
v <- addCtxs xs argsT $ checkExpr body t1
coerce (teleLam tel v) (telePi tel t1) target
useTargetType tel@(ExtendTel arg (Abs y EmptyTel)) btyp = do
verboseS "tc.term.lambda" 5 $ tick "lambda-with-target-type"
unless (getHiding arg == getHiding info) $ typeError $ WrongHidingInLambda target
let r = getRelevance info
r' = getRelevance arg
when (r == Irrelevant && r' /= r) $ typeError $ WrongIrrelevanceInLambda target
(pid, argT) <- newProblem $ isTypeEqualTo typ (unDom arg)
v <- add y (Dom (setRelevance r' info) argT) $ checkExpr body btyp
blockTermOnProblem target (Lam info $ Abs (nameToArgName x) v) pid
where
[x] = xs
add y dom | isNoName x = addContext (y, dom)
| otherwise = addContext (x, dom)
useTargetType _ _ = __IMPOSSIBLE__
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 ignoreSharing $ unEl t' of
Pi dom@(Dom info' a) b
| h /= getHiding 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
$ Defn (setRelevance rel info') aux t'
[Nonvariant] [Unused] (defaultDisplayForm aux)
0 noCompiledRep [] Nothing
$ Function
{ funClauses =
[Clause
{ clauseRange = getRange e
, clauseTel = EmptyTel
, clausePerm = Perm 1 []
, namedClausePats = [Arg info' $ Named (Just $ unranged $ absName b) $ VarP "()"]
, clauseBody = Bind $ NoAbs "()" NoBody
, clauseType = Just $ setRelevance rel $ defaultArg $ absBody b
}
]
, funCompiled = Just Fail
, funDelayed = NotDelayed
, funInv = NotInjective
, funAbstr = ConcreteDef
, funMutual = []
, funProjection = Nothing
, funStatic = False
, funCopy = False
, funTerminates = Just True
, funExtLam = Nothing
, funWith = Nothing
, funCopatternLHS = False
}
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
t <- instantiateFull t
ifBlockedType t (\ m t' -> postponeTypeCheckingProblem_ $ CheckExpr e t') $ \ t -> do
j <- currentOrFreshMutualBlock
rel <- asks envRelevance
let info = setRelevance rel defaultArgInfo
addConstant qname =<< do
useTerPragma $
(defaultDefn info qname t emptyFunction) { defMutual = j }
reportSDoc "tc.term.exlam" 50 $
text "extended lambda's implementation \"" <> prettyTCM qname <>
text "\" has type: " $$ prettyTCM t
args <- getContextArgs
top <- currentModule
freevars <- getModuleFreeVars top
let argsNoParam = genericDrop freevars args
let (hid, notHid) = partition isHidden argsNoParam
abstract (A.defAbstract di) $ checkFunDef' t info NotDelayed
(Just (length hid, length notHid)) Nothing di qname cs
return $ Def qname $ map Apply args
where
abstract ConcreteDef = inConcreteMode
abstract AbstractDef = inAbstractMode
checkRecordExpression :: A.Assigns -> A.Expr -> Type -> TCM Term
checkRecordExpression fs e t = do
reportSDoc "tc.term.rec" 10 $ sep
[ text "checking record expression"
, prettyA e
]
t <- reduce t
case ignoreSharing $ unEl t of
Def r es -> do
let ~(Just vs) = allApplyElims es
reportSDoc "tc.term.rec" 20 $ text $ " r = " ++ show r
reportSDoc "tc.term.rec" 30 $ text " xs = " <> do
text =<< show . map unArg <$> getRecordFieldNames r
reportSDoc "tc.term.rec" 30 $ text " ftel= " <> do
prettyTCM =<< getRecordFieldTypes r
reportSDoc "tc.term.rec" 30 $ text " con = " <> do
text =<< show <$> getRecordConstructor r
def <- getRecordDef r
let axs = recordFieldNames def
xs = map unArg axs
ftel = recTel def
con = killRange $ recConHead def
reportSDoc "tc.term.rec" 20 $ vcat
[ text $ " xs = " ++ show xs
, text " ftel= " <> prettyTCM ftel
, text $ " con = " ++ show con
]
scope <- getScope
let arg x e =
case [ a | a <- axs, unArg a == x ] of
[a] -> unnamed e <$ a
_ -> defaultNamedArg e
let meta x = A.Underscore $ A.MetaInfo (getRange e) scope Nothing (show x)
missingExplicits = [ (unArg a, [unnamed . meta <$> a])
| a <- axs, notHidden a
, notElem (unArg a) (map fst fs) ]
es <- concat <$> orderFields r [] xs ([ (x, [arg x e]) | (x, e) <- fs ] ++
missingExplicits)
let tel = ftel `apply` vs
args <- checkArguments_ ExpandLast (getRange e)
es
tel
reportSDoc "tc.term.rec" 20 $ text $ "finished record expression"
return $ Con con args
MetaV _ _ -> do
let fields = map fst fs
rs <- findPossibleRecords fields
case rs of
[] -> case fs of
[] -> typeError $ GenericError "There are no records in scope"
[(f, _)] -> typeError $ GenericError $ "There is no known record with the field " ++ show f
_ -> typeError $ GenericError $ "There is no known record with the fields " ++ unwords (map show fields)
[r] -> do
def <- getConstInfo r
let rt = defType def
vs <- newArgsMeta rt
target <- reduce $ piApply rt vs
s <- case ignoreSharing $ unEl target of
Level l -> return $ Type l
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
_ -> typeError $ ShouldBeRecordType t
checkRecordUpdate :: A.ExprInfo -> A.Expr -> A.Assigns -> A.Expr -> Type -> TCM Term
checkRecordUpdate ei recexpr fs e t = do
case ignoreSharing $ 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 (\(x, e) -> (x, Just e)) fs
let es' = zipWith (replaceFields name ei) projs es
checkExpr (A.Rec ei [ (x, e) | (x, Just e) <- zip xs es' ]) t
MetaV _ _ -> do
inferred <- inferExpr recexpr >>= reduce . snd
case ignoreSharing $ 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 -> I.Arg A.QName -> Maybe A.Expr -> Maybe A.Expr
replaceFields n ei a@(Arg _ p) Nothing | notHidden a =
Just $ A.App 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
checkArguments' ::
ExpandHidden -> ExpandInstances -> Range -> [I.NamedArg A.Expr] -> Type -> Type ->
(Args -> Type -> TCM Term) -> TCM Term
checkArguments' exph expIFS r args t0 t k = do
z <- runExceptT $ checkArguments exph expIFS r args t0 t
case z of
Right (vs, t1) -> k vs t1
Left (us, es, t0) -> do
reportSDoc "tc.term.expr.args" 80 $
sep [ text "postponed checking arguments"
, nest 4 $ prettyList (map (prettyA . namedThing . unArg) args)
, nest 2 $ text "against"
, nest 4 $ prettyTCM t0 ] $$
sep [ text "progress:"
, nest 2 $ text "checked" <+> prettyList (map prettyTCM us)
, nest 2 $ text "remaining" <+> sep [ prettyList (map (prettyA . namedThing . unArg) es)
, nest 2 $ text ":" <+> prettyTCM t0 ] ]
postponeTypeCheckingProblem_ (CheckArgs exph expIFS r es t0 t $ \vs t -> k (us ++ vs) t)
checkExpr :: A.Expr -> Type -> TCM Term
checkExpr e t0 =
verboseBracket "tc.term.expr.top" 5 "checkExpr" $
traceCall (CheckExprCall e t0) $ localScope $ doExpandLast $ shared <$> do
reportSDoc "tc.term.expr.top" 15 $
text "Checking" <+> sep
[ fsep [ prettyTCM e, text ":", prettyTCM t0 ]
, nest 2 $ text "at " <+> (text . show =<< 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
let scopedExpr (A.ScopedExpr scope e) = setScope scope >> scopedExpr e
scopedExpr e = return e
e <- scopedExpr e
case e of
A.ScopedExpr scope e -> __IMPOSSIBLE__
_ | Pi (Dom info _) _ <- ignoreSharing $ unEl t
, let h = getHiding info
, notVisible h
, not (hiddenLambdaOrHole h e)
-> do
x <- freshName rx (argName t)
info <- reify info
reportSLn "tc.term.expr.impl" 15 $ "Inserting implicit lambda"
checkExpr (A.Lam (A.ExprRange re) (domainFree info x) e) t
where
re = getRange e
rx = caseMaybe (rStart re) noRange $ \ pos -> posToRange pos pos
hiddenLambdaOrHole h e = case e of
A.AbsurdLam _ h' -> h == h'
A.ExtendedLam _ _ _ cls -> any hiddenLHS cls
A.Lam _ (A.DomainFree info' _) _ -> h == getHiding info'
A.Lam _ (A.DomainFull (A.TypedBindings _ (Arg info' _))) _
-> h == getHiding info'
A.QuestionMark{} -> True
_ -> False
hiddenLHS (A.Clause (A.LHS _ (A.LHSHead _ (a : _)) _) _ _) = notVisible a
hiddenLHS _ = False
A.QuestionMark i ii -> do
reportSDoc "tc.interaction" 20 $ sep
[ text "Found interaction point"
, text (show ii)
, text ":"
, prettyTCM t0
]
reportSDoc "tc.interaction" 40 $ sep
[ text "Raw:"
, text (show t0)
]
checkMeta (newQuestionMark ii) t0 i
A.Underscore i -> checkMeta (newValueMeta RunMetaOccursCheck) t0 i
A.WithApp _ e es -> typeError $ NotImplemented "type checking of with application"
A.App i s (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 $
checkExpr (namedThing l) lvl
reportSDoc "tc.univ.poly" 10 $
text "checking Set " <+> prettyTCM n <+>
text "against" <+> prettyTCM t
coerce (Sort $ Type n) (sort $ sSuc $ Type n) t
A.App i q (Arg ai e)
| A.Quote _ <- unScope q, visible ai -> do
let quoted (A.Def x) = return x
quoted (A.Proj x) = return x
quoted (A.Con (AmbQ [x])) = return x
quoted (A.Con (AmbQ xs)) = typeError $ GenericError $ "quote: Ambigous name: " ++ show xs
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)
q <- quoteTerm =<< etaContract =<< normalise 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 (convColor b) e t
A.Lam i (A.DomainFree info x) e0 -> checkExpr (A.Lam i (domainFree info x) e0) t
A.Lit lit -> checkLiteral lit t
A.Let i ds e -> checkLetBindings ds $ checkExpr e t
A.Pi _ tel e -> do
t' <- checkTelescope_ tel $ \tel -> do
t <- instantiateFull =<< isType_ e
tel <- instantiateFull tel
return $ telePi tel t
let s = getSort 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 (unEl t') (sort s) t
A.Fun _ (Arg info a) b -> do
a' <- isType_ a
b' <- isType_ b
s <- reduce $ getSort a' `sLub` getSort b'
coerce (Pi (convColor $ Dom info a') (NoAbs underscore b')) (sort s) t
A.Set _ n -> do
n <- ifM typeInType (return 0) (return n)
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
t' <- etaContract =<< normalise t
let metas = allMetas t'
case metas of
_:_ -> postponeTypeCheckingProblem (CheckExpr e0 t') $ andM $ map isInstantiatedMeta metas
[] -> do
quoted <- quoteTerm (unEl t')
tmType <- agdaTermType
(v, ty) <- addLetBinding defaultArgInfo x quoted tmType (inferExpr e)
blockTerm t' $ coerce v ty t'
e0@(A.QuoteContext _ x e) -> do
ctx <- getContext
thisModule <- currentModule
let contextNames = map (\(Dom _ (nm,_)) -> quoteName $ qualify thisModule nm) ctx
let names = contextNames
nameList <- buildList <*> return names
ctxType <- el (list primQName)
(v, ctxType) <- addLetBinding defaultArgInfo x nameList ctxType (inferExpr e)
blockTerm t $ coerce v ctxType t
A.ETel _ -> __IMPOSSIBLE__
_ | Application hd args <- appView e -> checkApplication hd args e t
checkApplication :: A.Expr -> A.Args -> A.Expr -> Type -> TCM Term
checkApplication hd args e t = do
case hd of
A.Con (AmbQ cs@(_:_:_)) -> do
reportSLn "tc.check.term" 40 $ "Ambiguous constructor: " ++ show cs
let getData Constructor{conData = d} = d
getData _ = __IMPOSSIBLE__
reportSLn "tc.check.term" 40 $ " ranges before: " ++ show (getRange cs)
cons <- mapM getConForm cs
reportSLn "tc.check.term" 40 $ " reduced: " ++ show cons
dcs <- zipWithM (\ c con -> (, setConName c con) . getData . theDef <$> getConInfo con) cs cons
let badCon t = typeError $ DoesNotConstructAnElementOf (head cs) t
let getCon :: TCM (Maybe ConHead)
getCon = do
TelV tel t1 <- telView t
addCtxTel tel $ do
reportSDoc "tc.check.term.con" 40 $ nest 2 $
text "target type: " <+> prettyTCM t1
ifBlockedType t1 (\ m t -> return Nothing) $ \ t' ->
caseMaybeM (isDataOrRecord $ unEl t') (badCon t') $ \ d ->
case [ c | (d', c) <- dcs, d == d' ] of
[c] -> do
reportSLn "tc.check.term" 40 $ " decided on: " ++ show c
storeDisambiguatedName $ conName c
return $ Just c
[] -> badCon $ t' $> Def d []
cs -> typeError $ CantResolveOverloadedConstructorsTargetingSameDatatype d $ map conName cs
let unblock = isJust <$> getCon
mc <- getCon
case mc of
Just c -> checkConstructorApplication e t c $ map convColor args
Nothing -> postponeTypeCheckingProblem (CheckExpr e t) unblock
A.Con (AmbQ [c]) -> do
con <- getOrigConHead c
checkConstructorApplication e t con $ map convColor args
A.PatternSyn n -> do
(ns, p) <- lookupPatternSyn n
p <- setRange (getRange n) . killRange <$> expandPatternSynonyms p
let meta r = A.Underscore $ A.emptyMetaInfo{ A.metaRange = r }
case A.insertImplicitPatSynArgs meta (getRange n) ns args of
Nothing -> typeError $ BadArgumentsToPatternSynonym n
Just (s, ns) -> do
let p' = A.patternToExpr p
e' = A.lambdaLiftExpr (map unArg ns) (A.substExpr s p')
checkExpr e' t
A.Unquote _
| [arg] <- args -> do
e <- unquoteTerm (namedArg arg)
checkExpr e t
| arg : args <- args -> do
e <- unquoteTerm (namedArg arg)
checkHeadApplication e t e $ map convColor args
where
unquoteTerm qv = do
qv <- checkExpr qv =<< el primAgdaTerm
mv <- runUnquoteM $ unquote qv
case mv of
Left err -> typeError $ UnquoteFailed err
Right v -> do
e <- reifyUnquoted (v :: Term)
reportSDoc "tc.unquote.term" 10 $
vcat [ text "unquote" <+> prettyTCM qv
, nest 2 $ text "-->" <+> prettyA e ]
return (killRange e)
_ -> checkHeadApplication e t hd $ map convColor args
domainFree :: A.ArgInfo -> A.Name -> A.LamBinding
domainFree info x =
A.DomainFull $ A.TypedBindings r $ Arg info $ A.TBind r [x] $ A.Underscore underscoreInfo
where
r = getRange x
underscoreInfo = A.MetaInfo
{ A.metaRange = r
, A.metaScope = emptyScopeInfo
, A.metaNumber = Nothing
, A.metaNameSuggestion = show $ A.nameConcrete x
}
checkMeta :: (Type -> TCM Term) -> Type -> A.MetaInfo -> TCM Term
checkMeta newMeta t i = fst <$> checkOrInferMeta newMeta (Just t) i
inferMeta :: (Type -> TCM Term) -> A.MetaInfo -> TCM (Args -> Term, Type)
inferMeta newMeta i = mapFst apply <$> checkOrInferMeta newMeta Nothing i
checkOrInferMeta :: (Type -> TCM 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
v <- newMeta t
setValueMetaName v (A.metaNameSuggestion i)
return (v, t)
Just n -> do
let v = MetaV (MetaId n) []
t' <- jMetaType . mvJudgement <$> lookupMeta (MetaId n)
case mt of
Nothing -> return (v, t')
Just t -> (,t) <$> coerce v t' t
inferHeadDef :: QName -> TCM (Args -> Term, Type)
inferHeadDef x = do
proj <- isProjection x
let app =
case proj of
Nothing -> \ f args -> return $ Def f $ map Apply args
Just p -> \ f args -> return $ projDropPars p `apply` args
mapFst apply <$> inferDef app x
inferHead :: A.Expr -> TCM (Args -> Term, Type)
inferHead e = do
case e of
(A.Var x) -> do
(u, a) <- getVarInfo x
when (unusableRelevance $ getRelevance a) $
typeError $ VariableIsIrrelevant x
return (apply u, unDom a)
(A.Def x) -> inferHeadDef x
(A.Proj x) -> inferHeadDef x
(A.Con (AmbQ [c])) -> do
(u, a) <- inferDef (\ c _ -> getOrigConTerm c) c
Constructor{conPars = n} <- theDef <$> (instantiateDef =<< getConstInfo c)
reportSLn "tc.term.con" 7 $ unwords [show c, "has", show n, "parameters."]
return (apply u . genericDrop n, a)
(A.Con _) -> __IMPOSSIBLE__
(A.QuestionMark i ii) -> inferMeta (newQuestionMark ii) i
(A.Underscore i) -> inferMeta (newValueMeta RunMetaOccursCheck) i
e -> do
(term, t) <- inferExpr e
return (apply term, t)
inferDef :: (QName -> Args -> TCM Term) -> QName -> TCM (Term, Type)
inferDef mkTerm x =
traceCall (InferDef (getRange x) x) $ do
d <- instantiateDef =<< getConstInfo x
let drel = defRelevance d
when (drel /= Relevant) $ do
rel <- asks envRelevance
reportSDoc "tc.irr" 50 $ vcat
[ text "declaration relevance =" <+> text (show drel)
, text "context relevance =" <+> text (show rel)
]
unless (drel `moreRelevant` rel) $ typeError $ DefinitionIsIrrelevant x
vs <- freeVarsToApply x
reportSDoc "tc.term.def" 10 $ do
text "inferred def " <+> prettyTCM x <+> hsep (map prettyTCM vs)
let t = defType d
reportSDoc "tc.term.def" 10 $ nest 2 $ text " : " <+> prettyTCM t
v <- mkTerm x vs
reportSDoc "tc.term.def" 10 $ nest 2 $ text " --> " <+> prettyTCM v
return (v, t)
checkConstructorApplication :: A.Expr -> Type -> ConHead -> [I.NamedArg A.Expr] -> TCM Term
checkConstructorApplication org t c args = do
reportSDoc "tc.term.con" 50 $ vcat
[ text "entering checkConstructorApplication"
, nest 2 $ vcat
[ text "org =" <+> prettyTCM org
, text "t =" <+> prettyTCM t
, text "c =" <+> prettyTCM c
, text "args =" <+> prettyTCM args
] ]
let paramsGiven = checkForParams args
if paramsGiven then fallback else do
reportSDoc "tc.term.con" 50 $ text "checkConstructorApplication: no parameters explicitly supplied, continuing..."
cdef <- getConInfo c
let Constructor{conData = d} = theDef cdef
reportSDoc "tc.term.con" 50 $ nest 2 $ text "d =" <+> prettyTCM d
t0 <- reduce (Def d [])
case (ignoreSharing t0, ignoreSharing $ unEl t) of
(Def d0 _, Def d' es) -> do
let ~(Just vs) = allApplyElims es
reportSDoc "tc.term.con" 50 $ nest 2 $ text "d0 =" <+> prettyTCM d0
reportSDoc "tc.term.con" 50 $ nest 2 $ text "d' =" <+> prettyTCM d'
reportSDoc "tc.term.con" 50 $ nest 2 $ text "vs =" <+> prettyTCM vs
if d' /= d0 then fallback else do
npars <- getNumberOfParameters d
npars' <- getNumberOfParameters d'
caseMaybe (sequenceA $ List2 (npars, npars')) fallback $ \ (List2 (n,n')) -> do
reportSDoc "tc.term.con" 50 $ nest 2 $ text $ "n = " ++ show n
reportSDoc "tc.term.con" 50 $ nest 2 $ text $ "n' = " ++ show n'
when (n > n')
__IMPOSSIBLE__
let ps = genericTake n $ genericDrop (n' n) vs
ctype = defType cdef
reportSDoc "tc.term.con" 20 $ vcat
[ text "special checking of constructor application of" <+> prettyTCM c
, nest 2 $ vcat [ text "ps =" <+> prettyTCM ps
, text "ctype =" <+> prettyTCM ctype ] ]
let ctype' = ctype `piApply` ps
reportSDoc "tc.term.con" 20 $ nest 2 $ text "ctype' =" <+> prettyTCM ctype'
TelV ptel _ <- telViewUpTo n ctype
let pnames = map (fst . unDom) $ telToList ptel
args' = dropArgs pnames args
expandLast <- asks envExpandLast
checkArguments' expandLast ExpandInstanceArguments (getRange c) args' ctype' t $ \us t' -> do
reportSDoc "tc.term.con" 20 $ nest 2 $ vcat
[ text "us =" <+> prettyTCM us
, text "t' =" <+> prettyTCM t' ]
coerce (Con c us) t' t
_ -> do
reportSDoc "tc.term.con" 50 $ nest 2 $ text "we are not at a datatype, falling back"
fallback
where
fallback = checkHeadApplication org t (A.Con (AmbQ [conName c])) args
checkForParams args =
let (hargs, rest) = span isHidden args
notUnderscore A.Underscore{} = False
notUnderscore _ = True
in any notUnderscore $ map (unScope . namedArg) hargs
dropArgs [] args = args
dropArgs ps [] = args
dropArgs ps args@(arg : _) | not (isHidden arg) = args
dropArgs (p:ps) args@(arg : args')
| elem name [Nothing, Just p] = dropArgs ps args'
| otherwise = dropArgs ps args
where
name = fmap rangedThing . nameOf $ unArg arg
checkHeadApplication :: A.Expr -> Type -> A.Expr -> [I.NamedArg A.Expr] -> TCM Term
checkHeadApplication e t hd args = do
kit <- coinductionKit
case hd of
A.Con (AmbQ [c]) | Just c == (nameOfSharp <$> kit) -> do
defaultResult
A.Con (AmbQ [c]) -> do
(f, t0) <- inferHead hd
reportSDoc "tc.term.con" 5 $ vcat
[ text "checkHeadApplication inferred" <+>
prettyTCM c <+> text ":" <+> prettyTCM t0
]
expandLast <- asks envExpandLast
checkArguments' expandLast ExpandInstanceArguments (getRange hd) args t0 t $ \vs t1 -> do
TelV eTel eType <- telView t
TelV fTel fType <- telViewUpTo (size eTel) t1
when (size eTel > size fTel) $
typeError $ UnequalTypes CmpLeq t1 t
reportSDoc "tc.term.con" 10 $ addCtxTel eTel $ vcat
[ text "checking" <+>
prettyTCM fType <+> text "?<=" <+> prettyTCM eType
]
blockTerm t $ f vs <$ workOnTypes (do
addCtxTel eTel $ leqType fType eType
compareTel t t1 CmpLeq eTel fTel)
(A.Def c) | Just c == (nameOfSharp <$> kit) -> do
lets <- envLetBindings <$> ask
unless (Map.null lets) $
typeError $ NotImplemented
"coinductive constructor in the scope of a let-bound variable"
i <- fresh :: TCM Int
let name = filter (/= '_') (show $ A.nameConcrete $ A.qnameName c) ++ "-" ++ show i
c' <- setRange (getRange c) <$>
liftM2 qualify (killRange <$> currentModule)
(freshName_ name)
e' <- Def c' . map Apply <$> getContextArgs
i <- currentOrFreshMutualBlock
tel <- getContextTelescope
rel <- asks envRelevance
addConstant c' =<< do
let ai = setRelevance rel defaultArgInfo
useTerPragma $
Defn ai c' t [] [] (defaultDisplayForm c') i noCompiledRep [] Nothing $
emptyFunction
ctx <- getContext >>= mapM (\d -> flip Dom (unDom d) <$> reify (domInfo d))
args' <- mapM (\a -> flip Arg (unArg a) <$> reify (argInfo a)) args
let info = A.mkDefInfo (A.nameConcrete $ A.qnameName c') defaultFixity'
PublicAccess ConcreteDef noRange
pats = map (\ (Dom info (n, _)) -> Arg info $ Named Nothing $ A.VarP n) $
reverse ctx
clause = A.Clause (A.LHS (A.LHSRange noRange) (A.LHSHead c' pats) [])
(A.RHS $ unAppView (A.Application (A.Con (AmbQ [c])) args'))
[]
reportSDoc "tc.term.expr.coind" 15 $ vcat $
[ text "The coinductive constructor application"
, nest 2 $ prettyTCM e
, text "was translated into the application"
, nest 2 $ prettyTCM e'
, text "and the function"
, nest 2 $ prettyTCM rel <> prettyTCM c' <+> text ":"
, nest 4 $ prettyTCM (telePi tel t)
, nest 2 $ prettyA clause <> text "."
]
inTopContext $ checkFunDef Delayed info c' [clause]
reportSDoc "tc.term.expr.coind" 15 $ do
def <- theDef <$> getConstInfo c'
text "The definition is" <+> text (show $ funDelayed def) <>
text "."
return e'
A.Con _ -> __IMPOSSIBLE__
_ -> defaultResult
where
defaultResult = do
(f, t0) <- inferHead hd
expandLast <- asks envExpandLast
checkArguments' expandLast ExpandInstanceArguments (getRange hd) args t0 t $ \vs t1 -> do
coerce (f vs) t1 t
instance Error (a, b, c) where
strMsg _ = __IMPOSSIBLE__
noMsg = __IMPOSSIBLE__
traceCallE :: Error e => (Maybe r -> Call) -> ExceptT e TCM r -> ExceptT e TCM r
traceCallE call m = do
z <- lift $ traceCall call' $ runExceptT m
case z of
Right e -> return e
Left err -> throwError err
where
call' Nothing = call Nothing
call' (Just (Left _)) = call Nothing
call' (Just (Right x)) = call (Just x)
checkArguments :: ExpandHidden -> ExpandInstances -> Range -> [I.NamedArg A.Expr] -> Type -> Type ->
ExceptT (Args, [I.NamedArg A.Expr], Type) TCM (Args, Type)
checkArguments DontExpandLast DontExpandInstanceArguments _ [] t0 t1 = return ([], t0)
checkArguments exh expandIFS r [] t0 t1 =
traceCallE (CheckArguments r [] t0 t1) $ lift $ do
t1' <- unEl <$> reduce t1
implicitArgs (1) (expand t1') t0
where
expand (Pi (Dom info _) _) Hidden = getHiding info /= Hidden &&
exh == ExpandLast
expand _ Hidden = exh == ExpandLast
expand (Pi (Dom info _) _) Instance = getHiding info /= Instance &&
expandIFS == ExpandInstanceArguments
expand _ Instance = expandIFS == ExpandInstanceArguments
expand _ NotHidden = False
checkArguments exh expandIFS r args0@(arg@(Arg info e) : args) t0 t1 =
traceCallE (CheckArguments r args0 t0 t1) $ do
lift $ reportSDoc "tc.term.args" 30 $ sep
[ text "checkArguments"
, nest 2 $ vcat
[ text "e =" <+> prettyA e
, text "t0 =" <+> prettyTCM t0
, text "t1 =" <+> prettyTCM t1
]
]
let hx = getHiding info
mx = fmap rangedThing $ nameOf e
expand NotHidden y = False
expand hy y = hy /= hx || maybe False (y /=) mx
(nargs, t) <- lift $ implicitNamedArgs (1) expand t0
let (mxs, us) = unzip $ map (\ (Arg ai (Named mx u)) -> (mx, Arg ai u)) nargs
xs = catMaybes mxs
ifBlockedType t (\ m t -> throwError ([], args0, t)) $ \ t0' -> do
let shouldBePi
| notHidden info = lift $ typeError $ ShouldBePi t0'
| null xs = lift $ typeError $ ShouldBePi t0'
| otherwise = lift $ typeError $ WrongNamedArgument arg
let wrongPi info'
| null xs = lift $ typeError $ WrongHidingInApplication t0'
| otherwise = lift $ typeError $ WrongNamedArgument arg
case ignoreSharing $ unEl t0' of
Pi (Dom info' a) b
| getHiding info == getHiding info'
&& (notHidden info || maybe True ((absName b ==) . rangedThing) (nameOf e)) -> do
u <- lift $ applyRelevanceToContext (getRelevance info') $
checkExpr (namedThing e) a
addCheckedArgs us (Arg info' u) $
checkArguments exh expandIFS (fuseRange r e) args (absApp b u) t1
| otherwise -> wrongPi info'
_ -> shouldBePi
where
addCheckedArgs us u rec =
(mapFst ((us ++) . (u :)) <$> rec)
`catchError` \(vs, es, t) ->
throwError (us ++ u : vs, es, t)
checkArguments_ :: ExpandHidden -> Range -> [I.NamedArg A.Expr] -> Telescope -> TCM Args
checkArguments_ exh r args tel = do
z <- runExceptT $ checkArguments exh ExpandInstanceArguments r args (telePi tel $ sort Prop) (sort Prop)
case z of
Right (args, _) -> return args
Left _ -> __IMPOSSIBLE__
inferExpr :: A.Expr -> TCM (Term, Type)
inferExpr e = case e of
_ | Application hd args <- appView e, defOrVar hd -> traceCall (InferExpr e) $ do
(f, t0) <- inferHead hd
res <- runExceptT $ checkArguments DontExpandLast ExpandInstanceArguments (getRange hd) (map convColor args) t0 (sort Prop)
case res of
Right (vs, t1) -> return (f vs, t1)
Left t1 -> fallback
_ -> fallback
where
fallback = do
t <- workOnTypes $ newTypeMeta_
v <- checkExpr e t
return (v,t)
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 $ shared <$> do
checkApplication hd args e t
_ -> checkExpr e t
isModuleFreeVar :: Int -> TCM Bool
isModuleFreeVar i = do
nfv <- getModuleFreeVars =<< currentModule
n <- getContextSize
let firstModuleVar = n nfv
when (firstModuleVar < 0) __IMPOSSIBLE__
return $ i >= firstModuleVar
inferExprForWith :: A.Expr -> TCM (Term, Type)
inferExprForWith e = traceCall (InferExpr e) $ do
(v, t) <- instantiateFull =<< inferExpr e
v0 <- reduce v
case ignoreSharing v0 of
Var i [] -> whenM (isModuleFreeVar i) $ typeError $ WithOnFreeVariable e
_ -> return ()
TelV tel t0 <- telViewUpTo' (1) ((NotHidden /=) . getHiding) t
case ignoreSharing $ unEl t0 of
Def d vs -> do
res <- isDataOrRecordType d
case res of
Nothing -> return (v, t)
Just{} -> do
(args, t1) <- implicitArgs (1) (NotHidden /=) 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 =
traceCallCPS_ (CheckLetBinding b) ret $ \ret -> do
t <- isType_ t
v <- applyRelevanceToContext (getRelevance info) $ checkDontExpandLast e t
addLetBinding (convColor info) x v t ret
checkLetBinding b@(A.LetPatBind i p e) ret =
traceCallCPS_ (CheckLetBinding b) ret $ \ret -> do
p <- expandPatternSynonyms p
(v, t) <- inferExpr 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) =" <+> text (show p)
, text "t =" <+> prettyTCM t
]
]
checkLeftHandSide (CheckPattern p EmptyTel t) Nothing [p0] t0 $ \ (LHSResult mgamma delta sub xs ps t' perm) -> do
let p = case ps of [p] -> namedArg p; _ -> __IMPOSSIBLE__
reportSDoc "tc.term.let.pattern" 20 $ nest 2 $ vcat
[ text "p (I) =" <+> text (show p)
, text "delta =" <+> text (show delta)
]
fs <- recordPatternToProjections p
cxt0 <- getContext
let (binds, cxt) = splitAt (size delta) cxt0
escapeContext (length binds) $ do
reportSDoc "tc.term.let.pattern" 20 $ nest 2 $ vcat
[ text "delta =" <+> prettyTCM delta
, text "binds =" <+> text (show binds)
]
let sigma = zipWith ($) fs (repeat v)
let sub = parallelS (reverse sigma)
let fdelta = flattenTel delta
reportSDoc "tc.term.let.pattern" 20 $ nest 2 $ vcat
[ text "fdelta =" <+> text (show 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 $ zip4 infos xs sigma ts
checkLetBinding (A.LetApply i x modapp rd rm) ret = do
fv <- getModuleFreeVars =<< currentModule
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 rd rm
withAnonymousModule x new ret
checkLetBinding A.LetOpen{} ret = ret
class ConvColor a i where
convColor :: a -> i
instance ConvColor A.ArgInfo I.ArgInfo where
convColor = mapArgInfoColors $ const []
instance ConvColor (A.Arg e) (I.Arg e) where
convColor = mapArgInfo convColor
instance ConvColor (A.Dom e) (I.Dom e) where
convColor = mapDomInfo convColor
instance ConvColor a i => ConvColor [a] [i] where
convColor = map convColor