Я следую руководству Liquid Haskell:
http://ucsd-progsys.github.io/liquidhaskell-tutorial/04-poly.html
и этот пример завершается ошибкой:
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
со следующей ошибкой:
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
Вопрос в том, почему? Охранник (i <длина vec) должен обеспечить безопасность (vec! I). </p>