Defining measures in Liquid Haskell

Question

Here's a simple function to calculate average of the numbers in a given list.

{-@ type NonZero = {v:Int | v/=0 } @-}

{-@ divide :: Int -> NonZero -> Int @-}
divide :: Int -> Int -> Int
divide n d = div n d

{-@ measure nonEmpty :: [a] -> Bool @-}
nonEmpty [] = False
nonEmpty _ = True

{-@ size :: xs:[a] -> {v:Nat | nonEmpty xs => v>0 } @-}
size :: [a] -> Int
size [] = 0
size (_:xs) = 1 + size xs

{-@ type NEList a = {v:[a] | nonEmpty v} @-}

{-@ avg :: NEList Int -> Int @-}
avg xs = divide (sum xs) (size xs)

Unfortunately this code doesn't typecheck.

But if I declare nonEmpty to be a measure after I define the function, it works:

{-@ type NonZero = {v:Int | v/=0 } @-}

{-@ divide :: Int -> NonZero -> Int @-}
divide :: Int -> Int -> Int
divide n d = div n d

{-@ nonEmpty :: [a] -> Bool @-}
nonEmpty [] = False
nonEmpty _ = True
{-@ measure nonEmpty @-}

{-@ size :: xs:[a] -> {v:Nat | nonEmpty xs => v>0 } @-}
size :: [a] -> Int
size [] = 0
size (_:xs) = 1 + size xs

{-@ type NEList a = {v:[a] | nonEmpty v} @-}

{-@ avg :: NEList Int -> Int @-}
avg xs = divide (sum xs) (size xs)

So can somebody explain why is it so?

Answer 1

This is because LH expects measures to be declared via the second syntax (not the first). However, unfortunately, LH currently does not give an error message with the first, it appears to just silently ignore the measure definition (or rather, treat it as "uninterpreted").

We will fix the code so that when there is an actual definition, it tells you about it.

In short: this is an unfortunate consequence of our syntax choices, my apologies!