<div dir="auto">Are you sure that modification of Carter's will compile?</div><br><div class="gmail_quote"><div dir="ltr">On Tue, Oct 30, 2018, 2:20 PM Eric Mertens <<a href="mailto:emertens@gmail.com">emertens@gmail.com</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div style="word-wrap:break-word;line-break:after-white-space"><br><div><br><blockquote type="cite"><div>On Oct 30, 2018, at 11:18 AM, David Feuer <<a href="mailto:david.feuer@gmail.com" target="_blank" rel="noreferrer">david.feuer@gmail.com</a>> wrote:</div><br class="m_3276582839067241509Apple-interchange-newline"><div><div dir="auto"><div>Your simpler version won't even compile, </div></div></div></blockquote></div><br><div>Here are the two versions edited so that both can compile (they needed some tweaks) for those playing along at home:</div><div><br></div><div><div><div><font face="Courier">{-# Language PatternSynonyms, FlexibleContexts, RoleAnnotations, RankNTypes, MagicHash #-}</font></div><div><font face="Courier">module Help where</font></div><div><font face="Courier"><br></font></div><div><font face="Courier">import GHC.Exts hiding (Ptr)</font></div><div><font face="Courier">import Data.Type.Coercion</font></div><div><font face="Courier">import Unsafe.Coerce</font></div><div><font face="Courier"><br></font></div><div><font face="Courier">{- Carter's version</font></div><div><font face="Courier">data Ptr a = Ptr Addr#</font></div><div><font face="Courier">type role Ptr nominal</font></div><div><font face="Courier"><br></font></div><div><font face="Courier"><br></font></div><div><font face="Courier">castPtr :: Ptr a -> Ptr b</font></div><div><font face="Courier">castPtr = unsafeCoerce</font></div><div><font face="Courier"><br></font></div><div><font face="Courier">ptrCoercible</font></div><div><font face="Courier">  :: (forall a b. Coercible (Ptr a) (Ptr b) => r)</font></div><div><font face="Courier">  -> r</font></div><div><font face="Courier">ptrCoercible r = r</font></div><div><font face="Courier"><br></font></div><div><font face="Courier">ptrCoercion :: Coercion (Ptr a) (Ptr b)</font></div><div><font face="Courier">ptrCoercion = Coercion</font></div><div><font face="Courier">-}</font></div><div><font face="Courier"><br></font></div><div><font face="Courier">data Addr = Addr_ Addr#</font></div><div><font face="Courier"><br></font></div><div><font face="Courier">newtype Ptr a = Ptr_ Addr</font></div><div><font face="Courier">type role Ptr nominal</font></div><div><font face="Courier"><br></font></div><div><font face="Courier">pattern Ptr :: Addr# -> Ptr a</font></div><div><font face="Courier">pattern Ptr a# = Ptr_ (Addr_ a#)</font></div><div><font face="Courier"><br></font></div><div><font face="Courier">castPtr :: Ptr a -> Ptr b</font></div><div><font face="Courier">castPtr (Ptr a) = Ptr a</font></div><div><font face="Courier"><br></font></div><div><font face="Courier">ptrCoercible</font></div><div><font face="Courier">  :: (forall a b. Coercible (Ptr a) (Ptr b) => r)</font></div><div><font face="Courier">  -> r</font></div><div><font face="Courier">ptrCoercible r = r</font></div><div><font face="Courier"><br></font></div><div><font face="Courier">ptrCoercion :: Coercion (Ptr a) (Ptr b)</font></div><div><font face="Courier">ptrCoercion = Coercion</font></div></div></div><div><br></div></div></blockquote></div>