Add roles declarations to allow safe coercions

[kl0tl]

This allows terms of type Object a and STObject r a to be coerced to type Object b and STArray r b when Coercible a b holds, hence allowing the zero cost coerce instead of map wrap and map unwrap to introduce and eliminate newtypes under objects and ST objects for instance.

I couldn’t think of a case where a phantom roled region is an issue but in doubt I preferred to keep it nominal.

[JordanMartinez]

I know you've been doing nominal in situations like this, but shouldn't this be phantom? At the end of the day, Region is a skolem type, so it shouldn't matter what type it gets coerced to, correct?

Also, I'm fine with leaving this as nominal and changing it to phantom in a later release.

[hdgarrood]

I don't see how you get from Region being a skolem type to it not mattering what it gets coerced to, that line of argument doesn't make sense to me. I think nominal is correct here: I think it's possible that if this were phantom then you could coerce an STObject in a way that allows the mutable reference to escape its scope. At least, we would need to prove that this wouldn't be an issue before being able to justify any role other than nominal here.

[kl0tl]

I don’t understand what could go wrong if we could coerce between two arbitrary regions, until then I would be reluctant to relax the role. That’s also consistent with Haskell:

module Example where

import GHC.ST (ST)
import Data.Coerce (coerce)

newtype N a = N a

example :: ST s0 a -> ST s1 (N a)
example = coerce

Example.hs:9:11: error:
    • Couldn't match type ‘s0’ with ‘s1’ arising from a use of ‘coerce’
      ‘s0’ is a rigid type variable bound by
        the type signature for:
          example :: forall s0 a s1. ST s0 a -> ST s1 (N a)
        at Example.hs:8:1-33
      ‘s1’ is a rigid type variable bound by
        the type signature for:
          example :: forall s0 a s1. ST s0 a -> ST s1 (N a)
        at Example.hs:8:1-33
    • In the expression: coerce
      In an equation for ‘example’: example = coerce
    • Relevant bindings include
        example :: ST s0 a -> ST s1 (N a) (bound at Example.hs:9:1)
  |
9 | example = coerce
  |           ^^^^^^

[hdgarrood]

Here's an example showing why ST ref types need to have nominal roles for their region parameters:

module Main where

import Prelude
import Effect (Effect)
import Control.Monad.ST (ST)
import Control.Monad.ST as ST
import Control.Monad.ST.Ref (STRef)
import Control.Monad.ST.Ref as STRef
import Effect.Console as Console
import Safe.Coerce

globalRef :: forall r. STRef r Int
globalRef = ST.run do
  r <- STRef.new 0
  pure (coerce r)

next :: Unit -> Int
next _ = ST.run do
  r <- STRef.read globalRef
  _ <- STRef.write (r + 1) globalRef
  pure (r + 1)

main :: Effect Unit
main = do
  Console.log (show (next unit))
  Console.log (show (next unit))
  Console.log (show (next unit))

which produces the output

1
2
3

showing that the next function is not pure.

[kl0tl]

Oh right, the regions r1 and r2 in Control.Monad.ST.Ref.new :: forall a r1 r2. a -> ST r1 (STRef r2 a) have to be the same or the ref can escape its mutable scope. Thanks a lot! That’s quite clear now.

[JordanMartinez]

Ah... Well, that settles that! Nice example @hdgarrood!

[JordanMartinez]

@kl0tl CI was failing because this PR was targeting a non-master branch. Can you update this PR to only keep your roles declaration commit?

[kl0tl]

I’ve rebased the commit on top of master!