<div dir="ltr">We haven't figured out what they did, but the other day we had someone in #haskell with an infinite loop evaluating a dictionary. So apparently it is possible for a dictionary to be bottom somehow.</div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Mon, Aug 9, 2021 at 11:27 AM Tom Smeding <<a href="mailto:x@tomsmeding.com">x@tomsmeding.com</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">Hi Mike,<div><br></div><div><br></div>> But wouldn't that imply that ghc can build dictionary-construction code<div><br></div>> that evaluates to bottom? Can that happen?<div><br></div><div><br></div>I assume no, but here the dictionary is embedded as a field in the GADT, right? So if the data value is bottom, there is not even a dictionary to be found, let alone not-bottom.<div><br></div><div><br></div>This assumes that the Dict in `Entail (Sub Dict)` is a GADT like<div><br></div><div><br></div>  Dict :: Con b => Dict something<div><br></div><div><br></div>where the Con dictionary is contained in the GADT. Remember that in Core, dictionaries are values, and there is no difference between => and ->.<div><br></div><div><br></div>- Tom<div><br></div><div><br></div><div><br></div>-------- Original Message --------<div><br></div>On 9 Aug 2021, 15:24, Michael Sperber < <a href="mailto:sperber@deinprogramm.de" target="_blank">sperber@deinprogramm.de</a>> wrote:<div><br></div><div><br></div>Thanks for thinking about this one!<div><br></div>On Fri, Aug 06 2021, Tom Smeding <<a href="mailto:x@tomsmeding.com" target="_blank">x@tomsmeding.com</a>> wrote:<div><br></div>> Would it not be unsound for ghc to elide dictionary construction here?<div><br></div>> After all, the right-hand side might actually be a bottom<div><br></div>> (e.g. undefined) at run-time, in which case the pattern match cannot<div><br></div>> succeed according to the semantics of Haskell.<div><br></div>But wouldn't that imply that ghc can build dictionary-construction code<div><br></div>that evaluates to bottom? Can that happen?<div><br></div>> I suspect that if you make the pattern match lazy (i.e. ~(Entail (Sub<div><br></div>> Dict))) or ignore the argument altogether (i.e. _), dictionary<div><br></div>> construction will be elided.<div><br></div>Thanks for the hint! ghc gives me this unfortunately, implying that it<div><br></div>agreed with your first comment:<div><br></div>src/ConCat/Category.hs:190:29: error:<div><br></div>• Could not deduce: Con b arising from a use of ‘r’<div><br></div>from the context: Con a<div><br></div>bound by the type signature for:<div><br></div>(<+) :: forall a b r. Con a => (Con b => r) -> (a |- b) -> r<div><br></div>at src/ConCat/Category.hs:189:1-46<div><br></div>• In the expression: r<div><br></div>In an equation for ‘<+’: r <+ ~(Entail (Sub Dict)) = r<div><br></div>• Relevant bindings include<div><br></div>r :: Con b => r (bound at src/ConCat/Category.hs:190:1)<div><br></div>(<+) :: (Con b => r) -> (a |- b) -> r<div><br></div>(bound at src/ConCat/Category.hs:190:3)<div><br></div>|<div><br></div>190 | r <+ ~(Entail (Sub Dict)) = r<div><br></div>| ^<div><br></div>Other ideas welcome!<div><br></div>--<div><br></div>Regards,<div><br></div>Mike<div><br></div>_______________________________________________<div><br></div>Glasgow-haskell-users mailing list<div><br></div><a href="mailto:Glasgow-haskell-users@haskell.org" target="_blank">Glasgow-haskell-users@haskell.org</a><div><br></div><a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users" target="_blank">http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users</a><div><br></div>_______________________________________________<br>
Glasgow-haskell-users mailing list<br>
<a href="mailto:Glasgow-haskell-users@haskell.org" target="_blank">Glasgow-haskell-users@haskell.org</a><br>
<a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users" rel="noreferrer" target="_blank">http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users</a><br>
</blockquote></div><br clear="all"><div><br></div>-- <br><div dir="ltr" class="gmail_signature"><div dir="ltr"><div><div dir="ltr"><div>brandon s allbery kf8nh</div><div><a href="mailto:allbery.b@gmail.com" target="_blank">allbery.b@gmail.com</a></div></div></div></div></div>