MonadUnliftIO instance allows escape

[tomjaguarpaw]

This seems bad:

{-# LANGUAGE GHC2021 #-}

import Bluefin.IO qualified as B
import Bluefin.State qualified as B
import Bluefin.System.IO qualified as B
import System.IO (IOMode(ReadMode))

-- ghci> example
-- *** Exception: /dev/null: hPutChar: illegal operation (handle is closed)
example :: IO ()
example = B.runEff $ \io -> do
  r <- B.withFile io "/dev/null" ReadMode $ \h -> do
    B.withEffToIO_ io $ \effToIO -> do
      pure (effToIO (B.hPutChar h 'X'))

  B.effIO io r

Effectful has a similar problem, although it actually detects that it's happening, which would lead to greater safety in situations where the handles themselves don't dynamically check whether they're still alive.

{-# LANGUAGE GHC2021 #-}

import Effectful
import Effectful.State.Static.Local


example :: IO ()
example = B.runEff $ \io -> do
  r <- B.withFile io "/dev/null" ReadMode $ \h -> do
    B.withEffToIO_ io $ \effToIO -> do
      pure (effToIO (B.hPutChar h 'X'))

  B.effIO io r

-- ghci> foo 
-- *** Exception: version (2) /= storageVersion (0)
-- If you're attempting to run an unlifting function outside of the scope of effects it captures, have a look at UnliftingStrategy (SeqForkUnlift).
-- CallStack (from HasCallStack):
--   error, called at src/Effectful/Internal/Env.hs:438:5 in effectful-core-2.5.0.0-8f0f88000fb1b321565aecfd7dab29776c11a03e795a51044aef3b74f0775084:Effectful.Internal.Env
--   getLocation, called at src/Effectful/Internal/Env.hs:390:14 in effectful-core-2.5.0.0-8f0f88000fb1b321565aecfd7dab29776c11a03e795a51044aef3b74f0775084:Effectful.Internal.Env
--   getEnv, called at src/Effectful/Internal/Monad.hs:621:35 in effectful-core-2.5.0.0-8f0f88000fb1b321565aecfd7dab29776c11a03e795a51044aef3b74f0775084:Effectful.Internal.Monad
--   getStaticRep, called at src/Effectful/State/Static/Local.hs:91:14 in effectful-core-2.5.0.0-8f0f88000fb1b321565aecfd7dab29776c11a03e795a51044aef3b74f0775084:Effectful.State.Static.Local
--   get, called at /home/tom//test28.hs:23:22 in fake-package-0-inplace:Main
foo = runEff $ do
  r <- evalState (0 :: Int) $ do
    withRunInIO $ \runInIO -> do
      pure (runInIO (get @Int))

  liftIO r

I think ultimately we have to declare that the MonadUnliftIO instance/withEffToIO_ are unsafe :(

[tomjaguarpaw]

It gets worse. Even "mapIO" is not safe:

mapIO ::  (e :> es) => IOE e ->  (IO r -> IO r) -> (Eff es r -> Eff es r)

It allows us to write bad, which allows us to write exampleBad. But it gets worse yet! "mapIOPoly" is not safe!

mapIOPoly :: (e :> es) => IOE e -> (forall r. IO r -> IO r) -> (forall r. Eff es r -> Eff es r)

It allows us to write worse, which allows us to write exampleWorse. Not even parametricity can save us. At this point I am convinced that there is no general safe way to convert IO "bracketing functions" to Bluefin bracketing functions safely.

{-# LANGUAGE GHC2021 #-}
{-# LANGUAGE LambdaCase #-}

import Bluefin.Eff (Eff, (:>))
import Bluefin.IO (IOE, effIO, runEff, withEffToIO_)
import Bluefin.System.IO (hPutChar, withFile)
import Data.IORef (IORef, newIORef, readIORef, writeIORef)
import System.IO (IOMode (ReadMode))

mapIO ::
  (e :> es) =>
  IOE e ->
  (IO r -> IO r) ->
  (Eff es r -> Eff es r)
mapIO io k eff = withEffToIO_ io $ \effToIO -> k (effToIO eff)

bad ::
  (e :> es) =>
  IOE e ->
  Eff es (IO ()) ->
  Eff es (IO ())
bad io = mapIO io (\m -> pure (m *> pure ()))

-- ghci> exampleBad
-- *** Exception: /dev/null: hPutChar: illegal operation (handle is closed)
exampleBad :: IO ()
exampleBad = runEff $ \io -> do
  r <- withFile io "/dev/null" ReadMode $ \h -> do
    bad io (hPutChar h 'X' *> pure (pure ()))

  effIO io r

mapIOPoly ::
  (e :> es) =>
  IOE e ->
  (forall r. IO r -> IO r) ->
  (forall r. Eff es r -> Eff es r)
mapIOPoly io k eff = mapIO io k eff

worse ::
  (e :> es) =>
  IOE e ->
  IORef (IO ()) ->
  Eff es () ->
  Eff es ()
worse io ref =
  mapIOPoly io $ \m -> do
    r <- m
    writeIORef ref (m *> pure ())
    pure r

-- ghci> exampleWorse
-- *** Exception: /dev/null: hPutChar: illegal operation (handle is not open for writing)
exampleWorse :: IO ()
exampleWorse = runEff $ \io -> do
  ref <- effIO io (newIORef (pure ()))

  withFile io "/dev/null" ReadMode $ \h -> do
    worse io ref (hPutChar h 'X')

  m <- effIO io (readIORef ref)
  effIO io m

[tomjaguarpaw]

Here's an even more direct bad function, smuggle, written using mapIOPoly:

{-# LANGUAGE GHC2021 #-}
{-# LANGUAGE LambdaCase #-}

import Bluefin.Eff (Eff, (:>))
import Bluefin.IO (IOE, effIO, runEff, withEffToIO_)
import Bluefin.System.IO (hPutChar, withFile)
import Data.IORef (newIORef, readIORef, writeIORef)
import System.IO (IOMode (ReadMode))

mapIO ::
  (e :> es) =>
  IOE e ->
  (IO r -> IO r) ->
  (Eff es r -> Eff es r)
mapIO io k eff = withEffToIO_ io $ \effToIO -> k (effToIO eff)

mapIOPoly ::
  (e :> es) =>
  IOE e ->
  (forall r. IO r -> IO r) ->
  (forall r. Eff es r -> Eff es r)
mapIOPoly io k eff = mapIO io k eff

smuggle ::
  (e :> es, e :> es') =>
  IOE e ->
  -- | @e@
  Eff es () ->
  -- | Runs @e@, but also returns it coerced to a different effect
  -- type.  Very bad!
  Eff es (Eff es' ())
smuggle io e = do
  ref <- effIO io (newIORef (pure ()))
  mapIOPoly
    io
    ( \m -> do
        writeIORef ref (effIO io (m *> pure ()))
        m
    )
    e
  effIO io (readIORef ref)

-- ghci> exampleSmuggle
-- *** Exception: /dev/null: hPutChar: illegal operation (handle is not open for writing)
exampleSmuggle :: IO ()
exampleSmuggle = runEff $ \io -> do
  a <- withFile io "/dev/null" ReadMode $ \h -> do
   smuggle io (hPutChar h 'X')

  a

[tomjaguarpaw]

Actually, effectful is subject to this:

{-# LANGUAGE GHC2021 #-}

import Effectful
  ( Limit (Unlimited),
    Persistence (Ephemeral),
    UnliftStrategy (ConcUnlift),
    liftIO,
    runEff,
    withEffToIO
  )
import Effectful.FileSystem.IO
  ( IOMode (ReadMode),
    hIsEOF,
    runFileSystem,
    withFile
  )

-- ghci> example
-- *** Exception: /dev/null: hIsEOF: illegal operation (handle is closed)
example :: IO Bool
example = runEff $ do
  r <- runFileSystem $ do
    withFile "/dev/null" ReadMode $ \h -> do
      withEffToIO (ConcUnlift Ephemeral Unlimited) $ \effToIO -> do
        pure (effToIO (hIsEOF h))

  liftIO r