Typed meta-programming has a very rich history. For a good overview of various approaches and main problems, please see the Related work section of the following paper http://okmij.org/ftp/tagless-final/TaglessStaged/beyond-journal.pdf There is a special subsection on Typed TH. (The version of that paper with minor revisions will be uploaded in two-three months). The main problems are how to ensure hygiene in the presence of effects, and how to generate polymorphic bindings (let-bindings). Both problems have been essentially solved. (The solution to the second problem has been presented at small meetings so far). The paper explains the combinator library to generate TH code that is ensured to be well-typed, *by construction*. The library permits arbitrary monadic effects. There is no Q monad since it turns out not necessary.