module Agda.TypeChecking.Empty where
import Control.Applicative
import Control.Monad
import Agda.Syntax.Common
import Agda.Syntax.Internal
import Agda.Syntax.Position
import Agda.TypeChecking.Monad
import Agda.TypeChecking.Coverage
import Agda.TypeChecking.Constraints
import Agda.TypeChecking.Reduce
import Agda.TypeChecking.Substitute
import Agda.Utils.Permutation
import Agda.Utils.Size
isEmptyType :: Range -> Type -> TCM ()
isEmptyType r t = do
tb <- reduceB t
let t = ignoreBlocking tb
postpone = addConstraint (IsEmpty r t)
case ignoreSharing . unEl <$> tb of
NotBlocked MetaV{} -> postpone
Blocked{} -> postpone
_ -> do
tel0 <- getContextTelescope
let gamma = telToList tel0 ++ [domFromArg $ defaultArg ("_", t)]
ps = [ Arg h r $ VarP x | Dom h r (x, _) <- gamma ]
tel = telFromList gamma
dontAssignMetas $ do
r <- splitLast Inductive tel ps
case r of
Left err -> case err of
CantSplit c tel us vs _ -> postpone
_ -> typeError $ ShouldBeEmpty t []
Right cov -> do
let cs = splitClauses cov
unless (null cs) $
typeError $ ShouldBeEmpty t $ map (unArg . last . scPats) $ cs