Add bindings to ghc's Debug.Trace

[gallais]

Turned out to be pretty convenient in agda/agda/issues/3410

[jmchapman]

It would be nice if it didn't prevent running stuff in Agda. I tried defining trace to be
trace _ x = x and asking Agda not to inline it but it still did.

[gallais]

Hmm. Good point, I didn't think of that. This seems to work:

{-# OPTIONS --rewriting #-}

module Main where

open import Agda.Builtin.String
open import Agda.Builtin.Equality

postulate
  trace : ∀ {a} {A : Set a} → String → A → A
  trace-eq : ∀ a (A : Set a) (a : A) str → trace str 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)) #-}

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

a : String
a = trace "The Traced" "The Value"

open import IO.Primitive
open import Codata.Musical.Costring

main = putStrLn (toCostring a)

C-c C-n on a yields "The Value"
./Main after compilation yields The Traced\nThe Value