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