Search code examples
haskellliquid-haskell

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?
Solution

  • Unfortunately by 'Numeric' it literally means 'Num' and not even subclasses thereof. We need to extend LH to support sub-classes in the form you describe above; I will create an issue for it, thanks for pointing out!

    Now, if you specialize your type to, e.g. Int or Integer then LH properly throws the 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} -> a @-}
die msg = error msg

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

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

    if you make the output type x > 0 then it is safe again.

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

    Thanks again for pointing out the Ratio issue!