This is something I've been wanting for a long time. Liquid Haskell and these solver-based systems should just be a special tactic library with some syntactic sugar on top of a standard dependently typed language.
One option is to treat the solver as a trusted "black box" rule if the user wants to—so theoretically, you could get all the benefits of something like Liquid Haskell simultaneously with the unbounded expressivity of full Nuprl.