Proposal: give Ptr a nominal role

[Eric Mertens]

> On Oct 30, 2018, at 11:18 AM, David Feuer <david.feuer at gmail.com> wrote:
> 
> Your simpler version won't even compile, 

Here are the two versions edited so that both can compile (they needed some tweaks) for those playing along at home:

{-# Language PatternSynonyms, FlexibleContexts, RoleAnnotations, RankNTypes, MagicHash #-}
module Help where

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

{- Carter's version
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

ptrCoercion :: Coercion (Ptr a) (Ptr b)
ptrCoercion = Coercion
-}

data Addr = Addr_ 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

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/libraries/attachments/20181030/5004bea7/attachment.html>