summaryrefslogtreecommitdiff
path: root/src/full/Agda/TypeChecking/CheckInternal.hs
diff options
context:
space:
mode:
Diffstat (limited to 'src/full/Agda/TypeChecking/CheckInternal.hs')
-rw-r--r--src/full/Agda/TypeChecking/CheckInternal.hs51
1 files changed, 28 insertions, 23 deletions
diff --git a/src/full/Agda/TypeChecking/CheckInternal.hs b/src/full/Agda/TypeChecking/CheckInternal.hs
index eedb07a..1563d98 100644
--- a/src/full/Agda/TypeChecking/CheckInternal.hs
+++ b/src/full/Agda/TypeChecking/CheckInternal.hs
@@ -1,6 +1,5 @@
-{-# LANGUAGE CPP #-}
-{-# LANGUAGE FlexibleInstances #-}
-{-# LANGUAGE TypeSynonymInstances #-}
+{-# LANGUAGE CPP #-}
+{-# LANGUAGE FlexibleInstances #-}
-- Initially authored by Andreas, 2013-10-22.
@@ -38,28 +37,31 @@ import Agda.Utils.Size
#include "undefined.h"
import Agda.Utils.Impossible
+-- -- | Entry point for e.g. checking WithFunctionType.
+-- checkType :: Type -> TCM ()
+-- checkType t = -- dontAssignMetas $ ignoreSorts $
+-- checkInternal (unEl t) (sort Inf)
+
-- | Entry point for e.g. checking WithFunctionType.
checkType :: Type -> TCM ()
-checkType t = -- dontAssignMetas $ ignoreSorts $
- checkInternal (unEl t) (sort Inf)
+checkType t = void $ checkType' t
-{- Alternative algorithm (does not buy us much)
+-- | Check a type and infer its sort.
+--
+-- Necessary because of PTS rule @(SizeUniv, Set i, Set i)@
+-- but @SizeUniv@ is not included in any @Set i@.
--
-- This algorithm follows
--- Abel, Coquand, Dybjer, MPC 08
+-- Abel, Coquand, Dybjer, MPC 08,
-- Verifying a Semantic βη-Conversion Test for Martin-Löf Type Theory
-
-checkType :: Type -> TCM ()
-checkType t = void $ checkType' t
-
--- | Check a type and infer its sort.
+--
checkType' :: Type -> TCM Sort
checkType' t = do
reportSDoc "tc.check.internal" 20 $ sep
[ text "checking internal type "
, prettyTCM t
]
- v <- elimView $ unEl t -- bring projection-like funs in post-fix form
+ v <- elimView True $ unEl t -- bring projection-like funs in post-fix form
case ignoreSharing v of
Pi a b -> do
s1 <- checkType' $ unDom a
@@ -84,11 +86,11 @@ checkType' t = do
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
--}
-- | Entry point for term checking.
checkInternal :: Term -> Type -> TCM ()
@@ -105,7 +107,7 @@ checkInternal v t = do
case ignoreSharing v of
Var i es -> do
a <- typeOfBV i
- checkSpine a (Var i []) es t
+ checkSpine a (Var i []) es t
Def f es -> do -- f is not projection(-like)!
a <- defType <$> getConstInfo f
checkSpine a (Def f []) es t
@@ -128,8 +130,9 @@ checkInternal v t = 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
+ checkInternal (unEl $ unDom a) st -- This does not work with SizeUniv
addContext (absName b, a) $ do
checkInternal (unEl $ absBody b) $ raise 1 st
Sort s -> do
@@ -169,11 +172,11 @@ checkDef' :: QName -> I.Arg Term -> Elims -> Type -> TCM ()
checkDef' f a es t = do
isProj <- isProjection f
case isProj of
- Nothing -> checkDef f (Apply a : es) t
- Just Projection{} -> do
+ Just Projection{ projIndex = n} | n > 0 -> do
let self = unArg a
b <- infer self
checkSpine b self (Proj f : es) t
+ _ -> checkDef f (Apply a : es) t
-}
checkSpine :: Type -> Term -> Elims -> Type -> TCM ()
@@ -209,7 +212,7 @@ checkRelevance r0 r0' = unless (r == r') $ typeError $ RelevanceMismatch r r'
where
r = canon r0
r' = canon r0'
- canon Forced = Relevant
+ canon Forced{} = Relevant
canon UnusedArg = Relevant
canon r = r
@@ -245,11 +248,11 @@ inferDef' :: QName -> I.Arg Term -> Elims -> TCM Type
inferDef' f a es = do
isProj <- isProjection f
case isProj of
- Nothing -> inferDef f (Apply a : es)
- Just Projection{} -> do
+ Just Projection{ projIndex = n } | n > 0 -> do
let self = unArg a
b <- infer self
inferSpine b self (Proj f : es)
+ _ -> inferDef f (Apply a : es)
-}
-- | @inferSpine t self es@ checks that spine @es@ eliminates
@@ -285,6 +288,7 @@ shouldBePi t = do
Pi a b -> return (a, b)
_ -> typeError $ ShouldBePi t
+-- | Result is in reduced form.
shouldBeSort :: Type -> TCM Sort
shouldBeSort t = ifIsSort t return (typeError $ ShouldBeASort t)
@@ -304,6 +308,7 @@ checkSort s =
-- the dummy Prop should not be part of a term we check
Inf -> typeError $ SetOmegaNotValidType
-- we cannot have Setω on the lhs of the colon
+ SizeUniv -> typeError $ InvalidTypeSort s
DLub a b -> do
checkSort a
addContext (absName b, defaultDom (sort a) :: I.Dom Type) $ do
@@ -320,8 +325,8 @@ checkLevel (Max ls) = mapM_ checkPlusLevel ls
lvl <- levelType
case l of
MetaLevel x es -> checkInternal (MetaV x es) lvl
- BlockedLevel x v -> checkInternal v lvl
- NeutralLevel v -> checkInternal v lvl
+ BlockedLevel _ v -> checkInternal v lvl
+ NeutralLevel _ v -> checkInternal v lvl
UnreducedLevel v -> checkInternal v lvl
-- | Type of a term or sort meta.