module Agda.TypeChecking.CheckInternal
( checkType
, checkInternal
) where
import Control.Monad
import Agda.Syntax.Common
import Agda.Syntax.Internal as I
import Agda.TypeChecking.Conversion
import Agda.TypeChecking.Datatypes (getConType)
import Agda.TypeChecking.Level
import Agda.TypeChecking.Monad
import Agda.TypeChecking.Monad.Builtin
import Agda.TypeChecking.Pretty
import Agda.TypeChecking.ProjectionLike (elimView)
import Agda.TypeChecking.Reduce
import Agda.TypeChecking.Substitute
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
[ text "checking internal type "
, prettyTCM t
]
v <- elimView True $ unEl t
case ignoreSharing v of
Pi a b -> do
s1 <- checkType' $ unDom a
s2 <- (b $>) <$> do
addContext (absName b, a) $ do
checkType' $ absBody b
return $ dLub s1 s2
Sort s -> do
checkSort s
return $ sSuc 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
ExtLam{} -> __IMPOSSIBLE__
Shared{} -> __IMPOSSIBLE__
checkTypeSpine :: Type -> Term -> Elims -> TCM Sort
checkTypeSpine a self es = shouldBeSort =<< inferSpine a self es
checkInternal :: Term -> Type -> TCM ()
checkInternal v t = do
reportSDoc "tc.check.internal" 20 $ sep
[ text "checking internal "
, prettyTCM v
, text " : "
, prettyTCM t
]
v <- elimView True v
case ignoreSharing v of
Var i es -> do
a <- typeOfBV i
checkSpine a (Var i []) es t
Def f es -> do
a <- defType <$> getConstInfo f
checkSpine a (Def f []) es t
MetaV x es -> do
a <- metaType x
checkSpine a (MetaV x []) es t
Con c vs -> do
TelV tel t <- telView t
addCtxTel tel $ do
let failure = typeError $ DoesNotConstructAnElementOf (conName c) t
vs' = raise (size tel) vs ++ teleArgs tel
a <- maybe failure return =<< getConType c t
checkArgs a (Con c []) vs' t
Lit l -> litType l >>= (`subtype` t)
Lam ai vb -> do
(a, b) <- shouldBePi t
checkArgInfo ai $ domInfo a
addContext (suggest vb b, a) $ do
checkInternal (absBody vb) (absBody b)
Pi a b -> do
s <- shouldBeSort t
when (s == SizeUniv) $ typeError $ FunctionTypeInSizeUniv v
let st = sort s
checkInternal (unEl $ unDom a) st
addContext (absName b, a) $ do
checkInternal (unEl $ absBody b) $ raise 1 st
Sort s -> do
checkSort s
(sSuc s `leqSort`) =<< shouldBeSort t
Level l -> do
checkLevel l
levelType >>= (`subtype` t)
DontCare v -> checkInternal v t
Shared{} -> __IMPOSSIBLE__
ExtLam{} -> __IMPOSSIBLE__
checkSpine :: Type -> Term -> Elims -> Type -> TCM ()
checkSpine a self es t = do
reportSDoc "tc.check.internal" 20 $ sep
[ text "checking spine "
, text "("
, prettyTCM self
, text " : "
, prettyTCM a
, text ")"
, prettyTCM es
, text " : "
, prettyTCM t
]
inferSpine a self es >>= (`subtype` t)
checkArgs :: Type -> Term -> Args -> Type -> TCM ()
checkArgs a self vs t = checkSpine a self (map Apply vs) t
checkArgInfo :: I.ArgInfo -> I.ArgInfo -> TCM ()
checkArgInfo ai ai' = do
checkHiding (getHiding ai) (getHiding ai')
checkRelevance (getRelevance ai) (getRelevance ai')
checkColor (argInfoColors ai) (argInfoColors ai')
checkHiding :: Hiding -> Hiding -> TCM ()
checkHiding h h' = unless (h == h') $ typeError $ HidingMismatch h h'
checkRelevance :: Relevance -> Relevance -> TCM ()
checkRelevance r0 r0' = unless (r == r') $ typeError $ RelevanceMismatch r r'
where
r = canon r0
r' = canon r0'
canon Forced{} = Relevant
canon UnusedArg = Relevant
canon r = r
checkColor :: [Color] -> [Color] -> TCM ()
checkColor c c' = unless (c == c') $ typeError $ ColorMismatch c c'
inferSpine :: Type -> Term -> Elims -> TCM Type
inferSpine t self [] = return t
inferSpine t self (e : es) =
case e of
Apply (Arg ai v) -> do
(a, b) <- shouldBePi t
checkArgInfo ai $ domInfo a
checkInternal v $ unDom a
inferSpine (b `absApp` v) (self `applyE` [e]) es
Proj f -> do
(a, b) <- shouldBePi =<< shouldBeProjectible t f
u <- f `applyDef` (argFromDom a $> self)
inferSpine (b `absApp` self) u es
shouldBeProjectible :: Type -> QName -> TCM Type
shouldBeProjectible t f = maybe failure return =<< getDefType f =<< reduce t
where failure = typeError $ ShouldBeRecordType t
shouldBePi :: Type -> TCM (I.Dom Type, Abs Type)
shouldBePi t = do
t <- reduce t
case ignoreSharing $ unEl t of
Pi a b -> return (a, b)
_ -> 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 ignoreSharing $ unEl t of
Sort s -> yes s
_ -> no
checkSort :: Sort -> TCM ()
checkSort s =
case s of
Type l -> checkLevel l
Prop -> __IMPOSSIBLE__
Inf -> typeError $ SetOmegaNotValidType
SizeUniv -> typeError $ InvalidTypeSort s
DLub a b -> do
checkSort a
addContext (absName b, defaultDom (sort a) :: I.Dom Type) $ do
checkSort (absBody b)
checkLevel :: Level -> TCM ()
checkLevel (Max ls) = mapM_ checkPlusLevel ls
where
checkPlusLevel ClosedLevel{} = return ()
checkPlusLevel (Plus _ l) = checkLevelAtom l
checkLevelAtom l = do
lvl <- levelType
case l of
MetaLevel x es -> checkInternal (MetaV x es) lvl
BlockedLevel _ v -> checkInternal v lvl
NeutralLevel _ v -> checkInternal v lvl
UnreducedLevel v -> checkInternal 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) $
leqType t1 t2