Re: Proposal: give Ptr a nominal role

Are you sure that modification of Carter's will compile? On Tue, Oct 30, 2018, 2:20 PM Eric Mertens wrote:

On Oct 30, 2018, at 11:18 AM, David Feuer 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