content: {-@ LIQUID "--no-termination" @-}
  {-@ LIQUID "--short-names"    @-}
  
  module Foo () where
  
  import Language.Haskell.Liquid.Prelude (liquidAssert)
  import Data.IORef
  
  {-@ type Upto N = {v:Nat | v < N} @-} 
  
  {-@ job :: IO () @-}
  job = do
    p <- newIORef (0 :: Int)
    writeIORef p 10
    v <- readIORef p
    liquidAssert (v == 0) $ return ()
    
  {-@ bob :: Nat -> IO () @-}
  bob n = do
    t <- newIO (n+1) (\_ -> 0)
    setIO t 0 100
    r <- getIO t 0
    liquidAssert (r == 0) $ return ()
  
   
  data IOArr a = IOA { size :: Int
                     , pntr :: IORef (Arr a)
                     }
  
  data Arr a   = A { alen :: Int
                   , aval :: Int -> a
                   }
  
  
  
  {-@ data IOArr a <p :: Int -> a -> Prop>
        = IOA { size :: Nat
              , pntr :: IORef ({v:Arr<p> a | alen v = size})
              }
    @-}
  
  
  {-@ data Arr a <p :: Int -> a -> Prop>
               = A { alen :: Nat 
                   , aval :: i:Upto alen -> a<p i>
                   }
    @-}
  
  
  
  {-@ newIO :: forall <p :: Int -> a -> Prop>.
                 n:Nat -> (i:Upto n -> a<p i>) -> IO ({v: IOArr<p> a | size v = n})
    @-}
  newIO :: Int -> (Int -> a) -> IO (IOArr a)
  newIO n f = undefined
  
  {-@ getIO :: forall <p :: Int -> a -> Prop>.
                a:IOArr<p> a -> i:Upto (size a) -> IO (a<p i>)
    @-}
  getIO :: IOArr a -> Int-> IO a
  getIO a@(IOA sz p) i = undefined
  
  {-@ setIO :: forall <p :: Int -> a -> Prop>.
                a:IOArr<p> a -> i:Upto (size a) -> a<p i> -> IO ()
    @-}
  setIO :: IOArr a -> Int -> a -> IO ()
  setIO a@(IOA sz p) i v = undefined
  
  