Superclasses of type families returning constraints?

[Richard Eisenberg]

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 <https://repository.brynmawr.edu/cgi/viewcontent.cgi?article=1075&context=compsci_pubs>, proposal:https://github.com/ghc-proposals/ghc-proposals/pull/177 <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.

Richard

> On Dec 27, 2019, at 7:16 PM, Alexis King <lexi.lambda at gmail.com> wrote:
> 
> Hello all,
> 
> I recently noticed that GHC rejects the following program:
> 
>    type family F a b :: Constraint where
>      F a a = ()
> 
>    eq :: F a b => a :~: b
>    eq = Refl
> 
> This is certainly not shocking, but it is a little unsatisfying: as far as I can tell, accepting this program would be entirely sound. That is, `a ~ b` is morally a “superclass” of `F a b`. In this example the type family is admittedly rather pointless, as `a ~ b` could be used instead, but it is possible to construct more sophisticated examples that cannot be so straightforwardly expressed in other ways.
> 
> I am therefore curious: has this kind of scenario ever been discussed before? If yes, is there a paper/GitLab issue/email thread somewhere that discusses it? And if no, is there any fundamental reason that GHC does not propagate such information (i.e. it’s incompatible with some aspect of the type system or constraint solver), or is it simply something that has not been explored? (Maybe you think the above program is horrible and *shouldn’t* be accepted even if it were possible, but that is a different question entirely. :))
> 
> Thanks,
> Alexis
> _______________________________________________
> ghc-devs mailing list
> ghc-devs at haskell.org
> http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-devs/attachments/20191229/32e46185/attachment.html>