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