Rank n types, interfaces, and unification idiris

Question

In Idris, this works:

appShow : Show a => ({b : _} -> Show b => b -> String) -> a -> String
appShow s x = s x

tAppShow : String
tAppShow = appShow show 5

However, a somewhat different version doesn't. This compiles:

specializeMonad : ({m : _} -> Monad m => m Int) -> IO Int
specializeMonad f = f

But if I try to use it:

tSpecializeMonad1 : IO Int
tSpecializeMonad1 = specializeMonad (return 5)

-- Or trying harder to keep it polymorphic
tSpecializeMonad2 : IO Int
tSpecializeMonad2 = specializeMonad (the ({m : _} -> Monad m => m Int) (return 5))

Then I get Can't find implementation for Monad m for the first and:

                Type mismatch between
                        m Integer (Type of return 5)
                and
                        m2 Int (Expected type)

For the second.

I noticed this happens even just with return 5. Eg, if I try in the repl:

> return 5
Can't find implementation for Monad m

Is there a way to have a value with a type that's interface-polymorphic? Is there something I'm misunderstanding about the principles behind Idris' typechecking? (I'm coming from Haskell, as might already be obvious.)