Ideas about testing and verifying code generated by typed template haskell
In the recent practical experience of myself, Jamie and Andes we have felt the need for some more support for verifing that the programs that we generate using typed template haskell adhere to certain properties we had in mind.
This ticket is a public place to write down some of these ideas so they are not lost forever.
Size of subtrees
We want to be able to assert, at compile time, that the size of the generated code bares some known relationship to a statically known input. For example, the generated code is linear in the size of the input list.
In order to implement this we need the compiler to be able to report the size of a quotation. If the size of a quotation can be inspected then the assertion functionality can be built into a library.
Certain constructors are not present
We want to assert that in generated code certain constructors are not present. In particular, asserting that generic constructors never appear is an important property. In our own closed programs you can know this with reasonable confidence but in a hypothetical open world where people provide more staged interfaces, a rogue library may inefficiently implement an operation.
This would be a limited analysis at first because you can easily call already compiled functions in your generated code but can't inspect their definition.
Thresholds for generating programs
A common mistake that people make when writing a staged program is to create an infinite compile time loop which generates an infinitely sized program rather than generating a loop which executes at runtime. This is much easier to do than when writing normal programs. It would be good if there was a limit as to how much recursion you were allowed to do at compile time so that beginners can get a good warning rather than puzzle, like we all did, about why the program is looping forever.
Other compile time evaluation features in GHC such as type class resolution and the inliner already have these warnings built in.
Warning for CSP by lifting
In general, cross-stage persistence is bad. It makes it easy to accidentally create bloated programs if you accidentally use a variable at the wrong stage. For advanced users it should be possible to at least issue a warning if your program contains a cross-stage reference as you probably didn't mean it. If you did mean it, write it using an explicit splice and lift.
Use overloaded quotes in order to perform analysis at runtime?
In order to perform some other verification it could be possible to instead perform runtime code generation by using overloaded quotations and inspecting the generating