Hmm, I imagine there's probably a generic way to do it; but I was imagining a straight port of the Haskell version. Note that it might be difficult to generate values of some heavily-constrained dependent type; you'd effectively be implementing a proof search!