&'a mut T in Linear Haskell?

Data.Temporal.hs

{-# LANGUAGE EmptyDataDeriving #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE NoImplicitPrelude #-}
{-# LANGUAGE UnboxedTuples #-}
{-# LANGUAGE MagicHash #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE LinearTypes #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE QualifiedDo #-}
module Data.Temporal where
import Data.Temporal.Unlifted
import Type.Reflection (Typeable)
import Prelude.Linear

data Mut s a = Mut (MVar# a)

data After a deriving (Typeable)

yield :: a -> Mut s a %1-> Mut (After s) a
yield a (Mut mv) = Mut (putMVar# a (ensureEmpty# mv))

put :: a -> Mut s a %1-> Mut s a
put a (Mut mv) = Mut (putMVar# a (ensureEmpty# mv))

read :: Mut s a %1-> (Ur a, Mut s a)
read (Mut mv) = wrap (readMVar# mv) 
  where
    wrap :: (# Ur a, MVar# a #) %1-> (Ur a, Mut s a)
    wrap (# ret, mv' #) = (ret, Mut mv')

data TemporalOps s a x where
  AndThen 
    :: (Mut s a %1-> (Mut (After s) a, Ur b)) 
    -> (Mut (After s) a %1-> b -> Ur x)
    -> TemporalOps s a x

runOnce
  :: forall a b. (forall s. Mut s a %1-> Ur b) -> Ur b
runOnce f = 
  withEmptyMVar# $ \mv -> f (Mut mv)

runTemporalOps :: forall a x. (forall s. TemporalOps s a x) -> Ur x
runTemporalOps flow = runOnce go
  where
    go :: forall s. Mut s a %1-> Ur x
    go mut = case flow of
      before `AndThen` after -> 
        before mut & \case
          (mut', Ur b) -> after mut' b

Data.Temporal.Unlifted.hs

{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE UnboxedTuples #-}
{-# LANGUAGE MagicHash #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE UnliftedNewtypes #-}
{-# LANGUAGE NoImplicitPrelude #-}
{-# LANGUAGE LinearTypes #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE QualifiedDo #-}
module Data.Temporal.Unlifted where
import GHC.Exts (RealWorld)
import Prelude.Linear
import qualified GHC.Exts as GHC
import qualified Unsafe.Linear as Unsafe
import qualified Prelude as Prel

newtype MVar# a = MVar# { runSink :: GHC.MVar# RealWorld a }

putMVar# :: a -> MVar# a %1-> MVar# a
{-# NOINLINE putMVar# #-}
putMVar# (x :: a) = Unsafe.toLinear go
  where
    go :: MVar# a -> MVar# a
    go (MVar# mv#) = case GHC.runRW# (GHC.putMVar# mv# x) of
      _ -> MVar# mv#

tryReadMVar# :: MVar# a %1-> (# Ur (Maybe a), MVar# a #)
{-# NOINLINE tryReadMVar# #-}
tryReadMVar# = Unsafe.toLinear go
  where
    go :: MVar# a -> (# Ur (Maybe a), MVar# a #)
    go (MVar# mv) = case GHC.runRW# (GHC.tryReadMVar# mv) of
      (# _, 1#, a #) -> (# Ur (Just a), MVar# mv #)
      (# _, _, _ #) -> (# Ur Nothing, MVar# mv #)

tryTakeMVar# :: MVar# a %1-> (# Ur (Maybe a), MVar# a #)
{-# NOINLINE tryTakeMVar# #-}
tryTakeMVar# = Unsafe.toLinear go
  where
    go :: MVar# a -> (# Ur (Maybe a), MVar# a #)
    go (MVar# mv) = case GHC.runRW# (GHC.tryTakeMVar# mv) of
      (# _, 1#, a #) -> (# Ur (Just a), MVar# mv #)
      (# _, _, _ #) -> (# Ur Nothing, MVar# mv #)

ensureEmpty# :: MVar# a %1-> MVar# a
{-# NOINLINE ensureEmpty# #-}
ensureEmpty# = Unsafe.toLinear go
  where
    go :: MVar# a -> MVar# a
    go (MVar# mv) = case GHC.runRW# (GHC.tryTakeMVar# mv) of
      (# _, _, _ #) -> MVar# mv

readMVar# :: MVar# a %1-> (# Ur a, MVar# a #)
{-# NOINLINE readMVar# #-}
readMVar# = Unsafe.toLinear go
  where
    go :: MVar# a -> (# Ur a, MVar# a #)
    go (MVar# mv) = case GHC.runRW# (GHC.readMVar# mv) of
      (# _, a #) -> (# Ur a, MVar# mv #)

withEmptyMVar# :: (MVar# a %1-> Ur b) %1-> Ur b
{-# NOINLINE withEmptyMVar# #-}
withEmptyMVar# (f :: MVar# a %1-> Ur b) =
  let new :: MVar# a
      new = GHC.runRW# Prel.$ \st ->
        case GHC.newMVar# st of
          (# _, mv #) -> MVar# mv
  in f new