[Agda] Compile-time parsing

[Andres Löh]

Hi Peter.

I don't understand completely why you're opposed to your first
solution. Code being highlighted in yellow *is* a (particular kind of)
type error in Agda. In fact, it's a particularly well-behaved kind of
type error from which the type checker can recover and still check the
rest of the program. There's no implication that yellow means "almost
correct" ...

Cheers,
  Andres