> ... And notice how the syntax in that message isn't even close to valid Agda!
That is unfair: I copied the type annotations from random places in the Agda library (and then edited them to make them more interesting). Stefan PS: Of course, any sequence of chars (especially funny Unicode symbols) is potentially valid Agda code (as long as you provide the appropriate context).