Comment by notjack

You might be able to use Rosette to implement refinement types on top of Hackett, giving you (I guess?) Liquid Hackett.