    {-# LANGUAGE CPP #-}
    -- | Eliminates case defaults by adding an alternative for all possible
    -- constructors. Literal cases are preserved as-is.
    module Agda.Compiler.Treeless.EliminateDefaults where

    import Control.Monad
    import qualified Data.List as List
    import Data.Maybe

    import Agda.Syntax.Abstract.Name (QName)
    import Agda.Syntax.Treeless
    import Agda.Syntax.Literal
    import qualified Agda.Syntax.Internal as I

    import Agda.TypeChecking.Monad
    import Agda.TypeChecking.Monad.Builtin
    import Agda.TypeChecking.Primitive
    import Agda.TypeChecking.Substitute

    import Agda.Compiler.Treeless.Subst

    import Agda.Utils.Impossible

    #include "undefined.h"

    eliminateCaseDefaults :: TTerm -> TCM TTerm
    eliminateCaseDefaults = tr
      where
        tr :: TTerm -> TCM TTerm
        tr t = case t of
          TCase sc ct@CaseInfo{caseType = CTData qn} def alts | not (isUnreachable def) -> do
            dtCons <- defConstructors . theDef <$> getConstInfo qn
            let missingCons = dtCons List.\\ map aCon alts
            def <- tr def
            newAlts <- forM missingCons $ \con -> do
              Constructor {conArity = ar} <- theDef <$> getConstInfo con
              return $ TACon con ar (TVar ar)

            alts' <- (++ newAlts) <$> mapM (trAlt . raise 1) alts

            return $ TLet def $ TCase (sc + 1) ct tUnreachable alts'
          TCase sc ct def alts -> TCase sc ct <$> tr def <*> mapM trAlt alts

          TVar{}    -> tt
          TDef{}    -> tt
          TCon{}    -> tt
          TPrim{}   -> tt
          TLit{}    -> tt
          TUnit{}   -> tt
          TSort{}   -> tt
          TErased{} -> tt
          TError{}  -> tt

          TCoerce a               -> TCoerce <$> tr a
          TLam b                  -> TLam <$> tr b
          TApp a bs               -> TApp <$> tr a <*> mapM tr bs
          TLet e b                -> TLet <$> tr e <*> tr b

          where tt = return t

        trAlt :: TAlt -> TCM TAlt
        trAlt a = case a of
          TAGuard g b -> TAGuard <$> tr g <*> tr b
          TACon q a b -> TACon q a <$> tr b
          TALit l b   -> TALit l <$> tr b