Proposal: give Ptr a nominal role

[Matthew Pickering]

Making `Ptr` (and ForeignPtr) have a nominal role would have prevented
recent bugs where it was possible to coerce Vectors between any types.

See: https://github.com/haskell/vector/pull/224
and: https://phabricator.haskell.org/D4941
On Tue, Oct 30, 2018 at 5: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