    {-# LANGUAGE Safe #-}

    -- | Custom functions to report error messages to users.
    module Copilot.Theorem.Misc.Error
      ( badUse
      , impossible
      , impossible_
      , fatal
      ) where

    -- | Tag used with error messages to help users locate the component that
    -- failed or reports the error.
    errorHeader :: String
    errorHeader :: String
    errorHeader = String
    "[Copilot-kind ERROR]  "

    -- | Report an error due to an error detected by Copilot (e.g., user error).
    badUse :: String -- ^ Description of the error.
           -> a
    badUse :: forall a. String -> a
    badUse String
    s = String -> a
    forall a. HasCallStack => String -> a
    error (String -> a) -> String -> a
    forall a b. (a -> b) -> a -> b
    $ String
    errorHeader String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    s

    -- | Report an error due to a bug in Copilot.
    impossible :: String -- ^ Error information to attach to the message.
               -> a
    impossible :: forall a. String -> a
    impossible String
    s = String -> a
    forall a. HasCallStack => String -> a
    error (String -> a) -> String -> a
    forall a b. (a -> b) -> a -> b
    $ String
    errorHeader String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    "Unexpected internal error : " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    s

    -- | Report an error due to a bug in Copilot.
    impossible_ :: a
    impossible_ :: forall a. a
    impossible_ = String -> a
    forall a. HasCallStack => String -> a
    error (String -> a) -> String -> a
    forall a b. (a -> b) -> a -> b
    $ String
    errorHeader String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    "Unexpected internal error"

    -- | Report an unrecoverable error (e.g., incorrect format).
    fatal :: String -> a
    fatal :: forall a. String -> a
    fatal = String -> a
    forall a. HasCallStack => String -> a
    error