<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=""><meta http-equiv="content-type" content="text/html; charset=utf-8" class=""><div dir="auto" class=""><div dir="auto" class=""><div dir="ltr" class=""><blockquote type="cite" class="">On Jan 6, 2020, at 05:29, Richard Eisenberg <<a href="mailto:rae@richarde.dev" class="">rae@richarde.dev</a>> wrote:<br class=""><br class=""></blockquote></div><blockquote type="cite" class=""><div dir="ltr" class="">You're absolutely right that improvement doesn't solve your problem. But what I didn't say is that there is no real reason (I think) that we can't improve improvement to produce givens. This would likely require a change to the coercion language in Core (and thus not to be taken lightly), but if we can identify a class of programs that clearly benefits from that work, it is more likely to happen. The thoughts about improvement were just a very basic proof-of-concept. Sadly, the proof-of-concept failed, so I think a first step in this direction would be to somehow encode these partial improvements, and then work on changing Core. That road seems too long, though, so in the end, I think constrained type families (with superclass constraints) might be a more fruitful direction.</div></blockquote></div></div><div dir="auto" class=""><br class=""></div><div dir="auto" class="">Thanks, this all makes sense to me. I actually went back and re-read the injective type families paper after responding to your previous email, and I discovered it actually alludes to the issue we’re discussing! At the end of the paper, in section 7.3, it provides the following example:<div class=""><br class=""></div><div class=""><div class=""></div><blockquote type="cite" class=""><div class="">Could closed type families move beyond injectivity and functional dependencies by applying closed-world reasoning that derives solutions of arbitrary equalities, provided a unique solution exists? Consider this example:</div></blockquote><blockquote type="cite" class=""><br class=""></blockquote><blockquote type="cite" class=""><div class="">type family J a where</div></blockquote><blockquote type="cite" class=""><div class=""> J Int = Char</div><div class=""> J Bool = Char</div><div class=""> J Double = Float</div></blockquote><blockquote type="cite" class=""><br class=""></blockquote><blockquote type="cite" class=""><div class="">One might reasonably expect that if we wish to prove (J a ∼ Float), we will simplify to (a ∼ Double). Yet GHC does not do this as neither injectivity nor functional dependencies can discover this solution.</div></blockquote><div class=""><br class=""></div>This is not <i class="">quite</i> the same as what we’re talking about here, but it’s clearly in the same ballpark.</div><div class=""><br class=""></div><div class="">I think what you’re describing makes a lot of sense, and it would be interesting to explore what it would take to encode into core. After thinking a little more on the topic, I think that probably makes by far the most sense from the core side of things. But I agree it seems like a significant change, and I don’t know enough about the formalism to know how difficult it would be to prove soundness. (I haven’t done much formal proving of anything!)<br class=""><br class=""><div dir="ltr" class=""><!-- signature open -->Alexis</div></div></div></body></html>