    ------------------------------------------------------------------------
    -- The Agda standard library
    --
    -- Primitive System.Exit simple bindings to Haskell functions
    ------------------------------------------------------------------------

    {-# OPTIONS --cubical-compatible #-}

    module System.Exit.Primitive where

    open import Agda.Builtin.Int using (Int)
    open import Agda.Builtin.IO using (IO)

    data ExitCode : Set where
      ExitSuccess : ExitCode
      ExitFailure : Int → ExitCode

    {-# FOREIGN GHC data AgdaExitCode = AgdaExitSuccess | AgdaExitFailure Integer #-}
    {-# COMPILE GHC ExitCode = data AgdaExitCode (AgdaExitSuccess | AgdaExitFailure) #-}

    {-# FOREIGN GHC import qualified System.Exit as SE #-}

    {-# FOREIGN GHC
    toExitCode :: AgdaExitCode -> SE.ExitCode
    toExitCode AgdaExitSuccess = SE.ExitSuccess
    toExitCode (AgdaExitFailure n) = SE.ExitFailure (fromIntegral n)

    fromExitCode :: SE.ExitCode -> AgdaExitCode
    fromExitCode SE.ExitSuccess = AgdaExitSuccess
    fromExitCode (SE.ExitFailure n) = AgdaExitFailure (fromIntegral n)
    #-}

    postulate
      exitWith : ∀ {a} {A : Set a} → ExitCode → IO A

    {-# COMPILE GHC exitWith = \ _ _ -> SE.exitWith . toExitCode #-}