Type inference of singular matches on GADTs

[Alexis King]

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.

Alexis