Zero ℕ instance breaks acyclic tactic

[fpfu]

import Mathlib

inductive Foo
| mk (t s : Foo)

-- `Lean.MVarId.acyclic` failed:
example (h: Foo.mk s s = s): False := nomatch h  -- missing cases

-- because of `simp_arith` can't solve this goal:
example: sizeOf s < sizeOf (Foo.mk s s) := by simp_arith  -- unsolved goals

-- problem arises there:
example {n: Nat}: Zero.zero ≤ n := by simp  -- simp made no progress

[alexjbest]

I think this is the same as https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/.E2.9C.94.20Function.20on.20Tree.20type btw