How can I define output range of foreign-function in agda?

open import Agda.Builtin.Int
open import Prelude

postulate randomRIO : Int → Int → IO Int
{-# FOREIGN GHC import qualified System.Random as Random #-}
{-# COMPILE GHC randomRIO = \a -> \b -> Random.randomRIO (a, b) #-}

main : IO Unit
main = do
  num ← randomRIO 1 10
  putStrLn $ show num

I imported haskell function randomRIO into Agda. I think output range of randomRIO is determined by first two arguments a and b, like a <= (return value) <= b. But I can't make these types from nothing. To make these types, it have to get some type information of return type. But randomIO is foreign function, I can't get any information of return type.

Is there way to define range of return value of foreign function?