#if __GLASGOW_HASKELL__ >= 710
#endif
module Agda.TypeChecking.Rules.Term where
import Prelude hiding (null)
import Control.Applicative hiding (empty)
import Control.Arrow ((&&&), (***), first, second)
import Control.Monad.Trans
import Control.Monad.State (get, put)
import Control.Monad.Reader
import Data.Maybe
import Data.Either (partitionEithers)
import Data.Monoid (mappend)
import Data.List hiding (sort, null)
import qualified Data.Map as Map
import Data.Traversable (sequenceA)
import Data.Void
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, exprFieldA)
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 qualified Agda.Syntax.Reflected as R
import Agda.Syntax.Scope.Base ( ThingsInScope, AbstractName
, emptyScopeInfo
, exportedNamesInScope)
import Agda.Syntax.Scope.Monad (getNamedScope)
import Agda.Syntax.Translation.InternalToAbstract (reify)
import Agda.Syntax.Translation.ReflectedToAbstract (toAbstract_)
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.Positivity.Occurrence
import Agda.TypeChecking.Pretty
import Agda.TypeChecking.Primitive
import Agda.TypeChecking.Quote
import Agda.TypeChecking.Unquote
import Agda.TypeChecking.RecordPatterns
import Agda.TypeChecking.Records
import Agda.TypeChecking.Reduce
import Agda.TypeChecking.SizedTypes
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.Lens
import Agda.Utils.Maybe
import Agda.Utils.Monad
import Agda.Utils.Null
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 =<< 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 <- ptsRule a 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)
noFunctionsIntoSize t0 t'
return t'
A.Set _ n -> do
return $ sort (mkType n)
A.App i s (Arg (ArgInfo NotHidden r) 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)
_ -> fallback
ptsRule :: (LensSort a, LensSort b) => a -> b -> TCM Sort
ptsRule a b = pts <$> reduce (getSort a) <*> reduce (getSort b)
noFunctionsIntoSize :: Type -> Type -> TCM ()
noFunctionsIntoSize t tBlame = do
reportSDoc "tc.fun" 20 $ do
let El s (Pi dom b) = ignoreSharing <$> 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 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 = 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
allowed <- optExperimentalIrrelevance <$> pragmaOptions
t <- modEnv lamOrPi allowed $ isType_ e
let info' = mapRelevance (modRel lamOrPi allowed) info
addContext (xs, Dom info' t) $
ret $ bindsWithHidingToTel xs (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 :: 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 = " ++ show xs
let numbinds = length xs
TelV tel btyp <- telViewUpTo numbinds target
if size tel < numbinds || 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
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 arg (Abs y EmptyTel)) btyp = do
verboseS "tc.term.lambda" 5 $ tick "lambda-with-target-type"
reportSLn "tc.term.lambda" 60 $ "useTargetType y = " ++ show y
info <- return $ mapHiding (mappend h) info
unless (getHiding arg == getHiding info) $ typeError $ WrongHidingInLambda target
let r = getRelevance info
r' = getRelevance arg
when (r == Irrelevant && r' /= r) $ typeError $ WrongIrrelevanceInLambda target
let a = unDom arg
checkSizeLtSat $ unEl a
(pid, argT) <- newProblem $ isTypeEqualTo typ a
v <- add (notInScopeName y) (Dom (setRelevance r' info) argT) $ checkExpr body btyp
blockTermOnProblem target (Lam info $ Abs (nameToArgName x) v) pid
where
[WithHiding h x] = xs
add y dom | isNoName x = addContext (y, dom)
| otherwise = addContext (x, dom)
useTargetType _ _ = __IMPOSSIBLE__
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
let r = getRelevance info
r' = getRelevance dom
info' = setHiding lamHiding $ setRelevance r' info
when (r == Irrelevant && r' /= r) $
typeError $ WrongIrrelevanceInLambda target
mpid <- caseMaybe mt (return Nothing) $ \ ascribedType -> Just <$> do
newProblem_ $ leqType (unDom dom) ascribedType
let add dom | isNoName x = addContext (absName b, dom)
| otherwise = addContext (x, dom)
v <- add (maybe dom (dom $>) mt) $
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 $ \ t0 -> do
let t = ignoreSharing <$> t0
case unEl t of
Pi dom b -> do
let h' = getHiding dom
if 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 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 $
(\ d -> (defaultDefn (setRelevance rel info') aux t' d)
{ defPolarity = [Nonvariant]
, defArgOccurrences = [Unused] })
$ Function
{ funClauses =
[Clause
{ clauseRange = getRange e
, clauseTel = telFromList [fmap ("()",) dom]
, namedClausePats = [Arg info' $ Named (Just $ unranged $ absName b) $ VarP (0,"()")]
, clauseBody = Bind $ NoAbs "()" NoBody
, clauseType = Just $ setRelevance rel $ defaultArg $ absBody b
, clauseCatchall = False
}
]
, funCompiled = Just Fail
, funTreeless = Nothing
, funDelayed = NotDelayed
, funInv = NotInjective
, funAbstr = ConcreteDef
, funMutual = []
, funProjection = Nothing
, funSmashable = False
, funStatic = False
, funInline = 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" 20 $
text (show $ A.defAbstract di) <+>
text "extended lambda's implementation \"" <> prettyTCM qname <>
text "\" has type: " $$ prettyTCM t
args <- getContextArgs
freevars <- getCurrentModuleFreeVars
let argsNoParam = genericDrop freevars args
let (hid, notHid) = partition isHidden argsNoParam
reportSDoc "tc.term.exlam" 30 $ vcat $
[ text "dropped args: " <+> prettyTCM (take freevars args)
, text "hidden args: " <+> prettyTCM hid
, text "visible args: " <+> prettyTCM notHid
]
mx <- catchIlltypedPatternBlockedOnMeta $ abstract (A.defAbstract di) $
checkFunDef' t info NotDelayed (Just $ ExtLamInfo (length hid) (length notHid)) Nothing di qname cs
case mx of
Nothing -> return $ Def qname $ map Apply args
Just (err, x) -> do
mm <- Map.lookup x <$> getMetaStore
case mvInstantiation <$> mm of
Nothing -> do
throwError err
Just InstV{} -> __IMPOSSIBLE__
Just InstS{} -> __IMPOSSIBLE__
Just{} -> do
postponeTypeCheckingProblem (CheckExpr e t) $ isInstantiatedMeta x
where
abstract ConcreteDef = inConcreteMode
abstract AbstractDef = inAbstractMode
catchIlltypedPatternBlockedOnMeta :: TCM () -> TCM (Maybe (TCErr, MetaId))
catchIlltypedPatternBlockedOnMeta m = (Nothing <$ m) `catchError` \ err -> do
let reraise = throwError err
case err of
TypeError s cl@(Closure sig env scope (IlltypedPattern p a)) ->
enterClosure cl $ \ _ -> do
ifBlockedType a (\ x _ -> return $ Just (err, x)) $ \ _ -> reraise
_ -> reraise
expandModuleAssigns :: [Either A.Assign A.ModuleName] -> [C.Name] -> TCM A.Assigns
expandModuleAssigns mfs exs = do
let (fs , ms) = partitionEithers mfs
exs' = exs \\ 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 $ GenericError $ "Ambiguity: the field " ++ show f ++ " appears in the following modules " ++ show (map 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 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
exs = filter notHidden axs
xs = map unArg axs
con = killRange $ recConHead def
reportSDoc "tc.term.rec" 20 $ vcat
[ text $ " xs = " ++ show xs
, text " ftel= " <> prettyTCM (recTel def)
, text $ " con = " ++ show con
]
fs <- expandModuleAssigns mfs (map unArg exs)
scope <- getScope
let re = getRange e
meta x = A.Underscore $ A.MetaInfo re scope Nothing (show x)
es <- insertMissingFields r meta fs axs
args <- checkArguments_ ExpandLast re es (recTel def `apply` vs) >>= \case
(args, remainingTel) | null remainingTel -> return args
_ -> __IMPOSSIBLE__
reportSDoc "tc.term.rec" 20 $ text $ "finished record expression"
return $ Con con 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 " ++ 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
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 (\ (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 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 -> 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 -> Range -> [NamedArg A.Expr] -> Type -> Type ->
(Args -> Type -> TCM Term) -> TCM Term
checkArguments' exph r args t0 t k = do
z <- runExceptT $ checkArguments exph 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 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 _) b <- ignoreSharing $ unEl t
, let h = getHiding info
, notVisible h
, not (hiddenLambdaOrHole h e)
-> do
x <- freshName rx $ notInScopeName $ absName b
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 _ bind _ -> h == getHiding bind
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
e0@(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)
et' <- etaContract =<< normalise 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 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)
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 <- ptsRule a' 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 tac = foldl (A.App i) (A.App i (A.App i e quotedCtx) quotedGoal) xs
result = foldl (A.App i) (A.Unquote i) (defaultNamedArg tac : ys)
checkExpr result t
A.ETel _ -> __IMPOSSIBLE__
_ | Application hd args <- appView e -> checkApplication hd args e t
quoteGoal :: Type -> TCM (Either [MetaId] Term)
quoteGoal t = do
t' <- etaContract =<< normalise 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 =<< normalise contextTypes
let metas = allMetas contextTypes
case metas of
_:_ -> return $ Left metas
[] -> do
quotedContext <- buildList <*> mapM quoteDom contextTypes
return $ Right quotedContext
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 args
Nothing -> postponeTypeCheckingProblem (CheckExpr e t) unblock
A.Con (AmbQ [c]) -> do
con <- getOrigConHead c
checkConstructorApplication e t con args
A.PatternSyn n -> do
(ns, p) <- lookupPatternSyn n
p <- setRange (getRange n) . killRange <$> expandPatternSynonyms (vacuous 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.Macro x -> do
TelV tel _ <- telView =<< normalise . defType =<< getConstInfo x
tTerm <- primAgdaTerm
tName <- primQName
let argTel = init $ telToList tel
mkArg :: Type -> NamedArg A.Expr -> NamedArg A.Expr
mkArg t a | unEl t == tTerm =
(fmap . fmap)
(A.App (A.ExprRange (getRange a)) (A.QuoteTerm A.exprNoRange) . defaultNamedArg) a
mkArg t a | unEl t == tName =
(fmap . fmap)
(A.App (A.ExprRange (getRange a)) (A.Quote A.exprNoRange) . defaultNamedArg) a
mkArg t a | otherwise = a
makeArgs :: [Dom (String, Type)] -> [NamedArg A.Expr] -> ([NamedArg A.Expr], [NamedArg A.Expr])
makeArgs [] args = ([], args)
makeArgs _ [] = ([], [])
makeArgs tel@(d : _) (arg : args) =
case insertImplicit arg (map (fmap fst . argFromDom) tel) of
ImpInsert is -> makeArgs (drop (length is) tel) (arg : args)
BadImplicits -> (arg : args, [])
NoSuchName{} -> (arg : args, [])
NoInsertNeeded -> first (mkArg (snd $ unDom d) arg :) $ makeArgs (tail tel) args
(macroArgs, otherArgs) = makeArgs argTel args
unq = A.App (A.ExprRange $ fuseRange x args) (A.Unquote A.exprNoRange) . defaultNamedArg
desugared = A.app (unq $ unAppView $ Application (A.Def x) $ macroArgs) otherArgs
checkExpr desugared t
A.Unquote _
| [arg] <- args -> do
hole <- newValueMeta RunMetaOccursCheck t
unquoteM (namedArg arg) hole t $ return hole
| arg : args <- args -> do
tel <- metaTel args
target <- addCtxTel tel newTypeMeta_
let holeType = telePi_ tel target
(vs, EmptyTel) <- checkArguments_ ExpandLast (getRange args) args tel
let rho = reverse (map unArg vs) ++# IdS
equalType (applySubst rho target) t
hole <- newValueMeta RunMetaOccursCheck holeType
unquoteM (namedArg arg) hole holeType $ return $ apply hole vs
where
metaTel :: [Arg a] -> TCM Telescope
metaTel [] = pure EmptyTel
metaTel (arg : args) = do
a <- newTypeMeta_
let dom = a <$ domFromArg arg
ExtendTel dom . Abs "x" <$> addCtxString "x" dom (metaTel args)
_ -> checkHeadApplication e t hd args
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
domainFree :: ArgInfo -> A.Name -> A.LamBinding
domainFree info x =
A.DomainFull $ A.TypedBindings r $ Arg info $ A.TBind r [pure 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 x -> do
let v = MetaV x []
t' <- jMetaType . mvJudgement <$> lookupMeta x
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
reportSDoc "tc.term.var" 20 $ hsep
[ text "variable" , text (show x)
, text "(" , text (show u) , text ")"
, text "has type:" , text (show a)
]
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 -> [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, conPars = npars} = 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'
caseMaybe (sequenceA $ List2 (Just 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'
let TelV ptel _ = telView'UpTo n ctype
let pnames = map (fst . unDom) $ telToList ptel
args' = dropArgs pnames args
expandLast <- asks envExpandLast
checkArguments' expandLast (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 -> [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 (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
arg <- case args of
[a] | getHiding a == NotHidden -> return $ namedArg a
_ -> typeError $ GenericError $ show c ++ " must be applied to exactly one argument."
i <- fresh :: TCM Int
let name = filter (/= '_') (show $ A.nameConcrete $ A.qnameName c) ++ "-" ++ show i
kit <- coinductionKit'
let flat = nameOfFlat kit
inf = nameOfInf kit
forcedType <- do
lvl <- levelType
l <- newValueMeta RunMetaOccursCheck lvl
lv <- levelView l
a <- newValueMeta RunMetaOccursCheck (sort $ Type lv)
return $ El (Type lv) $ Def inf [Apply $ setHiding Hidden $ defaultArg l, Apply $ defaultArg a]
wrapper <- inFreshModuleIfFreeParams $ do
c' <- setRange (getRange c) <$>
liftM2 qualify (killRange <$> currentModule)
(freshName_ name)
rel <- asks envRelevance
let info = A.mkDefInfo (A.nameConcrete $ A.qnameName c') noFixity'
PublicAccess ConcreteDef noRange
core = A.LHSProj { A.lhsDestructor = flat
, A.lhsPatsLeft = []
, A.lhsFocus = defaultNamedArg $ A.LHSHead c' []
, A.lhsPatsRight = [] }
clause = A.Clause (A.LHS (A.LHSRange noRange) core [])
(A.RHS arg)
[] False
i <- currentOrFreshMutualBlock
addConstant c' =<< do
let ai = setRelevance rel defaultArgInfo
useTerPragma $
(defaultDefn ai c' forcedType emptyFunction)
{ defMutual = i }
checkFunDef NotDelayed info c' [clause]
reportSDoc "tc.term.expr.coind" 15 $ do
def <- theDef <$> getConstInfo c'
vcat $
[ text "The coinductive wrapper"
, nest 2 $ prettyTCM rel <> prettyTCM c' <+> text ":"
, nest 4 $ prettyTCM t
, nest 2 $ prettyA clause
, text "The definition is" <+> text (show $ funDelayed def) <>
text "."
]
return c'
e' <- Def wrapper . map Apply <$> getContextArgs
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'
]
blockTerm t $ e' <$ workOnTypes (leqType forcedType t)
A.Con _ -> __IMPOSSIBLE__
_ -> defaultResult
where
defaultResult = do
(f, t0) <- inferHead hd
expandLast <- asks envExpandLast
checkArguments' expandLast (getRange hd) args t0 t $ \vs t1 -> do
coerce (f vs) t1 t
traceCallE ::
#if !MIN_VERSION_transformers(0,4,1)
Error e =>
#endif
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
checkArguments :: ExpandHidden -> Range -> [NamedArg A.Expr] -> Type -> Type ->
ExceptT (Args, [NamedArg A.Expr], Type) TCM (Args, Type)
checkArguments DontExpandLast _ [] t0 t1 = return ([], t0)
checkArguments exh 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
expand _ Instance = True
expand _ NotHidden = False
checkArguments exh 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 (us, 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
| 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 (fuseRange r e) args (absApp b u) t1
| otherwise -> do
reportSDoc "error" 10 $ nest 2 $ vcat
[ text $ "info = " ++ show info
, text $ "info' = " ++ show info'
, text $ "absName b = " ++ show (absName b)
, text $ "nameOf e = " ++ show (nameOf e)
]
wrongPi
_ -> shouldBePi
where
addCheckedArgs us u rec =
(mapFst ((us ++) . (u :)) <$> rec)
`catchError` \(vs, es, t) ->
throwError (us ++ u : vs, es, t)
checkArguments_
:: ExpandHidden
-> Range
-> [NamedArg A.Expr]
-> Telescope
-> TCM (Args, Telescope)
checkArguments_ exh r args tel = do
z <- runExceptT $
checkArguments exh r args (telePi tel typeDontCare) typeDontCare
case z of
Right (args, t) -> do
let TelV tel' _ = telView' t
return (args, tel')
Left _ -> __IMPOSSIBLE__
inferExpr :: A.Expr -> TCM (Term, Type)
inferExpr = inferExpr' DontExpandLast
inferExpr' :: ExpandHidden -> A.Expr -> TCM (Term, Type)
inferExpr' exh e = case e of
_ | Application hd args <- appView e, defOrVar hd -> traceCall (InferExpr e) $ do
(f, t0) <- inferHead hd
res <- runExceptT $ checkArguments exh (getRange hd) 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 <- getCurrentModuleFreeVars
n <- getContextSize
let firstModuleVar = n nfv
when (firstModuleVar < 0) __IMPOSSIBLE__
return $ i >= firstModuleVar
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 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 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' 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) =" <+> text (show p)
, text "t =" <+> prettyTCM t
]
]
checkLeftHandSide (CheckPattern p EmptyTel t) Nothing [p0] t0 $ \ (LHSResult delta 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 _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 rd rm
withAnonymousModule x new ret
checkLetBinding A.LetOpen{} ret = ret
checkLetBinding (A.LetDeclaredVariable _) ret = ret