
<html><head><meta http-equiv="Content-Type" content="text/html; charset=utf-8"></head><body style="word-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;" class=""><blockquote type="cite" class="">On May 4, 2020, at 04:25, Richard Eisenberg <<a href="mailto:rae@richarde.dev" class="">rae@richarde.dev</a>> wrote:<br class=""></blockquote><div><blockquote type="cite" class=""><div class=""><div style="word-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;" class=""><div class=""><br class=""></div><div class="">1. pprType seems a very challenging place to do this, given that pprType works on IfaceTypes, which are not amenable to much of any analysis. Maybe you could do the switcho-changeo before converting to IfaceType. Are your type families closed? Then it's just barely conceivable. If they're open, you won't have the instances available in pprType. Still, this seems like far too much processing to be done in pretty-printing.</div></div></div></blockquote><div><br class=""></div><div>You are right—I discovered this after my previous email. But they are more than closed: they are BuiltInSynFams, so they can be expanded easily by isBuiltInSynFamTyCon_maybe + sfMatchFam.</div><br class=""><blockquote type="cite" class=""><div class=""><div style="word-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;" class=""><div class="">2. tidyType really cannot change one type to another unequal one. Chaos will ensue.</div></div></div></blockquote><div><br class=""></div><div>Agreed.</div><br class=""><blockquote type="cite" class=""><div class=""><div style="word-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;" class=""><div class="">3. reportWanteds will have a similar problem: if we have -fdefer-type-errors, then reportWanteds may actually happen before desugaring and execution, and we can't have a type magically changed in the process. Doing so will lead to a core-lint error.</div></div></div></blockquote><div><br class=""></div><div>I don’t totally understand this point—I thought reportWanteds just printed things! It sounds like you’re saying it does something more, but I don’t immediately see what.</div><br class=""><blockquote type="cite" class=""><div class=""><div style="word-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;" class=""><div class="">4-5. These seem the post plausible. Yes, it's true that calls to ArrowStackTup might leak through, but doing so wouldn't be strictly *wrong*, just suboptimal. So it might be that a best-effort here is good enough.</div></div></div></blockquote><div><br class=""></div><div>I think 4 makes sense for situations where the type family is stuck, since in that case we can’t just expand it away, and there is a more useful error message we can report. Maybe 5 makes more sense for the other cases, but I started down that path and it’s quite awkward.</div><br class=""><blockquote type="cite" class=""><div class=""><div style="word-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;" class=""><div class="">Another possibility: when these ArrowStackTup calls are born, do you already sometimes know the arguments? That is, there must be some code that produces the ArrowStackTup '[a] call -- could it just special-case an '[a] argument and produce `a` instead? Then, the ArrowStackTup family is used only when you have an abstract argument, which might be considerably rarer.</div></div></div></blockquote><div><br class=""></div><div>I’m afraid not. The entire reason I have the type families in the first place is that the arguments are <i class="">not</i><span style="font-style: normal;" class="">, in general, fully known when the equality constraint is emitted. If that weren’t true, I could drop them completely. (The proposal discusses that in a little more detail, as do some Notes in my WIP MR.)</span></div></div><br class=""><div class="">It’s all a bit frustrating, because it’s really not like printing things this way is “cheating” or somehow morally wrong—these types are nominally equal, so from the user’s point of view they are completely interchangeable. It only becomes sketchy from the Core point of view, and I’m totally fine to not do any of this magic there!</div><div class=""><br class=""></div><div class="">Really, I think this <span style="font-style: normal;" class="">morally</span> belongs in the printer. This is just a display thing, nothing more. I want to be able to say “these type families are not something the user is likely to understand, so when printing error messages, expand them if at all possible.” But it’s very difficult to do that currently given the way pprType goes through IfaceType, since you’ve lost the necessary information by that point.</div><div class=""><br class=""></div><div class="">Alexis</div></body></html>