Chapter 4 Polymorphism

[matheussbernardo]

Hello! I am trying to go through the tutorial. But I think type inference is not working at.

`{-@ LIQUID "--no-termination" @-}

module DemoLib where

import Data.Vector

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 = Data.Vector.length vec
`

It is failing with

`
**** LIQUID: UNSAFE ************************************************************

app/DemoLib.hs:20:31: error:
Liquid Type Mismatch
.
The inferred type
VV : {v : GHC.Types.Int | v == i##a17O}
.
is not a subtype of the required type
VV : {VV##694 : GHC.Types.Int | VV##694 < vlen vec##a17L}
.
in the context
i##a17O : GHC.Types.Int

  vec##a17L : {vec##a17L : (Data.Vector.Vector GHC.Types.Int) | 0 <= vlen vec##a17L}
Constraint id 8

|
20 | body i acc = acc + (vec ! i)`

[VhRvo]

Did you put specifications in your code?

~~~~~{.spec}
loop :: lo:Nat -> hi:{Nat|lo <= hi} -> a -> (Btwn lo hi -> a -> a) -> a
~~~~~

[matheussbernardo]

I thought it would be automatically inferred though. Maybe I misunderstood the text.

…

On Thu, Sep 5, 2024 at 07:34 Samuel ***@***.***> wrote: Did you put specifications in your code? ~~~~~{.spec}loop :: lo:Nat -> hi:{Nat|lo <= hi} -> a -> (Btwn lo hi -> a -> a) -> a~~~~~ — Reply to this email directly, view it on GitHub <#130 (comment)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/ABSIB3SNPJMG6HTZXUGRNPTZU7UP3AVCNFSM6AAAAABNUKEHXCVHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMZDGMZQGYZTSMRXGI> . You are receiving this because you authored the thread.Message ID: ***@***.***>

[VhRvo]

How it going now?

[matheussbernardo]

Yeah! With the annotation it works.

…

On Fri, Sep 6, 2024 at 09:30 Samuel ***@***.***> wrote: How it going now? — Reply to this email directly, view it on GitHub <#130 (comment)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/ABSIB3SARRY4MA5ZAHHH47LZVFKZXAVCNFSM6AAAAABNUKEHXCVHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMZDGMZTGQZDMMBVG4> . You are receiving this because you authored the thread.Message ID: ***@***.***>