Possible bug with `simpa`

Stream: lean4

[Artie Khovanov]

The following code

theorem foo (P : Type*) [PartialOrder P] (b : P):

    ∀ {a : P}, a ≥ b → b ≥ a → a = b :=

  by simpa using ge_antisymm

gives the error

type mismatch
  h✝
has type
  ?m.5712 ≤ ?m.5713 → ?m.5713 ≤ ?m.5712 → ?m.5713 = ?m.5712 : Prop
but is expected to have type
  b ≤ a✝ → a✝ ≤ b → a✝ = b : Prop

However, if the argument is made explicit, then the same proof works:

import Mathlib.Order.Defs

theorem foo (P : Type*) [PartialOrder P] (b : P):
    ∀ (a : P), a ≥ b → b ≥ a → a = b :=
  fun a => by simpa using ge_antisymm

Additionally, using simp followed by exact also works:

import Mathlib.Order.Defs

theorem foo (P : Type*) [PartialOrder P] (b : P):
    ∀ {a : P}, a ≥ b → b ≥ a → a = b :=
  by simp; exact ge_antisymm

Is this an issue with simpa?

( @Yaël Dillies )