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 <r...@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.
_______________________________________________
ghc-devs mailing list
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
