module Agda.TypeChecking.Rules.Term where
import Control.Applicative
import Control.Arrow ((***), (&&&))
import Control.Monad.Trans
import Control.Monad.Reader
import Control.Monad.Error
import Data.Maybe
import Data.List hiding (sort)
import qualified Data.Map as Map
import qualified Data.Set as Set
import Data.Traversable (traverse,sequenceA)
import Agda.Interaction.Options
import qualified Agda.Syntax.Abstract as A
import qualified 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.Translation.AbstractToConcrete
import Agda.Syntax.Concrete.Pretty
import Agda.Syntax.Fixity
import Agda.Syntax.Internal
import Agda.Syntax.Position
import Agda.Syntax.Literal
import Agda.Syntax.Abstract.Views
import Agda.Syntax.Scope.Base (emptyScopeInfo)
import Agda.Syntax.Translation.InternalToAbstract (reify)
import Agda.TypeChecking.Monad
import Agda.TypeChecking.Monad.Builtin
import Agda.TypeChecking.Substitute
import Agda.TypeChecking.Reduce
import Agda.TypeChecking.MetaVars
import Agda.TypeChecking.Pretty
import Agda.TypeChecking.Records
import Agda.TypeChecking.RecordPatterns
import Agda.TypeChecking.Conversion
import Agda.TypeChecking.Implicit (implicitArgs)
import Agda.TypeChecking.InstanceArguments
import Agda.TypeChecking.Primitive
import Agda.TypeChecking.Constraints
import Agda.TypeChecking.Free hiding (Occurrence(..))
import Agda.TypeChecking.Telescope
import Agda.TypeChecking.Datatypes
import Agda.TypeChecking.Irrelevance
import Agda.TypeChecking.EtaContract
import Agda.TypeChecking.Quote
import Agda.TypeChecking.CompiledClause
import Agda.TypeChecking.Level
import Agda.TypeChecking.Rules.Builtin.Coinduction
import Agda.TypeChecking.Rules.LHS (checkLeftHandSide)
import Agda.Utils.Fresh
import Agda.Utils.Tuple
import Agda.Utils.Permutation
import Agda.Utils.List (zipWithTails)
import Agda.TypeChecking.Empty (isEmptyType)
import Agda.TypeChecking.Rules.Decl (checkSectionApplication)
import Agda.TypeChecking.Rules.Def (checkFunDef,checkFunDef')
import Agda.Utils.Monad
import Agda.Utils.Size
#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 h r t) b -> do
a <- Dom h r <$> isType_ t
b <- isType_ b
return $ El (sLub (getSort $ unDom a) (getSort b)) (Pi a (NoAbs "_" 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 NotHidden r l)
| A.Set _ 0 <- unScope s ->
ifM (not <$> hasUniversePolymorphism)
(typeError $ GenericError "Use --universe-polymorphism to enable level arguments to Set")
$ do
lvl <- primLevel
n <- levelView =<< applyRelevanceToContext NonStrict
(checkExpr (namedThing l) (El (mkType 0) 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 h rel b)) ret =
checkTypedBinding lamOrPi h rel b $ \bs ->
ret $ foldr (\(x,t) -> ExtendTel (Dom h rel t) . Abs x) EmptyTel bs
checkTypedBinding :: LamOrPi -> Hiding -> Relevance -> A.TypedBinding -> ([(String,Type)] -> TCM a) -> TCM a
checkTypedBinding lamOrPi h rel (A.TBind i xs e) ret = do
allowed <- optExperimentalIrrelevance <$> pragmaOptions
t <- modEnv lamOrPi allowed $ isType_ e
addCtxs xs (Dom h (modRel lamOrPi allowed rel) t) $ ret $ mkTel xs t
where
modEnv LamNotPi True = doWorkOnTypes
modEnv _ _ = id
modRel PiNotLam True = irrToNonStrict
modRel _ _ = id
mkTel [] t = []
mkTel (x:xs) t = (show $ nameConcrete x,t) : mkTel xs (raise 1 t)
checkTypedBinding lamOrPi h rel (A.TNoBind e) ret = do
t <- isType_ e
ret [("_",t)]
checkLambda :: Arg A.TypedBinding -> A.Expr -> Type -> TCM Term
checkLambda (Arg _ _ A.TNoBind{}) _ _ = __IMPOSSIBLE__
checkLambda (Arg h r (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 h r <$> isType_ typ
t1 <- addCtxs xs argsT $ workOnTypes newTypeMeta_
let tel = telFromList $ mkTel xs argsT
if (h /= 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 (domHiding arg == h) $ typeError $ WrongHidingInLambda target
let r' = domRelevance arg
when (r == Irrelevant && r' /= r) $ typeError $ WrongIrrelevanceInLambda target
(pid, argT) <- newProblem $ isTypeEqualTo typ (unDom arg)
v <- add x y (Dom h r' argT) $ checkExpr body btyp
blockTermOnProblem target (Lam h $ Abs (show $ nameConcrete x) v) pid
where
[x] = xs
add x y | C.isNoName (nameConcrete x) = addCtxString y
| otherwise = addCtx x
useTargetType _ _ = __IMPOSSIBLE__
mkTel [] t = []
mkTel (x : xs) t = ((,) s <$> t) : mkTel xs (raise 1 t)
where s = show $ nameConcrete x
checkLiteral :: Literal -> Type -> TCM Term
checkLiteral lit t = do
t' <- litType lit
coerce (Lit lit) t' t
reduceCon :: QName -> TCM QName
reduceCon c = do
Con c [] <- ignoreSharing <$> (constructorForm =<< reduce (Con c []))
return c
checkArguments' ::
ExpandHidden -> ExpandInstances -> Range -> [NamedArg A.Expr] -> Type -> Type -> A.Expr ->
(Args -> Type -> TCM Term) -> TCM Term
checkArguments' exph expIFS r args t0 t e k = do
z <- runErrorT $ checkArguments exph expIFS r args t0 t
case z of
Right (vs, t1) -> k vs t1
Left t0 -> postponeTypeCheckingProblem e t (unblockedTester t0)
unScope (A.ScopedExpr scope e) = unScope e
unScope e = e
checkExpr :: A.Expr -> Type -> TCM Term
checkExpr e t =
verboseBracket "tc.term.expr.top" 5 "checkExpr" $
traceCall (CheckExpr e t) $ localScope $ shared <$> do
reportSDoc "tc.term.expr.top" 15 $
text "Checking" <+> sep
[ fsep [ prettyTCM e, text ":", prettyTCM t ]
, nest 2 $ text "at " <+> (text . show =<< getCurrentRange)
]
reportSDoc "tc.term.expr.top.detailed" 80 $
text "Checking" <+> fsep [ prettyTCM e, text ":", text (show t) ]
t <- reduce t
reportSDoc "tc.term.expr.top" 15 $
text " --> " <+> prettyTCM t
let scopedExpr (A.ScopedExpr scope e) = setScope scope >> scopedExpr e
scopedExpr e = return e
unScope (A.ScopedExpr scope e) = unScope e
unScope e = e
e <- scopedExpr e
case e of
_ | Pi (Dom h rel _) _ <- ignoreSharing $ unEl t
, not (hiddenLambdaOrHole h e)
, h /= NotHidden -> do
x <- freshName r (argName t)
reportSLn "tc.term.expr.impl" 15 $ "Inserting implicit lambda"
checkExpr (A.Lam (A.ExprRange $ getRange e) (domainFree h rel x) e) t
where
r = case rStart $ getRange e of
Nothing -> noRange
Just pos -> posToRange pos pos
hiddenLambdaOrHole h (A.AbsurdLam _ h') | h == h' = True
hiddenLambdaOrHole h (A.ExtendedLam _ _ _ []) = False
hiddenLambdaOrHole h (A.ExtendedLam _ _ _ cls) = any hiddenLHS cls
hiddenLambdaOrHole h (A.Lam _ (A.DomainFree h' _ _) _) | h == h' = True
hiddenLambdaOrHole h (A.Lam _ (A.DomainFull (A.TypedBindings _ (Arg h' _ _))) _)
| h == h' = True
hiddenLambdaOrHole _ (A.QuestionMark _) = True
hiddenLambdaOrHole _ _ = False
hiddenLHS (A.Clause (A.LHS _ (A.LHSHead _ (a : _)) _) _ _) = elem (argHiding a) [Hidden, Instance]
hiddenLHS _ = False
A.QuestionMark i -> checkMeta newQuestionMark t i
A.Underscore i -> checkMeta (newValueMeta RunMetaOccursCheck) t i
A.WithApp _ e es -> typeError $ NotImplemented "type checking of with application"
A.App i s (Arg NotHidden r l)
| A.Set _ 0 <- unScope s ->
ifM (not <$> hasUniversePolymorphism)
(typeError $ GenericError "Use --universe-polymorphism to enable level arguments to Set")
$ do
lvl <- primLevel
n <- levelView =<< applyRelevanceToContext NonStrict
(checkExpr (namedThing l) (El (mkType 0) 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 NotHidden r e)
| A.Quote _ <- unScope q -> do
let quoted (A.Def 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 =<< normalise et
ty <- el primAgdaTerm
coerce q ty t
| A.Unquote _ <- unScope q ->
do e1 <- checkExpr (namedThing e) =<< el primAgdaTerm
e2 <- unquote e1
checkTerm e2 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 -> do
t <- instantiateFull t
ifBlockedType t (\ m t' -> postponeTypeCheckingProblem_ e t') $ \ t' -> do
case ignoreSharing $ unEl t' of
Pi dom@(Dom h' r a) _
| h == h' && not (null $ allMetas a) ->
postponeTypeCheckingProblem e t' $
null . allMetas <$> instantiateFull a
| h == h' -> blockTerm t' $ do
isEmptyType (getRange i) a
top <- currentModule
let name = "absurd"
aux <- qualify top <$> freshName (getRange i) name
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 rel aux t' [Nonvariant] [Unused] (defaultDisplayForm aux) 0 noCompiledRep
$ Function
{ funClauses =
[Clause
{ clauseRange = getRange e
, clauseTel = EmptyTel
, clausePerm = Perm 1 []
, clausePats = [Arg h r $ VarP "()"]
, clauseBody = Bind $ NoAbs "()" NoBody
}
]
, funCompiled = Fail
, funDelayed = NotDelayed
, funInv = NotInjective
, funAbstr = ConcreteDef
, funMutual = []
, funProjection = Nothing
, funStatic = False
, funCopy = False
, funTerminates = Just True
}
tel <- getContextTelescope
return $ Def aux $ teleArgs tel
| otherwise -> typeError $ WrongHidingInLambda t'
_ -> typeError $ ShouldBePi t'
A.ExtendedLam i di qname cs -> do
t <- instantiateFull t
ifBlockedType t (\ m t' -> postponeTypeCheckingProblem_ e t') $ \ t -> do
j <- currentOrFreshMutualBlock
rel <- asks envRelevance
addConstant qname $
Defn rel qname t [] [] (defaultDisplayForm qname) j noCompiledRep Axiom
reportSDoc "tc.term.exlam" 50 $
text "extended lambda's implementation \"" <> prettyTCM qname <>
text "\" has type: " $$ prettyTCM t
abstract (A.defAbstract di) $ checkFunDef' t rel NotDelayed di qname cs
args <- getContextArgs
top <- currentModule
freevars <- getSecFreeVars top
let argsNoParam = genericDrop freevars args
let (hid, notHid) = partition ((Hidden ==) . argHiding) argsNoParam
addExtLambdaTele qname (length hid, length notHid)
reduce $ (Def qname [] `apply` args)
where
abstract ConcreteDef = inConcreteMode
abstract AbstractDef = inAbstractMode
A.Lam i (A.DomainFull (A.TypedBindings _ b)) e -> checkLambda b e t
A.Lam i (A.DomainFree h rel x) e0 -> checkExpr (A.Lam i (domainFree h rel 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 h r a) b -> do
a' <- isType_ a
b' <- isType_ b
s <- reduce $ getSort a' `sLub` getSort b'
coerce (Pi (Dom h r a') (NoAbs "_" 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 -> do
t <- reduce t
case ignoreSharing $ unEl t of
Def r vs -> do
axs <- getRecordFieldNames r
let xs = map unArg axs
ftel <- getRecordFieldTypes r
con <- getRecordConstructor r
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, argHiding a == NotHidden
, 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
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
vs <- newArgsMeta (defType def)
let target = piApply (defType def) vs
s = case ignoreSharing $ unEl target of
Level l -> Type l
Sort s -> s
_ -> __IMPOSSIBLE__
inferred = El s $ Def r 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_ e t
_ -> typeError $ ShouldBeRecordType t
A.RecUpdate ei recexpr fs -> do
case ignoreSharing $ unEl t of
Def r vs -> do
rec <- checkExpr recexpr t
name <- freshNoName (getRange recexpr)
addLetBinding Relevant name rec 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_ 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 (Arg NotHidden _ p) Nothing = Just $ A.App ei (A.Def p) $ defaultNamedArg $ A.Var n
replaceFields _ _ (Arg _ _ _) Nothing = Nothing
replaceFields _ _ _ (Just e) = Just $ e
A.DontCare e ->
ifM ((Irrelevant ==) <$> asks envRelevance)
(DontCare <$> do applyRelevanceToContext Irrelevant $ checkExpr e t)
(internalError "DontCare may only appear in irrelevant contexts")
A.ScopedExpr scope e -> setScope scope >> checkExpr e t
e0@(A.QuoteGoal _ x e) -> do
t' <- etaContract =<< normalise t
let metas = allMetas t'
case metas of
_:_ -> postponeTypeCheckingProblem e0 t' $ andM $ map isInstantiatedMeta metas
[] -> do
quoted <- quoteTerm (unEl t')
tmType <- agdaTermType
(v, ty) <- addLetBinding Relevant x quoted tmType (inferExpr e)
blockTerm t' $ coerce v ty t'
A.ETel _ -> __IMPOSSIBLE__
_ | Application (A.Con (AmbQ cs@(_:_:_))) args <- appView e -> 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)
cs <- zip cs . zipWith setRange (map getRange cs) <$> mapM reduceCon cs
reportSLn "tc.check.term" 40 $ " ranges after: " ++ show (getRange cs)
reportSLn "tc.check.term" 40 $ " reduced: " ++ show cs
dcs <- mapM (\(c0, c1) -> (getData /\ const c0) . theDef <$> getConstInfo c1) cs
let badCon t = typeError $ DoesNotConstructAnElementOf
(fst $ head cs) t
let getCon = do
TelV _ t1 <- telView t
reportSDoc "tc.check.term.con" 40 $ nest 2 $
text "target type: " <+> prettyTCM t1
ifBlocked (unEl t1) (\ m t -> return Nothing) $ \ t' ->
(isDataOrRecord t' >>=) $ maybe (badCon t') $ \ d ->
case [ c | (d', c) <- dcs, d == d' ] of
[c] -> do
reportSLn "tc.check.term" 40 $ " decided on: " ++ show c
return (Just c)
[] -> badCon (Def d [])
cs -> typeError $ GenericError $
"Can't resolve overloaded constructors targeting the same datatype (" ++ show d ++
"): " ++ unwords (map show cs)
let unblock = isJust <$> getCon
mc <- getCon
case mc of
Just c -> checkConstructorApplication e t c args
Nothing -> postponeTypeCheckingProblem e t unblock
| Application (A.Con (AmbQ [c])) args <- appView e ->
checkConstructorApplication e t c args
| Application (A.PatternSyn n) args <- appView e -> do
(ns, p) <- lookupPatternSyn n
let (zs, ns', as) = zipWithTails (\n a -> (n, namedThing (unArg a))) ns args
p' = A.patternToExpr $ setRange (getRange n) p
e' = A.lambdaLiftExpr ns' (A.substExpr zs p') `A.app` as
checkExpr e' t
| Application hd args <- appView e ->
checkHeadApplication e t hd args
domainFree h rel x =
A.DomainFull $ A.TypedBindings r $ Arg h rel $ A.TBind r [x] $ A.Underscore info
where
r = getRange x
info = A.MetaInfo
{ A.metaRange = r
, A.metaScope = emptyScopeInfo
, A.metaNumber = Nothing
, A.metaNameSuggestion = show x
}
checkMeta :: (Type -> TCM Term) -> Type -> A.MetaInfo -> TCM Term
checkMeta newMeta t i = do
case A.metaNumber i of
Nothing -> do
setScope (A.metaScope i)
v <- newMeta t
setValueMetaName v (A.metaNameSuggestion i)
return v
Just n -> do
let v = MetaV (MetaId n) []
t' <- jMetaType . mvJudgement <$> lookupMeta (MetaId n)
coerce v t' t
inferMeta :: (Type -> TCM Term) -> A.MetaInfo -> TCM (Args -> Term, Type)
inferMeta newMeta i =
case A.metaNumber i of
Nothing -> do
setScope (A.metaScope i)
t <- workOnTypes $ newTypeMeta_
v <- newMeta t
return (apply v, t)
Just n -> do
let v = MetaV (MetaId n)
t' <- jMetaType . mvJudgement <$> lookupMeta (MetaId n)
return (v, t')
inferHead :: A.Expr -> TCM (Args -> Term, Type)
inferHead (A.Var x) = do
(u, a) <- getVarInfo x
when (unusableRelevance $ domRelevance a) $
typeError $ VariableIsIrrelevant x
return (apply u, unDom a)
inferHead (A.Def x) = do
proj <- isProjection x
case proj of
Nothing -> do
(u, a) <- inferDef Def x
return (apply u, a)
Just{} -> do
Just (r, n) <- funProjection . theDef <$> getConstInfo x
cxt <- size <$> freeVarsToApply x
m <- getDefFreeVars x
reportSDoc "tc.term.proj" 10 $ sep
[ text "building projection" <+> prettyTCM x
, nest 2 $ parens (text "ctx =" <+> text (show cxt))
, nest 2 $ parens (text "n =" <+> text (show n))
, nest 2 $ parens (text "m =" <+> text (show m)) ]
let hs | n == 0 = __IMPOSSIBLE__
| otherwise = genericReplicate (n 1) NotHidden
names = [ s ++ [c] | s <- "" : names, c <- ['a'..'z'] ]
eta = foldr (\(h, s) -> Lam h . NoAbs s) (Def x []) (zip hs names)
(u, a) <- inferDef (\f vs -> eta `apply` vs) x
return (apply u, a)
inferHead (A.Con (AmbQ [c])) = do
(u, a) <- inferDef (\c _ -> Con c []) c
Constructor{conPars = n} <- theDef <$> (instantiateDef =<< getConstInfo c)
verboseS "tc.term.con" 7 $ do
reportSLn "" 0 $ unwords [show c, "has", show n, "parameters."]
return (apply u . genericDrop n, a)
inferHead (A.Con _) = __IMPOSSIBLE__
inferHead (A.QuestionMark i) = inferMeta newQuestionMark i
inferHead (A.Underscore i) = inferMeta (newValueMeta RunMetaOccursCheck) i
inferHead e = do (term, t) <- inferExpr e
return (apply term, t)
inferDef :: (QName -> Args -> 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
verboseS "tc.term.def" 10 $ do
ds <- mapM prettyTCM vs
dx <- prettyTCM x
dt <- prettyTCM $ defType d
reportSLn "" 0 $ "inferred def " ++ unwords (show dx : map show ds) ++ " : " ++ show dt
return (mkTerm x vs, defType d)
checkConstructorApplication :: A.Expr -> Type -> QName -> [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 (args', paramsGiven) = checkForParams args
if paramsGiven then fallback else do
reportSDoc "tc.term.con" 50 $ text "checkConstructorApplication: no parameters explicitly supplied, continuing..."
cdef <- getConstInfo 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' vs) -> do
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'
flip (maybe fallback) (sequenceA $ List2 (npars, npars')) $ \(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') bla
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'
checkArguments' ExpandLast ExpandInstanceArguments (getRange c) args' ctype' t org $ \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 [c])) args
bla = __IMPOSSIBLE__
checkForParams args =
let (hargs, rest) = span isHiddenArg args
removeScope (A.ScopedExpr _ e) = removeScope e
removeScope e = e
notUnderscore A.Underscore{} = False
notUnderscore _ = True
in (rest,) $ any notUnderscore $ map (removeScope . namedArg) hargs
checkHeadApplication :: A.Expr -> Type -> A.Expr -> [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
]
checkArguments' ExpandLast ExpandInstanceArguments (getRange hd) args t0 t e $ \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 $ 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.qnameName c) ++ "-" ++ show i
c' <- setRange (getRange c) <$>
liftM2 qualify (killRange <$> currentModule)
(freshName_ name)
e' <- Def c' <$> getContextArgs
i <- currentOrFreshMutualBlock
tel <- getContextTelescope
rel <- asks envRelevance
addConstant c' (Defn rel c' t [] [] (defaultDisplayForm c') i noCompiledRep $ Axiom)
ctx <- getContext
let info = A.mkDefInfo (A.nameConcrete $ A.qnameName c') defaultFixity'
PublicAccess ConcreteDef noRange
pats = map (\ (Dom h r (n, _)) -> Arg h r $ 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 "."
]
escapeContextToTopLevel $ 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
checkArguments' ExpandLast ExpandInstanceArguments (getRange hd) args t0 t e $ \vs t1 ->
coerce (f vs) t1 t
instance Error Type where
strMsg _ = __IMPOSSIBLE__
noMsg = __IMPOSSIBLE__
traceCallE :: Error e => (Maybe r -> Call) -> ErrorT e TCM r -> ErrorT e TCM r
traceCallE call m = do
z <- lift $ traceCall call' $ runErrorT 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 -> [NamedArg A.Expr] -> Type -> Type ->
ErrorT Type TCM (Args, Type)
checkArguments DontExpandLast _ _ [] 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 h _ _) _) Hidden = h /= Hidden
expand _ Hidden = True
expand (Pi (Dom h _ _) _) Instance = h /= Instance && expandIFS == ExpandInstanceArguments
expand _ Instance = expandIFS == ExpandInstanceArguments
expand _ NotHidden = False
checkArguments exh expandIFS r args0@(Arg h _ 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
]
]
t0b <- lift $ reduceB t0
let isMeta t = case ignoreSharing $ unEl t of { MetaV{} -> True; _ -> False }
case t0b of
Blocked{} -> throwError $ ignoreBlocking t0b
NotBlocked t0' | isMeta t0' -> throwError $ ignoreBlocking t0b
NotBlocked t0' -> do
e' <- return $ namedThing e
case ignoreSharing $ unEl t0' of
Pi (Dom h' rel a) _ |
h == h' && (h == NotHidden || sameName (nameOf e) (nameInPi $ unEl t0')) -> do
u <- lift $ applyRelevanceToContext rel $ checkExpr e' a
let arg = Arg h rel u
(us, t0'') <- checkArguments exh expandIFS (fuseRange r e) args (piApply t0' [arg]) t1
return (arg : us, t0'')
Pi (Dom Instance rel a) b | expandIFS == ExpandInstanceArguments ->
insertIFSUnderscore rel (absName b) a
Pi (Dom Hidden rel a) b -> insertUnderscore rel (absName b)
Pi (Dom NotHidden _ _) _ -> lift $ typeError $ WrongHidingInApplication t0'
_ -> lift $ typeError $ ShouldBePi t0'
where
insertIFSUnderscore rel x a = do
lift $ reportSLn "tc.term.args.ifs" 15 $ "inserting implicit meta (2) for type " ++ show a
v <- lift $ applyRelevanceToContext rel $ initializeIFSMeta x a
let arg = Arg Instance rel v
(vs, t0'') <- checkArguments exh expandIFS r args0 (piApply t0 [arg]) t1
return (arg : vs, t0'')
insertUnderscore rel x = do
scope <- lift $ getScope
let m = A.Underscore $ A.MetaInfo
{ A.metaRange = r
, A.metaScope = scope
, A.metaNumber = Nothing
, A.metaNameSuggestion = x
}
checkArguments exh expandIFS r (Arg Hidden rel (unnamed m) : args0) t0 t1
name (Named _ (A.Var x)) = show x
name (Named (Just x) _) = x
name _ = "x"
sameName Nothing _ = True
sameName n1 n2 = n1 == n2
nameInPi (Pi _ b) = Just $ absName b
nameInPi (Shared p) = nameInPi (derefPtr p)
nameInPi _ = __IMPOSSIBLE__
checkArguments_ :: ExpandHidden -> Range -> [NamedArg A.Expr] -> Telescope -> TCM Args
checkArguments_ exh r args tel = do
z <- runErrorT $ 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 = inferOrCheck e Nothing
defOrVar :: A.Expr -> Bool
defOrVar A.Var{} = True
defOrVar A.Def{} = True
defOrVar _ = False
inferOrCheck :: A.Expr -> Maybe Type -> TCM (Term, Type)
inferOrCheck e mt = case e of
_ | Application hd args <- appView e, defOrVar hd -> traceCall (InferExpr e) $ do
(f, t0) <- inferHead hd
res <- runErrorT $ checkArguments DontExpandLast ExpandInstanceArguments (getRange hd) args t0 $ maybe (sort Prop) id mt
case res of
Right (vs, t1) -> maybe (return (f vs, t1))
(\ t -> (,t) <$> coerce (f vs) t1 t)
mt
Left t1 -> fallback
_ -> fallback
where
fallback = do
t <- maybe (workOnTypes $ newTypeMeta_) return mt
v <- checkExpr e t
return (v,t)
inferExprForWith :: A.Expr -> TCM (Term, Type)
inferExprForWith e = do
(v, t) <- inferExpr e
TelV tel t0 <- telViewUpTo' (1) ((NotHidden /=) . domHiding) 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)
checkTerm :: Term -> Type -> TCM Term
checkTerm tm ty = do atm <- reify tm
checkExpr atm ty
checkLetBindings :: [A.LetBinding] -> TCM a -> TCM a
checkLetBindings = foldr (.) id . map checkLetBinding
checkLetBinding :: A.LetBinding -> TCM a -> TCM a
checkLetBinding b@(A.LetBind i rel x t e) ret =
traceCallCPS_ (CheckLetBinding b) ret $ \ret -> do
t <- isType_ t
v <- applyRelevanceToContext rel $ checkExpr e t
addLetBinding rel x v t ret
checkLetBinding b@(A.LetPatBind i p e) ret =
traceCallCPS_ (CheckLetBinding b) ret $ \ret -> do
(v, t) <- inferExpr e
let
t0 = El (getSort t) $ Pi (Dom NotHidden Relevant t) (NoAbs "_" typeDontCare)
p0 = Arg NotHidden Relevant (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) [p0] t0 $ \ mgamma delta sub xs ps t' perm -> do
let p = case ps of [p] -> unArg 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 rels = map domRelevance tsl
let xs = map (fst . unDom) (reverse binds)
foldr (uncurry4 addLetBinding) ret $ zip4 rels xs sigma ts
checkLetBinding (A.LetApply i x modapp rd rm) ret = do
fv <- getModuleFreeVars =<< currentModule
n <- size <$> getContext
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