anomaly on Hoare logic `match` when the precondition is an existential

[fdupress]

MFE

require import List.

module M = {
  var r : int option

  proc hd(xs : int list) = {
    r <- match r with | None => None | Some _ => None end;
    match xs with
    | [] => { }
    | x :: xs => r <- Some x;
    end;
    return r;
  }
}.

hoare toto &m y ys:
     M.hd: arg = y :: ys ==> res = Some y.
proof.
proc. sp.
match. (* Fails with "anomaly: EcLib.EcCoreGoal.InvalidGoalShape" *)

[fdupress]

This was introduced by #510 .

[fdupress]

And also triggers:

• when the precondition merely contains an existential quantifier (and perhaps a universal quantifier?);
• in one-sided match applications in pRHL.

[strub]

Fix by #577