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