From c0d490ad9090b9b0c3a823ace26d6092dce80ac9 Mon Sep 17 00:00:00 2001
From: hashirama <hashirama@noreply.localhost>
Date: Thu, 30 Oct 2025 23:08:10 +0000
Subject: [PATCH] refined data instead of measure

---
 LiquidExamples.hs | 8 +++-----
 1 file changed, 3 insertions(+), 5 deletions(-)

diff --git a/LiquidExamples.hs b/LiquidExamples.hs
index 41f7623..b91fc20 100644
--- a/LiquidExamples.hs
+++ b/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