FFIs should compose ;)

cursed.agda

{-# OPTIONS --guardedness #-}
module cursed where
    open import Agda.Builtin.String
    open import IO
    postulate 
        ex' : String

        
    {-# FOREIGN GHC
        {-# LANGUAGE ForeignFunctionInterface #-}
        import Data.Text
        foreign import ccall "exp" c_exp :: Double -> Double



        ex :: Text
        ex = pack $ show $ c_exp 2
    #-}

    {-# COMPILE GHC ex' = ex #-}
    main = run (putStrLn "Hello, World!")