simp can't discharge side goal for a simp lemma

Stream: lean4

[Ted Hwa]

Why can't the side goal be discharged here?

opaque P: Nat → Prop
opaque Q: Nat → Prop

@[simp]
theorem foo (d: Nat) (h: Q d): P 0 ↔ P d := by sorry

example (h: Q 1): P 0 := by
  set_option trace.Meta.Tactic.simp true in simp [h]  -- fails because can't discharge side goal
  /-
    [Meta.Tactic.simp.discharge] foo discharge ❌
        Q ?d ▼
    [unify] h:1000, failed to unify
          Q 1
        with
          Q ?d
  -/

It says "failed to unify" when it should clearly unify.
Instead, I have to write simp [foo 1 h] (or rw) in which case I didn't need to register foo as a simp lemma.

[Kyle Miller]

If you do simp [foo 1, h] it works. I'm guessing this is by design, that dischargers unify at a greater depth, making the metavariable for d not assignable when discharging. (Though I looked through the code and it didn't look like there were any withNewMCtxDepths that would inhibit this unification...)

[Tomas Skrivan]

All the theorem arguments are initialized to meta variables at new depth here but I'm not sure if this extra depth is really causing this unification failure.