Interface for deep freezing in GHC

deep_freeze.hs

-- This is a hypothetical API that extends the ST with an alternative to
-- runST. The alternative can be described as a "deep freeze". It calls
-- performs an in-place freeze on many variables at once. Surprisingly,
-- this API is safer than the API provided by the existing functions
-- that unsafely freeze mutable arrays.
--
-- The first step is merging lifted and unlifted arrays into a single
-- data type. Instead of:

data FooArray# :: TYPE 'UnliftedRep
data MutableFooArray# :: Type -> TYPE 'UnliftedRep

-- We would have:

data Mutability = Mutable Type | Immutable
data VariableFooArray# :: Mutability -> Type 'UnliftedRep
type role VariableFooArray# representational

-- That role will be important later. Notice that users cannot
-- actually use it to do any coercing, but our extension to
-- runST needs this role for safety. For backwards compatibility,
-- we may recover the original types in GHC.Exts using UnliftedNewtypes:

newtype FooArray# = FooArray# (VariableFooArray# 'Immutable)
newtype MutableFooArray# s = FooArray# (VariableFooArray# ('Mutable s))

-- Now that the groundwork has been laid, let's get to the meat of this
-- proposal. For clarity, I'm going to use lifted wrappers for the
-- rest of this instead of putting state tokens and hashes everywhere.

data Chain :: Type -> Type -> Type

push :: VariableFooArray ('Mutable s) -> Chain r s -> ST s (VariableFooArray ('Mutable r))
recover :: Chain r s -> VariableFooArray ('Mutable r) -> VariableFooArray ('Mutable s)

-- A chain is just an append-only (the user cannot inspect the elements)
-- list of mutable things. Appending a mutable array to a chain provides
-- the user with an alias that has the chain's type variable. We
-- are always able to recover the original type variable from the chain's
-- type variable. Under the hood, recover is a no-op. The chain argument
-- is not needed for code generation, only for type safety. Although it
-- is possible for the user to add the same mutable array to a chain
-- twice, doing so does not impact the correctness of the interface.
-- (It does mildly degrade performance.)
--
-- And now the final part of the interface, using QuantifiedConstraints
-- to bring a representational-role-check under the mantle of the type
-- system:

runFreezeST :: forall (f :: Mutability -> Type).
     (forall a b. Coercible a b => Coercible (f a) (f b))
  => (forall r s. Chain r s -> ST s (f ('Mutable r)))
  -> f 'Immutable

-- The typeclass constraint would not actually be used either by
-- a user-space implementation or a built-in implementation.
-- Notice that running and freezing are done together. These
-- have to be done together for this to work correctly. This
-- operation walks every mutable array in the chain and freezes
-- all of them.
--
-- After UnliftedNewtypes lands, it should be possible to
-- implement this whole thing in user space. It requires a
-- lot of unsafe coercions, but the user-facing interface
-- should be completely safe.