A Pointless Library Proposal

[Ashley Yakeley]

Conor McBride wrote:

>> magic :: Zero -> a
>> magic _ = error "There's magic, as no such thing!"
> 
> It's a little frustrating to have to define this function lazily. I
> prefer the strict definition with no lines, but it isn't valid
> Haskell!

This issue comes up a lot with GADTs. For instance:

   data MyGADT a where
     MyInt :: MyGADT Int
     MyChar :: MyGADT Char

   never :: MyGADT Bool -> a

Annoyingly, this doesn't compile without adding a definition line 
mentioning a bottom value.

-- 
Ashley Yakeley