    ------------------------------------------------------------------------
    -- The Agda standard library
    --
    -- Printing Strings During Evaluation
    ------------------------------------------------------------------------

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

    -- see README.Debug.Trace for a use-case

    module Debug.Trace where

    open import Agda.Builtin.String using (String)
    open import Agda.Builtin.Equality using (_≡_)

    -- Postulating the `trace` function and explaining how to compile it

    postulate
      trace : ∀ {a} {A : Set a} → String → A → A

    {-# FOREIGN GHC import qualified Debug.Trace as Debug #-}
    {-# FOREIGN GHC import qualified Data.Text as Text #-}
    {-# COMPILE GHC trace = const (const (Debug.trace . Text.unpack)) #-}

    -- Because expressions involving postulates get stuck during evaluation,
    -- we also postulate an equality characterising `trace`'s behaviour. By
    -- declaring it as a rewrite rule we internalise that evaluation rule.

    postulate
      trace-eq : ∀ {a} {A : Set a} (a : A) str → trace str a ≡ a

    {-# BUILTIN REWRITE _≡_ #-}
    {-# REWRITE trace-eq #-}

    -- Specialised version of `trace` returning the traced message.

    traceId : String → String
    traceId str = trace str str