Violating memory safety with Haskell's value restriction

Links
2

Thanks! Very clear, well-written and interesting article. Does that mean that this definition from linear-base is unsafe?

I attempted to use your same trick to derive something unsafe, but I couldn’t get it to work. It don’t know whether it doesn’t work because of some issue with linear lets, or Ur, or something else, and whether the “issue” is intended (and is a theoretical means of preventing unsafety) or it’s unintended and can be worked around.

Not working linear example 
{-# LANGUAGE UnboxedTuples #-}
{-# LANGUAGE LinearTypes #-}
{-# LANGUAGE QualifiedDo #-}
{-# LANGUAGE ImpredicativeTypes #-}
{-# LANGUAGE MagicHash #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE GHC2021 #-}
{-# LANGUAGE BlockArguments #-}
{-# LANGUAGE ImportQualifiedPost #-}

import System.IO.Linear
import Control.Functor.Linear qualified as L
import Control.Functor.Linear hiding (state)
import Prelude hiding (IO, (<$>), (>>=), pure, Monad)
import GHC.Exts
import System.IO.Linear
import Data.IORef (IORef)
import Data.Unrestricted.Linear

class (Monad m) => MonadGen m where
    generalize :: forall f. (forall a. m (f a)) -> m (forall a. f a)

data BoxedState s = BoxedState {state :: State# s}

liftState :: (# State# s, b #) %1 -> (BoxedState s, b)
liftState (# s, b #) = (BoxedState s, b)

myGeneralize :: forall f. (forall a. IO (f a)) -> IO (forall a. f a)
myGeneralize m = do
        let (IO f) = m
        IO \s -> do
            let (!boxedState, !result) = liftState (f s)
            let BoxedState{state} = boxedState
            (# state, result #)

instance MonadGen IO where
    generalize = myGeneralize

newtype MaybeRef a = MaybeRef (IORef (Maybe a))

unsafeCoerceIO :: forall a b. a -> IO b
unsafeCoerceIO x = L.do
    maybeRef <- generalize (newIORef Nothing)
    let MaybeRef ref = maybeRef
    writeIORef ref (Just x)
    readIORef ref >>= \case
        Ur (Just y) -> pure y
        Ur Nothing -> error "unreachable"
1 Like