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
isEmptyType :: Range -> Type -> TCM ()
isEmptyType r t = do
let postpone t = addConstraint $ IsEmpty r t
ifBlockedType t (\ _ t -> postpone t) $ \ t -> do
tel0 <- getContextTelescope
let gamma = telToList tel0 ++ [domFromArg $ defaultArg (underscore, t)]
ps = [ Arg info $ namedVarP x | Dom info (x, _) <- gamma ]
tel = telFromList gamma
dontAssignMetas $ do
r <- splitLast Inductive tel ps
case r of
Left (CantSplit c tel us vs) -> postpone t
Left _ -> typeError $ ShouldBeEmpty t []
Right cov -> do
let cs = splitClauses cov
unless (null cs) $
typeError $ ShouldBeEmpty t $ map (namedArg . last . scPats) $ cs