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?

—
Reply to this email directly, view it on GitHub
<https://github.com/ucsd-progsys/liquidhaskell-tutorial/issues/130#issuecomment-2330639272>,
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 https://github.com/ucsd-progsys/liquidhaskell-tutorial/issues/130#issuecomment-2333426057, or unsubscribe https://github.com/notifications/unsubscribe-auth/ABSIB3SARRY4MA5ZAHHH47LZVFKZXAVCNFSM6AAAAABNUKEHXCVHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMZDGMZTGQZDMMBVG4 . You are receiving this because you authored the thread.Message ID: @.***>