[Agda] Agda can't find an obvious instance.

[effectfully]

open import Relation.Binary.PropositionalEquality
open import Data.Nat
open import Data.Fin

instance
  fz : Fin 1
  fz = zero

z : ∀ {n} {{_ : Fin n}} -> ℕ
z = 0

yellow : z ≡ 0
yellow = refl

ok : z {1} ≡ 0
ok = refl

----

The instance is not picked in `yellow'. Agda can't find the instance
even in this case:

----

record R (n m : ℕ) : Set where

instance
  r : R 0 1
  r = _

z' : ∀ {m} {{_ : R 0 m}} -> ℕ
z' = 0

yellow' : z' ≡ 0
yellow' = refl

ok' : z' {1} ≡ 0
ok' = refl

----

Should I report this as a bug, or is this a known limitation?