Add support for Exception typeclass and throw/catch functions

[jespercockx]

As it says on the tin, it would be nice to have support for at least some subset of Control.Exception in the agda2hs prelude. I think this is just adding some bindings to existing Haskell functions so it wouldn't require any changes to the agda2hs binary.

[jespercockx]

I'm considering how to implement the throw function without running into the same problem we have in #428 (and possibly also fixing that issue on the way). One way to do this would be to essentially make all exceptions "checked", i.e. add them to the type signature of the functions that may throw them.

Something like this:

postulate
  @0 MayThrow : Set → Set
  throw : {{Exception e}} → @0 {{MayThrow e}} → e → a
  catch : {{Exception e}} → (@0 {{MayThrow e}} → IO a) → (e → IO a) → IO a

Then we could fix #428 by changing the type of assert to

assert : @0{{MayThrow AssertionFailed}} → (@0 b : Type ℓ) → {{Dec b}} → (@0 {{b}} → a) → a

Since we remain agnostic about the nature of the MayThrow type (in particular it could be assumed to be empty) this makes the type of assert be no longer inconsistent. However, dealing with the MayThrow instances might prove to be cumbersome in some cases. For those cases there would always be an escape hatch which is to simply postulate a global instance of type MayThrow AssertionFailed (or even MayThrow e for any exception type e) so there is an upper bound to how annoying this could become compared to the status quo.

I'd be curious to hear opinions on this or ideas for alternative designs.