Failed attempt at added abstract predicate to mutable vectors

mutable_vectors_satisfying.hs

module Lib
    ( someFunc
    ) where

import Control.Monad.Primitive
import Data.Vector.Mutable (MVector,IOVector,unsafeNew,unsafeWrite)
import qualified Data.Vector.Mutable as MV

{-@ measure mvlen    :: Data.Vector.MVector s a -> Int @-}
{-@ invariant       { v : Data.Vector.MVector s a | 0 <= mvlen v } @-}

{-@ assume unsafeNew :: PrimMonad m => x : Nat -> ( m { v : ( MVector ( PrimState m ) a ) | mvlen v = x } ) @-}

{-@ assume MV.replicate :: PrimMonad m => x : Nat -> a -> ( m { v : ( MVector ( PrimState m ) a ) | mvlen v = x } ) @-}

{-@ assume unsafeWrite :: Control.Monad.Primitive.PrimMonad m
      => x:(Data.Vector.MVector (Control.Monad.Primitive.PrimState m) a)
      -> ix:{v:Nat | v < mvlen x }
		  -> a
		  -> m ()
@-}

{-@ restrictedWrite :: forall <p :: a -> Prop>. PrimMonad m => mv:MVector (PrimState m) a<p> -> {ix:Nat | ix < mvlen mv} -> a<p> -> m () @-}
restrictedWrite :: PrimMonad m => MVector (PrimState m) a -> Int -> a -> m ()
restrictedWrite mv ix a = unsafeWrite mv ix a

{-@ restrictedNew :: forall <p :: a -> Prop>. PrimMonad m => x : Nat -> ( m { v : ( MVector ( PrimState m ) a<p> ) | mvlen v = x } ) @-}
restrictedNew :: PrimMonad m => Int -> m (MVector (PrimState m) a)
restrictedNew = unsafeNew

{-@ restrictedReplicate :: forall <p :: a -> Prop>. PrimMonad m => x : Nat -> a<p> -> ( m { v : ( MVector ( PrimState m ) (a<p>)) | mvlen v = x } ) @-}
restrictedReplicate :: PrimMonad m => Int -> a -> m (MVector (PrimState m) a)
restrictedReplicate = MV.replicate

{-@ testFunc :: IO ( MVector RealWorld ( Int<{\x -> x < 100}> ) ) @-}
testFunc :: IO (MVector RealWorld Int)
testFunc = restrictedReplicate 12 99
  -- myVec <- restrictedNew 8
  -- restrictedWrite myVec 6 55
  -- return myVec
  -- restrictedReplicate 12 6

someFunc :: IO ()
someFunc = putStrLn "someFunc"