Getting your Agda code to type-check faster

As I, like many others of good will and high aspiration, battle the POPL ’16 submission deadline, I feel compelled to write a quick post about how to get your Agda code through the type-checker faster.  For my submission fight, I have got about 3000 lines of Agda that is intended to be compiled and executed (imagine!), and Agda is getting bogged down.  Compilations are taking productivity-killing minutes instead of seconds, or not completing at all!  Argh.  Here are three things I did that seemed to help (YMMV, of course):

1. Do not use anonymous lets in your code.  Always give a type for let-bound variables.  I had three nested anonymous lets in sequence, and they seemed to be slowing Agda down a lot.
2. Instead of nested tuples, use a new datatype.  Agda seems to have more trouble with (a1 , a2 , a3 , a4) then with (c a1 a2 a3 a4), where c is a new constructor.
3. Sadly, you may be forced to break up big mutually recursive functions.  I have got a doozy going, with maybe 12-15 mutually recursive functions.  Since they all have to go in one file (right?), we get a big Agda file, which seems to give Agda more trouble, generally, than a small Agda file.  The solution is to break up the mutually recursive functions.  To do this, you have to use {-# NO_TERMINATION_CHECK #-} right before the function declarations, and then you have to pass some of those functions explicitly to the other functions, to use for making the recursive calls.  So if f calls g and h, you put f into one file, and add two extra function arguments to f.  These are the functions to use when f wants to call g and wants to call h. Then you put the code for g and h in another file which imports the file containing f.  Where g or h calls f, now instead (f g h) should be called (since f is taking in g and h explicitly as arguments).

Fun fun!