Re: Ptr type

I think Ptr should almost certainly be representational, as it is a case where the actual underlying value is the same, but what it points to is not (I'll ignore castPtr here for a second). This makes me think of something I talked about before with Andres - in general, phantom roles seem somewhat dangerous, and I kind of wonder if they should be inferred by default. Often you see some code along the lines of: ---------------------------------- module A ( Bar, newBarInt ) where data Bar a = Bar Int newBarInt :: Int -> Bar Int --------------------------------- where A is exported to the client and the module boundary enforces some restrictions on 'Bar', like what types we can instantiate 'Bar a' to (the example is dumb but bear with me). In the above example, I believe the `a` in `Bar a` would be inferred at phantom role. The question I have is: what legitimate case would there be for phantom roles like this? Such usage of phantom type parameters seems very common, but in almost *all* cases I can't think of a reason why I would ever want a user to be allowed to `coerce` away the type information, if the `a` parameter was phantom. It seems like in the above example, I would almost certainly want `a` to be representational instead. What other cases exist for legitimate phantom roles such as this where we want this inference? I wonder if instead we should require an explicit role annotation for phantoms in this case - not the other way around. Ptr is a similar story - by default it would maybe seem reasonable to be phantom, but that seems like an especially grievous error, given we don't want people to `poke` incorrect values in or something (again, ignoring castPtr for a second, but I think the general idea holds.) On Tue, Jun 3, 2014 at 7:24 AM, Richard Eisenberg wrote:

It seemed clear to me that Ptr *should* be representational, thinking that we don't want to coerce a `Ptr Int` to a `Ptr Bool`. I don't see any reason why this couldn't be changed.

Why is Ptr a `data` not a `newtype`? If it were a newtype, we could keep the role annotation and use `coerce` internally, according to the updated Coercible solver.

However, it is crucial that FunPtr have a representational argument, as normaliseFfiType' depends on this fact. There is a brief comment in TcForeign, but clearly more comments are necessary. Will do shortly. If we want to change FunPtr's role, normaliseFfiType' would have to be updated, too, but it shouldn't be hard.

More comments in the code later today.

Richard

On Jun 3, 2014, at 7:13 AM, Simon Peyton Jones wrote:

Richard

In GHC.Ptr we see

type role Ptr representational data Ptr a = Ptr Addr# deriving (Eq, Ord)

with no comments. Why is Ptr representational?

In the same module we have castPtr, which unpacks and repacks a Ptr. If Ptr was phantom, we could use coerce. And that in turn would actually make a lot of code more efficient – there are lots of calls to castPtr.

Simon

_______________________________________________ ghc-devs mailing list ghc-devs@haskell.org http://www.haskell.org/mailman/listinfo/ghc-devs

-- Regards, Austin Seipp, Haskell Consultant Well-Typed LLP, http://www.well-typed.com/