Superclasses of type families returning constraints?

[Alexis King]

Hi Richard,

Thanks for the pointer to constrained type families—that’s helpful to clarify some of my thoughts about this, and it is indeed relevant! One example I had in my real code seems difficult to express even with constrained type families, however; here is a stripped-down version of it:

    type family F a b :: Constraint where
      F '[]        (A _)   = ()
      F (B a ': b) (C c d) = (a ~ c, F b d)

With the above type family, if we have the given `F (B a ': b) c`, we’d really like GHC to be able to derive `c ~ C t1 t2` so that the type family can continue to reduce, yielding the givens `a ~ t1` and `F b t2`. But we can’t use your trick of moving the equality into the RHS because we need to procure two fresh unification variables, something we are unable to do. The family is simply stuck, and there isn’t much we can do to cajole GHC into believing otherwise.

In the above example, what the “superclasses” of F are is much less clear. We end up with a few different implications:

    F '[] a         :-  a ~ A t1
    F a (A b)       :-  a ~ '[]
    F (B a ': b) c  :-  c ~ C t1 t2
    F a (C b c)     :-  a ~ (B t1 ': t2)

I don’t know if there is a way to encode those using the constraint language available in source Haskell today. If I understand correctly, I don’t think they can be expressed using quantified constraints. Maybe it’s more trouble than it’s worth, but I find it a little interesting to think about.

Anyway, thank you for the response; I think my original question has been answered. :)

Alexis

> On Dec 29, 2019, at 21:02, Richard Eisenberg <rae at richarde.dev> wrote:
> 
> Hi Alexis,
> 
> I'm not aware of any work in this direction. It's an interesting idea to think about. A few such disconnected thoughts:
> 
> - You could refactor the type family equation to be `F a b = a ~ b`. Then your program would be accepted. And -- assuming the more sophisticated example is also of kind constraint -- any non-linear pattern could be refactored similarly, so perhaps this observation would carry over.
> 
> - If we had constrained type families (paper: https://repository.brynmawr.edu/cgi/viewcontent.cgi?article=1075&context=compsci_pubs, proposal:https://github.com/ghc-proposals/ghc-proposals/pull/177), you could express a superclass constraint on the enclosing type family, which would likely work very much in the way you would want.