Hmm, you're right, in a total language you can't define such a Psi for Id. Maybe the type class should go like this:

class Prov p f where
fix :: p (f a -> a (f a))
unfix :: p (a (f a) -> f a)
dup :: p a -> p (p a)
mp :: p (a -> b) -> p a -> p b

I don't know if that's enough. One problem is that fix and unfix are really inconvenient to use without type lambdas, which Haskell doesn't have. Maybe I should try Scala, which has them.

Another problem is in step 13. To do that without soundness, I probably need versions of dup and mp that work inside p, as well as outside. But that makes the type class too complicated.