Proposal: give Ptr a nominal role

[David Feuer]

Are you sure that modification of Carter's will compile?

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

>
>
> 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/2f9813e0/attachment.html>