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

i'm trying write specifications data.ratio module. far have:

module spec data.ratio  import ghc.real  data.ratio.denominator :: ghc.real.integral => r : ghc.real.ratio -> {x:a | x > 0} 

the code i'm verifying is:

{-@ die :: {v:string | false} -> @-} die msg = error msg  main :: io () main =   let x = 3 % 5   print $ denominator x   if denominator x < 0     die "bad ending"     else putstrln "good ending" 

the code judged safe, because denominator never returns negative value.

i found strange because have written x <= 0 postcondition, according documentation of data.ratio module impossible. apparently liquid haskell not compare postcondition implementation of denominator.

my understanding since function implementation not checked, i'm better off using assume keyword:

assume data.ratio.denominator :: ghc.real.integral => r : ghc.real.ratio -> {x:a | x > 0} 

however, get:

 error: bad type specification  assumed type ghc.real.denominator :: (ratio a) -> {vv : | vv > 0}      sort error in refinement: {vv : a_a2kc | vv > 0}      unbound symbol a_a2kc  perhaps meant: papp5, papp3, papp4, head, papp2, papp7, papp6, papp1, tail   because sort a_a2kc not numeric 

my questions are

1. shouldn't lh force me use assume keyword in case if didn't verify correctness of refined type comparing function implementation?
2. am right in thinking should use assume keyword?
3. how come a not numeric? wasn't numeric when didn't use assume?

unfortunately 'numeric' literally means 'num' , not subclasses thereof. need extend lh support sub-classes in form describe above; create issue it, pointing out!

now, if specialize type to, e.g. int or integer lh throws error:

import ghc.real  {-@ assume denom :: r:ghc.real.ratio int -> {x:int | x >= 0} @-} denom :: ghc.real.ratio int -> int  denom = denominator  {-@ die :: {v:string | false} -> @-} die msg = error msg  main :: io () main =   let x = 3 % 5   print $ denom x   if denom x <= 0     die "bad ending"     else putstrln "good ending" 

http://goto.ucsd.edu:8090/index.html#?demo=permalink%2f1504739852_3583.hs

if make output type x > 0 safe again.

http://goto.ucsd.edu:8090/index.html#?demo=permalink%2f1504739907_3585.hs

thanks again pointing out ratio issue!