Would it not be unsound for ghc to elide dictionary construction here? After all, the right-hand side might actually be a bottom (e.g. undefined) at run-time, in which case the pattern match cannot succeed according to the semantics of Haskell. I suspect that if you make the pattern match lazy (i.e. ~(Entail (Sub Dict))) or ignore the argument altogether (i.e. _), dictionary construction will be elided.<div><br /></div><div><br /></div>- Tom<div><br /></div><div><br /></div><div><br /></div><div><br /></div><div><br /></div><div><br /></div><div><br /></div><br>-------- Original Message --------<br>On 6 Aug 2021, 15:06, Michael Sperber < sperber@deinprogramm.de> wrote:<blockquote class="protonmail_quote"><br><p dir="ltr"><br>
I have another optimization problem. ConCat includes this definition:</p>
<p dir="ltr">(&lt;+) :: Con a =&gt; (Con b =&gt; r) -&gt; (a |- b) -&gt; r<br>
r &lt;+ Entail (Sub Dict) = r</p>
<p dir="ltr">The right-hand argument of &lt;+ leads to a dictionary construction that is<br>
a proof of a certain property, but the dictionary itself ends up being<br>
dead, like so:</p>
<p dir="ltr">case $w$dOpCon_r2kGJ ...<br>
of<br>
{ (# ww1_s27L3 #) -&gt; ... }<br>
^^^^^^^^^<br>
never used</p>
<p dir="ltr">Yet, ghc (8.10.4) never elides this code. (I'm naively assuming because<br>
of the unboxed tuple, but actually have no clue.)</p>
<p dir="ltr">Is there any chance of convincing ghc of erasing the dictionary<br>
construction?</p>
<p dir="ltr">Help would be much appreciated!</p>
<p dir="ltr">--<br>
Regards,<br>
Mike</p>
<p dir="ltr">_______________________________________________<br>
Glasgow-haskell-users mailing list<br>
Glasgow-haskell-users@haskell.org<br>
<a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users">http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users</a><br>
</p>
</div>