haskell - PS で新しいバイト文字列を作成する Liquid haskell

Question

私は Haskell から C へのバインディングを作成し、LiquidHaskell でより安全にしようとしています。LH 型注釈でバイト文字列の長さを指定するのに問題があります。

私は、LiquidHaskell に長さを含む拡張 ByteString 型を持っています。

{-@ 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} @-}