Re: Superclasses of type families returning constraints?

On Dec 30, 2019, at 11:16 AM, Alexis King wrote:

I don’t know if there is a way to encode those using the constraint language available in source Haskell today.

I gave it a good try, but failed. The trick I was hoping to leverage was *partial improvement*. Here is an example of partial improvement:

class FD1 a b | a -> b class FD2 a b | a -> b

instance FD1 a b => FD2 (Maybe a) (Maybe b)

f :: FD2 a b => a -> b f = undefined

x = f (Just True)

This program will require solving [W] FD2 (Maybe Bool) beta, where the [W] indicates that we have a "wanted" constraint (a goal we are trying to satisfy) and beta is a unification variable. GHC can figure out from the fundep on FD2 that the only FD2 instance that can apply is the one we see above. It thus knows that beta must be Maybe beta2 (for some fresh beta2). This is the essence of partial improvement, when we solve one unification variable with an expression involving another (but is more informative somehow). I thought that, maybe, we could use partial improvement to give you what you want, by replacing the RHSs of the type family with expressions involving classes with fundeps. (Injective type families work very analogously, but it's not worthwhile showing the translation of this idea to that domain here.) I couldn't quite get it to work out, though. Maybe you can, armed with this description... but I doubt it. The problem is that partial improvement must always be a shadow of some "total" improvement process. In the example above, note that I haven't written down an instance of FD1. Clearly, we'll need to satisfy the FD1 constraint in order to satisfy the FD2 constraint. The problem is that, in your example, we really only want partial improvement... and I don't think there's a way to state that. What's tantalizing is that GHC already does all this partial improvement stuff -- it's just that we can't seem to write the instance declarations the way we want to satisfy your use case. I don't know if this really moves us forward at all, but maybe a description of my failure can lead to someone's success. Or perhaps it will lead to a language improvement that will allow us to express what you want. Richard