Proposal: give Ptr a nominal role

[Carter Schonwald]

hey David, heres a simpler version (attached below), that I think
accomplishes the same goal.

One issue, that would need to be evaluated empirically: how many type class
instances would break from this change? Would any?

is it Storable instances that are an issue, or things that use storable?

what safety is gained vs what is impacted? (i guess i mostly just wanna
understand what would be broken by this change, a lot of code in the wild
uses pointers for systems integrations)


    newtype Ptr a = Ptr  Addr#
    type role Ptr nominal


    castPtr :: Ptr a -> Ptr b
    castPtr = unsafeCoerce

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

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


On Tue, Oct 30, 2018 at 1:57 PM David Feuer <david.feuer at gmail.com> wrote:

> 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.
> _______________________________________________
> Libraries mailing list
> Libraries at haskell.org
> http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/libraries/attachments/20181030/a115c9fd/attachment.html>