Jesper Cockx

The problem here is that the definition of the `Eq` record in the `Haskell.Prelude` is wrong: the `_/=_` should be defined either as a field or as a standalone function,...

I'm not convinced why this is safe to do. In particular, if a `COMPILE AGDA2HS` pragma on a record type has been changed from a regular pragma to a `class`...

See also #74 for some motivation

The types of `if_then_else_` and `case_of_` are now more general so there's less need for having multiple versions of them, and for literals and ranges the need to have multiple...

This close to impossible to support with the current architecture of Agda: `as` patterns are treated as `let`-bindings, and let-bindings are inlined eagerly in the internal syntax. So we would...

Actually, let-bindings do not work either, for the same reason.

I think all record expressions get desugared to constructor applications in the internal syntax, so there's indeed no way to know from just the internal syntax. We could try to...

Thank you, assigned! I think having one file per typeclass makes sense, yeah.

Currently, we do not allow forced patterns in non-erased positions due to https://github.com/agda/agda2hs/issues/142, but this would be too strict when we support GADTs. So in order to support GADTs we...

Yes, the proofs would indeed be erased. What does need to be done are the issues Wen lists above: the dependencies on stdlib and agdarsec, and the work of mapping...