Superclasses of type families returning constraints?

[Alexis King]

> On Jan 6, 2020, at 05:29, Richard Eisenberg <rae at richarde.dev> wrote:
> 
> 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.


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:

> 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:
> 
> type family J a where
>   J Int = Char
>   J Bool = Char
>   J Double = Float
> 
> 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.

This is not quite the same as what we’re talking about here, but it’s clearly in the same ballpark.

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!)

Alexis
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-devs/attachments/20200106/d3820c4a/attachment.html>