Implement Extended Type Language
This has quite a few benefits.
-
We can have a custom quasi-quoter, which helps us both from an ergonomics and tooling perspective. This would enable the syntax:
tactic [thm| foo :: a -> b -> (a, b) |] $ do ..., as well as allow us to (potentially) usetactic-haskellas an editor tool. -
New types. This would open the door for actual dependent types, which would be a huge win. I'm not sure about the exact specifics of what the desugaring would look like in a few cases, but we could always limit the tricky bits to be only usable within the context of tactics.
Now that I think about it, the only thing that really ties us to template-haskell is reify and friends.
If we take an intero style approach, and use ghci to get our info, we could totally remove template-haskell as a dependency, which would allow us to operate without being stuck in Q. It would probably make sense to keep some ability to use Q directly though, so perhaps using some sort of mtl style api would make the most sense.