free/alloc M but no cigar

liquid haskell.hs

-- needs to be a `M i o a', but almost there. LH is difficult (bad docs, bad errors, changing syntax)

{-# LANGUAGE GADTs #-}
{-# OPTIONS_GHC -fplugin=LiquidHaskell #-}
{-# language GeneralizedNewtypeDeriving, DeriveFunctor #-}

  {-@ LIQUID "--prune-unsorted" @-}

import Control.Monad.State
import Data.Set qualified as Set
import Data.Set (Set)

newtype M s a = M (State s a)
  deriving (Functor, Applicative, Monad)

data Ptr k a = Ptr k
{-@ measure ptrKey :: Ptr k a -> k @-}

{-@ assume free
      :: k:(Ptr Int ())
      -> M (Set Int,Set Int)<{\fld v -> Set_mem (ptrKey k) fld &&
                                        not (Set_mem (ptrKey k) v)}>
           ()
  @-}
free :: Ptr Int () -> M (Set Int,Set Int) ()
free (Ptr k) = M (modify (\(x,y) -> (Set.delete k x, Set.delete k y)))

{-@ assume alloc
      :: k:Int
      -> M (Set Int,Set Int)<{\fld v -> not (Set_mem k fld) &&
                                        Set_mem k v}>
           (Ptr {i:Int|i=k} ())
  @-}
alloc :: Int -> M (Set Int,Set Int) (Ptr Int ())
alloc k = M (do modify (\(x,y) -> (Set.insert k x, Set.insert k y)); pure (Ptr k))

demo :: M (Set Int, Set Int) ()
demo = do
  ptr <- alloc 1
  free ptr