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