liquid-haskell

Why does LiquidHaskell fail to take guard into account?

I am following the Liquid Haskell tutorial:

http://ucsd-progsys.github.io/liquidhaskell-tutorial/04-poly.html

and this example fails:

module Test2 where

import Data.Vector
import Prelude hiding (length)

vectorSum :: Vector Int -> Int
vectorSum vec = go 0 0
  where
    go acc i
      | i < length vec  = go (acc + (vec ! i)) (i + 1)
      | otherwise       = acc

with the following error:

Error: Liquid Type Mismatch

 10 |       | i < length vec  = go (acc + (vec ! i)) (i + 1)
                                   ^^^^^^^^^^^^^^^^^

   Inferred type
     VV : {v : GHC.Types.Int | v == acc + ?b}

   not a subtype of Required type
     VV : {VV : GHC.Types.Int | VV < acc
                                && VV >= 0}

   In Context
     ?b : GHC.Types.Int
     acc : GHC.Types.Int

The question is why? The guard (i < length vec) should ensure that (vec ! i) is safe.

Solution

  • This looks like a termination error. Liquid Haskell here seems to assume that acc is the termination metric of go (probably because it's the first Int argument). As such it should always be non-negative and decreasing in each iteration (hence the error message you get).

    The way to fix this is providing a correct termination metric, which fulfills the above criteria. Here this would be length vec - i and the corresponding signature for go is:

    {-@ go :: _ -> i:_ -> _ /[length vec - i] @-}

    or something along those lines.