Proposal: give Ptr a nominal role

[David Feuer]

Your simpler version won't even compile, and it gives Ptr the wrong kind.

I don't *think* anything breaks at all, unless it's using coerce on Ptr
types (the fix is easy). Note in particular that Ptr doesn't have a Generic
instance.

The extra safety is at the Storable use sites. If you have some type that
has a Ptr buried in it somewhere, coerce it to something else, and then
call a function that uses a (different) Storable instance for that field,
you're in trouble. With this change, the compiler will let you know that
there's a buried Ptr in there and (after verifying that it's okay) you can
introduce the coercibility explicitly to explain that it's fine.

On Tue, Oct 30, 2018, 2:06 PM Carter Schonwald <carter.schonwald at gmail.com>
wrote:

> 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/aa2c19ae/attachment.html>