Proposal: give Ptr a nominal role

[Carter Schonwald]

so i'm taking a look at the current docs / definition in base (and  i'm
testing testing out seeing what happens if we changed the role and just
build ghc and base as is)
https://github.com/ghc/ghc/blob/82a716431cc680392e332bc2b1a1fd0d7faa4cd8/libraries/base/GHC/Ptr.hs#L37-L57

i'm replicating the docs below:

but the important detail is the phantom role in the current code is
deliberate ...
because no guarantees are made about the relationship between the choice in
type parameter ( which putatively will always  have the same heap rep in
haskell land)
and the representation at the other side of the pointer.

a good example might be Ptr Char.  Is this a single location of a 32bit /
utf32 code point, or an array of utf8 code points or utf32 code points?
is it null terminated vs there being an extra sequence length? These are
all valid things that can be happening. And

-- Data pointers.
-- The role of Ptr's parameter is phantom, as there is no relation between
-- the Haskell representation and whathever the user puts at the end of the
-- pointer. And phantom is useful to implement castPtr (see #9163)
-- redundant role annotation checks that this doesn't change
type role Ptr phantom
data Ptr a = Ptr Addr#
deriving ( Eq -- ^ @since 2.01
, Ord -- ^ @since 2.01
)
-- ^ A value of type @'Ptr' a@ represents a pointer to an object, or an
-- array of objects, which may be marshalled to or from Haskell values
-- of type @a at .
--
-- The type @a@ will often be an instance of class
-- 'Foreign.Storable.Storable' which provides the marshalling operations.
-- However this is not essential, and you can provide your own operations
-- to access the pointer. For example you might write small foreign
-- functions to get or set the fields of a C @struct at .

unrelatedly, while i'm not familiar with how to use modern coercible bits,
the folllowing subset of what i mentioned earlier seems to work fine

{-# Language PatternSynonyms, FlexibleContexts, RoleAnnotations,
RankNTypes, MagicHash #-}

module Ptr where


import GHC.Exts hiding (Ptr)
import Data.Type.Coercion
import Unsafe.Coerce


data 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


On Tue, Oct 30, 2018 at 2:24 PM Eric Mertens <emertens at gmail.com> wrote:

> No, it won’t compile, but it at least loads far enough to generate the
> right error that you can’t coerce data like that. I thought about sending a
> clarifying email afterward but I didn’t want to spam the list with a second
> message. The point is that all the syntactic errors are cleaned up to the
> point that one can actually play with the code now.
>
> > On Oct 30, 2018, at 11:22 AM, David Feuer <david.feuer at gmail.com> wrote:
> >
> > Are you sure that modification of Carter's will compile?
> >
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/libraries/attachments/20181101/b1147555/attachment.html>