Жидкий haskell создает новую бистринг с PS

Question

Я делаю некоторые привязки к C из Haskell и пытаюсь сделать его более безопасным с помощью LiquidHaskell. У меня возникли проблемы с указанием длины строки байтов в аннотации типа LH.

У меня есть расширенный тип ByteString в LiquidHaskell, который включает в себя его длину:

{-@ type ByteString Blen = {v:B.ByteString | bslen v == Blen} @-}

Я получаю следующую ошибку при запуске Liquidhaskell:

**** RESULT: UNSAFE ************************************************************


 /home/t/liquidproblem/Main.hs:47:3-22: Error: Liquid Type Mismatch

 47 |   Bi.PS foreignPtr 0 l
        ^^^^^^^^^^^^^^^^^^^^

   Inferred type
     VV : {v : Data.ByteString.Internal.ByteString | 0 <= bslen v
                                                     && bslen v == stringlen v}

   not a subtype of Required type
     VV : {VV : Data.ByteString.Internal.ByteString | bslen VV == l}

   In Context
     l : {l : GHC.Types.Int | l >= 0}

Строка 47:

44 {-@ makeBs :: ForeignPtr Word8 -> l:NonNeg -> ByteString l @-}
45 makeBs :: F.ForeignPtr F.Word8 -> Int -> B.ByteString
46 makeBs foreignPtr l =
47   Bi.PS foreignPtr 0 l

(Я знаю, что это кажется немного глупой функцией, но она была вставлена, потому что процесс отладки состоял в том, чтобы выделять биты и помещать в них аннотации LH, пока я не обнаружил проблему.)

Соответствующий импорт:

import qualified Data.ByteString.Internal as Bi
import qualified Data.ByteString as B
import qualified Foreign as F

Тип LH NonNeg

{-@ type NonNeg = {i:Int | i >= 0} @-}

Answer 1

LiquidHaskell не знает, что ByteString вернулся makeBs имеет длину lи это не может доказать это из имеющейся у него информации.

Вы знаете, что это произойдет, потому что вы знаете, что третий аргумент PS Конструктор это длина. Итак, на данный момент у вас есть два (или, возможно, один) варианта:

1. Вы можете попытаться рассказать ЛХ, что вы знаете о PS конструктор, и дать ему аннотацию как {-@ Bi.PS :: _ -> _ -> l:NonNeg -> ByteString l @-}, Я попробовал это, и это не совсем сработало, потому что в сигнатуре есть внутренние типы GHC PS что LH не так хорош в обращении. YMMV. Или вы можете:
2. Забудьте об аннотировании PS и пометить свою функцию с assume: {-@ assume makeBs :: ForeignPtr Word8 -> l:NonNeg -> ByteString l @-}, Конечно, это становится более рискованным, если функция отмечена assume становится больше - глупо, хотя может показаться, что вы можете сохранить makeBs вокруг, если вы идете по этому маршруту.