Proposal: give Ptr a nominal role

[David Feuer]

Currently, we have

data Ptr a = Ptr Addr#
type role Ptr phantom

This is weird: accidentally coercing a pointer to a different type is very
bad. The only reason Ptr has this role is that without it, castPtr and such
may not be free or will involve unsafe coercions.

Thankfully, we have enough power to fix this now.

    data Addr = Ptr_ Addr#

    newtype Ptr a = Ptr_ Addr
    type role Ptr nominal

    pattern Ptr :: Addr# -> Ptr a
    pattern Ptr a# = Ptr_ (Addr a#)

    castPtr :: Ptr a -> Ptr b
    castPtr (Ptr a) = Ptr a

    ptrCoercible
      :: ((forall a b. Coercible (Ptr a) (Ptr b)) => r)
      -> r
    ptrCoercible r = r

    ptrCoercion :: Coercion (Ptr a) (Ptr b)
    ptrCoercion = Coercion

I propose that we do this.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/libraries/attachments/20181030/fe776936/attachment.html>