Superclasses of type families returning constraints?

[Alexis King]

> On Jan 4, 2020, at 20:38, Richard Eisenberg <rae at richarde.dev> wrote:
> 
> I thought that, maybe, we could use partial improvement to give you what you want

I think that improvement alone cannot possibly be enough here, as improvement by its nature does not provide evidence. Improvement allows us to take a set of constraints like

    [G] FD2 a Bool
    [W] FD2 a b

and derive [WD] b ~ Bool, but importantly this does not produce a new given! This only works if b is a metavariable, since we can solve the new wanted by simply taking b := Bool, but if b is rigid, we are just as stuck as before. In other words, improvement only helps resolve ambiguities, not derive any new information.

That’s why I think the “superclass” characterization is more useful. If instead we express your FD2 class as

    class b ~ B a => FD2 a b where
      type B a

then if we have [G] FD2 a Bool, we can actually derive [G] B a ~ Bool, which is much stronger than what we were able to derive using improvement.

I imagine you are aware of all of the above already, but it’s not immediately clear to me from your description why you need functional dependencies (and therefore improvement) rather than this kind of approximation using superclasses and type families. Would modeling things with that approximation help at all? If not, why not? I think that would help me understand what you’re saying a little better.

Thanks,
Alexis