[Agda] Adding "print" to TC monad?

[David Christiansen]

Hi Jon,

> I am starting to learn to use Agda's excellent reflection facilities /
> TC monad to implement some proof automation, and I have been thinking
> that it would be very useful to have a way to do "printf"-style
> debugging in elaborator scripts. Right now, I can kind of simulate this
> by throwing an error, but I would like to be able to print information
> without aborting the proof.
>
> Does anybody have any thoughts about adding another operation to the TC
> monad for printing (i.e. whether this is a good idea)? If people think
> this sounds like a good idea, I would probably be willing to do the
> hacking and submit a pull request.

I've been meaning to add this to Idris for ages, and I think it's a very
good idea. I saw on the Agda docs recently that there's a system like
the one in Idris for re-using the pretty-printer inside of things like
custom error messages, so it's probably worth having your log effect use
the same part.

The Lean folks have also been implementing elaborator reflection lately,
with a focus on performance and tools, so it might be worth seeing what
they offer for debugging.

/David