<html><head><meta http-equiv="Content-Type" content="text/html charset=utf-8"></head><body style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space;" class=""><div class="">I don't think that wiki reference is really about this problem.</div><div class=""><br class=""></div><div class="">Instead, I think that we'd need Constraint# to be able to offer users ~# and ~R#. The problem, then, is that there is no answer to this question: Constraint is to Type as Constraint# is to what? Currently, if ~# and ~R# are the only two generators of Constraint#, then Constraint# is like TYPE (TupleRep '[]). But I think wiring that in would be short-sighted.</div><div class=""><br class=""></div><div class="">Instead, this road leads to CONSTRAINT :: RuntimeRep -> Type, which is like TYPE. Today's Constraint would be CONSTRAINT LiftedRep. And we would have (~#), (~R#) :: forall k1 k2. k1 -> k2 -> CONSTRAINT (TupleRep '[]). In the Glorious Future, we'll have CONSTRAINT ~R TYPE, but we're not there yet. </div><div class=""><br class=""></div><div class="">This all feel like the Right Answer to me, but it's unclear if we should start down this road before we have roles in kinds.</div><div class=""><br class=""></div><div class="">Richard</div> <br class=""><div><blockquote type="cite" class=""><div class="">On Sep 5, 2018, at 10:54 AM, Ryan Scott <<a href="mailto:ryan.gl.scott@gmail.com" class="">ryan.gl.scott@gmail.com</a>> wrote:</div><br class="Apple-interchange-newline"><div class=""><div dir="ltr" class=""><div dir="ltr" class=""><div dir="ltr" class="">> We could utterly lie and say<br class="">> <br class="">>               data Coercion a b where<br class="">> <br class="">>                   Coercion :: Coercion a a<br class="">> <br class="">>  <br class="">> <br class="">> That would generate the right bits in in the .o file, and we’d totally ignore the .hi file.  Gruesome but I think it would work.</div><div dir="ltr" class=""><br class=""></div><div class="">This was precisely what I had in mind. We already perform this trick for several things defined in ghc-prim (e.g., the (~) and (~~) classes), so this would just be another example of that.</div><div class=""><br class=""></div><div class=""><font size="2" class="">> <span class="">But rather than all this circumlocution, 
why don’t we just make it possible to write ~# and ~R# directly.  Even 
if we dodge the need right now, it’ll surely come back.</span></font><br class=""></div><div class=""><br class=""></div><div class="">Hah, the reason David is suggesting his idea in the first place is to avoid having to do this! My understanding is that making it possible to write (~#) and (~R#) directly would involve quite a number of complications, as Richard's wiki entry on the subject [1] demonstrates.</div><div class=""><br class=""></div><div class="">That's not to say that I wouldn't like to see that happen some day. But a mere mortal like myself couldn't possibly implement this, whereas David's idea is actually within reach.<br class=""></div><div class=""><br class=""></div><div class="">Ryan S.</div><div class="">-----</div><div class="">[1] <a href="https://ghc.haskell.org/trac/ghc/wiki/DependentHaskell/Internal#Liftedvs.Unliftedequality" class="">https://ghc.haskell.org/trac/ghc/wiki/DependentHaskell/Internal#Liftedvs.Unliftedequality</a><br class=""></div></div></div><div class="gmail_extra"><br class=""><div class="gmail_quote">On Wed, Sep 5, 2018 at 10:45 AM, Simon Peyton Jones <span dir="ltr" class=""><<a href="mailto:simonpj@microsoft.com" target="_blank" class="">simonpj@microsoft.com</a>></span> wrote:<br class=""><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">





<div link="blue" vlink="purple" lang="EN-GB" class="">
<div class="m_7258715947657041120WordSection1"><p class="MsoNormal" style="margin-right:0cm;margin-bottom:6.0pt;margin-left:36.0pt">
I think the intention is to have that proposal (which proposes a language change) be superseded by this idea (which does not change the language).<u class=""></u><u class=""></u></p><p class="MsoNormal"><span style="font-size:12.0pt" class="">Oh, I did not know that.   I’ll ignore the proposal for now, in that case.<u class=""></u><u class=""></u></span></p><p class="MsoNormal"><span style="font-size:12.0pt" class=""><u class=""></u> <u class=""></u></span></p><p class="MsoNormal" style="margin-right:0cm;margin-bottom:6.0pt;margin-left:36.0pt">
All that would take is putting Coercion in TysWiredIn, and moving Coercion from Data.Type.Coercion to somewhere in ghc-prim.<u class=""></u><u class=""></u></p><p class="MsoNormal"><span style="font-size:12.0pt" class=""><u class=""></u> <u class=""></u></span></p><p class="MsoNormal"><span style="font-size:12.0pt" class="">I don’t think it’s quite as simple as that.  Yes, we can wire it into the compiler; but we still need a module that defines the info table, curried data constructor etc for the type.  And we have no way to
 do that.<u class=""></u><u class=""></u></span></p><p class="MsoNormal"><span style="font-size:12.0pt" class=""><u class=""></u> <u class=""></u></span></p><p class="MsoNormal"><span style="font-size:12.0pt" class="">We could utterly lie and say<u class=""></u><u class=""></u></span></p><p class="MsoNormal"><span style="font-size:12.0pt" class="">              data Coercion a b where<u class=""></u><u class=""></u></span></p><p class="MsoNormal"><span style="font-size:12.0pt" class="">                  Coercion :: Coercion a a<u class=""></u><u class=""></u></span></p><p class="MsoNormal"><span style="font-size:12.0pt" class=""><u class=""></u> <u class=""></u></span></p><p class="MsoNormal"><span style="font-size:12.0pt" class="">That would generate the right bits in in the .o file, and we’d totally ignore the .hi file.  Gruesome but I think it would work.<u class=""></u><u class=""></u></span></p><p class="MsoNormal"><span style="font-size:12.0pt" class=""><u class=""></u> <u class=""></u></span></p><p class="MsoNormal"><span style="font-size:12.0pt" class=""><u class=""></u> <u class=""></u></span></p><p class="MsoNormal"><span style="font-size:12.0pt" class="">But rather than all this circumlocution, why don’t we just make it possible to write ~# and ~R# directly.  Even if we dodge the need right now, it’ll surely come back.<u class=""></u><u class=""></u></span></p><p class="MsoNormal"><span style="font-size:12.0pt" class=""><u class=""></u> <u class=""></u></span></p><p class="MsoNormal"><span style="font-size:12.0pt" class="">If that is lexically tiresome, we could I suppose provide builtin-aliases for them, as if we had<u class=""></u><u class=""></u></span></p><p class="MsoNormal"><span style="font-size:12.0pt" class="">              type NomEq# = (~#)<u class=""></u><u class=""></u></span></p><p class="MsoNormal"><span style="font-size:12.0pt" class="">             type ReprEq# = (~R#)<u class=""></u><u class=""></u></span></p><p class="MsoNormal"><span style="font-size:12.0pt" class=""><u class=""></u> <u class=""></u></span></p><p class="MsoNormal"><span style="font-size:12.0pt" class="">Simon<u class=""></u><u class=""></u></span></p><p class="MsoNormal"><span style="font-size:12.0pt" class=""><u class=""></u> <u class=""></u></span></p>
<div style="border:none;border-left:solid blue 1.5pt;padding:0cm 0cm 0cm 4.0pt" class="">
<div class="">
<div style="border:none;border-top:solid #e1e1e1 1.0pt;padding:3.0pt 0cm 0cm 0cm" class=""><p class="MsoNormal"><b class=""><span lang="EN-US" class="">From:</span></b><span lang="EN-US" class=""> Ryan Scott <<a href="mailto:ryan.gl.scott@gmail.com" target="_blank" class="">ryan.gl.scott@gmail.com</a>>
<br class="">
<b class="">Sent:</b> 05 September 2018 15:26<br class="">
<b class="">To:</b> Simon Peyton Jones <<a href="mailto:simonpj@microsoft.com" target="_blank" class="">simonpj@microsoft.com</a>><br class="">
<b class="">Cc:</b> <a href="mailto:ghc-devs@haskell.org" target="_blank" class="">ghc-devs@haskell.org</a><br class="">
<b class="">Subject:</b> Re: Unpacking coercions<u class=""></u><u class=""></u></span></p>
</div>
</div><p class="MsoNormal"><u class=""></u> <u class=""></u></p>
<div class="">
<div class="">
<div class=""><p class="MsoNormal" style="margin-right:0cm;margin-bottom:6.0pt;margin-left:0cm">
> <span style="font-size:12.0pt" class="">Simple is good.  But what is this dead simple idea?</span><u class=""></u><u class=""></u></p>
</div>
<div class=""><p class="MsoNormal" style="margin-right:0cm;margin-bottom:6.0pt;margin-left:0cm">
<u class=""></u> <u class=""></u></p>
</div>
<div class=""><p class="MsoNormal" style="margin-right:0cm;margin-bottom:6.0pt;margin-left:0cm">
I'm referring to David's first e-mail on this thread: <a href="https://mail.haskell.org/pipermail/ghc-devs/2018-September/016191.html" target="_blank" class="">
https://mail.haskell.org/<wbr class="">pipermail/ghc-devs/2018-<wbr class="">September/016191.html</a><u class=""></u><u class=""></u></p>
</div>
<div class=""><p class="MsoNormal" style="margin-right:0cm;margin-bottom:6.0pt;margin-left:0cm">
<u class=""></u> <u class=""></u></p>
</div>
<div class=""><p class="MsoNormal" style="margin-right:0cm;margin-bottom:6.0pt;margin-left:0cm">
All that would take is putting Coercion in TysWiredIn, and moving Coercion from Data.Type.Coercion to somewhere in ghc-prim.<u class=""></u><u class=""></u></p>
</div>
<div class=""><p class="MsoNormal" style="margin-right:0cm;margin-bottom:6.0pt;margin-left:0cm">
<u class=""></u> <u class=""></u></p>
</div>
<div class=""><p class="MsoNormal" style="margin-right:0cm;margin-bottom:6.0pt;margin-left:0cm">
> <span style="font-size:12.0pt" class="">Maybe this thread belongs with the proposal, unless I’m misunderstanding.</span><u class=""></u><u class=""></u></p>
</div>
<div class=""><p class="MsoNormal" style="margin-right:0cm;margin-bottom:6.0pt;margin-left:0cm">
<u class=""></u> <u class=""></u></p>
</div>
<div class=""><p class="MsoNormal" style="margin-right:0cm;margin-bottom:6.0pt;margin-left:0cm">
I think the intention is to have that proposal (which proposes a language change) be superseded by this idea (which does not change the language).<u class=""></u><u class=""></u></p>
</div>
<div class=""><p class="MsoNormal" style="margin-right:0cm;margin-bottom:6.0pt;margin-left:0cm">
<u class=""></u> <u class=""></u></p>
</div>
<div class=""><p class="MsoNormal" style="margin-right:0cm;margin-bottom:6.0pt;margin-left:0cm">
Ryan S.<u class=""></u><u class=""></u></p>
</div><p class="MsoNormal" style="margin-right:0cm;margin-bottom:6.0pt;margin-left:0cm">
<u class=""></u> <u class=""></u></p>
</div>
</div>
<div class=""><p class="MsoNormal" style="margin-right:0cm;margin-bottom:6.0pt;margin-left:0cm">
<u class=""></u> <u class=""></u></p>
<div class=""><p class="MsoNormal" style="margin-right:0cm;margin-bottom:6.0pt;margin-left:0cm">
On Wed, Sep 5, 2018 at 10:20 AM, Simon Peyton Jones <<a href="mailto:simonpj@microsoft.com" target="_blank" class="">simonpj@microsoft.com</a>> wrote:<u class=""></u><u class=""></u></p>
<blockquote style="border:none;border-left:solid #cccccc 1.0pt;padding:0cm 0cm 0cm 6.0pt;margin-left:4.8pt;margin-right:0cm" class="">
<div class="">
<div class=""><p class="MsoNormal"><span style="font-size:12.0pt" class="">Simple is good.  But what is this dead simple idea?</span><u class=""></u><u class=""></u></p><p class="MsoNormal"><span style="font-size:12.0pt" class=""> </span><u class=""></u><u class=""></u></p><p class="MsoNormal"><span style="font-size:12.0pt" class="">Perhaps:
<a href="https://na01.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgithub.com%2Fghc-proposals%2Fghc-proposals%2Fpull%2F116&data=02%7C01%7Csimonpj%40microsoft.com%7Cab6e886b24b548eab26608d6133b91b5%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C636717543898919689&sdata=XKBwJiLM%2FcH5FeRLuodH3SKXQUppYT0QYDojH4fO7Tg%3D&reserved=0" target="_blank" class="">
https://github.com/ghc-<wbr class="">proposals/ghc-proposals/pull/<wbr class="">116</a></span><u class=""></u><u class=""></u></p><p class="MsoNormal"><span style="font-size:12.0pt" class="">But that proposal lists several possible alternatives.  Which one did you mean?</span><u class=""></u><u class=""></u></p><p class="MsoNormal"><span style="font-size:12.0pt" class=""> </span><u class=""></u><u class=""></u></p><p class="MsoNormal"><span style="font-size:12.0pt" class="">And all of them are language changes. Making evidence strict would require no language changes to solve the original problem.</span><u class=""></u><u class=""></u></p><p class="MsoNormal"><span style="font-size:12.0pt" class=""> </span><u class=""></u><u class=""></u></p><p class="MsoNormal"><span style="font-size:12.0pt" class="">Maybe this thread belongs with the proposal, unless I’m misunderstanding.</span><u class=""></u><u class=""></u></p><p class="MsoNormal"><span style="font-size:12.0pt" class=""> </span><u class=""></u><u class=""></u></p><p class="MsoNormal"><span style="font-size:12.0pt" class="">Simon</span><u class=""></u><u class=""></u></p><p class="MsoNormal"><span style="font-size:12.0pt" class=""> </span><u class=""></u><u class=""></u></p>
<div style="border:none;border-left:solid blue 1.5pt;padding:0cm 0cm 0cm 4.0pt" class="">
<div class="">
<div style="border:none;border-top:solid #e1e1e1 1.0pt;padding:3.0pt 0cm 0cm 0cm" class=""><p class="MsoNormal"><b class=""><span lang="EN-US" class="">From:</span></b><span lang="EN-US" class=""> ghc-devs <<a href="mailto:ghc-devs-bounces@haskell.org" target="_blank" class="">ghc-devs-bounces@haskell.org</a>>
<b class="">On Behalf Of </b>Ryan Scott<br class="">
<b class="">Sent:</b> 05 September 2018 15:15<br class="">
<b class="">To:</b> <a href="mailto:ghc-devs@haskell.org" target="_blank" class="">ghc-devs@haskell.org</a><br class="">
<b class="">Subject:</b> Re: Unpacking coercions</span><u class=""></u><u class=""></u></p>
</div>
</div><p class="MsoNormal"> <u class=""></u><u class=""></u></p>
<div class="">
<div class=""><p class="MsoNormal" style="margin-bottom:6.0pt">These aren't mutually exclusive ideas. While I'm sure there's many ways we could solve this problem, David's idea has the distinct advantage of being dead simple. I'd rather not block
 his vision on some other large refactor that may never materialize. (And if it _does_ materialize, we could revert any wiring-in of Coercible quite easily.)<u class=""></u><u class=""></u></p>
</div>
<div class=""><p class="MsoNormal" style="margin-bottom:6.0pt"> <u class=""></u><u class=""></u></p>
</div>
<div class=""><p class="MsoNormal" style="margin-bottom:6.0pt">Ryan S.<u class=""></u><u class=""></u></p>
</div>
</div>
</div>
</div>
</div>
</blockquote>
</div><p class="MsoNormal"><u class=""></u> <u class=""></u></p>
</div>
</div>
</div>
</div>

</blockquote></div><br class=""></div>
_______________________________________________<br class="">ghc-devs mailing list<br class=""><a href="mailto:ghc-devs@haskell.org" class="">ghc-devs@haskell.org</a><br class="">http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs<br class=""></div></blockquote></div><br class=""></body></html>