refined data instead of measure

LiquidExamples.hs

@@ -104,20 +104,18 @@ safeLookup x i
 
 
 -- | A pointer tagged with its size
+{-@ data PtrSized a = PtrSized { ptrData :: Ptr a , ptrSz   :: {n:Int | n >= 0}}  @-}
 data PtrSized a = PtrSized
   { ptrData :: Ptr a
   , ptrSz   :: Int
   }
 
-{-@ measure ptrSize @-}
-ptrSize :: PtrSized a -> Int
-ptrSize (PtrSized _ n) = n
 
-{-@ type SafeIndex N = {i:Int | 0 <= i && i < N} @-}
+{-@ type SafeIndex v = {i:Int | 0 <= i && i < ptrSz v} @-}
 
 {-@ peekElemN :: Storable a
               => v:PtrSized a
-              -> SafeIndex (ptrSize v)
+              -> SafeIndex v
               -> IO a
   @-}
 peekElemN :: Storable a => PtrSized a -> Int -> IO a