This is my first attempt to fix #408 (closed), by making expr and val separate typeclass parameters of Wp. That fails type-checking in cases where coercions are involved, since TC inference fails before coercions are inserted (so e.g. using a val as the expression of the WP fails). We only rarely rely on this (3 times total in Iris master, and all of them in tests/), but it would be a breaking change.