add GEq instnaces for IORef and STRef

[sorki]

PoC, taken from hnix.

[phadej]

Because IORef is representational in it's argument these instances are unsound use of unsafeCoerce:

{-# LANGUAGE GADTs #-}

import Data.GADT.Compare
import Data.GADT.Instances
import Data.IORef
import Data.Coerce
import Data.Type.Equality

newtype Int2 = Int2 Int

wrong :: Int ~ Int2 => a
wrong = error "impossible"

main :: IO ()
main = do
    ref  <- newIORef (1 :: Int)
    let ref' :: IORef Int2
        ref' = coerce ref

    case geq ref ref' of
        Nothing -> putStrLn "ok"
        Just r  -> gcastWith r wrong

{-

*Main> main
*** Exception: impossible
CallStack (from HasCallStack):
  error, called at Bad.hs:12:9 in main:Main

-}

[Ericson2314]

Can we wrap the type parameter in something the forces a nominal role?

[phadej]

If you can wrap IORefs, you could wrap already coerced references. One would need nominal IORef clone (and that package could depend on some, not other way around).

[Ericson2314]

data MakeNominal a = MkNominal {-# UNPACK #-} !a
type role MakeNominal nominal

newtype NominalORef a = MkNominalORef (IORef (MakeNominal a))

If you want that in a separate library, I would instead advocate solving the problem for real, with a CPP'd superclass for GEq:

#if not too old GHC
class GCoercible f where
  gcoercible :: f a -> f b -> Maybe (a `Coersion` b)
  default gcoercible :: GEq f =>  f a -> f b -> Maybe (a `Coersion` b)
  gcoercible x y = (\Refl -> Coercion) <$> geq x y
#endif

class
#if not too old GHC
  GCoercible f
#else
  ()
#endif
  => GEq f where

[phadej]

@Ericson2314 if MkNominal is public constructor, it doesn't change anything:

{-# LANGUAGE EmptyCase         #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs             #-}
{-# LANGUAGE RoleAnnotations   #-}
{-# LANGUAGE TypeOperators     #-}
{-# OPTIONS_GHC -Wall #-}

import Data.Coerce
import Data.GADT.Compare
import Data.GADT.Instances
import Data.IORef
import Data.Type.Equality
import Unsafe.Coerce       (unsafeCoerce)

newtype Int2 = Int2 Int

wrong :: Int :~: Int2 -> a
wrong _ = error "impossible"

-- | If the constructor is public:
data MakeNominal f a = MkNominal {-# UNPACK #-} !(f a)
type role MakeNominal nominal nominal

instance GEq (MakeNominal IORef) where
  MkNominal a `geq` MkNominal b = if a == unsafeCoerce b then Just $ unsafeCoerce Refl else Nothing

main :: IO ()
main = do
    ref  <- newIORef (1 :: Int)
    let ref' :: IORef Int2
        ref' = coerce ref

    let nom  = MkNominal ref
        nom' = MkNominal ref'

    case geq nom nom' of
        Nothing -> putStrLn "ok"
        Just r  -> wrong r


{-

*Main> main
*** Exception: impossible
CallStack (from HasCallStack):
  error, called at Bad.hs:12:9 in main:Main

-}

As I mentioned. You need nominal (opaque) IORef to prevent such breakages. Yet if you make such library, it could depend on some.

---

There could be a variant of GEq :

class GCoercible f where
    gIsCoercible :: f a -> f b -> Maybe (Coercion a b)

then IORef could be instance of that one. I don't know if it would be usable for hnix.

[Ericson2314]

@phadej

1. That's different than how I used MkNominal. With mine, coercing the underlying IORef is no use.

2. Looks like we both arrived at GCoercible? How do you feel about adding that class, and my conditional superclass?

[Ericson2314]

#46 adds GCoercible.

---

@sorki Also, you could make a library that makes NominalORef. @phadej's example blows up because one is making the same IORef into two nominal ones. This is just like the "value restriction" which is why newIORef must be monadic in the first place!

If a newNominalIORef is the only (safe) way to make a NominalORef, then there is no issue, so the NominalORef library could do that.

---

Between those two things I think this can be closed.