FFIs should compose ;)

cursed.agda

{-# OPTIONS --guardedness --type-in-type #-}
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 ex')