
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

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
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

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
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/

I've moved this thread to https://ghc.haskell.org/trac/ghc/ticket/9163
| -----Original Message-----
| From: mad.one@gmail.com [mailto:mad.one@gmail.com] On Behalf Of Austin
| Seipp
| Sent: 03 June 2014 14:22
| To: Richard Eisenberg
| Cc: Simon Peyton Jones; ghc-devs@haskell.org
| Subject: 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
participants (3)
-
Austin Seipp
-
Richard Eisenberg
-
Simon Peyton Jones