Yet another irrelevant instance bug

[ncfavier]

Minimised from https://github.com/the1lab/1lab/pull/427#discussion_r1732698143

open import Agda.Builtin.Nat
open import Agda.Builtin.Equality

data _≤_ : Nat → Nat → Set where
  0≤x : ∀ {x} → 0 ≤ x
  s≤s : ∀ {x y} → x ≤ y → suc x ≤ suc y

instance
  s≤s' : ∀ {x y} → ⦃ x ≤ y ⦄ → suc x ≤ suc y
  s≤s' ⦃ x ⦄ = s≤s x

  x≤sucy : ∀ {x y} ⦃ p : x ≤ y ⦄ → x ≤ suc y
  x≤sucy {.0} {y} ⦃ 0≤x ⦄ = 0≤x
  x≤sucy {.(suc _)} {.(suc _)} ⦃ s≤s p ⦄ = s≤s (x≤sucy ⦃ p ⦄)

  {-# INCOHERENT x≤sucy #-}

Positive : Nat → Set
Positive n = 1 ≤ n

postulate
  z : (b : Nat) → .⦃ _ : Positive b ⦄ → Nat
  foo : ∀ n → .⦃ _ : Positive n ⦄ → z n ≡ 0

bar : ∀ n → ⦃ _ : Positive n ⦄ → z n ≡ 0
bar n@(suc _) ⦃ p ⦄ = foo n

{-
p != s≤s _54 of type 1 ≤ suc n₁
when checking that n is a valid argument to a function of type
(n₂ : Nat) .⦃ _ = z₁ : Positive n₂ ⦄ → z n₂ ≡ 0
-}

If the instance argument to foo is not marked irrelevant, then the error is

Failed to solve the following constraints:
  Resolve instance argument _58 : Positive (suc n₁)
  Candidates
    s≤s' : {x y : Nat} ⦃ _ : x ≤ y ⦄ → suc x ≤ suc y
    p : 1 ≤ suc n₁
    (stuck)

I think it's trying to compare z n ⦃ p ⦄ with z n ⦃ s≤s' ⦄, which should succeed but fails (why?)