module Agda.TypeChecking.Empty (isEmptyType) where
import Control.Applicative
import Control.Monad
import Control.Monad.Except
import Data.Semigroup
import Data.Monoid
import Agda.Syntax.Common
import Agda.Syntax.Internal
import Agda.Syntax.Internal.Pattern
import Agda.Syntax.Position
import Agda.TypeChecking.Monad
import Agda.TypeChecking.Coverage
import Agda.TypeChecking.Constraints
import Agda.TypeChecking.Records
import Agda.TypeChecking.Reduce
import Agda.TypeChecking.Substitute
import Agda.TypeChecking.Telescope
import Agda.Utils.Either
import Agda.Utils.Monad
data ErrorNonEmpty
= Fail
| FailBecause TCErr
| DontKnow
instance Semigroup ErrorNonEmpty where
DontKnow <> _ = DontKnow
_ <> DontKnow = DontKnow
FailBecause err <> _ = FailBecause err
Fail <> err = err
instance Monoid ErrorNonEmpty where
mempty = Fail
mappend = (Data.Semigroup.<>)
isEmptyType :: Range -> Type -> TCM ()
isEmptyType r t = caseEitherM (loop t) failure return
where
failure DontKnow = addConstraint $ IsEmpty r t
failure (FailBecause err) = throwError err
failure Fail = typeError $ ShouldBeEmpty t []
loop :: Type -> TCM (Either ErrorNonEmpty ())
loop t = do
mr <- tryRecordType t
case mr of
Left Nothing -> return $ Left DontKnow
Left (Just t) -> do
tel0 <- getContextTelescope
let gamma = telToList tel0 ++ [domFromArg $ defaultArg (underscore, t)]
tel = telFromList gamma
ps = teleNamedArgs tel
dontAssignMetas $ do
r <- splitLast Inductive tel ps
case r of
Left UnificationStuck{} -> return $ Left DontKnow
Left _ -> return $ Left Fail
Right cov -> do
let ps = map (namedArg . last . scPats) $ splitClauses cov
if (null ps) then return (Right ()) else
Left . FailBecause <$> do typeError_ $ ShouldBeEmpty t ps
Right (r, pars, def) -> do
if not $ recEtaEquality def then return $ Left Fail else do
checkTel $ recTel def `apply` pars
checkTel :: Telescope -> TCM (Either ErrorNonEmpty ())
checkTel EmptyTel = return $ Left Fail
checkTel (ExtendTel dom tel) = orEitherM
[ loop (unDom dom)
, underAbstraction dom tel checkTel
]