`apply` ignores reducibility hints in some cases

[digama0]

Prerequisites

• [X] Put an X between the brackets on this line if you have done all of the following:
  • Checked that your issue isn't already filed.
    • Specifically, check out the wishlist, open RFCs, or feature requests.
  • Reduced the issue to a self-contained, reproducible test case.

Description

def foo : Type := sorry
@[irreducible] def foo.le (a b : foo) : Prop := ∀ n : nat, true
instance : has_le foo := ⟨foo.le⟩
instance : preorder foo :=
{ le := (≤), le_refl := sorry, le_trans := sorry }

example (a : foo) : a ≤ a := by refl
example (a : foo) : a ≤ a := by apply le_refl
example (a : foo) : a ≤ a := by tactic.mk_const `le_refl >>= tactic.apply_core

invalid apply tactic, failed to unify
  a ≤ a
with
  ∀ (a : ?m_1), a ≤ a

All three examples fail with the same error (they all call in to the third one), while other alternatives like le_refl _ or refine le_refl _ do not fail. The issue appears to be the forall in the definition of foo.le. Note that apply will unfold its way all the way to the bottom looking for a forall, even if it has to go through an irreducible definition like foo.le here. I assume this has something to do with the way that apply figures out how many arguments to apply. The md setting in apply_core has no effect on this bug.