mutable variables with permissions

perms.hs

{-# LANGUAGE DataKinds             #-}
{-# LANGUAGE FlexibleContexts      #-}
{-# LANGUAGE FlexibleInstances     #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PolyKinds             #-}
{-# LANGUAGE TypeFamilies          #-}
{-# LANGUAGE TypeOperators         #-}
{-# LANGUAGE UndecidableInstances  #-}

module Lib where

import Control.Concurrent.MVar
import Data.IORef

class Member t r where

instance {-# OVERLAPPING #-} Member t (t  ': r') where
instance Member t rs' => Member t (t' ': rs') where

data Permission = ReadP | WriteP

newtype IORef' (ps :: [Permission]) a = IORef' (IORef a)

writeIORef' :: Member 'WriteP ps => IORef' ps a -> a -> IO ()
writeIORef' = undefined

readIORef' :: Member 'ReadP ps => IORef' ps a -> IO a
readIORef' = undefined

toReadOnlyIORef :: IORef a -> IORef' '[ReadP] a
toReadOnlyIORef ref = IORef' ref

toWriteIORef :: IORef a -> IORef' '[WriteP, ReadP] a
toWriteIORef ref = IORef' ref

someFunc :: IO ()
someFunc = do
    ref1 <- newIORef 123
    let
      ref2 :: IORef' '[ReadP] Int
      ref2 = toReadOnlyIORef ref1

    readIORef' ref2 >>= print

    -- This is a type error
    -- writeIORef' ref2 987

    -- Also a type error
    -- let
    --   ref3 :: IORef' '[ReadP, WriteP] Int
    --   ref3 = toReadOnlyIORef ref1

    let
      -- ref4 :: (Member ReadP r, Member WriteP r) => IORef' p Int
      ref4 :: IORef' '[WriteP, ReadP] Int
      ref4 = toWriteIORef ref1

    readIORef' ref4 >>= print
    writeIORef' ref4 0
    readIORef' ref4 >>= print

--------------------------------------------------------------------------------

data MVarPermission = ReadMVar | PutMVar | TakeMVar

newtype MVar' (ps :: [MVarPermission]) a = MVar' (MVar a)

mvarWPermissions :: MVar a -> MVar' ps a
mvarWPermissions = MVar'

readMVar' :: Member 'ReadMVar r => MVar' r a -> IO a
readMVar' (MVar' v) = readMVar v

putMVar' :: Member 'PutMVar r => MVar' r a -> a -> IO ()
putMVar' (MVar' v) a = putMVar v a

takeMVar' :: Member 'TakeMVar r => MVar' r a -> IO a
takeMVar' (MVar' v) = takeMVar v

f :: IO ()
f = do
    var <- newEmptyMVar
    let
      readOnlyMVar :: MVar' '[ReadMVar] Int
      readOnlyMVar = mvarWPermissions var

      takeAndPutMVar :: MVar' '[TakeMVar, PutMVar] Int
      takeAndPutMVar = mvarWPermissions var

    -- compiles fine
    readMVar' readOnlyMVar >>= print

    -- fails
    -- readMVar' takeAndPutMVar >>= print

    -- fails
    -- takeMVar' readOnlyMVar >>= print

    -- compiles fine
    takeMVar' takeAndPutMVar >>= print
    -- compiles fine
    putMVar' takeAndPutMVar 10
    return ()