MultiInstMeasures.hs

module Blank where

import Data.Word
import GHC.Ptr

{-@ class measure sizeOf :: forall a . Ptr a -> Int @-}

{-@ instance measure sizeOf :: (Ptr GHC.Word.Word16) -> Int
      sizeOf (Ptr x) = 2
@-}

{-@ instance measure sizeOf :: (Ptr GHC.Word.Word32) -> Int
      sizeOf (Ptr y) = 4
@-}

{-@ bar :: { p : Ptr Word32 | plen p >= (sizeOf p) } -> () @-}
bar :: Ptr Word32 -> ()
bar (Ptr unused) = ()

{-@ qux :: { p : Ptr Word32 | plen p >= 0 } -> () @-}
qux :: Ptr Word32 -> ()
qux (Ptr addr) = let x = Ptr addr in bar x