Also true. The slowness is relatively unpredictable, too: sometimes changing a 'rewrite' to a 'with' can increase memory usage tenfold.

While we're at it, another major concern for me is the inscrutability of Agda's error messages. I've had one error message single-handedly overflow my tmux scrollback buffer. There's no way I'm going to be able to interpret that.