<html><head><meta http-equiv="Content-Type" content="text/html; charset=utf-8"></head><body style="word-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;" class="">Hi Alexis,<div class=""><br class=""></div><div class="">I'm not aware of any work in this direction. It's an interesting idea to think about. A few such disconnected thoughts:</div><div class=""><br class=""></div><div class="">- 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.</div><div class=""><br class=""></div><div class="">- If we had constrained type families (paper: <a href="https://repository.brynmawr.edu/cgi/viewcontent.cgi?article=1075&context=compsci_pubs" class="">https://repository.brynmawr.edu/cgi/viewcontent.cgi?article=1075&context=compsci_pubs</a>, proposal:<a href="https://github.com/ghc-proposals/ghc-proposals/pull/177" class="">https://github.com/ghc-proposals/ghc-proposals/pull/177</a>), you could express a superclass constraint on the enclosing type family, which would likely work very much in the way you would want.</div><div class=""><br class=""></div><div class="">Richard<br class=""><div><br class=""><blockquote type="cite" class=""><div class="">On Dec 27, 2019, at 7:16 PM, Alexis King <<a href="mailto:lexi.lambda@gmail.com" class="">lexi.lambda@gmail.com</a>> wrote:</div><br class="Apple-interchange-newline"><div class=""><div class="">Hello all,<br class=""><br class="">I recently noticed that GHC rejects the following program:<br class=""><br class=""> type family F a b :: Constraint where<br class=""> F a a = ()<br class=""><br class=""> eq :: F a b => a :~: b<br class=""> eq = Refl<br class=""><br class="">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.<br class=""><br class="">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. :))<br class=""><br class="">Thanks,<br class="">Alexis<br class="">_______________________________________________<br class="">ghc-devs mailing list<br class=""><a href="mailto:ghc-devs@haskell.org" class="">ghc-devs@haskell.org</a><br class="">http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs<br class=""></div></div></blockquote></div><br class=""></div></body></html>