module Agda.TypeChecking.Empty (isEmptyType) where
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.Coverage.Match ( fromSplitPatterns )
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 (Blocked m t) -> return $ Left DontKnow
Left (NotBlocked nb 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 . fromSplitPatterns . scPats) $ splitClauses cov
if (null ps) then return (Right ()) else
Left . FailBecause <$> do typeError_ $ ShouldBeEmpty t ps
Right (r, pars, def) -> do
if recEtaEquality def == NoEta 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
]