{-# LANGUAGE CPP #-}
{-# LANGUAGE NondecreasingIndentation #-}
module Agda.TypeChecking.Rules.Application
( checkArguments
, checkArguments_
, checkApplication
, inferApplication
, checkProjAppToKnownPrincipalArg
) where
#if MIN_VERSION_base(4,11,0)
import Prelude hiding ( (<>), null )
#else
import Prelude hiding ( null )
#endif
import Control.Arrow (first, second)
import Control.Monad.Trans
import Control.Monad.Trans.Maybe
import Control.Monad.Reader
import Data.Maybe
import qualified Data.List as List
import Data.Either (partitionEithers)
import Data.Traversable (sequenceA)
import Data.Void
import qualified Data.IntSet as IntSet
import Agda.Interaction.Highlighting.Generate (storeDisambiguatedName)
import Agda.Interaction.Options
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.Common
import Agda.Syntax.Fixity
import Agda.Syntax.Internal as I
import Agda.Syntax.Position
import Agda.TypeChecking.Conversion
import Agda.TypeChecking.Constraints
import Agda.TypeChecking.Datatypes
import Agda.TypeChecking.Free
import Agda.TypeChecking.Implicit
import Agda.TypeChecking.Injectivity
import Agda.TypeChecking.Irrelevance
import Agda.TypeChecking.InstanceArguments (postponeInstanceConstraints)
import Agda.TypeChecking.Level
import Agda.TypeChecking.MetaVars
import Agda.TypeChecking.Names
import Agda.TypeChecking.Pretty
import Agda.TypeChecking.Primitive
import Agda.TypeChecking.Monad
import Agda.TypeChecking.Monad.Builtin
import Agda.TypeChecking.Pretty
import Agda.TypeChecking.Records
import Agda.TypeChecking.Reduce
import Agda.TypeChecking.Rules.Def
import Agda.TypeChecking.Rules.Term
import Agda.TypeChecking.Substitute
import Agda.TypeChecking.Telescope
import Agda.Utils.Either
import Agda.Utils.Except
import Agda.Utils.Functor
import Agda.Utils.Lens
import Agda.Utils.List
import Agda.Utils.Maybe
import Agda.Utils.Monad
import Agda.Utils.Null
import Agda.Utils.NonemptyList
import Agda.Utils.Pretty ( prettyShow )
import Agda.Utils.Size
import Agda.Utils.Tuple
#include "undefined.h"
import Agda.Utils.Impossible
type MaybeRanges = [Maybe Range]
checkApplication :: Comparison -> A.Expr -> A.Args -> A.Expr -> Type -> TCM Term
checkApplication cmp hd args e t = postponeInstanceConstraints $ do
reportSDoc "tc.check.app" 20 $ vcat
[ "checkApplication"
, nest 2 $ "hd = " <+> prettyA hd
, nest 2 $ "args = " <+> sep (map prettyA args)
, nest 2 $ "e = " <+> prettyA e
, nest 2 $ "t = " <+> prettyTCM t
]
reportSDoc "tc.check.app" 70 $ vcat
[ "checkApplication (raw)"
, nest 2 $ text $ "hd = " ++ show hd
, nest 2 $ text $ "args = " ++ show (deepUnscope args)
, nest 2 $ text $ "e = " ++ show (deepUnscope e)
, nest 2 $ text $ "t = " ++ show t
]
case unScope hd of
A.Proj _ p | Just _ <- getUnambiguous p -> checkHeadApplication cmp e t hd args
A.Proj o p -> checkProjApp cmp e o (unAmbQ p) args t
A.Con ambC | Just c <- getUnambiguous ambC -> do
con <- fromRightM (sigError __IMPOSSIBLE_VERBOSE__ (typeError $ AbstractConstructorNotInScope c)) $
getOrigConHead c
checkConstructorApplication cmp e t con args
A.Con (AmbQ cs0) -> disambiguateConstructor cs0 t >>= \ case
Left unblock -> postponeTypeCheckingProblem (CheckExpr cmp e t) unblock
Right c -> checkConstructorApplication cmp e t c args
A.PatternSyn n -> do
(ns, p) <- lookupPatternSyn n
p <- return $ setRange (getRange n) $ killRange $ 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' cmp e' t
A.Macro x -> do
TelV tel _ <- telView =<< normalise . defType =<< instantiateDef =<< 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.defaultAppInfo (getRange a)) (A.QuoteTerm A.exprNoRange) . defaultNamedArg) a
mkArg t a | unEl t == tName =
(fmap . fmap)
(A.App (A.defaultAppInfo (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 tel of
NoInsertNeeded -> first (mkArg (snd $ unDom d) arg :) $ makeArgs (tail tel) args
ImpInsert is -> makeArgs (drop (length is) tel) (arg : args)
BadImplicits -> (arg : args, [])
NoSuchName{} -> (arg : args, [])
(macroArgs, otherArgs) = makeArgs argTel args
unq = A.App (A.defaultAppInfo $ fuseRange x args) (A.Unquote A.exprNoRange) . defaultNamedArg
desugared = A.app (unq $ unAppView $ Application (A.Def x) $ macroArgs) otherArgs
checkExpr' cmp 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 <- addContext tel newTypeMeta_
let holeType = telePi_ tel target
(Just vs, EmptyTel) <- mapFst allApplyElims <$> 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" <$>
addContext ("x" :: String, dom) (metaTel args)
_ -> do
v <- checkHeadApplication cmp e t hd args
reportSDoc "tc.term.app" 30 $ vcat
[ "checkApplication: checkHeadApplication returned"
, nest 2 $ "v = " <+> prettyTCM v
]
return v
inferApplication :: ExpandHidden -> A.Expr -> A.Args -> A.Expr -> TCM (Term, Type)
inferApplication exh hd args e | not (defOrVar hd) = do
t <- workOnTypes $ newTypeMeta_
v <- checkExpr' CmpEq e t
return (v, t)
inferApplication exh hd args e = postponeInstanceConstraints $
case unScope hd of
A.Proj o p | isAmbiguous p -> inferProjApp e o (unAmbQ p) args
_ -> do
(f, t0) <- inferHead hd
let r = getRange hd
res <- runExceptT $ checkArgumentsE exh (getRange hd) args t0 Nothing
case res of
Right (_, vs, t1, _) -> (,t1) <$> unfoldInlined (f vs)
Left problem -> do
t <- workOnTypes $ newTypeMeta_
v <- postponeArgs problem exh r args t $ \ _ vs _ _ -> unfoldInlined (f vs)
return (v, t)
inferHeadDef :: ProjOrigin -> QName -> TCM (Elims -> Term, Type)
inferHeadDef o x = do
proj <- isProjection x
let app =
case proj of
Nothing -> \ args -> Def x $ map Apply args
Just p -> \ args -> projDropParsApply p o args
mapFst applyE <$> inferDef app x
inferHead :: A.Expr -> TCM (Elims -> Term, Type)
inferHead e = do
case e of
A.Var x -> do
(u, a) <- getVarInfo x
reportSDoc "tc.term.var" 20 $ hsep
[ "variable" , prettyTCM x
, "(" , text (show u) , ")"
, "has type:" , prettyTCM a
]
unless (usableRelevance a) $
typeError $ VariableIsIrrelevant x
unless (usableQuantity a) $
typeError $ VariableIsErased x
return (applyE u, unDom a)
A.Def x -> inferHeadDef ProjPrefix x
A.Proj o ambP | Just d <- getUnambiguous ambP -> inferHeadDef o d
A.Proj{} -> __IMPOSSIBLE__
A.Con ambC | Just c <- getUnambiguous ambC -> do
con <- fromRightM (sigError __IMPOSSIBLE_VERBOSE__ (typeError $ AbstractConstructorNotInScope c)) $
getOrigConHead c
(u, a) <- inferDef (\ _ -> Con con ConOCon []) c
Constructor{conPars = n} <- theDef <$> (instantiateDef =<< getConstInfo c)
reportSLn "tc.term.con" 7 $ unwords [prettyShow c, "has", show n, "parameters."]
return (applyE u . drop 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 (applyE term, t)
inferDef :: (Args -> Term) -> QName -> TCM (Term, Type)
inferDef mkTerm x =
traceCall (InferDef x) $ do
d <- instantiateDef =<< getConstInfo x
checkRelevance x d
case theDef d of
GeneralizableVar{} -> do
val <- fromMaybe __IMPOSSIBLE__ <$> viewTC (eGeneralizedVars . key x)
sub <- checkpointSubstitution (genvalCheckpoint val)
let (v, t) = applySubst sub (genvalTerm val, genvalType val)
debug [] t v
return (v, t)
_ -> do
vs <- freeVarsToApply x
let t = defType d
v = mkTerm vs
debug vs t v
return (v, t)
where
debug :: Args -> Type -> Term -> TCM ()
debug vs t v = do
reportSDoc "tc.term.def" 60 $
"freeVarsToApply to def " <+> hsep (map (text . show) vs)
reportSDoc "tc.term.def" 10 $ vcat
[ "inferred def " <+> prettyTCM x <+> hsep (map prettyTCM vs)
, nest 2 $ ":" <+> prettyTCM t
, nest 2 $ "-->" <+> prettyTCM v ]
checkRelevance :: QName -> Definition -> TCM ()
checkRelevance x def = maybe (return ()) typeError =<< checkRelevance' x def
checkRelevance' :: QName -> Definition -> TCM (Maybe TypeError)
checkRelevance' x def = do
case defRelevance def of
Relevant -> return Nothing
drel -> do
ifM (return (isJust $ isProjection_ $ theDef def) `and2M`
(not .optIrrelevantProjections <$> pragmaOptions)) needIrrProj $ do
rel <- asksTC envRelevance
reportSDoc "tc.irr" 50 $ vcat
[ "declaration relevance =" <+> text (show drel)
, "context relevance =" <+> text (show rel)
]
return $ if (drel `moreRelevant` rel) then Nothing else Just $ DefinitionIsIrrelevant x
where
needIrrProj = Just . GenericDocError <$> do
sep [ "Projection " , prettyTCM x, " is irrelevant."
, " Turn on option --irrelevant-projections to use it (unsafe)."
]
checkHeadApplication :: Comparison -> A.Expr -> Type -> A.Expr -> [NamedArg A.Expr] -> TCM Term
checkHeadApplication cmp e t hd args = do
sharp <- fmap nameOfSharp <$> coinductionKit
conId <- getNameOfConstrained builtinConId
pOr <- getNameOfConstrained builtinPOr
pComp <- getNameOfConstrained builtinComp
pHComp <- getNameOfConstrained builtinHComp
pTrans <- getNameOfConstrained builtinTrans
mglue <- getNameOfConstrained builtin_glue
case hd of
A.Def c | Just c == sharp -> checkSharpApplication e t c args
A.Def c | Just c == pComp -> defaultResult' $ Just $ checkPrimComp c
A.Def c | Just c == pHComp -> defaultResult' $ Just $ checkPrimHComp c
A.Def c | Just c == pTrans -> defaultResult' $ Just $ checkPrimTrans c
A.Def c | Just c == conId -> defaultResult' $ Just $ checkConId c
A.Def c | Just c == pOr -> defaultResult' $ Just $ checkPOr c
A.Def c | Just c == mglue -> defaultResult' $ Just $ check_glue c
_ -> defaultResult
where
defaultResult :: TCM Term
defaultResult = defaultResult' Nothing
defaultResult' :: Maybe (MaybeRanges -> Args -> Type -> TCM Args) -> TCM Term
defaultResult' mk = do
(f, t0) <- inferHead hd
expandLast <- asksTC envExpandLast
checkArguments expandLast (getRange hd) args t0 t $ \ rs vs t1 checkedTarget -> do
let check = do
k <- mk
as <- allApplyElims vs
pure $ k rs as t1
vs <- case check of
Just ck -> do
map Apply <$> ck
Nothing -> do
return vs
v <- unfoldInlined (f vs)
coerce' cmp checkedTarget v t1 t
traceCallE :: 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
coerce' :: Comparison -> CheckedTarget -> Term -> Type -> Type -> TCM Term
coerce' cmp NotCheckedTarget v inferred expected = coerce cmp v inferred expected
coerce' cmp (CheckedTarget Nothing) v _ _ = return v
coerce' cmp (CheckedTarget (Just pid)) v _ expected = blockTermOnProblem expected v pid
checkArgumentsE :: ExpandHidden -> Range -> [NamedArg A.Expr] -> Type -> Maybe Type ->
ExceptT (MaybeRanges, Elims, [NamedArg A.Expr], Type) TCM (MaybeRanges, Elims, Type, CheckedTarget)
checkArgumentsE = checkArgumentsE' NotCheckedTarget
checkArgumentsE'
:: CheckedTarget
-> ExpandHidden
-> Range
-> [NamedArg A.Expr]
-> Type
-> Maybe Type
-> ExceptT (MaybeRanges, Elims, [NamedArg A.Expr], Type) TCM (MaybeRanges, Elims, Type, CheckedTarget)
checkArgumentsE' chk DontExpandLast _ [] t0 _ = return ([], [], t0, chk)
checkArgumentsE' chk ExpandLast r [] t0 mt1 =
traceCallE (CheckArguments r [] t0 mt1) $ lift $ do
mt1' <- traverse (unEl <.> reduce) mt1
(us, t) <- implicitArgs (-1) (expand mt1') t0
return (replicate (length us) Nothing, map Apply us, t, chk)
where
expand (Just (Pi dom _)) Hidden = not (hidden dom)
expand _ Hidden = True
expand (Just (Pi dom _)) Instance{} = not (isInstance dom)
expand _ Instance{} = True
expand _ NotHidden = False
checkArgumentsE' chk exh r args0@(arg@(Arg info e) : args) t0 mt1 =
traceCallE (CheckArguments r args0 t0 mt1) $ do
lift $ reportSDoc "tc.term.args" 30 $ sep
[ "checkArgumentsE"
, nest 2 $ vcat
[ "e =" <+> prettyA e
, "t0 =" <+> prettyTCM t0
, "t1 =" <+> maybe "Nothing" prettyTCM mt1
]
]
let hx = getHiding info
mx = fmap rangedThing $ nameOf e
expand NotHidden y = False
expand hy y = not (sameHiding hy hx) || maybe False (y /=) mx
reportSDoc "tc.term.args" 30 $ vcat
[ "calling implicitNamedArgs"
, nest 2 $ "t0 = " <+> prettyTCM t0
, nest 2 $ "hx = " <+> text (show hx)
, nest 2 $ "mx = " <+> maybe "nothing" prettyTCM mx
]
(nargs, t) <- lift $ implicitNamedArgs (-1) expand t0
let (mxs, us) = unzip $ map (\ (Arg ai (Named mx u)) -> (mx, Apply $ Arg ai u)) nargs
xs = catMaybes mxs
t <- lift $ forcePiUsingInjectivity t
ifBlockedType t (\ m t -> throwError (replicate (length us) Nothing, us, args0, t)) $ \ _ t0' -> do
let shouldBePi
| visible 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
viewPath <- lift pathView'
chk' <- lift $
case (chk, mt1) of
(NotCheckedTarget, Just t1) | all visible args0 -> do
let n = length args0
TelV tel tgt <- telViewUpTo n t0'
let dep = any (< n) $ IntSet.toList $ freeVars tgt
vis = all visible (telToList tel)
isRigid t | PathType{} <- viewPath t = return False
isRigid (El _ (Pi dom _)) = return $ visible dom
isRigid (El _ (Def d _)) = theDef <$> getConstInfo d >>= return . \ case
Axiom{} -> True
DataOrRecSig{} -> True
AbstractDefn{} -> True
Function{funClauses = cs} -> null cs
Datatype{} -> True
Record{} -> True
Constructor{} -> __IMPOSSIBLE__
GeneralizableVar{} -> __IMPOSSIBLE__
Primitive{} -> False
isRigid _ = return False
rigid <- isRigid tgt
isSizeLt <- reduce t1 >>= isSizeType <&> \case
Just (BoundedLt _) -> True
_ -> False
if | dep -> return chk
| not rigid -> return chk
| not vis -> return chk
| isSizeLt -> return chk
| otherwise -> do
let tgt1 = applySubst (strengthenS __IMPOSSIBLE__ $ size tel) tgt
reportSDoc "tc.term.args.target" 30 $ vcat
[ "Checking target types first"
, nest 2 $ "inferred =" <+> prettyTCM tgt1
, nest 2 $ "expected =" <+> prettyTCM t1 ]
traceCall (CheckTargetType (fuseRange r args0) tgt1 t1) $
CheckedTarget <$> ifNoConstraints_ (leqType tgt1 t1)
(return Nothing) (return . Just)
_ -> return chk
case unEl t0' of
Pi (Dom{domInfo = info', domName = dname, unDom = a}) b
| let name = maybe "_" rangedThing dname,
sameHiding info info'
&& (visible info || maybe True ((name ==) . rangedThing) (nameOf e)) -> do
u <- lift $ applyModalityToContext info' $ do
let e' = e { nameOf = maybe dname Just (nameOf e) }
checkNamedArg (Arg info' e') a
addCheckedArgs us (getRange e) (Apply $ Arg info' u) $
checkArgumentsE' chk' exh (fuseRange r e) args (absApp b u) mt1
| otherwise -> do
reportSDoc "error" 10 $ nest 2 $ vcat
[ text $ "info = " ++ show info
, text $ "info' = " ++ show info'
, text $ "absName b = " ++ absName b
, text $ "nameOf e = " ++ show (nameOf e)
]
wrongPi
_
| visible info
, PathType s _ _ bA x y <- viewPath t0' -> do
lift $ reportSDoc "tc.term.args" 30 $ text $ show bA
u <- lift $ checkExpr (namedThing e) =<< elInf primInterval
addCheckedArgs us (getRange e) (IApply (unArg x) (unArg y) u) $
checkArgumentsE exh (fuseRange r e) args (El s $ unArg bA `apply` [argN u]) mt1
_ -> shouldBePi
where
addCheckedArgs us r u rec = do
(rs, vs, t, chk) <- rec
let rs' = replicate (length us) Nothing ++ Just r : rs
return (rs', us ++ u : vs, t, chk)
`catchError` \ (rs, vs, es, t) -> do
let rs' = replicate (length us) Nothing ++ Just r : rs
throwError (rs', us ++ u : vs, es, t)
checkArguments_
:: ExpandHidden
-> Range
-> [NamedArg A.Expr]
-> Telescope
-> TCM (Elims, Telescope)
checkArguments_ exh r args tel = postponeInstanceConstraints $ do
z <- runExceptT $
checkArgumentsE exh r args (telePi tel __DUMMY_TYPE__) Nothing
case z of
Right (_, args, t, _) -> do
let TelV tel' _ = telView' t
return (args, tel')
Left _ -> __IMPOSSIBLE__
checkArguments ::
ExpandHidden -> Range -> [NamedArg A.Expr] -> Type -> Type ->
(MaybeRanges -> Elims -> Type -> CheckedTarget -> TCM Term) -> TCM Term
checkArguments exph r args t0 t k = postponeInstanceConstraints $ do
z <- runExceptT $ checkArgumentsE exph r args t0 (Just t)
case z of
Right (rs, vs, t1, pid) -> k rs vs t1 pid
Left problem -> postponeArgs problem exph r args t k
postponeArgs :: (MaybeRanges, Elims, [NamedArg A.Expr], Type) -> ExpandHidden -> Range -> [NamedArg A.Expr] -> Type ->
(MaybeRanges -> Elims -> Type -> CheckedTarget -> TCM Term) -> TCM Term
postponeArgs (rs, us, es, t0) exph r args t k = do
reportSDoc "tc.term.expr.args" 80 $
sep [ "postponed checking arguments"
, nest 4 $ prettyList (map (prettyA . namedThing . unArg) args)
, nest 2 $ "against"
, nest 4 $ prettyTCM t0 ] $$
sep [ "progress:"
, nest 2 $ "checked" <+> prettyList (map prettyTCM us)
, nest 2 $ "remaining" <+> sep [ prettyList (map (prettyA . namedThing . unArg) es)
, nest 2 $ ":" <+> prettyTCM t0 ] ]
postponeTypeCheckingProblem_ (CheckArgs exph r es t0 t $ \ rs' vs t pid -> k (rs ++ rs') (us ++ vs) t pid)
checkConstructorApplication :: Comparison -> A.Expr -> Type -> ConHead -> [NamedArg A.Expr] -> TCM Term
checkConstructorApplication cmp org t c args = do
reportSDoc "tc.term.con" 50 $ vcat
[ "entering checkConstructorApplication"
, nest 2 $ vcat
[ "org =" <+> prettyTCM org
, "t =" <+> prettyTCM t
, "c =" <+> prettyTCM c
, "args =" <+> prettyTCM args
] ]
let paramsGiven = checkForParams args
if paramsGiven then fallback else do
reportSDoc "tc.term.con" 50 $ "checkConstructorApplication: no parameters explicitly supplied, continuing..."
cdef <- getConInfo c
let Constructor{conData = d, conPars = npars} = theDef cdef
reportSDoc "tc.term.con" 50 $ nest 2 $ "d =" <+> prettyTCM d
t0 <- reduce (Def d [])
case (t0, unEl t) of
(Def d0 _, Def d' es) -> do
let ~(Just vs) = allApplyElims es
reportSDoc "tc.term.con" 50 $ nest 2 $ "d0 =" <+> prettyTCM d0
reportSDoc "tc.term.con" 50 $ nest 2 $ "d' =" <+> prettyTCM d'
reportSDoc "tc.term.con" 50 $ nest 2 $ "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 = take n $ drop (n' - n) vs
ctype = defType cdef
reportSDoc "tc.term.con" 20 $ vcat
[ "special checking of constructor application of" <+> prettyTCM c
, nest 2 $ vcat [ "ps =" <+> prettyTCM ps
, "ctype =" <+> prettyTCM ctype ] ]
let ctype' = ctype `piApply` ps
reportSDoc "tc.term.con" 20 $ nest 2 $ "ctype' =" <+> prettyTCM ctype'
let TelV ptel _ = telView'UpTo n ctype
let pnames = map (fmap fst) $ telToList ptel
args' = dropArgs pnames args
expandLast <- asksTC envExpandLast
checkArguments expandLast (getRange c) args' ctype' t $ \ rs es t' targetCheck -> do
reportSDoc "tc.term.con" 20 $ nest 2 $ vcat
[ text "es =" <+> prettyTCM es
, text "t' =" <+> prettyTCM t' ]
coerce' cmp targetCheck (Con c ConOCon es) t' t
_ -> do
reportSDoc "tc.term.con" 50 $ nest 2 $ "we are not at a datatype, falling back"
fallback
where
fallback = checkHeadApplication cmp org t (A.Con (unambiguous $ conName c)) args
checkForParams args =
let (hargs, rest) = span (not . visible) args
notUnderscore A.Underscore{} = False
notUnderscore _ = True
in any notUnderscore $ map (unScope . namedArg) hargs
dropArgs [] args = args
dropArgs ps [] = args
dropArgs ps args@(arg : args')
| Just p <- name,
Just ps' <- namedPar p ps = dropArgs ps' args'
| Nothing <- name,
Just ps' <- unnamedPar h ps = dropArgs ps' args'
| otherwise = args
where
name = fmap rangedThing . nameOf $ unArg arg
h = getHiding arg
namedPar x = dropPar ((x ==) . unDom)
unnamedPar h = dropPar (sameHiding h)
dropPar this (p : ps) | this p = Just ps
| otherwise = dropPar this ps
dropPar _ [] = Nothing
disambiguateConstructor :: NonemptyList QName -> Type -> TCM (Either (TCM Bool) ConHead)
disambiguateConstructor cs0 t = do
reportSLn "tc.check.term.con" 40 $ "Ambiguous constructor: " ++ prettyShow cs0
let getData Constructor{conData = d} = d
getData _ = __IMPOSSIBLE__
reportSLn "tc.check.term.con" 40 $ " ranges before: " ++ show (getRange cs0)
(cs, cons) <- unzip . snd . partitionEithers <$> do
forM (toList cs0) $ \ c -> mapRight (c,) <$> getConForm c
reportSLn "tc.check.term.con" 40 $ " reduced: " ++ prettyShow cons
case cons of
[] -> typeError $ AbstractConstructorNotInScope $ headNe cs0
[con] -> do
let c = setConName (fromMaybe __IMPOSSIBLE__ $ headMaybe cs) con
reportSLn "tc.check.term.con" 40 $ " only one non-abstract constructor: " ++ prettyShow c
storeDisambiguatedName $ conName c
return (Right c)
_ -> do
dcs <- zipWithM (\ c con -> (, setConName c con) . getData . theDef <$> getConInfo con) cs cons
let badCon t = typeError $ flip DoesNotConstructAnElementOf t $
fromMaybe __IMPOSSIBLE__ $ headMaybe cs
let getCon :: TCM (Maybe ConHead)
getCon = do
TelV tel t1 <- telView t
addContext tel $ do
reportSDoc "tc.check.term.con" 40 $ nest 2 $
"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.con" 40 $ " decided on: " ++ prettyShow c
storeDisambiguatedName $ conName c
return $ Just c
[] -> badCon $ t' $> Def d []
cs -> typeError $ CantResolveOverloadedConstructorsTargetingSameDatatype d $ map conName cs
getCon >>= \ case
Nothing -> return $ Left $ isJust <$> getCon
Just c -> return $ Right c
inferProjApp :: A.Expr -> ProjOrigin -> NonemptyList QName -> A.Args -> TCM (Term, Type)
inferProjApp e o ds args0 = do
(v, t, _) <- inferOrCheckProjApp e o ds args0 Nothing
return (v, t)
checkProjApp :: Comparison -> A.Expr -> ProjOrigin -> NonemptyList QName -> A.Args -> Type -> TCM Term
checkProjApp cmp e o ds args0 t = do
(v, ti, targetCheck) <- inferOrCheckProjApp e o ds args0 (Just (cmp, t))
coerce' cmp targetCheck v ti t
checkProjAppToKnownPrincipalArg :: Comparison -> A.Expr -> ProjOrigin -> NonemptyList QName -> A.Args -> Type -> Int -> Term -> Type -> TCM Term
checkProjAppToKnownPrincipalArg cmp e o ds args0 t k v0 pt = do
(v, ti, targetCheck) <- inferOrCheckProjAppToKnownPrincipalArg e o ds args0 (Just (cmp, t)) k v0 pt
coerce' cmp targetCheck v ti t
inferOrCheckProjApp
:: A.Expr
-> ProjOrigin
-> NonemptyList QName
-> A.Args
-> Maybe (Comparison, Type)
-> TCM (Term, Type, CheckedTarget)
inferOrCheckProjApp e o ds args mt = do
reportSDoc "tc.proj.amb" 20 $ vcat
[ "checking ambiguous projection"
, text $ " ds = " ++ prettyShow ds
, text " args = " <+> sep (map prettyTCM args)
, text " t = " <+> caseMaybe mt "Nothing" prettyTCM
]
let cmp = caseMaybe mt CmpEq fst
postpone m = do
tc <- caseMaybe mt newTypeMeta_ (return . snd)
v <- postponeTypeCheckingProblem (CheckExpr cmp e tc) $ isInstantiatedMeta m
return (v, tc, NotCheckedTarget)
case filter (visible . snd) $ zip [0..] args of
[] -> caseMaybe mt (refuseProjNotApplied ds) $ \ (cmp , t) -> do
TelV _ptel core <- telViewUpTo' (-1) (not . visible) t
ifBlockedType core (\ m _ -> postpone m) $ \ _ core -> do
ifNotPiType core (\ _ -> refuseProjNotApplied ds) $ \ dom _b -> do
ifBlockedType (unDom dom) (\ m _ -> postpone m) $ \ _ ta -> do
caseMaybeM (isRecordType ta) (refuseProjNotRecordType ds) $ \ (_q, _pars, defn) -> do
case defn of
Record { recFields = fs } -> do
case forMaybe fs $ \ (Arg _ f) -> List.find (f ==) (toList ds) of
[] -> refuseProjNoMatching ds
[d] -> do
storeDisambiguatedName d
(, t, CheckedTarget Nothing) <$>
checkHeadApplication cmp e t (A.Proj o $ unambiguous d) args
_ -> __IMPOSSIBLE__
_ -> __IMPOSSIBLE__
((k, arg) : _) -> do
(v0, ta) <- inferExpr $ namedArg arg
reportSDoc "tc.proj.amb" 25 $ vcat
[ " principal arg " <+> prettyTCM arg
, " has type " <+> prettyTCM ta
]
inferOrCheckProjAppToKnownPrincipalArg e o ds args mt k v0 ta
inferOrCheckProjAppToKnownPrincipalArg ::
A.Expr -> ProjOrigin -> NonemptyList QName -> A.Args -> Maybe (Comparison, Type) ->
Int -> Term -> Type -> TCM (Term, Type, CheckedTarget)
inferOrCheckProjAppToKnownPrincipalArg e o ds args mt k v0 ta = do
let cmp = caseMaybe mt CmpEq fst
postpone m = do
tc <- caseMaybe mt newTypeMeta_ (return . snd)
v <- postponeTypeCheckingProblem (CheckProjAppToKnownPrincipalArg cmp e o ds args tc k v0 ta) $ isInstantiatedMeta m
return (v, tc, NotCheckedTarget)
(vargs, ta) <- implicitArgs (-1) (not . visible) ta
let v = v0 `apply` vargs
ifBlockedType ta (\ m _ -> postpone m) $ \ _ ta -> do
caseMaybeM (isRecordType ta) (refuseProjNotRecordType ds) $ \ (q, _pars0, _) -> do
let try d = do
reportSDoc "tc.proj.amb" 30 $ vcat
[ text $ "trying projection " ++ prettyShow d
, " td = " <+> caseMaybeM (getDefType d ta) "Nothing" prettyTCM
]
def <- lift $ getConstInfo d
let isP = isProjection_ $ theDef def
reportSDoc "tc.proj.amb" 40 $ vcat $
[ text $ " isProjection = " ++ caseMaybe isP "no" (const "yes")
] ++ caseMaybe isP [] (\ Projection{ projProper = proper, projOrig = orig } ->
[ text $ " proper = " ++ show proper
, text $ " orig = " ++ prettyShow orig
])
let orig = caseMaybe isP d projOrig
(dom, u, tb) <- MaybeT (projectTyped v ta o d `catchError` \ _ -> return Nothing)
reportSDoc "tc.proj.amb" 30 $ vcat
[ " dom = " <+> prettyTCM dom
, " u = " <+> prettyTCM u
, " tb = " <+> prettyTCM tb
]
(q', pars, _) <- MaybeT $ isRecordType $ unDom dom
reportSDoc "tc.proj.amb" 30 $ vcat
[ " q = " <+> prettyTCM q
, " q' = " <+> prettyTCM q'
]
guard (q == q')
let tfull = defType def
TelV tel _ <- lift $ telViewUpTo' (-1) (not . visible) tfull
reportSDoc "tc.proj.amb" 30 $ vcat
[ text $ " size tel = " ++ show (size tel)
, text $ " size pars = " ++ show (size pars)
]
guard =<< do isNothing <$> do lift $ checkRelevance' d def
return (orig, (d, (pars, (dom, u, tb))))
cands <- groupOn fst . catMaybes <$> mapM (runMaybeT . try) (toList ds)
case cands of
[] -> refuseProjNoMatching ds
[[]] -> refuseProjNoMatching ds
(_:_:_) -> refuseProj ds $ "several matching candidates found: "
++ prettyShow (map (fst . snd) $ concat cands)
[ (_orig, (d, (pars, (_dom,u,tb)))) : _ ] -> do
storeDisambiguatedName d
tfull <- typeOfConst d
(_,_) <- checkKnownArguments (take k args) pars tfull
let r = getRange e
args' = drop (k + 1) args
z <- runExceptT $ checkArgumentsE ExpandLast r args' tb (snd <$> mt)
case z of
Right (rs, us, trest, targetCheck) -> return (u `applyE` us, trest, targetCheck)
Left problem -> do
tc <- caseMaybe mt newTypeMeta_ (return . snd)
v <- postponeArgs problem ExpandLast r args' tc $ \ rs us trest targetCheck ->
coerce' cmp targetCheck (u `applyE` us) trest tc
return (v, tc, NotCheckedTarget)
refuseProj :: NonemptyList QName -> String -> TCM a
refuseProj ds reason = typeError $ GenericError $
"Cannot resolve overloaded projection "
++ prettyShow (A.nameConcrete $ A.qnameName $ headNe ds)
++ " because " ++ reason
refuseProjNotApplied, refuseProjNoMatching, refuseProjNotRecordType :: NonemptyList QName -> TCM a
refuseProjNotApplied ds = refuseProj ds "it is not applied to a visible argument"
refuseProjNoMatching ds = refuseProj ds "no matching candidate found"
refuseProjNotRecordType ds = refuseProj ds "principal argument is not of record type"
checkSharpApplication :: A.Expr -> Type -> QName -> [NamedArg A.Expr] -> TCM Term
checkSharpApplication e t c args = do
arg <- case args of
[a] | visible a -> return $ namedArg a
_ -> typeError $ GenericError $ prettyShow c ++ " must be applied to exactly one argument."
i <- fresh :: TCM Int
let name = filter (/= '_') (prettyShow $ 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 <- asksTC envRelevance
abs <- aModeToDef <$> asksTC envAbstractMode
let info = A.mkDefInfo (A.nameConcrete $ A.qnameName c') noFixity'
PublicAccess abs noRange
core = A.LHSProj { A.lhsDestructor = unambiguous flat
, A.lhsFocus = defaultNamedArg $ A.LHSHead c' []
, A.lhsPats = [] }
clause = A.Clause (A.LHS empty core) []
(A.RHS arg Nothing)
A.noWhereDecls 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 $
[ "The coinductive wrapper"
, nest 2 $ prettyTCM rel <> prettyTCM c' <+> ":"
, nest 4 $ prettyTCM t
, nest 2 $ prettyA clause
, "The definition is" <+> text (show $ funDelayed def) <>
"."
]
return c'
e' <- Def wrapper . map Apply <$> getContextArgs
reportSDoc "tc.term.expr.coind" 15 $ vcat $
[ "The coinductive constructor application"
, nest 2 $ prettyTCM e
, "was translated into the application"
, nest 2 $ prettyTCM e'
]
blockTerm t $ e' <$ workOnTypes (leqType forcedType t)
pathAbs :: PathView -> Abs Term -> TCM Term
pathAbs (OType _) t = __IMPOSSIBLE__
pathAbs (PathType s path l a x y) t = do
return $ Lam defaultArgInfo t
checkPrimComp :: QName -> MaybeRanges -> Args -> Type -> TCM Args
checkPrimComp c rs vs _ = do
case vs of
l : a : phi : u : a0 : rest -> do
iz <- Arg defaultArgInfo <$> intervalUnview IZero
let lz = unArg l `apply` [iz]
az = unArg a `apply` [iz]
ty <- elInf $ primPartial <#> (pure $ unArg l `apply` [iz]) <@> (pure $ unArg phi) <@> (pure $ unArg a `apply` [iz])
bAz <- el' (pure $ lz) (pure $ az)
a0 <- blockArg bAz (rs !!! 4) a0 $ do
equalTerm ty
(Lam defaultArgInfo $ NoAbs "_" $ unArg a0)
(apply (unArg u) [iz])
return $ l : a : phi : u : a0 : rest
_ -> typeError $ GenericError $ show c ++ " must be fully applied"
checkPrimHComp :: QName -> MaybeRanges -> Args -> Type -> TCM Args
checkPrimHComp c rs vs _ = do
case vs of
l : a : phi : u : a0 : rest -> do
iz <- Arg defaultArgInfo <$> intervalUnview IZero
ty <- elInf $ primPartial <#> (pure $ unArg l) <@> (pure $ unArg phi) <@> (pure $ unArg a)
bA <- el' (pure $ unArg l) (pure $ unArg a)
a0 <- blockArg bA (rs !!! 4) a0 $ do
equalTerm ty
(Lam defaultArgInfo $ NoAbs "_" $ unArg a0)
(apply (unArg u) [iz])
return $ l : a : phi : u : a0 : rest
_ -> typeError $ GenericError $ show c ++ " must be fully applied"
checkPrimTrans :: QName -> MaybeRanges -> Args -> Type -> TCM Args
checkPrimTrans c rs vs _ = do
case vs of
l : a : phi : rest -> do
iz <- Arg defaultArgInfo <$> intervalUnview IZero
ty <- runNamesT [] $ do
l <- open $ unArg l
nPi' "i" (elInf $ cl primInterval) $ \ i -> (sort . tmSort <$> (l <@> i))
a <- blockArg ty (rs !!! 1) a $ do
equalTermOnFace (unArg phi) ty
(unArg a)
(Lam defaultArgInfo $ NoAbs "_" $ apply (unArg a) [iz])
return $ l : a : phi : rest
_ -> typeError $ GenericError $ show c ++ " must be fully applied"
blockArg :: HasRange r => Type -> r -> Arg Term -> TCM () -> TCM (Arg Term)
blockArg t r a m =
setCurrentRange (getRange $ r) $ fmap (a $>) $ blockTerm t $ m >> return (unArg a)
checkConId :: QName -> MaybeRanges -> Args -> Type -> TCM Args
checkConId c rs vs t1 = do
case vs of
args@[_, _, _, _, phi, p] -> do
iv@(PathType s _ l a x y) <- idViewAsPath t1
let ty = pathUnview iv
const_x <- blockTerm ty $ do
equalTermOnFace (unArg phi) (El s (unArg a)) (unArg x) (unArg y)
pathAbs iv (NoAbs (stringToArgName "_") (unArg x))
p <- blockArg ty (rs !!! 5) p $ do
equalTermOnFace (unArg phi) ty (unArg p) const_x
return $ init args ++ [p]
_ -> typeError $ GenericError $ show c ++ " must be fully applied"
checkPOr :: QName -> MaybeRanges -> Args -> Type -> TCM Args
checkPOr c rs vs _ = do
case vs of
l : phi1 : phi2 : a : u : v : rest -> do
phi <- intervalUnview (IMin phi1 phi2)
reportSDoc "tc.term.por" 10 $ text (show phi)
t1 <- runNamesT [] $ do
[l,a] <- mapM (open . unArg) [l,a]
psi <- open =<< intervalUnview (IMax phi1 phi2)
pPi' "o" psi $ \ o -> el' l (a <..> o)
tv <- runNamesT [] $ do
[l,a,phi1,phi2] <- mapM (open . unArg) [l,a,phi1,phi2]
pPi' "o" phi2 $ \ o -> el' l (a <..> (cl primIsOne2 <@> phi1 <@> phi2 <@> o))
v <- blockArg tv (rs !!! 5) v $ do
equalTermOnFace phi t1 (unArg u) (unArg v)
return $ l : phi1 : phi2 : a : u : v : rest
_ -> typeError $ GenericError $ show c ++ " must be fully applied"
check_glue :: QName -> MaybeRanges -> Args -> Type -> TCM Args
check_glue c rs vs _ = do
case vs of
la : lb : bA : phi : bT : e : t : a : rest -> do
let iinfo = setRelevance Irrelevant defaultArgInfo
v <- runNamesT [] $ do
[lb, la, bA, phi, bT, e, t] <- mapM (open . unArg) [lb, la, bA, phi, bT, e, t]
let f o = cl primEquivFun <#> lb <#> la <#> (bT <..> o) <#> bA <@> (e <..> o)
glam iinfo "o" $ \ o -> f o <@> (t <..> o)
ty <- runNamesT [] $ do
[lb, phi, bA] <- mapM (open . unArg) [lb, phi, bA]
elInf $ cl primPartialP <#> lb <@> phi <@> (glam iinfo "o" $ \ _ -> bA)
let a' = Lam iinfo (NoAbs "o" $ unArg a)
ta <- el' (pure $ unArg la) (pure $ unArg bA)
a <- blockArg ta (rs !!! 7) a $ equalTerm ty a' v
return $ la : lb : bA : phi : bT : e : t : a : rest
_ -> typeError $ GenericError $ show c ++ " must be fully applied"