{-# LANGUAGE CPP #-}
module Agda.TypeChecking.CheckInternal
( checkType
, checkType'
, checkSort
, checkInternal
, checkInternal'
, Action(..), defaultAction, eraseUnusedAction
, infer
, inferSort
, shouldBeSort
) where
import Control.Arrow ((&&&), (***), first, second)
import Control.Monad
import Agda.Syntax.Common
import Agda.Syntax.Internal
import Agda.TypeChecking.Conversion
import Agda.TypeChecking.Datatypes
import Agda.TypeChecking.Level
import Agda.TypeChecking.Monad
import Agda.TypeChecking.Monad.Builtin
import Agda.TypeChecking.Pretty
import Agda.TypeChecking.Primitive
import Agda.TypeChecking.ProjectionLike (elimView)
import Agda.TypeChecking.Records (getDefType)
import Agda.TypeChecking.Reduce
import Agda.TypeChecking.Substitute
import Agda.TypeChecking.Sort
import Agda.TypeChecking.Telescope
import Agda.Utils.Functor (($>))
import Agda.Utils.Monad
import Agda.Utils.Size
#include "undefined.h"
import Agda.Utils.Impossible
checkType :: Type -> TCM ()
checkType t = void $ checkType' t
checkType' :: Type -> TCM Sort
checkType' t = do
reportSDoc "tc.check.internal" 20 $ sep
[ "checking internal type "
, prettyTCM t
]
v <- elimView True $ unEl t
case v of
Pi a b -> do
s1 <- checkType' $ unDom a
s2 <- (b $>) <$> do
let goInside = case b of Abs{} -> addContext (absName b, a)
NoAbs{} -> id
goInside $ checkType' $ unAbs b
inferPiSort s1 s2
Sort s -> do
_ <- checkSort defaultAction s
inferUnivSort s
Var i es -> do
a <- typeOfBV i
checkTypeSpine a (Var i []) es
Def f es -> do
a <- defType <$> getConstInfo f
checkTypeSpine a (Def f []) es
MetaV x es -> do
a <- metaType x
checkTypeSpine a (MetaV x []) es
v@Lam{} -> typeError $ InvalidType v
v@Con{} -> typeError $ InvalidType v
v@Lit{} -> typeError $ InvalidType v
v@Level{} -> typeError $ InvalidType v
DontCare v -> checkType' $ t $> v
Dummy s -> __IMPOSSIBLE_VERBOSE__ s
checkTypeSpine :: Type -> Term -> Elims -> TCM Sort
checkTypeSpine a self es = shouldBeSort =<< do snd <$> inferSpine a self es
data Action = Action
{ preAction :: Type -> Term -> TCM Term
, postAction :: Type -> Term -> TCM Term
, relevanceAction :: Relevance -> Relevance -> Relevance
}
defaultAction :: Action
defaultAction = Action
{ preAction = \ _ -> return
, postAction = \ _ -> return
, relevanceAction = \ _ -> id
}
eraseUnusedAction :: Action
eraseUnusedAction = defaultAction { postAction = eraseUnused }
where
eraseUnused :: Type -> Term -> TCM Term
eraseUnused t v = case v of
Def f es -> do
pols <- getPolarity f
return $ Def f $ eraseIfNonvariant pols es
_ -> return v
eraseIfNonvariant :: [Polarity] -> Elims -> Elims
eraseIfNonvariant [] es = es
eraseIfNonvariant pols [] = []
eraseIfNonvariant (Nonvariant : pols) (e : es) = (fmap DontCare e) : eraseIfNonvariant pols es
eraseIfNonvariant (_ : pols) (e : es) = e : eraseIfNonvariant pols es
checkInternal :: Term -> Type -> TCM ()
checkInternal v t = void $ checkInternal' defaultAction v t
checkInternal' :: Action -> Term -> Type -> TCM Term
checkInternal' action v t = do
reportSDoc "tc.check.internal" 20 $ sep
[ "checking internal "
, nest 2 $ sep [ prettyTCM v <+> ":"
, nest 2 $ prettyTCM t ] ]
v <- elimView True =<< preAction action t v
postAction action t =<< case v of
Var i es -> do
a <- typeOfBV i
checkSpine action a (Var i []) es t
Def f es -> do
a <- defType <$> getConstInfo f
checkSpine action a (Def f []) es t
MetaV x es -> do
a <- metaType x
checkSpine action a (MetaV x []) es t
Con c ci vs -> do
fullyApplyCon c vs t $ \ _d _dt _pars a vs' tel t -> do
Con c ci vs2 <- checkSpine action a (Con c ci []) vs' t
return $ applySubst (strengthenS __IMPOSSIBLE__ (size tel))
$ Con c ci $ take (length vs) vs2
Lit l -> Lit l <$ ((`subtype` t) =<< litType l)
Lam ai vb -> do
(a, b) <- maybe (shouldBePi t) return =<< isPath t
ai <- checkArgInfo action ai $ domInfo a
addContext (suggest vb b, a) $ do
Lam ai . Abs (absName vb) <$> checkInternal' action (absBody vb) (absBody b)
Pi a b -> do
s <- shouldBeSort t
when (s == SizeUniv) $ typeError $ FunctionTypeInSizeUniv v
let st = sort s
sa = getSort a
sb = getSort (unAbs b)
mkDom v = El sa v <$ a
mkRng v = fmap (v <$) b
goInside = case b of Abs{} -> addContext (absName b, a)
NoAbs{} -> id
a <- mkDom <$> checkInternal' action (unEl $ unDom a) (sort sa)
goInside $ Pi a . mkRng <$> checkInternal' action (unEl $ unAbs b) (sort sb)
Sort s -> do
s <- checkSort action s
Sort s <$ ((sortFitsIn s) =<< shouldBeSort t)
Level l -> do
l <- checkLevel action l
Level l <$ ((`subtype` t) =<< levelType)
DontCare v -> DontCare <$> checkInternal' action v t
Dummy s -> __IMPOSSIBLE_VERBOSE__ s
fullyApplyCon
:: ConHead
-> Elims
-> Type
-> (QName -> Type -> Args -> Type -> Elims -> Telescope -> Type -> TCM a)
-> TCM a
fullyApplyCon c vs t0 ret = do
TelV tel t <- telView t0
addContext tel $ do
getFullyAppliedConType c t >>= \case
Nothing ->
typeError $ DoesNotConstructAnElementOf (conName c) t
Just ((d, dt, pars), a) ->
ret d dt pars a (raise (size tel) vs ++ map Apply (teleArgs tel)) tel t
checkSpine
:: Action
-> Type
-> Term
-> Elims
-> Type
-> TCM Term
checkSpine action a self es t = do
reportSDoc "tc.check.internal" 20 $ sep
[ "checking spine "
, nest 2 $ sep [ parens (sep [ prettyTCM self <+> ":"
, nest 2 $ prettyTCM a ])
, nest 4 $ prettyTCM es <+> ":"
, nest 2 $ prettyTCM t ] ]
((v, v'), t') <- inferSpine' action a self self es
t' <- reduce t'
v' <$ coerceSize subtype v t' t
checkArgs
:: Action
-> Type
-> Term
-> Args
-> Type
-> TCM Term
checkArgs action a self vs t = checkSpine action a self (map Apply vs) t
checkArgInfo :: Action -> ArgInfo -> ArgInfo -> TCM ArgInfo
checkArgInfo action ai ai' = do
checkHiding (getHiding ai) (getHiding ai')
r <- checkRelevance action (getRelevance ai) (getRelevance ai')
return $ setRelevance r ai
checkHiding :: Hiding -> Hiding -> TCM ()
checkHiding h h' = unless (sameHiding h h') $ typeError $ HidingMismatch h h'
checkRelevance :: Action -> Relevance -> Relevance -> TCM Relevance
checkRelevance action r r' = do
unless (r == r') $ typeError $ RelevanceMismatch r r'
return $ relevanceAction action r' r
infer :: Term -> TCM Type
infer v = do
case v of
Var i es -> do
a <- typeOfBV i
snd <$> inferSpine a (Var i []) es
Def f (Apply a : es) -> inferDef' f a es
Def f es -> inferDef f es
MetaV x es -> do
a <- metaType x
snd <$> inferSpine a (MetaV x []) es
_ -> __IMPOSSIBLE__
inferDef :: QName -> Elims -> TCM Type
inferDef f es = do
a <- defType <$> getConstInfo f
snd <$> inferSpine a (Def f []) es
inferDef' :: QName -> Arg Term -> Elims -> TCM Type
inferDef' f a es = do
isProj <- isProjection f
case isProj of
Just Projection{ projIndex = n } | n > 0 -> do
let self = unArg a
b <- infer self
snd <$> inferSpine b self (Proj ProjSystem f : es)
_ -> inferDef f (Apply a : es)
inferSpine :: Type -> Term -> Elims -> TCM (Term, Type)
inferSpine a v es = first fst <$> inferSpine' defaultAction a v v es
inferSpine' :: Action -> Type -> Term -> Term -> Elims -> TCM ((Term, Term), Type)
inferSpine' action t self self' [] = return ((self, self'), t)
inferSpine' action t self self' (e : es) = do
reportSDoc "tc.infer.internal" 30 $ sep
[ "inferSpine': "
, "type t = " <+> prettyTCM t
, "self = " <+> prettyTCM self
, "self' = " <+> prettyTCM self'
, "eliminated by e = " <+> prettyTCM e
]
case e of
IApply x y r -> do
(a, b) <- shouldBePath t
r' <- checkInternal' action r (unDom a)
izero <- primIZero
ione <- primIOne
x' <- checkInternal' action x (b `absApp` izero)
y' <- checkInternal' action y (b `absApp` ione)
inferSpine' action (b `absApp` r) (self `applyE` [e]) (self' `applyE` [IApply x' y' r']) es
Apply (Arg ai v) -> do
(a, b) <- shouldBePi t
ai <- checkArgInfo action ai $ domInfo a
v' <- checkInternal' action v $ unDom a
inferSpine' action (b `absApp` v) (self `applyE` [e]) (self' `applyE` [Apply (Arg ai v')]) es
Proj o f -> do
(a, b) <- shouldBePi =<< shouldBeProjectible t f
u <- applyDef o f (argFromDom a $> self)
u' <- applyDef o f (argFromDom a $> self')
inferSpine' action (b `absApp` self) u u' es
shouldBeProjectible :: Type -> QName -> TCM Type
shouldBeProjectible t f = maybe failure return =<< getDefType f =<< reduce t
where failure = typeError $ ShouldBeRecordType t
shouldBePath :: Type -> TCM (Dom Type, Abs Type)
shouldBePath t = do
m <- isPath t
case m of
Just p -> return p
Nothing -> typeError $ ShouldBePath t
shouldBePi :: Type -> TCM (Dom Type, Abs Type)
shouldBePi t = ifPiType t (\ a b -> return (a, b)) $ const $ typeError $ ShouldBePi t
shouldBeSort :: Type -> TCM Sort
shouldBeSort t = ifIsSort t return (typeError $ ShouldBeASort t)
ifIsSort :: Type -> (Sort -> TCM a) -> TCM a -> TCM a
ifIsSort t yes no = do
t <- reduce t
case unEl t of
Sort s -> yes s
_ -> no
checkSort :: Action -> Sort -> TCM Sort
checkSort action s =
case s of
Type l -> Type <$> checkLevel action l
Prop l -> Prop <$> checkLevel action l
Inf -> return Inf
SizeUniv -> return SizeUniv
PiSort a b -> do
a <- checkSort action a
addContext (absName b, defaultDom (sort a) :: Dom Type) $ do
PiSort a . Abs (absName b) <$> checkSort action (absBody b)
UnivSort s -> UnivSort <$> checkSort action s
MetaS x es -> do
a <- metaType x
let self = Sort $ MetaS x []
((_,v),_) <- inferSpine' action a self self es
case v of
Sort s -> return s
MetaV x es -> return $ MetaS x es
Def d es -> return $ DefS d es
_ -> __IMPOSSIBLE__
DefS d es -> do
a <- defType <$> getConstInfo d
let self = Sort $ DefS d []
((_,v),_) <- inferSpine' action a self self es
case v of
Sort s -> return s
MetaV x es -> return $ MetaS x es
Def d es -> return $ DefS d es
_ -> __IMPOSSIBLE__
DummyS s -> __IMPOSSIBLE_VERBOSE__ s
checkLevel :: Action -> Level -> TCM Level
checkLevel action (Max ls) = Max <$> mapM checkPlusLevel ls
where
checkPlusLevel l@ClosedLevel{} = return l
checkPlusLevel (Plus k l) = Plus k <$> checkLevelAtom l
checkLevelAtom l = do
lvl <- levelType
UnreducedLevel <$> case l of
MetaLevel x es -> checkInternal' action (MetaV x es) lvl
BlockedLevel _ v -> checkInternal' action v lvl
NeutralLevel _ v -> checkInternal' action v lvl
UnreducedLevel v -> checkInternal' action v lvl
metaType :: MetaId -> TCM Type
metaType x = jMetaType . mvJudgement <$> lookupMeta x
subtype :: Type -> Type -> TCM ()
subtype t1 t2 = do
ifIsSort t1 (\ s1 -> (s1 `leqSort`) =<< shouldBeSort t2) $ do
dontAssignMetas $ leqType t1 t2
inferSort :: Term -> TCM Sort
inferSort t = case t of
Var i es -> do
a <- typeOfBV i
(_, s) <- eliminate (Var i []) a es
shouldBeSort s
Def f es -> do
a <- defType <$> getConstInfo f
(_, s) <- eliminate (Def f []) a es
shouldBeSort s
MetaV x es -> do
a <- metaType x
(_, s) <- eliminate (MetaV x []) a es
shouldBeSort s
Pi a b -> inferPiSort (getSort a) (getSort <$> b)
Sort s -> inferUnivSort s
Con{} -> __IMPOSSIBLE__
Lit{} -> __IMPOSSIBLE__
Lam{} -> __IMPOSSIBLE__
Level{} -> __IMPOSSIBLE__
DontCare{} -> __IMPOSSIBLE__
Dummy s -> __IMPOSSIBLE_VERBOSE__ s
eliminate :: Term -> Type -> Elims -> TCM (Term, Type)
eliminate self t [] = return (self, t)
eliminate self t (e : es) = case e of
Apply (Arg _ v) -> ifNotPiType t __IMPOSSIBLE__ $ \ _ b ->
eliminate (self `applyE` [e]) (b `absApp` v) es
IApply _ _ v -> do
(_, b) <- shouldBePath t
eliminate (self `applyE` [e]) (b `absApp` v) es
Proj o f -> do
(Dom{domInfo = ai}, b) <- shouldBePi =<< shouldBeProjectible t f
u <- applyDef o f $ Arg ai self
eliminate u (b `absApp` self) es