Re: Proposal: give Ptr a nominal role

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 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 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@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries