module Agda.TypeChecking.Empty
( isEmptyType
, isEmptyTel
, ensureEmptyType
, checkEmptyTel
) where
import Control.Monad.Except
import Data.Semigroup
import Agda.Syntax.Common
import Agda.Syntax.Internal
import Agda.Syntax.Position
import Agda.TypeChecking.Monad
import Agda.TypeChecking.Coverage
import Agda.TypeChecking.Coverage.Match ( fromSplitPatterns )
import Agda.TypeChecking.Records
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.<>)
ensureEmptyType
:: Range
-> Type
-> TCM ()
ensureEmptyType r t = caseEitherM (checkEmptyType r t) failure return
where
failure DontKnow = addConstraint $ IsEmpty r t
failure (FailBecause err) = throwError err
failure Fail = typeError $ ShouldBeEmpty t []
isEmptyType :: Type -> TCM Bool
isEmptyType ty = isRight <$> checkEmptyType noRange ty
isEmptyTel :: Telescope -> TCM Bool
isEmptyTel tel = isRight <$> checkEmptyTel noRange tel
checkEmptyType :: Range -> Type -> TCM (Either ErrorNonEmpty ())
checkEmptyType range 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
void <$> do checkEmptyTel range $ recTel def `apply` pars
checkEmptyTel :: Range -> Telescope -> TCM (Either ErrorNonEmpty Int)
checkEmptyTel r = loop 0
where
loop i EmptyTel = return $ Left Fail
loop i (ExtendTel dom tel) = orEitherM
[ (i <$) <$> checkEmptyType r (unDom dom)
, underAbstraction dom tel $ loop (succ i)
]