LiquidHaskell: Trying to use assume keyword, but data type is not numeric

I'm trying to write some specifications for the Data.Ratio module. So far I have:

module spec Data.Ratio where

import GHC.Real

Data.Ratio.denominator :: GHC.Real.Integral a => r : GHC.Real.Ratio a -> {x:a | x > 0}

The code I'm verifying is:

{-@ die :: {v:String | false} -> a @-}
die msg = error msg

main :: IO ()
main = do
  let x = 3 % 5
  print $ denominator x
  if denominator x < 0
    then die "bad ending"
    else putStrLn "good ending"

The code is judged safe, because denominator never returns a negative value.

I found this strange because I could have just written x <= 0 as a postcondition, which according to the documentation of the Data.Ratio module is impossible. Apparently Liquid Haskell does not compare my postcondition to the implementation of denominator.

My understanding is that since the function implementation was not checked, I'm better off using the assume keyword:

assume Data.Ratio.denominator :: GHC.Real.Integral a => r : GHC.Real.Ratio a -> {x:a | x > 0}

However, I then get:

Error: Bad Type Specification
 assumed type GHC.Real.denominator :: (Ratio a) -> {VV : a | VV > 0}
     Sort Error in Refinement: {VV : a_a2kc | VV > 0}
     Unbound Symbol a_a2kc
 Perhaps you meant: papp5, papp3, papp4, head, papp2, papp7, papp6, papp1, tail
  because
The sort a_a2kc is not numeric

My questions are

1. Shouldn't LH force me to use the assume keyword in this case if it clearly didn't verify the correctness of my refined type by comparing with the function implementation?
2. Am I right in thinking I should use the assume keyword?
3. How come a is suddenly not numeric? Wasn't it numeric when I didn't use assume?