module Agda.TypeChecking.Empty where
import Control.Applicative
import Agda.Syntax.Common
import Agda.Syntax.Internal
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
isReallyEmptyType :: Type -> TCM ()
isReallyEmptyType t = noConstraints $ isEmptyType t
isEmptyType :: Type -> TCM ()
isEmptyType t = do
tb <- reduceB t
let t = ignoreBlocking tb
case unEl <$> tb of
NotBlocked MetaV{} -> addConstraint (IsEmpty t)
Blocked{} -> addConstraint (IsEmpty t)
_ -> do
tel0 <- getContextTelescope
let gamma = telToList tel0 ++ [defaultArg ("_", t)]
ps = [ Arg h r $ VarP x | Arg h r (x, _) <- gamma ]
tel = telFromList gamma
r <- split Inductive tel (idP $ size tel) ps 0
case r of
Left err -> case err of
CantSplit c tel us vs _ -> traceCall (CheckIsEmpty t) $ typeError $ CoverageCantSplitOn c tel us vs
_ -> typeError $ ShouldBeEmpty t []
Right [] -> return ()
Right cs -> typeError $ ShouldBeEmpty t $ map (unArg . last . scPats) cs