Type inference of singular matches on GADTs
lexi.lambda at gmail.com
Wed Mar 31 02:53:04 UTC 2021
On 3/28/21 9:17 PM, Richard Eisenberg wrote:
> I think this is the key part of Alexis's plea: that the type checker
> take into account exhaustivity in choosing how to proceed.
> Does this match your understanding?
Yes, precisely. :) Without GADTs, exhaustivity doesn’t yield any useful
information to the typechecker, but with them, it can.
I agree with Simon that it seems tricky—his examples are good ones—and I
agree with Richard that I don’t know if this is actually a good or
fruitful idea. I’m certainly not demanding anyone else produce a
solution! But I was curious if anyone had explored this before, and it
sounds like perhaps the answer is “no.” Fair enough! I still appreciate
More information about the ghc-devs