My "hidden agenda" is to liberate the SBV library to work on Haskell programs directly. (
http://hackage.haskell.org/package/sbv)
SBV allows programming with symbolic values, allowing a certain class of "proofs" to be done. It uses SMT solvers to do the actual "solving." It's limited in what it can do so far as reasoning goes: It's mostly limited to number types really (Word/Int/Float/Double etc.), but when it works, it really can be effective. Right now, users of this library have to write things like this:
foo x y = ite (x .> y) (x+2) (x .< y)
Since I "cannot" reliably steal if-then-else (yes, I'm aware of RebindableSyntax; but it has its own problems.), nor I can just use comparison operators that insist on returning Bool that I cannot change. But those are smaller problems: The bigger issue is that I cannot support "case" expressions, pattern-matching, and all that stuff; since all that mechanism is baked into the compiler and I've no way to arrange for a pattern to "symbolically" match. This latter issue with pattern-matching and lack of support for case-expressions is why the library is sort of "hard-to-use" for a newcomer.
I tried TH/HSE before to see if I can let users write regular-Haskell and have the expressions automatically made "symbolic" aware, but ran into a lot of accidental complexity due to the extremely rich surface syntax. I'm currently working on a plugin to do the same, which is much nicer to work with; though you are correct that dealing with explicitly-typed core has its complexities as well. However, I do find it to be much easier to work with as compared to surface Haskell.
I suspect you guys went down to the "stand-alone" route with LiquidHaskell when you had similar problems. That definitely is a great approach as well, though I don't have the luxury of an academic research team to pursue that line of thought. (LiquidHaskell rocks by the way; I'm a real fan.)
-Levent.