[Agda] Re: Agda reflection overhaul

[David Raymond Christiansen]

>     - Since typeError expects a String, maybe it would be useful to have
>     some functions for pretty-printing terms/types? Or alternatively we
>     could have a richer type for error messages.
> 
> I'm going for the latter. I have an implementation of an error message
> type with string and term constructors that I did before the current
> overhaul. I just need to merge it.

The latter is what we have in Idris, and it's proven to be a good
choice. The pretty printer can be made pretty smart, and having a
structured error message datatype allows those smarts to be quite
cheaply made available to errors that arise from metaprograms.

/David