    module Agda.TypeChecking.Empty
      ( isEmptyType
      , isEmptyTel
      , ensureEmptyType
      , checkEmptyTel
      ) where

    import Control.Monad        ( void )
    import Control.Monad.Except ( MonadError(..) )

    import Data.Semigroup
    import qualified Data.Set as Set

    import Agda.Syntax.Common
    import Agda.Syntax.Internal
    import Agda.Syntax.Internal.MetaVars
    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.List
    import Agda.Utils.Monad

    import Agda.Utils.Impossible

    data ErrorNonEmpty
      = Fail               -- ^ Generic failure
      | FailBecause TCErr  -- ^ Failure with informative error
      | DontKnow Blocker   -- ^ Emptyness check blocked

    instance Semigroup ErrorNonEmpty where
      DontKnow Blocker
    u1     <> :: ErrorNonEmpty -> ErrorNonEmpty -> ErrorNonEmpty
    <> DontKnow Blocker
    u2  = Blocker -> ErrorNonEmpty
    DontKnow (Blocker -> ErrorNonEmpty) -> Blocker -> ErrorNonEmpty
    forall a b. (a -> b) -> a -> b
    $ Blocker
    u1 Blocker -> Blocker -> Blocker
    forall a. Semigroup a => a -> a -> a
    <> Blocker
    u2  -- Both must unblock for this to proceed
      e :: ErrorNonEmpty
    e@DontKnow{}    <> ErrorNonEmpty
    _            = ErrorNonEmpty
    e
      ErrorNonEmpty
    _               <> e :: ErrorNonEmpty
    e@DontKnow{} = ErrorNonEmpty
    e
      FailBecause TCErr
    err <> ErrorNonEmpty
    _            = TCErr -> ErrorNonEmpty
    FailBecause TCErr
    err
      ErrorNonEmpty
    Fail            <> ErrorNonEmpty
    err          = ErrorNonEmpty
    err

    instance Monoid ErrorNonEmpty where
      mempty :: ErrorNonEmpty
    mempty  = ErrorNonEmpty
    Fail
      mappend :: ErrorNonEmpty -> ErrorNonEmpty -> ErrorNonEmpty
    mappend = ErrorNonEmpty -> ErrorNonEmpty -> ErrorNonEmpty
    forall a. Semigroup a => a -> a -> a
    (Data.Semigroup.<>)

    -- | Ensure that a type is empty.
    --   This check may be postponed as emptiness constraint.
    ensureEmptyType
      :: Range -- ^ Range of the absurd pattern.
      -> Type  -- ^ Type that should be empty (empty data type or iterated product of such).
      -> TCM ()
    ensureEmptyType :: Range -> Type -> TCM ()
    ensureEmptyType Range
    r Type
    t = TCMT IO (Either ErrorNonEmpty ())
    -> (ErrorNonEmpty -> TCM ()) -> (() -> TCM ()) -> TCM ()
    forall (m :: * -> *) a b c.
    Monad m =>
    m (Either a b) -> (a -> m c) -> (b -> m c) -> m c
    caseEitherM (Range -> Type -> TCMT IO (Either ErrorNonEmpty ())
    checkEmptyType Range
    r Type
    t) ErrorNonEmpty -> TCM ()
    failure () -> TCM ()
    forall (m :: * -> *) a. Monad m => a -> m a
    return
      where
      failure :: ErrorNonEmpty -> TCM ()
    failure (DontKnow Blocker
    u)      = Blocker -> Constraint -> TCM ()
    forall (m :: * -> *).
    MonadConstraint m =>
    Blocker -> Constraint -> m ()
    addConstraint Blocker
    u (Constraint -> TCM ()) -> Constraint -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ Range -> Type -> Constraint
    IsEmpty Range
    r Type
    t
      failure (FailBecause TCErr
    err) = TCErr -> TCM ()
    forall e (m :: * -> *) a. MonadError e m => e -> m a
    throwError TCErr
    err
      failure ErrorNonEmpty
    Fail              = TypeError -> TCM ()
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    TypeError -> m a
    typeError (TypeError -> TCM ()) -> TypeError -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ Type -> [DeBruijnPattern] -> TypeError
    ShouldBeEmpty Type
    t []

    -- | Check whether a type is empty.
    isEmptyType :: Type -> TCM Bool
    isEmptyType :: Type -> TCM Bool
    isEmptyType Type
    ty = Either ErrorNonEmpty () -> Bool
    forall a b. Either a b -> Bool
    isRight (Either ErrorNonEmpty () -> Bool)
    -> TCMT IO (Either ErrorNonEmpty ()) -> TCM Bool
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Range -> Type -> TCMT IO (Either ErrorNonEmpty ())
    checkEmptyType Range
    forall a. Range' a
    noRange Type
    ty

    -- | Check whether some type in a telescope is empty.
    isEmptyTel :: Telescope -> TCM Bool
    isEmptyTel :: Tele (Dom' Term Type) -> TCM Bool
    isEmptyTel Tele (Dom' Term Type)
    tel = Either ErrorNonEmpty Int -> Bool
    forall a b. Either a b -> Bool
    isRight (Either ErrorNonEmpty Int -> Bool)
    -> TCMT IO (Either ErrorNonEmpty Int) -> TCM Bool
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Range
    -> Tele (Dom' Term Type) -> TCMT IO (Either ErrorNonEmpty Int)
    checkEmptyTel Range
    forall a. Range' a
    noRange Tele (Dom' Term Type)
    tel

    -- Either the type is possibly non-empty (Left err) or it is really empty
    -- (Right ()).
    checkEmptyType :: Range -> Type -> TCM (Either ErrorNonEmpty ())
    checkEmptyType :: Range -> Type -> TCMT IO (Either ErrorNonEmpty ())
    checkEmptyType Range
    range Type
    t = do
      Either (Blocked Type) (QName, Args, Defn)
    mr <- Type -> TCMT IO (Either (Blocked Type) (QName, Args, Defn))
    forall (m :: * -> *).
    PureTCM m =>
    Type -> m (Either (Blocked Type) (QName, Args, Defn))
    tryRecordType Type
    t
      case Either (Blocked Type) (QName, Args, Defn)
    mr of

        -- If t is blocked or a meta, we cannot decide emptiness now.  Postpone.
        Left (Blocked Blocker
    b Type
    t) -> Either ErrorNonEmpty () -> TCMT IO (Either ErrorNonEmpty ())
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Either ErrorNonEmpty () -> TCMT IO (Either ErrorNonEmpty ()))
    -> Either ErrorNonEmpty () -> TCMT IO (Either ErrorNonEmpty ())
    forall a b. (a -> b) -> a -> b
    $ ErrorNonEmpty -> Either ErrorNonEmpty ()
    forall a b. a -> Either a b
    Left (Blocker -> ErrorNonEmpty
    DontKnow Blocker
    b)

        -- If t is not a record type, try to split
        Left (NotBlocked NotBlocked' Term
    nb Type
    t) -> do
          -- from the current context xs:ts, create a pattern list
          -- xs _ : ts t and try to split on _ (the last variable)
          Tele (Dom' Term Type)
    tel0 <- TCMT IO (Tele (Dom' Term Type))
    forall (m :: * -> *).
    (Applicative m, MonadTCEnv m) =>
    m (Tele (Dom' Term Type))
    getContextTelescope
          let gamma :: [Dom (ArgName, Type)]
    gamma = Tele (Dom' Term Type) -> [Dom (ArgName, Type)]
    forall t. Tele (Dom t) -> [Dom (ArgName, t)]
    telToList Tele (Dom' Term Type)
    tel0 [Dom (ArgName, Type)]
    -> [Dom (ArgName, Type)] -> [Dom (ArgName, Type)]
    forall a. [a] -> [a] -> [a]
    ++ [Arg (ArgName, Type) -> Dom (ArgName, Type)
    forall a. Arg a -> Dom a
    domFromArg (Arg (ArgName, Type) -> Dom (ArgName, Type))
    -> Arg (ArgName, Type) -> Dom (ArgName, Type)
    forall a b. (a -> b) -> a -> b
    $ (ArgName, Type) -> Arg (ArgName, Type)
    forall a. a -> Arg a
    defaultArg (ArgName
    forall a. Underscore a => a
    underscore, Type
    t)]
              tel :: Tele (Dom' Term Type)
    tel   = [Dom (ArgName, Type)] -> Tele (Dom' Term Type)
    telFromList [Dom (ArgName, Type)]
    gamma
              ps :: [NamedArg DeBruijnPattern]
    ps    = Tele (Dom' Term Type) -> [NamedArg DeBruijnPattern]
    forall a. DeBruijn a => Tele (Dom' Term Type) -> [NamedArg a]
    teleNamedArgs Tele (Dom' Term Type)
    tel

          TCMT IO (Either ErrorNonEmpty ())
    -> TCMT IO (Either ErrorNonEmpty ())
    forall (m :: * -> *) a.
    (MonadTCEnv m, HasOptions m, MonadDebug m) =>
    m a -> m a
    dontAssignMetas (TCMT IO (Either ErrorNonEmpty ())
     -> TCMT IO (Either ErrorNonEmpty ()))
    -> TCMT IO (Either ErrorNonEmpty ())
    -> TCMT IO (Either ErrorNonEmpty ())
    forall a b. (a -> b) -> a -> b
    $ do
            Either SplitError Covering
    r <- Induction
    -> Tele (Dom' Term Type)
    -> [NamedArg DeBruijnPattern]
    -> TCM (Either SplitError Covering)
    splitLast Induction
    Inductive Tele (Dom' Term Type)
    tel [NamedArg DeBruijnPattern]
    ps
            case Either SplitError Covering
    r of
              Left UnificationStuck{} -> Either ErrorNonEmpty () -> TCMT IO (Either ErrorNonEmpty ())
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Either ErrorNonEmpty () -> TCMT IO (Either ErrorNonEmpty ()))
    -> Either ErrorNonEmpty () -> TCMT IO (Either ErrorNonEmpty ())
    forall a b. (a -> b) -> a -> b
    $ ErrorNonEmpty -> Either ErrorNonEmpty ()
    forall a b. a -> Either a b
    Left (ErrorNonEmpty -> Either ErrorNonEmpty ())
    -> ErrorNonEmpty -> Either ErrorNonEmpty ()
    forall a b. (a -> b) -> a -> b
    $ Blocker -> ErrorNonEmpty
    DontKnow (Blocker -> ErrorNonEmpty) -> Blocker -> ErrorNonEmpty
    forall a b. (a -> b) -> a -> b
    $ Tele (Dom' Term Type) -> Blocker
    forall t. AllMetas t => t -> Blocker
    unblockOnAnyMetaIn Tele (Dom' Term Type)
    tel
              Left SplitError
    _                  -> Either ErrorNonEmpty () -> TCMT IO (Either ErrorNonEmpty ())
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Either ErrorNonEmpty () -> TCMT IO (Either ErrorNonEmpty ()))
    -> Either ErrorNonEmpty () -> TCMT IO (Either ErrorNonEmpty ())
    forall a b. (a -> b) -> a -> b
    $ ErrorNonEmpty -> Either ErrorNonEmpty ()
    forall a b. a -> Either a b
    Left ErrorNonEmpty
    Fail
              Right Covering
    cov -> do
                let ps :: [DeBruijnPattern]
    ps = (SplitClause -> DeBruijnPattern)
    -> [SplitClause] -> [DeBruijnPattern]
    forall a b. (a -> b) -> [a] -> [b]
    map (NamedArg DeBruijnPattern -> DeBruijnPattern
    forall a. NamedArg a -> a
    namedArg (NamedArg DeBruijnPattern -> DeBruijnPattern)
    -> (SplitClause -> NamedArg DeBruijnPattern)
    -> SplitClause
    -> DeBruijnPattern
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . NamedArg DeBruijnPattern
    -> [NamedArg DeBruijnPattern] -> NamedArg DeBruijnPattern
    forall a. a -> [a] -> a
    lastWithDefault NamedArg DeBruijnPattern
    forall a. HasCallStack => a
    __IMPOSSIBLE__ ([NamedArg DeBruijnPattern] -> NamedArg DeBruijnPattern)
    -> (SplitClause -> [NamedArg DeBruijnPattern])
    -> SplitClause
    -> NamedArg DeBruijnPattern
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [NamedArg SplitPattern] -> [NamedArg DeBruijnPattern]
    fromSplitPatterns ([NamedArg SplitPattern] -> [NamedArg DeBruijnPattern])
    -> (SplitClause -> [NamedArg SplitPattern])
    -> SplitClause
    -> [NamedArg DeBruijnPattern]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . SplitClause -> [NamedArg SplitPattern]
    scPats) ([SplitClause] -> [DeBruijnPattern])
    -> [SplitClause] -> [DeBruijnPattern]
    forall a b. (a -> b) -> a -> b
    $ Covering -> [SplitClause]
    splitClauses Covering
    cov
                if ([DeBruijnPattern] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null [DeBruijnPattern]
    ps) then Either ErrorNonEmpty () -> TCMT IO (Either ErrorNonEmpty ())
    forall (m :: * -> *) a. Monad m => a -> m a
    return (() -> Either ErrorNonEmpty ()
    forall a b. b -> Either a b
    Right ()) else
                  ErrorNonEmpty -> Either ErrorNonEmpty ()
    forall a b. a -> Either a b
    Left (ErrorNonEmpty -> Either ErrorNonEmpty ())
    -> (TCErr -> ErrorNonEmpty) -> TCErr -> Either ErrorNonEmpty ()
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . TCErr -> ErrorNonEmpty
    FailBecause (TCErr -> Either ErrorNonEmpty ())
    -> TCMT IO TCErr -> TCMT IO (Either ErrorNonEmpty ())
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> do TypeError -> TCMT IO TCErr
    forall (m :: * -> *).
    (HasCallStack, MonadTCEnv m, ReadTCState m) =>
    TypeError -> m TCErr
    typeError_ (TypeError -> TCMT IO TCErr) -> TypeError -> TCMT IO TCErr
    forall a b. (a -> b) -> a -> b
    $ Type -> [DeBruijnPattern] -> TypeError
    ShouldBeEmpty Type
    t [DeBruijnPattern]
    ps

        -- If t is a record type, see if any of the field types is empty
        Right (QName
    r, Args
    pars, Defn
    def) -> do
          if | NoEta{} <- Defn -> HasEta' PatternOrCopattern
    recEtaEquality Defn
    def -> Either ErrorNonEmpty () -> TCMT IO (Either ErrorNonEmpty ())
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Either ErrorNonEmpty () -> TCMT IO (Either ErrorNonEmpty ()))
    -> Either ErrorNonEmpty () -> TCMT IO (Either ErrorNonEmpty ())
    forall a b. (a -> b) -> a -> b
    $ ErrorNonEmpty -> Either ErrorNonEmpty ()
    forall a b. a -> Either a b
    Left ErrorNonEmpty
    Fail
             | Bool
    otherwise -> Either ErrorNonEmpty Int -> Either ErrorNonEmpty ()
    forall (f :: * -> *) a. Functor f => f a -> f ()
    void (Either ErrorNonEmpty Int -> Either ErrorNonEmpty ())
    -> TCMT IO (Either ErrorNonEmpty Int)
    -> TCMT IO (Either ErrorNonEmpty ())
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> do Range
    -> Tele (Dom' Term Type) -> TCMT IO (Either ErrorNonEmpty Int)
    checkEmptyTel Range
    range (Tele (Dom' Term Type) -> TCMT IO (Either ErrorNonEmpty Int))
    -> Tele (Dom' Term Type) -> TCMT IO (Either ErrorNonEmpty Int)
    forall a b. (a -> b) -> a -> b
    $ Defn -> Tele (Dom' Term Type)
    recTel Defn
    def Tele (Dom' Term Type) -> Args -> Tele (Dom' Term Type)
    forall t. Apply t => t -> Args -> t
    `apply` Args
    pars

    -- | Check whether one of the types in the given telescope is constructor-less
    --   and if yes, return its index in the telescope (0 = leftmost).
    checkEmptyTel :: Range -> Telescope -> TCM (Either ErrorNonEmpty Int)
    checkEmptyTel :: Range
    -> Tele (Dom' Term Type) -> TCMT IO (Either ErrorNonEmpty Int)
    checkEmptyTel Range
    r = Int -> Tele (Dom' Term Type) -> TCMT IO (Either ErrorNonEmpty Int)
    loop Int
    0
      where
      loop :: Int -> Tele (Dom' Term Type) -> TCMT IO (Either ErrorNonEmpty Int)
    loop Int
    i Tele (Dom' Term Type)
    EmptyTel            = Either ErrorNonEmpty Int -> TCMT IO (Either ErrorNonEmpty Int)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Either ErrorNonEmpty Int -> TCMT IO (Either ErrorNonEmpty Int))
    -> Either ErrorNonEmpty Int -> TCMT IO (Either ErrorNonEmpty Int)
    forall a b. (a -> b) -> a -> b
    $ ErrorNonEmpty -> Either ErrorNonEmpty Int
    forall a b. a -> Either a b
    Left ErrorNonEmpty
    Fail
      loop Int
    i (ExtendTel Dom' Term Type
    dom Abs (Tele (Dom' Term Type))
    tel) = [TCMT IO (Either ErrorNonEmpty Int)]
    -> TCMT IO (Either ErrorNonEmpty Int)
    forall e (m :: * -> *) b.
    (Monoid e, Monad m, Functor m) =>
    [m (Either e b)] -> m (Either e b)
    orEitherM
        [ (Int
    i Int -> Either ErrorNonEmpty () -> Either ErrorNonEmpty Int
    forall (f :: * -> *) a b. Functor f => a -> f b -> f a
    <$) (Either ErrorNonEmpty () -> Either ErrorNonEmpty Int)
    -> TCMT IO (Either ErrorNonEmpty ())
    -> TCMT IO (Either ErrorNonEmpty Int)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Range -> Type -> TCMT IO (Either ErrorNonEmpty ())
    checkEmptyType Range
    r (Dom' Term Type -> Type
    forall t e. Dom' t e -> e
    unDom Dom' Term Type
    dom)
        , Dom' Term Type
    -> Abs (Tele (Dom' Term Type))
    -> (Tele (Dom' Term Type) -> TCMT IO (Either ErrorNonEmpty Int))
    -> TCMT IO (Either ErrorNonEmpty Int)
    forall a (m :: * -> *) b.
    (Subst a, MonadAddContext m) =>
    Dom' Term Type -> Abs a -> (a -> m b) -> m b
    underAbstraction Dom' Term Type
    dom Abs (Tele (Dom' Term Type))
    tel ((Tele (Dom' Term Type) -> TCMT IO (Either ErrorNonEmpty Int))
     -> TCMT IO (Either ErrorNonEmpty Int))
    -> (Tele (Dom' Term Type) -> TCMT IO (Either ErrorNonEmpty Int))
    -> TCMT IO (Either ErrorNonEmpty Int)
    forall a b. (a -> b) -> a -> b
    $ Int -> Tele (Dom' Term Type) -> TCMT IO (Either ErrorNonEmpty Int)
    loop (Int -> Int
    forall a. Enum a => a -> a
    succ Int
    i)
        ]