Type inference of singular matches on GADTs

Alexis King 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 
the discussion.


More information about the ghc-devs mailing list