wp_bind does not report a failure message
The first [ t1 | fail ] here is incorrect: https://gitlab.mpi-sws.org/iris/iris/-/blob/4c96a5043ab4f648f4082f2398888c879efd3c36/iris_heap_lang/proofmode.v#L200
first [ reshape_expr e ltac:(fun K e' => unify e' efoc; wp_bind_core K)
| fail "wp_bind: cannot find" efoc "in" e ]The failure causes the entire construct to fail with a generic error message; what was intended is fail 1 to bubble it up. Furthermore there's no test of this failure.
This bug was originally reported by François Pottier against https://github.com/tchajed/iris-simp-lang/, which inherited this bug from heap_lang.