don't tie bi.weakestpre to program_logic.language (full TC approach)
This is my first attempt to fix #408 (closed), by making
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.