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 H

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.