Cannot make a Storable instance

[trinhtuanlong]

So I have a type that I want to make a Storable instance:

{-# LANGUAGE ScopedTypeVariables, RecordWildCards, DeriveFunctor, DeriveFoldable, DeriveTraversable #-}

module Renderer.DataTypes.Vec2 where

import Foreign.Ptr
import Foreign.Storable

data Vec2 a = Vec2
  { x :: a
  , y :: a
  } deriving (Show, Eq, Ord, Functor, Foldable, Traversable)

{-@ class measure size :: forall a. a -> {s: Int | s > 0} @-}
{-@ assume sizeOf :: Storable a => x:a -> {s: Nat | s = size x} @-}
instance Storable a => Storable (Vec2 a)
 {-@ instance Storable a => Storable (Vec2 a) where
       sizeOf :: v2:Vec2 a -> {v:Int | v == 2 * size (x v2)}
       alignment :: v2:Vec2 a -> {v:Int | v == size(x v2)}
       peek :: p:{Ptr (Vec2 a) | plen p >= size (deref p)} -> IO (Vec2 a)
       poke :: p:{Ptr (Vec2 a) | plen p >= size (deref p)} -> Vec2 a -> IO ()
 @-}
     where
  sizeOf _ = 2 * sizeOf (undefined :: a)
  alignment _ = sizeOf (undefined :: a)
  peek ptr = do
    let pBase = castPtr ptr
    xVal <- peek pBase
    yVal <- peekByteOff pBase $ sizeOf (undefined :: a)
    return $ Vec2 xVal yVal
  poke ptr Vec2 {..} = do
    let pBase = castPtr ptr
    poke pBase x
    pokeByteOff pBase (sizeOf (undefined :: a)) y

xx :: Vec2 a -> Vec2 a
xx Vec2 {..} = Vec2 x x

xy :: Vec2 a -> Vec2 a
xy Vec2 {..} = Vec2 x y

yx :: Vec2 a -> Vec2 a
yx Vec2 {..} = Vec2 y x

yy :: Vec2 a -> Vec2 a
yy Vec2 {..} = Vec2 y y

But liquidHaskell throws several errors:

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

src/Renderer/DataTypes/Vec2.hs:15:10: error:
    Liquid Type Mismatch
    .
    The inferred type
      VV : (GHC.Ptr.Ptr (Renderer.DataTypes.Vec2.Vec2 a))
    .
    is not a subtype of the required type
      VV : {VV##6256 : (GHC.Ptr.Ptr (Renderer.DataTypes.Vec2.Vec2 a)) | plen VV##6256 >= size (deref VV##6256)}
    .
    Constraint id 71
   |
15 | instance Storable a => Storable (Vec2 a)
   |          ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

src/Renderer/DataTypes/Vec2.hs:15:10: error:
    Liquid Type Mismatch
    .
    The inferred type
      VV : {v : (GHC.Ptr.Ptr (Renderer.DataTypes.Vec2.Vec2 a)) | v == ?a}
    .
    is not a subtype of the required type
      VV : {VV##6182 : (GHC.Ptr.Ptr (Renderer.DataTypes.Vec2.Vec2 a)) | plen VV##6182 >= size (deref VV##6182)}
    .
    in the context
      ?a : (GHC.Ptr.Ptr (Renderer.DataTypes.Vec2.Vec2 a))
    Constraint id 62
   |
15 | instance Storable a => Storable (Vec2 a)
   |          ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

src/Renderer/DataTypes/Vec2.hs:26:25: error:
    Liquid Type Mismatch
    .
    The inferred type
      VV : {v : (GHC.Ptr.Ptr (Renderer.DataTypes.Vec2.Vec2 a)) | v == ptr##a2BA
                                                                 && plen v >= size (deref v)}
    .
    is not a subtype of the required type
      VV : {VV##6879 : (GHC.Ptr.Ptr (Renderer.DataTypes.Vec2.Vec2 a)) | 0 <= plen VV##6879}
    .
    in the context
      ptr##a2BA : {ptr##a2BA : (GHC.Ptr.Ptr (Renderer.DataTypes.Vec2.Vec2 a)) | plen ptr##a2BA >= size (deref ptr##a2BA)}
    Constraint id 124
   |
26 |     let pBase = castPtr ptr
   |                         ^^^

src/Renderer/DataTypes/Vec2.hs:27:13: error:
    Liquid Type Mismatch
    .
    The inferred type
      VV : {v : (GHC.Ptr.Ptr a) | v == GHC.Ptr.castPtr ptr##a2BA
                                  && plen v == plen ptr##a2BA
                                  && 0 <= plen v}
    .
    is not a subtype of the required type
      VV : {VV##6874 : (GHC.Ptr.Ptr a) | 0 < plen VV##6874}
    .
    in the context
      ptr##a2BA : {ptr##a2BA : (GHC.Ptr.Ptr (Renderer.DataTypes.Vec2.Vec2 a)) | plen ptr##a2BA >= size (deref ptr##a2BA)}
    Constraint id 121
   |
27 |     xVal <- peek pBase
   |             ^^^^^^^^^^

src/Renderer/DataTypes/Vec2.hs:31:25: error:
    Liquid Type Mismatch
    .
    The inferred type
      VV : {v : (GHC.Ptr.Ptr (Renderer.DataTypes.Vec2.Vec2 a)) | v == ptr##a2BE
                                                                 && plen v >= size (deref v)}
    .
    is not a subtype of the required type
      VV : {VV##7144 : (GHC.Ptr.Ptr (Renderer.DataTypes.Vec2.Vec2 a)) | 0 <= plen VV##7144}
    .
    in the context
      ptr##a2BE : {ptr##a2BE : (GHC.Ptr.Ptr (Renderer.DataTypes.Vec2.Vec2 a)) | plen ptr##a2BE >= size (deref ptr##a2BE)}
    Constraint id 146
   |
31 |     let pBase = castPtr ptr
   |                         ^^^

src/Renderer/DataTypes/Vec2.hs:32:5: error:
    Liquid Type Mismatch
    .
    The inferred type
      VV : {v : (GHC.Ptr.Ptr a) | v == GHC.Ptr.castPtr ptr##a2BE
                                  && plen v == plen ptr##a2BE
                                  && 0 <= plen v}
    .
    is not a subtype of the required type
      VV : {VV##7139 : (GHC.Ptr.Ptr a) | 0 < plen VV##7139}
    .
    in the context
      ptr##a2BE : {ptr##a2BE : (GHC.Ptr.Ptr (Renderer.DataTypes.Vec2.Vec2 a)) | plen ptr##a2BE >= size (deref ptr##a2BE)}
    Constraint id 143
   |
32 |     poke pBase x
   |     ^^^^^^^^^^^^

If I remove the annotations the errors are:

src/Renderer/DataTypes/Vec2.hs:15:10: error:
    Liquid Type Mismatch
    .
    The inferred type
      VV : {v : (GHC.Ptr.Ptr (Renderer.DataTypes.Vec2.Vec2 a)) | v == ?a}
    .
    is not a subtype of the required type
      VV : {VV##6298 : (GHC.Ptr.Ptr (Renderer.DataTypes.Vec2.Vec2 a)) | 0 < plen VV##6298}
    .
    in the context
      ?a : (GHC.Ptr.Ptr (Renderer.DataTypes.Vec2.Vec2 a))
    Constraint id 62
   |
15 | instance Storable a => Storable (Vec2 a) where
   |          ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

src/Renderer/DataTypes/Vec2.hs:19:25: error:
    Liquid Type Mismatch
    .
    The inferred type
      VV : {v : (GHC.Ptr.Ptr (Renderer.DataTypes.Vec2.Vec2 a)) | v == ptr##a2BA}
    .
    is not a subtype of the required type
      VV : {VV##6918 : (GHC.Ptr.Ptr (Renderer.DataTypes.Vec2.Vec2 a)) | 0 <= plen VV##6918}
    .
    in the context
      ptr##a2BA : (GHC.Ptr.Ptr (Renderer.DataTypes.Vec2.Vec2 a))
    Constraint id 137
   |
19 |     let pBase = castPtr ptr
   |                         ^^^

src/Renderer/DataTypes/Vec2.hs:20:13: error:
    Liquid Type Mismatch
    .
    The inferred type
      VV : {v : (GHC.Ptr.Ptr a) | v == GHC.Ptr.castPtr ptr##a2BA
                                  && plen v == plen ptr##a2BA
                                  && 0 <= plen v}
    .
    is not a subtype of the required type
      VV : {VV##6913 : (GHC.Ptr.Ptr a) | 0 < plen VV##6913}
    .
    in the context
      ptr##a2BA : (GHC.Ptr.Ptr (Renderer.DataTypes.Vec2.Vec2 a))
    Constraint id 134
   |
20 |     xVal <- peek pBase
   |             ^^^^^^^^^^

src/Renderer/DataTypes/Vec2.hs:24:25: error:
    Liquid Type Mismatch
    .
    The inferred type
      VV : {v : (GHC.Ptr.Ptr (Renderer.DataTypes.Vec2.Vec2 a)) | v == ptr##a2BE}
    .
    is not a subtype of the required type
      VV : {VV##7133 : (GHC.Ptr.Ptr (Renderer.DataTypes.Vec2.Vec2 a)) | 0 <= plen VV##7133}
    .
    in the context
      ptr##a2BE : (GHC.Ptr.Ptr (Renderer.DataTypes.Vec2.Vec2 a))
    Constraint id 163
   |
24 |     let pBase = castPtr ptr
   |                         ^^^

src/Renderer/DataTypes/Vec2.hs:25:5: error:
    Liquid Type Mismatch
    .
    The inferred type
      VV : {v : (GHC.Ptr.Ptr a) | v == GHC.Ptr.castPtr ptr##a2BE
                                  && plen v == plen ptr##a2BE
                                  && 0 <= plen v}
    .
    is not a subtype of the required type
      VV : {VV##7128 : (GHC.Ptr.Ptr a) | 0 < plen VV##7128}
    .
    in the context
      ptr##a2BE : (GHC.Ptr.Ptr (Renderer.DataTypes.Vec2.Vec2 a))
    Constraint id 160
   |
25 |     poke pBase x
   |     ^^^^^^^^^^^^

It seems that I have to somehow inform the functions in this instance that Ptr (Vec2 a), or at least the ptr in peek and poke, would always have plen > 0, but how do I do this? I cannot find any examples anywhere.

[facundominguez]

Hello @trinhtuanlong. Which is your GHC version? I tried your example and had to add an annotation:

{-@ data Vec2 a = Vec2 { x :: a, y :: a } @-}

which makes me think you are not trying the latest LH.

Anyway, I can think of at least the next factors which influence verification:

• your instance annotations only concern the instance for Vec2, and not the instance for a, which the instance for Vec2 uses.
• There are assumptions about peek and poke that LH might bring automatically. They are in Foreign.Storable_LHAssumptions.

Grepping for Storable in the liquidhaskell repo yields a few hits. Some of them are in docs/slides.

There is some discussion on the state of typeclass support in #2450.

[trinhtuanlong]

I am currently using GHC-9.8.2.
I already knew about the Storable assumption in LiquidHaskell, but I guess I am just asking for guidance to make this simple Storable instance using liquid Haskell which enforces the correct size for the data when passing pointer. I tried to add your annotation but the error remained. For example: why is the error:

src/Renderer/DataTypes/Vec2.hs:26:25: error:
    Liquid Type Mismatch
    .
    The inferred type
      VV : {v : (GHC.Ptr.Ptr (Renderer.DataTypes.Vec2.Vec2 a)) | v == ptr##a2BA
                                                                 && plen v >= size (deref v)}
    .
    is not a subtype of the required type
      VV : {VV##6879 : (GHC.Ptr.Ptr (Renderer.DataTypes.Vec2.Vec2 a)) | 0 <= plen VV##6879}
    .
    in the context
      ptr##a2BA : {ptr##a2BA : (GHC.Ptr.Ptr (Renderer.DataTypes.Vec2.Vec2 a)) | plen ptr##a2BA >= size (deref ptr##a2BA)}
    Constraint id 124
   |
26 |     let pBase = castPtr ptr
   |                         ^^^

even though in class measure size I explicitly enforced that the result must be greater than 0

{-@ class measure size :: forall a. a -> {s: Int | s > 0} @-}

And if the error is that the pointer must have the correct size, then how would I ensure this in my annotations?

[facundominguez]

The way I think about it, the constraint only assumes that plen ptr >= size (deref ptr). To prove that plen ptr > 0, we would need in addition the fact that size (deref ptr) > 0. But there is no such assumption, and LH is not going to pick it automatically from the type of the uninterpreted size measure.

It would be different, for instance, if one defined

{-@ assume sizeOf :: Storable a => x:a -> {s: Nat | s = size x && s > 0} @-}

sizeOf can then be used where the assumption is needed

let pBase = castPtr
      (const
         ptr
         (sizeOf (deref ptr) {- :: {s:Nat | s = size (deref ptr) && s > 0 } -})
      )

[trinhtuanlong]

Actually deref is a measure defined in liquidHaskell. As you can see in the Storable and Ptr default assumptions of liquidHaskell. I tried to do what you suggested but the issue is still there.
I think it would be easier to divide the errors so I have tried to enforce the plen p > 0 constraint but there is still an error:
My new code:

{-# LANGUAGE ScopedTypeVariables, RecordWildCards, DeriveFunctor, DeriveFoldable, DeriveTraversable #-}

module Renderer.DataTypes.Vec2 where

import Foreign.Ptr
import Foreign.Storable

{-@ class measure size :: forall a. a -> {s: Int | s > 0} @-}
{-@ assume sizeOf :: Storable a => x:a -> {s: Nat | s = size x && s > 0} @-}
{-@ data Vec2 a = Vec2
  { x :: {v:a | size v > 0}
  , y :: {v:a | size v > 0}
  } @-}
data Vec2 a = Vec2
  { x :: a
  , y :: a
  } deriving (Show, Eq, Ord, Functor, Foldable, Traversable)

instance Storable a => Storable (Vec2 a)
 {-@ instance Storable a => Storable (Vec2 a) where
       sizeOf :: v2:Vec2 a -> {v:Int | v == 2 * size (x v2)}
       alignment :: v2:Vec2 a -> {v:Int | v == size (x v2)}
       peek :: p:{Ptr (Vec2 a) | plen p >= size (deref p)} -> IO (Vec2 a)
       poke :: p:{Ptr (Vec2 a) | plen p >= size (deref p)} -> Vec2 a -> IO ()
 @-}
     where
  sizeOf _ = 2 * sizeOf (undefined :: a)
  alignment _ = sizeOf (undefined :: a)
  peek ptr = do
    let pBase = castPtr $ const ptr $ sizeOf (undefined :: Vec2 a)
    xVal <- peek pBase
    yVal <- peekByteOff pBase $ sizeOf (undefined :: a)
    return $ Vec2 xVal yVal
  poke ptr Vec2 {..} = do
    let pBase = castPtr $ const ptr $ sizeOf (undefined :: Vec2 a)
    poke pBase x
    pokeByteOff pBase (sizeOf (undefined :: a)) y

xx :: Vec2 a -> Vec2 a
xx Vec2 {..} = Vec2 x x

xy :: Vec2 a -> Vec2 a
xy Vec2 {..} = Vec2 x y

yx :: Vec2 a -> Vec2 a
yx Vec2 {..} = Vec2 y x

yy :: Vec2 a -> Vec2 a
yy Vec2 {..} = Vec2 y y

The error that remains:

[typecheck] Liquid Type Mismatch
    .
    The inferred type
      VV : {v : (GHC.Ptr.Ptr (Renderer.DataTypes.Vec2.Vec2 a)) | v == ?a}
    .
    is not a subtype of the required type
      VV : {VV##6911 : (GHC.Ptr.Ptr (Renderer.DataTypes.Vec2.Vec2 a)) | plen VV##6911 >= size (deref VV##6911)}
    .
    in the context
      ?a : (GHC.Ptr.Ptr (Renderer.DataTypes.Vec2.Vec2 a))
    Constraint id 93

I do not understand this error. What does ?a mean? It seems that liquidHaskell requires me to prove that Ptr(Vec2 a) always satisfy the constraint in the instance refinement.
If I remove the instance refinement I get this error instead:

[typecheck] Liquid Type Mismatch
    .
    The inferred type
      VV : {v : GHC.Types.Int | v == ?a}
    .
    is not a subtype of the required type
      VV : {VV##6951 : GHC.Types.Int | 0 <= VV##6951}
    .
    in the context
      ?a : GHC.Types.Int
    Constraint id 88

for the following code:

{-# LANGUAGE ScopedTypeVariables, RecordWildCards, DeriveFunctor, DeriveFoldable, DeriveTraversable #-}

module Renderer.DataTypes.Vec2 where

import Foreign.Ptr
import Foreign.Storable

{-@ class measure size :: forall a. a -> {s: Int | s > 0} @-}
{-@ assume sizeOf :: Storable a => x:a -> {s: Nat | s = size x && s > 0} @-}
{-@ data Vec2 a = Vec2
  { x :: {v:a | size v > 0}
  , y :: {v:a | size v > 0}
  } @-}
data Vec2 a = Vec2
  { x :: a
  , y :: a
  } deriving (Show, Eq, Ord, Functor, Foldable, Traversable)

instance Storable a => Storable (Vec2 a)
     where
  sizeOf _ = 2 * sizeOf (undefined :: a)
  alignment _ = sizeOf (undefined :: a)
  peek ptr = do
    let pBase = castPtr $ const ptr $ sizeOf (undefined :: Vec2 a)
    xVal <- peek pBase
    yVal <- peekByteOff pBase $ sizeOf (undefined :: a)
    return $ Vec2 xVal yVal
  poke ptr Vec2 {..} = do
    let pBase = castPtr $ const ptr $ sizeOf (undefined :: Vec2 a)
    poke pBase x
    pokeByteOff pBase (sizeOf (undefined :: a)) y

xx :: Vec2 a -> Vec2 a
xx Vec2 {..} = Vec2 x x

xy :: Vec2 a -> Vec2 a
xy Vec2 {..} = Vec2 x y

yx :: Vec2 a -> Vec2 a
yx Vec2 {..} = Vec2 y x

yy :: Vec2 a -> Vec2 a
yy Vec2 {..} = Vec2 y y

I do not understand this error. Why is ?a Int now? Why does it have to be nonnegative?

If it helps, here are the flags for liquidHaskell:

-fplugin=LiquidHaskell
-fplugin-opt=LiquidHaskell:--prune-unsorted
-fplugin-opt=LiquidHaskell:--higherorder
-fplugin-opt=LiquidHaskell:--counter-examples

I tried remove --counter-examples but the error remains.

[facundominguez]

I don't think this code is going to work.

let pBase = castPtr $ const ptr $ sizeOf (undefined :: Vec2 a)

sizeOf (undefined :: Vec2 a) has refinement type {s: Nat | s = size undefined && s > 0}, where we needed {s: Nat | s = size (deref ptr) && s > 0}.

But I tried your example again with the latest LH. The following passes, and you can fiddle with it to see how approximating your initial example starts introducing errors. Some notable changes:

• The assumed signatures for poke, peek, etc have been redefined to drop all the predicates they had.
• The Storable instance now explicitly defines peekByteOff and pokeByteOff. Otherwise, they would get default implementations that could generate constraints that were failing.

I don't claim to understand how verification of type classes work. But this would be my starting point to approach it.

{-# LANGUAGE ScopedTypeVariables, RecordWildCards, DeriveFunctor, DeriveFoldable, DeriveTraversable #-}
module Test where

import Foreign.Ptr
import Foreign.Storable

{-@
assume poke        :: (Storable a) => Ptr a -> a -> IO ()
assume peek        :: (Storable a) => (Ptr a) -> (IO a)
assume peekByteOff :: (Storable a) => forall b. Ptr b -> Int -> (IO a)
assume pokeByteOff :: (Storable a) => forall b. Ptr b -> Int -> a -> IO ()
@-}

data Vec2 a = Vec2
  { x :: a
  , y :: a
  } deriving (Show, Eq, Ord, Functor, Foldable, Traversable)

instance Storable a => Storable (Vec2 a) where
  sizeOf _ = 2 * sizeOf (undefined :: a)
  alignment _ = sizeOf (undefined :: a)
  peek ptr = do
    let pBase = castPtr $ const ptr $ sizeOf (undefined :: Vec2 a)
    xVal <- peek pBase
    yVal <- peekByteOff pBase $ sizeOf (undefined :: a)
    return $ Vec2 xVal yVal
  poke ptr Vec2 {..} = do
    let pBase = castPtr $ const ptr $ sizeOf (undefined :: Vec2 a)
    poke pBase x
    pokeByteOff pBase (sizeOf (undefined :: a)) y

  peekByteOff ptr off = undefined -- peek (ptr `plusPtr` off)
  pokeByteOff ptr off = undefined -- poke (ptr `plusPtr` off)

xx :: Vec2 a -> Vec2 a
xx Vec2 {..} = Vec2 x x

xy :: Vec2 a -> Vec2 a
xy Vec2 {..} = Vec2 x y

yx :: Vec2 a -> Vec2 a
yx Vec2 {..} = Vec2 y x

yy :: Vec2 a -> Vec2 a
yy Vec2 {..} = Vec2 y y

[trinhtuanlong]

Thank you very much for your guidance. There is only a slight hiccup left. So this code passed:

{-# LANGUAGE ScopedTypeVariables, RecordWildCards, DeriveFunctor, DeriveFoldable, DeriveTraversable #-}

module Renderer.DataTypes.Vec2 where

import Foreign.Ptr
import Foreign.Storable

data Vec2 a = Vec2
  { x :: a
  , y :: a
  } deriving (Show, Eq, Ord, Functor, Foldable, Traversable)

{-@
class measure size :: Storable a => a -> {s: Int | s > 0}
assume sizeOf :: Storable a => x:a -> {s: Nat | s = size x && s > 0}
assume peek        :: Storable a => {p:Ptr a | plen p >= size (deref p)} -> IO a
assume poke        :: Storable a => {p:Ptr a | plen p >= size (deref p)} -> a -> IO ()
assume peekByteOff :: Storable a => forall b. p:Ptr b -> {off:Nat | off <= plen p} -> IO a
assume pokeByteOff :: Storable a => forall b. p:Ptr b -> Int -> a -> IO ()
@-}
instance Storable a => Storable (Vec2 a) where
  sizeOf _ = 2 * sizeOf (undefined :: a)
  alignment _ = sizeOf (undefined :: a)
  peek ptr = do
    let pBase = castPtr $ const ptr $ sizeOf (undefined :: Vec2 a)
    xVal <- peek pBase
    yVal <- peekByteOff pBase $ sizeOf (undefined :: a)
    return $ Vec2 xVal yVal
  poke ptr Vec2 {..} = do
    let pBase = castPtr $ const ptr $ sizeOf (undefined :: Vec2 a)
    poke pBase x
    pokeByteOff pBase (sizeOf (undefined :: a)) y
  peekByteOff ptr off =
    peek $ (const ptr $ sizeOf (undefined :: Vec2 a)) `plusPtr` off
  pokeByteOff ptr off val =
    poke ((const ptr $ sizeOf (undefined :: Vec2 a)) `plusPtr` off) val

xx :: Vec2 a -> Vec2 a
xx Vec2 {..} = Vec2 x x

xy :: Vec2 a -> Vec2 a
xy Vec2 {..} = Vec2 x y

yx :: Vec2 a -> Vec2 a
yx Vec2 {..} = Vec2 y x

yy :: Vec2 a -> Vec2 a
yy Vec2 {..} = Vec2 y y

But however this did not pass:

{-# LANGUAGE ScopedTypeVariables, RecordWildCards, DeriveFunctor, DeriveFoldable, DeriveTraversable #-}

module Renderer.DataTypes.Vec2 where

import Foreign.Ptr
import Foreign.Storable

data Vec2 a = Vec2
  { x :: a
  , y :: a
  } deriving (Show, Eq, Ord, Functor, Foldable, Traversable)

{-@
class measure size :: Storable a => a -> {s: Int | s > 0}
assume sizeOf :: Storable a => x:a -> {s: Nat | s = size x && s > 0}
assume peek        :: Storable a => {p:Ptr a | plen p >= size (deref p)} -> IO a
assume poke        :: Storable a => {p:Ptr a | plen p >= size (deref p)} -> a -> IO ()
assume peekByteOff :: Storable a => forall b. p:Ptr b -> {off:Nat | off <= plen p} -> IO a
assume pokeByteOff :: Storable a => forall b. p:Ptr b -> {off:Nat | off <= plen p} -> a -> IO ()
@-}
instance Storable a => Storable (Vec2 a) where
  sizeOf _ = 2 * sizeOf (undefined :: a)
  alignment _ = sizeOf (undefined :: a)
  peek ptr = do
    let pBase = castPtr $ const ptr $ sizeOf (undefined :: Vec2 a)
    xVal <- peek pBase
    yVal <- peekByteOff pBase $ sizeOf (undefined :: a)
    return $ Vec2 xVal yVal
  poke ptr Vec2 {..} = do
    let pBase = castPtr $ const ptr $ sizeOf (undefined :: Vec2 a)
    poke pBase x
    pokeByteOff pBase (sizeOf (undefined :: a)) y
  peekByteOff ptr off =
    peek $ (const ptr $ sizeOf (undefined :: Vec2 a)) `plusPtr` off
  pokeByteOff ptr off val =
    poke ((const ptr $ sizeOf (undefined :: Vec2 a)) `plusPtr` off) val

xx :: Vec2 a -> Vec2 a
xx Vec2 {..} = Vec2 x x

xy :: Vec2 a -> Vec2 a
xy Vec2 {..} = Vec2 x y

yx :: Vec2 a -> Vec2 a
yx Vec2 {..} = Vec2 y x

yy :: Vec2 a -> Vec2 a
yy Vec2 {..} = Vec2 y y

The only change is the refinement on pokeByteOff:

assume pokeByteOff :: Storable a => forall b. p:Ptr b -> {off:Nat | off <= plen p} -> a -> IO ()

The error is:

src/Renderer/DataTypes/Vec2.hs:21:10: error:
    Liquid Type Mismatch
    .
    The inferred type
      VV : {v : GHC.Types.Int | v == ?a}
    .
    is not a subtype of the required type
      VV : {VV##7469 : GHC.Types.Int | VV##7469 <= plen ptr##a3yX}
    .
    in the context
      ?a : GHC.Types.Int

      ptr##a3yX : (GHC.Ptr.Ptr (Renderer.DataTypes.Vec2.Vec2 a))
    Constraint id 79
   |
21 | instance Storable a => Storable (Vec2 a) where
   |          ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

[trinhtuanlong]

If I simply use plain liquidHaskell right now, there would still be error. This code:

{-# LANGUAGE ScopedTypeVariables, RecordWildCards, DeriveFunctor, DeriveFoldable, DeriveTraversable #-}

module Renderer.DataTypes.Vec2 where

import Foreign.Ptr
import Foreign.Storable

data Vec2 a = Vec2
  { x :: a
  , y :: a
  } deriving (Show, Eq, Ord, Functor, Foldable, Traversable)

instance Storable a => Storable (Vec2 a)
         where
  sizeOf _ = 2 * sizeOf (undefined :: a)
  alignment _ = sizeOf (undefined :: a)
  peek ptr = do
    let pBase = castPtr $ const ptr $ sizeOf (undefined :: Vec2 a)
    xVal <- peek pBase
    yVal <- peekByteOff pBase $ sizeOf (undefined :: a)
    return $ Vec2 xVal yVal
  poke ptr Vec2 {..} = do
    let pBase = castPtr $ const ptr $ sizeOf (undefined :: Vec2 a)
    poke pBase x
    pokeByteOff pBase (sizeOf (undefined :: a)) y
  peekByteOff ptr off =
    peek $ (const ptr $ sizeOf (undefined :: Vec2 a)) `plusPtr` off
  pokeByteOff ptr off val =
    (const ptr $ sizeOf (undefined :: Vec2 a)) `plusPtr` off `poke` val

xx :: Vec2 a -> Vec2 a
xx Vec2 {..} = Vec2 x x

xy :: Vec2 a -> Vec2 a
xy Vec2 {..} = Vec2 x y

yx :: Vec2 a -> Vec2 a
yx Vec2 {..} = Vec2 y x

yy :: Vec2 a -> Vec2 a
yy Vec2 {..} = Vec2 y y

did not pass with the error:

src/Renderer/DataTypes/Vec2.hs:21:10: error:
    Liquid Type Mismatch
    .
    The inferred type
      VV : {v : GHC.Types.Int | v == ?a}
    .
    is not a subtype of the required type
      VV : {VV##7466 : GHC.Types.Int | 0 <= VV##7466}
    .
    in the context
      ?a : GHC.Types.Int
    Constraint id 80
   |
21 | instance Storable a => Storable (Vec2 a)
   |          ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

which makes me wonder if there is a verified example of a simple Storable instance using plain liquidHaskell somewhere.

[facundominguez]

The method pokeByteOff is used by the default implementation of the method pokeElemOff. Strengthening the specification of the former must be causing the error in the later. Adding an implementation of pokeElemOff should make the error more obvious.

which makes me wonder if there is a verified example of a simple Storable instance using plain liquidHaskell somewhere.

I'm not finding tests that actually try to define instances of Storable.

[trinhtuanlong]

Thank you very much! Now my code passed with this version:

{-# LANGUAGE ScopedTypeVariables, RecordWildCards, DeriveFunctor, DeriveFoldable, DeriveTraversable #-}

module Renderer.DataTypes.Vec2 where

import Foreign.Ptr
import Foreign.Storable

data Vec2 a = Vec2
  { x :: a
  , y :: a
  } deriving (Show, Eq, Ord, Functor, Foldable, Traversable)

instance Storable a => Storable (Vec2 a)
         where
  sizeOf _ = 2 * sizeOf (undefined :: a)
  alignment _ = sizeOf (undefined :: a)
  peek ptr = do
    let pBase = castPtr $ const ptr $ sizeOf (undefined :: Vec2 a)
    xVal <- peek pBase
    yVal <- peekByteOff pBase $ sizeOf (undefined :: a)
    return $ Vec2 xVal yVal
  poke ptr Vec2 {..} = do
    let pBase = castPtr $ const ptr $ sizeOf (undefined :: Vec2 a)
    poke pBase x
    pokeByteOff pBase (sizeOf (undefined :: a)) y
  peekByteOff ptr off =
    peek $ (const ptr $ sizeOf (undefined :: Vec2 a)) `plusPtr` off
  pokeByteOff ptr off val =
    (const ptr $ sizeOf (undefined :: Vec2 a)) `plusPtr` off `poke` val
  pokeElemOff ptr off val = pokeByteOff ptr (off * sizeOf (undefined :: a)) val

xx :: Vec2 a -> Vec2 a
xx Vec2 {..} = Vec2 x x

xy :: Vec2 a -> Vec2 a
xy Vec2 {..} = Vec2 x y

yx :: Vec2 a -> Vec2 a
yx Vec2 {..} = Vec2 y x

yy :: Vec2 a -> Vec2 a
yy Vec2 {..} = Vec2 y y

[trinhtuanlong]

I just wanted to ask a little question before closing this: Why does const ptr $ sizeOf (undefined :: a) works but not ptr? They seem to do the same thing.

[facundominguez]

They do the same thing. But when type checking const a b the constraint that Liquid Haskell produces includes in the hypotheses the refinement types of both a and b. const is very much like the combinator ? used to introduce lemmas when using Liquid Haskell as a theorem prover.

[trinhtuanlong]

I am afraid it still feels very opaque to me. I cannot find any assumption for const in Base_LHAssumptions.hs nor do I see any definition of sizeOf. If I use const ptr 3 instead liquidHaskell throws an error, but somehow sizeOf anything works? Also in the Storable_LHAssumptions.hs, peek already has a assumed precondition that 0 < plen v, so why cannot castPtr just assume ptr has plen > 0 but throw an error instead?
I am sorry for the additional question. I am very new to liquidHaskell.

[facundominguez]

but somehow sizeOf anything works?

Looking at the constraints that LH is producing, sizeOf undefined is introducing false as an hypothesis, which allows to any statement to be admitted. undefined is not a total function after all.

I cannot find any assumption for const in Base_LHAssumptions.hs nor do I see any definition of sizeOf.

The behavior is explained because of how constraints (proof obligations) are generated in LH, rather than because of assumptions. I don't have a good reference handy, though the papers in the website must cover it. Perhaps @ranjitjhala can provide a concrete account.