Re: Proposal: give Ptr a nominal role

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