Wrong type expected by foldl'

[yourcomrade]

Hi everyone, I am currently following the liquid haskell tutorial. In the section 4 Polymorphism, there is an example with calculating sparseProduct' by using foldl':

{-@ sparseProduct'  :: x:Vector _ -> SparseN _ (vlen x) -> _ @-}
sparseProduct'::Num a => Vector a -> [(Int, a)] -> a -- this is added by myself
sparseProduct' x y  = foldl' body 0 y
  where
    body sum (i, v) = sum + (x ! i) * v

However, I get this error:

* Couldn't match expected type: Vector (Int, a)
                  with actual type: [(Int, a)]
    * In the third argument of foldl', namely `y'
      In the expression: foldl' body 0 y
      In an equation for sparseProduct':
          sparseProduct' x y
            = foldl' body 0 y
            where
                body sum (i, v) = sum + (x ! i) * v
    * Relevant bindings include
        body :: a -> (Int, a) -> a (bound at src\Demo\Example.hs:98:5)
        y :: [(Int, a)] (bound at src\Demo\Example.hs:96:18)
        x :: Vector a (bound at src\Demo\Example.hs:96:16)
        sparseProduct' :: Vector a -> [(Int, a)] -> a
          (bound at src\Demo\Example.hs:96:1)
   |
96 | sparseProduct' x y  = foldl' body 0 y

What do you think I should do to fix this error?
I use GHC 9.8.2 on windows environment.

[AlecsFerra]

That's a GHC error not a LH error, there foldl' is inferred to be the one from Data.Vector, instead
there you want foldl' operating on lists, it's also pointed out two lines above the exercise.

[AlecsFerra]

I don't know how foldl is defined in the book (if via reflection or something else) but this should do what you expect and passes verification

{-@ LIQUID "--reflection" @-}
module Test where

import Prelude hiding (length, foldl')
import Data.Vector hiding (foldl')

{-@ type Btwn Lo Hi = {v:Int | Lo <= v && v < Hi} @-}
{-@ type SparseN a N = [(Btwn 0 N, a)] @-}

{-@
measure vlen :: Vector a -> Int
assume length :: x:Vector a -> {v:Int | v = vlen x}
assume (!) :: x:Vector a -> {v:Nat | v < vlen x} -> a
@-}

{-@ reflect foldl' @-}
foldl' :: (a -> b -> a) -> a -> [b] -> a
foldl' f z []     = z
foldl' f z (x:xs) = foldl' f (f z x) xs

{-@ sparseProduct'  :: x:Vector _ -> SparseN _ (vlen x) -> _ @-}
sparseProduct' :: Vector Int -> [(Int, Int)] -> Int
sparseProduct' x y  = foldl' body 0 y
  where
    body sum (i, v) = sum + (x ! i) * v

[yourcomrade]

I have imported foldl' from the Data.List like in this code:

import qualified Data.List as L
{-@ sparseProduct'  :: x:Vector _ -> SparseN _ (vlen x) -> _ @-}
sparseProduct'::Num a => Vector a -> [(Int, a)] -> a
sparseProduct' x y  = L.foldl' body 0 y
  where
    body sum (i, v) = sum + (x ! i) * v

However, I get this error:

Specified type does not refine Haskell type for `Demo.Example.sparseProduct'` (Checked)

[AlecsFerra]

The type of foldl' from Data.List is not the one that is written in the book, I suppose the one used there was defined in some of the previous chapters. But the one using Traversable should work anyway and I can't reproduce your issue.

module Test where

import Prelude hiding (length, foldl')
import qualified Data.List as L
import Data.Vector hiding (foldl')

{-@ type Btwn Lo Hi = {v:Int | Lo <= v && v < Hi} @-}
{-@ type SparseN a N = [(Btwn 0 N, a)] @-}

{-@
measure vlen :: Vector a -> Int
assume length :: x:Vector a -> {v:Int | v = vlen x}
assume (!) :: x:Vector a -> {v:Nat | v < vlen x} -> a
@-}

{-@ sparseProduct' :: x:Vector _ -> SparseN _ (vlen x) -> _ @-}
sparseProduct' :: (Num a) => Vector a -> [(Int, a)] -> a
sparseProduct' x y  = L.foldl' body 0 y
  where
    body sum (i, v) = sum + (x ! i) * v

This works just fine.

Can you send the whole file?

[yourcomrade]

Yeah, sure
Here is my Haskell file

{-# OPTIONS_GHC -fplugin=LiquidHaskell #-}
module Demo.Example where
import Data.Vector 
import Prelude hiding (length)
import qualified Prelude as P
import qualified Data.List as L
{-@ LIQUID "--no-termination" @-}
{-@ type VectorN a N = {v:Vector a | vlen v == N} @-}

{-@ type Btwn Lo Hi = {v:Int | Lo <= v && v < Hi} @-}

{-@ type NEVector a = {v:Vector a | 0 < vlen v} @-}

{-@ head' :: NEVector a -> a @-}
head'     :: Vector a -> a
head' vec = vec ! 0


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

{-@ loop :: lo:Nat -> hi:{Nat|lo <= hi} -> a -> (Btwn lo hi -> a -> a) -> a @-}
loop :: Int -> Int -> a -> (Int -> a -> a) -> a
loop lo hi base f =  go base lo
  where
    go acc i
      | i < hi    = go (f i acc) (i + 1)
      | otherwise = acc

vectorSum'      :: Vector Int -> Int
vectorSum' vec  = loop 0 n 0 body
  where
    body i acc  = acc + (vec ! i)
    n           = length vec
{-@ type SparseN a N = [(Btwn 0 N, a)] @-}
{-@ sparseProduct'  :: x:Vector _ -> SparseN _ (vlen x) -> _ @-}
sparseProduct'::Num a => Vector a -> [(Int, a)] -> a
sparseProduct' x y  = L.foldl' body 0 y
  where
    body sum (i, v) = sum + (x ! i) * v